טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
Ph.D Thesis
Ph.D StudentShoham Buchbinder Sharon
SubjectAbstraction-Refinement and Modularity in Mu-Calculus
Model Checking
DepartmentDepartment of Computer Science
Supervisor Professor Orna Grumberg
Full Thesis textFull thesis text - English Version


Abstract

Model checking is an automated technique for checking 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, which refers to its high space requirements. Two of the most successful approaches to fighting the state-explosion problem in model checking are abstraction and compositional model checking.

                                        

Abstractions hide certain details of the system in order to result in a smaller model. In some cases the abstraction is too coarse, resulting in an inconclusive model checking result. Thus, the abstract model is refined by adding more details into it, making it more similar to the concrete model. Iterating this process is called abstraction-refinement. In compositional model checking, on the other hand, one tries to verify parts of the system separately in order to avoid the construction of the entire system.


In this research, we investigate abstraction-refinement and compositional techniques for specifications in the mu-calculus, which is a powerful formalism for expressing properties of transition systems using fixpoint operators. Our work exploits and extends the game-based approach to mu-calculus model checking, in which the model checking problem is formulated as a game between a verifier and a falsifier. We develop novel abstraction-refinement schemes for the mu-calculus, based on a 3-valued semantics. The 3-valued semantics allows an abstract model to be used for verification as well as falsification, unlike traditional abstraction which is only used for verification. We investigate both the efficiency and the precision of abstract models used within the abstraction-refinement framework. We then extend our work on abstraction-refinement to the arena of compositional verification, thus joining the forces of both approaches. We use techniques taken from the game-based 3-valued model checking for abstract models to obtain a novel fully automatic compositional technique that can determine the truth value of the full mu-calculus with respect to a given system.