Generalized Model Checking

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 (also called may/must 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. Generalized model checking generalizes both model checking (when the model is complete) and satisfiability (when everything in the model is unknown), probably the two most studied problems related to temporal logic and verification. In this talk, the main ideas behind this framework, namely models for three-valued abstractions, completeness preorders (to measure the level of completeness of such models), three-valued temporal logics and generalized model checking was presented . The algorithms and complexity bounds for three-valued model checking and generalized model-checking for various temporal logics, was also discussed. The applications to program verification via automatic abstraction, was then discussed. Examples of programs and properties that can be verified by generalized model checking but not with current abstraction-based verification tools, was shown. Classes of temporal-logic formulas for which model checking is guaranteed to always have the same precision as generalized model checking, was also presented. The final topic is a brief discussion of three-valued abstractions for reasoning about open systems and about games in general, as well as completeness issues (i.e., given an infinite-state program and a property, is there a finite-state abstraction of that program that satisfies this property?).