Back to Search
Start Over
Incompleteness of states w.r.t. traces in model checking
- Source :
-
Information & Computation . Mar2006, Vol. 204 Issue 3, p376-407. 32p. - Publication Year :
- 2006
-
Abstract
- Abstract: Cousot and Cousot introduced and studied a general past/future-time specification language, called ▪-calculus, featuring a natural time-symmetric trace-based semantics. The standard state-based semantics of the ▪-calculus is an abstract interpretation of its trace-based semantics, which turns out to be incomplete, that is trace-incom-plete, even for finite systems. As a consequence, standard state-based model checking of the ▪-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 ▪-calculus. This derives from a number of results, one for each incomplete logical/temporal connective of the ▪-calculus, that characterize the structure of models, i.e., transition systems, whose corresponding state-based semantics of the ▪-calculus is trace-complete. [Copyright &y& Elsevier]
Details
- Language :
- English
- ISSN :
- 08905401
- Volume :
- 204
- Issue :
- 3
- Database :
- Academic Search Index
- Journal :
- Information & Computation
- Publication Type :
- Academic Journal
- Accession number :
- 19965330
- Full Text :
- https://doi.org/10.1016/j.ic.2006.01.001