Cousot and Cousot introduced and studied a general past/future-time specification language, called mu-calculus, featuring a natural time-symmetric trace-based semantics. The standard state-based semantics of the mu-calculus is an abstract interpretation of its trace-based semantics, which turns out to be incomplete, that is trace-incomplete, even for finite systems. As a consequence, standard state-based model checking of the mu-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 mu-calculus. This derives from a number of results, one for each incomplete logical/temporal connective of the mu-calculus, that characterize the structure of models, i.e., transition systems, whose corresponding state-based semantics of the mu-calculus is trace-complete.
Incompleteness of states w.r.t. traces in model checking
RANZATO, FRANCESCO
2006
Abstract
Cousot and Cousot introduced and studied a general past/future-time specification language, called mu-calculus, featuring a natural time-symmetric trace-based semantics. The standard state-based semantics of the mu-calculus is an abstract interpretation of its trace-based semantics, which turns out to be incomplete, that is trace-incomplete, even for finite systems. As a consequence, standard state-based model checking of the mu-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 mu-calculus. This derives from a number of results, one for each incomplete logical/temporal connective of the mu-calculus, that characterize the structure of models, i.e., transition systems, whose corresponding state-based semantics of the mu-calculus is trace-complete.File | Dimensione | Formato | |
---|---|---|---|
publishedPaper.pdf
accesso aperto
Tipologia:
Published (publisher's version)
Licenza:
Accesso libero
Dimensione
439.7 kB
Formato
Adobe PDF
|
439.7 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.