Incompleteness of States w.r.t. Traces in Model Checking

TL;DR

This paper investigates the inherent incompleteness of state-based semantics in mu*-calculus model checking, revealing that refinements do not fully capture trace-based properties, especially for propositional fragments.

Contribution

It demonstrates that state-based semantics of mu*-calculus are inherently trace-incomplete and characterizes models where state-based semantics are trace-complete.

Findings

State-based semantics are incomplete for trace-based properties.

Refinements of state domains do not resolve trace-incompleteness.

Characterization of models with trace-complete semantics.

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 (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.