Logic in Computer Science (LICS 2005)

Paper: Model Checking Vs. Generalized Model Checking: Semantic Minimizations for Temporal Logics (at LICS 2005)

Authors: Patrice Godefroid Michael Huth

Abstract

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 satis- fiability as a special case (when everything in the model is unknown), it is in general more expensive than traditional model checking. In this paper, we study how to reduce generalized model checking to model checking by a temporallogic formula transformation, which generalizes a transformation for propositional logic known as semantic minimization in the literature. We show that many temporallogic 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.

BibTeX

  @InProceedings{GodefroidHuth-ModelCheckingVsGene,
    author = 	 {Patrice Godefroid and Michael Huth},
    title = 	 {Model Checking Vs. Generalized Model Checking:  Semantic Minimizations for Temporal Logics},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005},
    year =	 2005,
    editor =	 {Prakash Panangaden},
    month =	 {June}, 
    pages =      {158--167},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }