Logic in Computer Science (LICS 2004)

Paper: The Existence of Finite Abstractions for Branching Time Model Checking (at LICS 2004)

Authors: Dennis Dams Kedar S. Namjoshi

Abstract

Abstraction is often essential to verify a program with model checking. Typically, a concrete source program with an infinite (or finite, but large) state space is reduced to a small, finite state, abstract program on which a correctness property can be checked. The fundamental question we investigate in this paper is whether such a reduction to finite state programs is always possible, for arbitrary branching time temporal properties. We begin by showing that existing abstraction frameworks are inherently incomplete for verifying purely existential or mixed universal-existential properties. We then propose a new, complete abstraction framework which is based on a class of focused transition systems (FTS's). The key new feature in FTS's is a way of "focusing" an abstract state to a set of more precise abstract states. While focus operators have been defined for specific contexts, this result shows their fundamental usefulness for proving non-universal properties. The constructive completeness proof provides linear size maximal models for properties expressed in logics such as CTL and the mu-calculus. This substantially improves upon known (worst-case) exponential size constructions for their universal fragments.

BibTeX

  @InProceedings{DamsNamjoshi-TheExistenceofFinit,
    author = 	 {Dennis Dams and Kedar S. Namjoshi},
    title = 	 {The Existence of Finite Abstractions for Branching Time Model Checking},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2004},
    year =	 2004,
    editor =	 {Harald Ganzinger},
    month =	 {July}, 
    pages =      {335--344},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }