Abstract interpretation-based strong preservation of abstract model checking

Francesco Ranzato
Dipartimento di Matematica Pura ed Applicata, Università di Padova
Friday, 17 February, 2006 (All day)

Standard abstract model checking relies on abstract Kripke structures which approximate the concrete model by gluing together indistinguishable states, namely by a partition of the concrete state space. Strong preservation for a specification language L encodes the equivalence of concrete and abstract model checking of formulas in L. We show how abstract interpretation can be used to design abstract models which are more general than abstract Kripke structures. Accordingly, strong preservation can be generalized to this abstract interpretation-based model checking framework. This also provides a generalized abstract interpretation-based view of partition refinement algorithms for reducing the state space of a Kripke structure in order to obtain strong preservation for a specification language L. In particular, the well-known Paige and Tarjan algorithm reduces the state space in order to obtain bisimulation, that is strong preservation for CTL or mu-calculus. We show how our abstract interpretation-based view leads to design a generalized Paige-Tarjan algorithm for computing the minimal refinement of a generic abstract model which is strongly preserving for a generic language.