States vs. Traces in Model Checking by Abstract Interpretation

By: R. Giacobazzi and F. Ranzato

Roberto Giacobazzi
Dipartimento di Informatica
Univ. di Verona
Strada Le Grazie a Ca' Vignal 2, 37134 Verona (Italy)


In POPL'00, Cousot and Cousot showed that the classical state-based model checking of a very general temporal language called $\mus$-calculus is an incomplete abstract interpretation of its trace-based semantics. In ESOP'01, Ranzato showed that the least refinement of the state-based model checking semantics of the mu-calculus which is complete w.r.t. its trace-based semantics exists, and it is essentially the trace-based semantics itself. The analogous problem in the opposite direction is solved by the present paper. First, relatively to any incomplete temporal connective of the mu-calculus, we characterize the structure of the models, i.e. transition systems, for which the state-based model checking is trace-complete. On this basis, we prove that the unique abstraction of the state-based model checking semantics of the mu-calculus (actually, of any fragment allowing conjunctions) which is complete w.r.t. the trace-based semantics is the straightforward semantics carrying no information at all. The following consequence can be drawn: there is no way to either refine or abstract sets of states in order to get a model checking algorithm for (any fragment allowing conjunctions of) the mu-calculus which is trace-complete.

Available: DVI, PostScript, BibTeX Entry.

Related papers:
  • On the completeness of model checking by F. Ranzato (ESOP'01, LNCS 2028:137-154, 2001)
  • Incompleteness, Counterexamples and Refinements in Abstract Model-Checking (SAS'01, LNCS 2126:356-373, 2001)
  • Completeness in abstract interpretation: A domain perspective (AMAST'97, LNCS 1349: 231-245, 1997)
  • Complete abstract interpretations made constructive (MFCS'98, LNCS 1450:366-377, 1998)
  • Making abstract interpretations complete (Journal of the ACM. 47(2):361-416 2000).