Proofs about folklore: why model checking = reachability? Seminars/Workshops

Abstract

In the talk we address a problem of model checkers reuse, i.e. when a model checker for a state-based program logic can be used for checking another state-based program logic. It continues our previous study. The cited paper has examined the propositional mu-Calculus of D. Kozen muC and the second-order propositional program logic 2M of C. Stirling. It has been known that muC$lt;2M in terms of expressive power. We has proved that muC and 2M enjoy the equal model checking power in the following sense: there are particular formulae in muC and 2M such that every checker for any of these particular formulae for models in any class closed w.r.t. finite models, Cartesian products and power-sets can be used for checking all formulae in muC and 2M in all models in this class. An example of these particular formulae is any muC-formula WIN for winning strategies in finite games. In the talk we demonstrate that a branching time Computation Tree Logic CTL also has equal model checking power with muC and 2M in the same settings as above. An example of a corresponding CTL-formulae is a basic reachability CTL-formulae (EF p) (where p is any Boolean property).