Property-driven Parallel Symbolic Model Checking of LTL

Model checking is an automated method used to formally verify systems by checking them against properties. However, a major problem in model checking is the state explosion. To overcome this challenge, one approach is to utilize parallel processing capabilities to either speed up computations or handle larger-scale problems. Explicit model checking has lower computational complexity and can be easily parallelized. There are numerous parallel explicit model checking algorithms available in the literature. Symbolic model checking offers significant advantages over explicit model checking in terms of problem scalability and verification speed. However, treating states encountered during the search as sets poses a challenge in devising efficient parallel algorithms. As a result, current research on parallelizing symbolic model checking has primarily focused on reachability analysis or safety properties, rather than attempting to parallelize the nested fixpoint calculations. In this paper, we propose a novel property-driven approach for parallel symbolic model checking of full LTL. Our algorithm introduces a fair model state labelling function that forms a partition of the nested fixpoint across the product combining the model and the property Büchi automaton. The experimental results demonstrate significant speedup, ranging from 2.81 to 17.19 times compared to sequential approaches on a 32-core machine. Moreover, in comparison to existing parallel model checking methods, our approach not only surpasses those relying on BDD libraries with a maximum improvement of up to 134% and an average improvement of 33.1% but also demonstrates significant superiority over the state-of-theart parallel explicit model checker.