Incompleteness of States w.r.t. Traces in Model Checking
| dc.creator | Giacobazzi, Roberto | |
| dc.creator | Ranzato, Francesco | |
| dc.date | 2004-04-23 | |
| dc.date | 2005-08-24 | |
| dc.date.accessioned | 2026-07-07T03:21:08Z | |
| dc.date.available | 2026-07-07T03:21:08Z | |
| dc.description | 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 (i.e., 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. | |
| dc.identifier | https://arxiv.org/abs/cs/0404048 | |
| dc.identifier | http://arxiv.org/abs/cs/0404048 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/32086 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | D.2.4; F.3.1; F.3.2 | |
| dc.title | Incompleteness of States w.r.t. Traces in Model Checking | |
| dc.type | text |