שרון שוהם בוכבינדר, הרצאה סמינריונית לדוקטורט
יום רביעי, 14.5.2008, 16:00
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.