2002 | OriginalPaper | Buchkapitel
States vs. Traces in Model Checking by Abstract Interpretation
verfasst von : Roberto Giacobazzi, Francesco Ranzato
Erschienen in: Static Analysis
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In POPL’00, Cousot and Cousot showed that the classical state-based model checking of a very general temporal language called $$ \mu \curvearrowleft \star $$-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 \curvearrowleft \star $$-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 \curvearrowleft \star $$-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 \curvearrowleft \star $$-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 \curvearrowleft \star $$-calculus which is trace-complete.