Concurrent On-the-fly SCC Detection for Automata-based Model Checking with Fairness Assumption

Zhimin Wu, Akin Gunay, Yang Liu, Shengchao Qin

Research output: Contribution to conferencePaper

107 Downloads (Pure)

Abstract

Model checking is an automated technique for verifying temporal logic properties of finite state systems. Tarjan’s algorithm for detecting Strongly Connected Components (SCCs) is a widely used depth-first search procedure for Automatabased (LTL) model checking. It works on the SCC detection on-the-fly with the composition of transition systems and B¨uchi Automaton (state space generation), which has been deployed as sequential implementations in many tools. However, these implementations suffer from heavy time cost for systems which involve a large number of SCC explorations. To address this issue, in this paper, we develop a concurrent SCC detection approach for the on-the-fly generated state space in LTL model checking by expanding the existing concurrent Tarjan’s algorithm. Besides, we involve fairness checking. Different that the previous work, which performs fairness checking after the generation of a complete SCC, in our approach we perform fairness checking during SCC generation to improve efficiency. We implement our approach in PAT model checker. Our experimental results show that our approach achieves up to 2X speedup for the complete SCC detection in large-scale system models compared to the sequential on-the-fly model checking in PAT. Besides, our parallel on-the-fly fairness checking approach speedups fairness checking around 2X45X.
Original languageEnglish
Publication statusPublished - 6 Nov 2016
Event21st International Conference on Engineering of Complex Computer Systems - Dubai, United Arab Emirates
Duration: 6 Nov 20168 Nov 2016

Conference

Conference21st International Conference on Engineering of Complex Computer Systems
Abbreviated titleICECCS 2016
CountryUnited Arab Emirates
CityDubai
Period6/11/168/11/16

Fingerprint Dive into the research topics of 'Concurrent On-the-fly SCC Detection for Automata-based Model Checking with Fairness Assumption'. Together they form a unique fingerprint.

  • Cite this

    Wu, Z., Gunay, A., Liu, Y., & Qin, S. (2016). Concurrent On-the-fly SCC Detection for Automata-based Model Checking with Fairness Assumption. Paper presented at 21st International Conference on Engineering of Complex Computer Systems, Dubai, United Arab Emirates.