CTL model checking with model generation theorem prover

摘要

This paper presents a method performing CTL model checking with a model generation theorem prover. In this method, a transition system and a negation of its specification are represented by a clause set. The model checking is performed by checking satisfiability of the clause set. If the transition system satisfies the specification, the clause set are unsatisfiable, otherwise, it is satisfiable. In the latter, the theorem prover returns a model as a counter example which show a possible error of the transition system.