Skip to content (access key 's')
Logo of Technion
Logo of CS Department
Logo of CS4People

The Taub Faculty of Computer Science Events and Talks

Abstraction-Refinement and Modularity in mu-Calculus Model Checking
event speaker icon
Sharon Shoham Buchbinder (Ph.D. Thesis Seminar)
event date icon
Wednesday, 14.05.2008, 16:00
event location icon
Taub 601
event speaker icon
Advisor: Prof. Orna Grumberg
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 work we join the forces of abstraction-refinement and compositional verification to obtain a novel fully automatic compositional technique that can determine the truth value of the full $\mu$-calculus w.r.t. a given system. Our approach is based on a game-based 3-valued model checking for abstract models.