States vs. traces in model checking by abstract interpretation

In POPL’00, Cousot and Cousot showed that the classical state-based model checking of a verygeneral temporal language called μ-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 μ-calculus which is complete w.r.t. its trace-based semantics exists, and it is essentiallythe tracebased semantics itself. The analogous problem in the opposite direction is solved bythe present paper. First, relativelyto anyincomplete temporal connective of the μ-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 μ-calculus (actually, of anyfragmen t allowing conjunctions) which is complete w.r.t. the tracebased semantics is the straightforward semantics carrying no information at all. The following consequence can be drawn: there is no wayto either refine or abstract sets of states in order to get a model checking algorithm for (anyfragmen t allowing conjunctions of) the μ-calculus which is trace-complete.