M.Sc Thesis

M.Sc StudentShoham Buchbinder Sharon
SubjectA Game-Based Framework for CTL Counterexamples and
DepartmentDepartment of Computer Science
Supervisor PROFESSOR EMERITUS Orna Grumberg


Model checking is an efficient procedure that checks whether or not a given system model fulfills a desired property, described as a temporal logic formula. Yet, as real models tend to be very big, model checking encounters the state-explosion problem. One solution to this problem is the use of abstraction, that hides some of the details of the original (concrete) model. In this work we consider the branching time logic CTL (Computation Tree Logic). Our work exploits and extends the game-based framework of CTL model checking for incremental abstraction-refinement and counterexamples. We define a game-based CTL model checking for abstract models over the 3-valued semantics, which can be used for verification as well as refutation. The model checking process of an abstract model may end with an indefinite result, in which case we suggest a new notion of refinement, which eliminates indefinite results of the model checking. This provides an iterative abstraction-refinement framework. This framework is enhanced by an incremental algorithm, where refinement is applied only where indefinite results exist and definite results from prior iterations are used within the model checking algorithm. We also define the notion of  annotated counterexamples, which are sufficient and minimal counterexamples for full CTL. We present an algorithm that uses the game board of the model checking game to

derive an annotated counterexample in case the examined system model refutes the checked formula.