A Tableau-Based Approach to Model Checking Linear Temporal Properties

This paper proposes a tableau-based approach to model checking linear temporal properties to mitigate the state space explosion 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. We prove a theorem to guarantee that the multiple smaller model checking problems are equivalent to the original model checking problem. We use Maude, a high-level specification and programming language based on rewriting logic, to develop a tool called DCA2MC to support our approach. Some case studies are conducted to compare DCA2MC with Maude LTL model checker, Spin, and LTSmin model checkers in terms of running performance and memory usage, showing the power of our proposed approach.