Improving Quality of Counterexamples in Model Checking via Automated Planning

There is a wide agreement that model checking and automated planning (planning for short) are closely related fields. Planning is the task of finding a sequence of appropriate moves that achieves a goal. Model checking aims to prove or disprove a system model that satisfies a given property which is often specified by temporal logics. In this paper we investigate the application of advanced planning techniques to model checking. To this end, a system model is expressed by means of a planning model, and temporal logic property can be treated as a special form of planning goal, i.e., Temporally Extended Goal (TEG). Therefore, the model checking task can be reduced into a planning scheme what we call planning with TEG. In order to utilize the state-of-the-art planners, we further propose two novel compilation methods to translate a planning with TEG problem into a classical planning problem and a non-deterministic planning one respectively. The obtained valid plans in planning just correspond to the counterexamples in model checking. We provide detailed evaluations of our approach on a series of benchmarks. The experimental results are encouraging, showing that existing planners can provide significant improvements in the quality of the counterexamples compared with the model checkers.