Abstract:Logic model checking raise unique challenges to the efficiency and scalability of various algorithms. In this paper, it argues that the linear temporal logic model checking algorithm calls for an efficient and common solution. We then introduces a novel parallel on-the-fly model checking algorithm based on subset of states, namely SCPLM. According to the density property of subgraph with active states subset, SCPLM schedules parallel computing tasks dynamically, which has been proven to reduce the synchronization overhead significantly. It implements SCPLM on a lightweight parallel graph processing system, Ligra. A detailed evaluation using benchmarks shows that SCPLM outperforms the existing state-of-art algorithm by up to 1.2~1.3X, yet with much better scalability.