The Taub Faculty of Computer Science Events and Talks

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.