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

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 Automata-based (LTL) model checking. It works on the SCC detection on-the-fly with the composition of transition systems and Buchi 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 2X similar to 45X.