2004/04/23 by Roberto Giacobazzi, Giacobazzi, Roberto, Francesco Ranzato +1 · 1 citation
Computer Science · #D.2.4 #F.3.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Software Testing and Debugging Techniques #cs.LO
paper · pdf · doi:10.48550/arxiv.cs/0404048
openalex publication_date 2004/04/23 · arxiv created 2005/08/24 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.