Incompleteness of States w.r.t. Traces in Model Checking

By: R. Giacobazzi and F. Ranzato

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


Cousot and Cousot introduced and studied a general past/future-time specification language, called mus-calculus, featuring a natural time-symmetric trace-based semantics. The standard state-based semantics of the mus-calculus is an abstract interpretation of its trace-based semantics, which turns out to be incomplete (i.e., trace-incomplete), even for finite systems. As a consequence, standard state-based model checking of the mus-calculus is incomplete w.r.t. trace-based model checking. This paper shows that any refinement or abstraction of the domain of sets of states induces a corresponding semantics which is still trace-incomplete for any propositional fragment of the mus-calculus. This derives from a number of results, one for each incomplete logical/temporal connective of the mus-calculus, that characterize the structure of models, i.e. transition systems, whose corresponding state-based semantics of the mus-calculus 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).