# 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)

`giaco@sci.univr.it`

### Abstract:

*
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:
* giaco@sci.univr.it *