What Do We Really Need? Identifying Minimal Sufficient Temporal Properties via Refinement

Research question

Specification suites written in Computation Tree Logic (CTL) tend to grow with every design iteration, and many of their properties end up overlapping or depending on one another. This short paper asks how to tell, without a system model, which CTL properties are already guaranteed by others, so that engineers can see what is really needed and avoid verifying redundant properties.

Approach

The paper defines property refinement for CTL: a property refines another when its set of satisfying execution traces is included in the other’s and is non-empty. The non-emptiness guard is what separates refinement from plain logical implication or subsumption: an unsatisfiable property implies everything but guarantees nothing, so it must not be allowed to replace weaker properties. Refinement forms a partial order up to logical equivalence, which lets mutually refining properties be collapsed into one representative and lets transitivity prune checks.

To extract a minimal sufficient subset (MSS), properties are first grouped by shared atomic propositions. Within each group, candidate pairs are compared by building alternating tree automata; because exact language inclusion is EXPTIME-complete, the paper uses a simulation relation between automata as a sound, polynomial-time approximation. The MSS consists of the properties that are not refined by any other.

Results

On 69 benchmark suites drawn from the Model Checking Contest (MCC) and the RERS 2019 challenge, the analysis removes on average 36.6% of the properties, with reductions of up to 70%. In end-to-end experiments on synthetic models, refinement analysis followed by model checking of the MSS outperforms checking every property once models and properties become non-trivial, with speedups of up to 30×; for very small models the analysis overhead is not yet recovered.

Why it matters

The paper shows that redundancy is common even in curated CTL suites, and that refinement gives engineers traceable insight into where dependencies between requirements come from. It complements the LTL theory published at FSE 2026; its outlook — exact refinement checking via satisfiability instead of simulation — is taken up in the later work on complete property refinement for CTL.