Semantic minimizations for temporal logics

Photograph of Michael Huth

Michael Huth

(Imperial College London)

Three-valued models, in which properties of a system are either true,
false or unknown, have recently been advocated as a better
representation for reactive program abstractions generated by automatic
techniques such as predicate abstraction. Indeed, for the same cost,
model checking three-valued abstractions can be used to both prove and
disprove any temporal-logic property, whereas traditional conservative
abstractions can only prove universal properties. Also, verification
results can be more precise with generalized model checking, which
checks whether there exists a concretization of an abstraction
satisfying a temporal-logic formula. Since generalized model checking
includes satisfiability as a special case (when everything in the model
is unknown), it is in general more expensive than traditional model
checking. In this talk, we study how to reduce generalized model
checking to model checking by a temporal-logic formula transformation,
which generalizes a transformation for propositional logic known as
semantic minimization in the literature. We show that many
temporal-logic formulas of practical interest are self-minimizing, i.e.,
are their own semantic minimizations, and hence that model checking for
these formulas has the same precision as generalized model checking.


(Joint work with Patrice Godefroid.)


Thursday 2nd March 2006, 14:00
Robert Recorde Room
Department of Computer Science