An improved case-based approach to LTL model checking

The state space explosion is the key obstacle of model checking. Even a relatively small system specification may yield a very large state space. The case-based approach based on search space partition has been proposed in [18,19] for reducing model checking complexity. This paper extends the approach by considering wider ranges of case-bases of models and multiple case-bases such that it can be applied to more types of applications. The improved approach also combines the search space partition and static analysis or expert knowledge for guaranteeing the completeness of the cases. The case study demonstrates the potential advantages of the strategy and show that the strategy may improve the efficiency of system verification and therefore scale up the applicability of the verification approach.