A Divide & Conquer Approach to Model Checking Linear Temporal Properties

This paper proposes a divide & conquer approach to model checking linear temporal properties to mitigate the state space explosion problem in model checking. The core idea of the approach is to split an original model checking problem into multiple smaller model checking problems using the tableau method and tackle each smaller one independently. We prove a theorem ensuring that these smaller model checking problems are equivalent to the original model checking problem. By leveraging the natural parallelism of the divide-and-conquer approach, the smaller model checking problems can be tackled simultaneously to improve the verification time significantly. To support our approach, we develop a tool in Maude called DCA2MC , which uses Maude LTL model checker as a software component to conduct model checking experiments and supports both sequential and parallelization modes for verification. DCA2MC also supports the integration of external model checkers, such as Spin, allowing users to choose between Maude LTL model checker and Spin to conduct model checking experiments. This integration shows that other model checkers can leverage our approach to mitigate the state space explosion and handle larger state spaces more effectively. To maximize the effectiveness of our approach, layer configuration selection plays a crucial role. We introduce a semi-automated method for finding a good layer configuration, supported by custom commands developed in DCA2MC . Finally, we conduct case studies on five mutual exclusion protocols and provide extensive experimental results comparing DCA2MC with Maude LTL model checker, Spin, and LTSmin in terms of memory consumption and runtime performance, thereby demonstrating the power of our approach.