[pl-seminar] talk reminder

["Thomas Reps" <reps@xxxxxxxxxxx>]

Title: Message

This is to remind you that there will be a PL seminar today

at 1:15 PM (non-standard time) in 2310 CS:

  Abstract interpretation-based strong preservation of abstract model checking

Francesco Ranzato
University of Padova, Italy
Monday, July 30, 2007
1:15, 2310 CS

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 that 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 that is strongly preserving for a generic language.