Detecting redundant LTL requirements with Spot

When can a requirement check be omitted?

If a system satisfies an LTL property, it also satisfies every property that follows from it. For example, “every request is granted in the next step” implies “every request is eventually granted.” Once the stronger requirement has been verified, the weaker one needs no separate model-checking run.

To find these relations, check satisfiability and consistency, then compare the properties' languages with Spot. Equivalent properties need only one representative; weaker properties are covered by retained stronger ones. Keep the original requirements and record these dependencies for traceability.

This is the basis of LTL property refinement, developed in the FSE 2026 paper by Brodo, Scalora and Henkler [1]. It applies to formalized requirements. Natural-language requirements need a reviewed formalization before this analysis can establish anything about them.

What counts as redundancy?

A requirement is redundant with respect to a set when the other requirements already entail it. This can happen even when their wording and formula syntax differ.

Consider a lift controller maintained by several teams. One team requires that the door remain closed while the lift moves. A legacy specification states the same rule in different words. Elsewhere, a response deadline of one control cycle already covers a more general promise of eventual service. Each requirement has a reason to appear in the documentation, but they need not all be checked independently. The paper describes the accumulation of redundant and interdependent properties as specification debt [1].

Text comparison finds exact duplicates. Semantic analysis can also establish equivalence and implication. Unsatisfiability needs separate attention: a contradiction logically implies every formula, so implication alone can produce a misleading reduction.

LTL for requirements

Linear Temporal Logic describes properties of infinite executions [2]. At each step, atomic propositions describe what is true. Our controller uses door_open and moving for its physical state, request and grant for service events, and error and alarm for fault handling.

LTL combines these propositions with Boolean connectives and temporal operators. Spot writes negation, conjunction, disjunction and implication as !, &, | and ->.

Operators can be nested to express safety, response and fairness requirements:

G ¬(door_open ∧ moving)The door is never open while the lift is moving.

G (request → F grant)At every step with a request, a grant occurs at that step or later.

GF request → GF grantIf requests occur infinitely often, grants also occur infinitely often.

These formulas use a deliberately small event model. They do not distinguish passengers or match individual requests to individual grants. A specification that needs those distinctions must represent them explicitly.

Traces and languages

For a set of propositions A, a trace is an infinite sequence σ = A₀A₁A₂…, where Aᵢ ⊆ A lists the propositions true at step i. A formula's language is the set of traces that satisfy it:

L_A(φ) = { σ ∈ (2^A)^ω | σ ⊨ φ }All infinite executions over A that satisfy φ.

A system model T satisfies φ when all its traces belong to this language: Traces(T) ⊆ L(φ) [3]. An automata-based model checker typically translates ¬φ into a Büchi automaton and looks for a system execution accepted by that automaton [5]. Such an execution is a counterexample to φ.

What is LTL property refinement?

Let φ₁ = G(p ∧ q), meaning that p and q always hold, and φ₂ = G p, meaning that p always holds. Every trace satisfying φ₁ also satisfies φ₂:

L(φ₁) ⊆ L(φ₂)φ₁ implies φ₂. The stronger property has the smaller language.

If every execution of a model satisfies φ₁, each also satisfies φ₂. A successful verification of φ₁ therefore establishes φ₂ for the same model. If the check of φ₁ fails, that result alone does not tell us whether φ₂ holds.

The non-emptiness condition

The second relation excludes vacuous refinement by contradictions. An unsatisfiable formula has an empty language and therefore implies everything, but no system with at least one execution can satisfy it. It cannot serve as evidence that the requirements have been met.

Equivalence is implication in both directions. Equivalent properties can be grouped, with one representative selected for verification. Refinement is also transitive: if one property implies a second and the second implies a third, no additional inclusion check is needed to infer the first-to-third relation.

Which property should be verified?

The converse does not follow in these examples. Eventual service, for instance, permits a delay of several steps and cannot establish next-step service.

Checking implication with Spot

Spot provides LTL parsing, translation to ω-automata, and language inclusion and equivalence checks [7]. These examples require its Python bindings. See the official installation instructions for supported packages; one option is conda install -c conda-forge spot [10].

Implication, equivalence and satisfiability

spot.contains(left, right) tests whether the language of right is included in that of left [8]. To ask whether stronger implies weaker, write spot.contains(weaker, stronger).

import spot

stronger = spot.formula("G (p & q)")   # always p and q
weaker = spot.formula("G p")           # always p

# spot.contains(left, right) is True iff L(right) is a subset of L(left).
# "stronger implies weaker" is therefore spot.contains(weaker, stronger).
print(spot.contains(weaker, stronger))   # True:  G(p & q) implies G p
print(spot.contains(stronger, weaker))   # False: G p does not imply G(p & q)

# Equivalence is implication in both directions.
print(spot.are_equivalent("G !(a & b)", "G (b -> !a)"))   # True

# Satisfiability: a formula is unsatisfiable iff its automaton is empty.
print(spot.translate("G p & F !p").is_empty())   # True: no trace satisfies it

True
False
True
True

The first two results show the implication direction: always having both p and q entails always having p, while always having p says nothing about q. The third confirms that the two safety formulations are equivalent.

The final result is an emptiness test. spot.translate(f).is_empty() returns True when no trace satisfies f. Here, requiring p always and ¬p eventually is a contradiction.

An example suite

The following script checks ten controller requirements. It reports contradictions and tautologies, checks that the remaining requirements are jointly satisfiable, compares pairs, and selects properties for verification. It uses spot.language_containment_checker() to cache automata across repeated comparisons [8].

"""Detect redundant LTL requirements with Spot -- a simplified illustration.

Educational example for https://lucabrodohshl.github.io/tutorials/ltl-property-redundancy/
It shows the idea of LTL property refinement on a toy suite. It is not the
tool evaluated in Brodo, Scalora and Henkler, FSE 2026 (doi:10.1145/3808127).
"""
import spot

# A small requirement suite for a door-and-lift controller, written by
# several teams over time. Keys are requirement IDs, values are LTL formulas.
SUITE = {
    "R1": "G !(door_open & moving)",          # safety team
    "R2": "G (moving -> !door_open)",         # legacy spec
    "R3": "G (request -> X grant)",           # control team
    "R4": "G (request -> F grant)",           # product requirements
    "R5": "GF request -> GF grant",           # fairness requirement
    "R6": "G (request -> grant) & F (request & !grant)",  # merged by mistake
    "R7": "F grant | G !grant",               # tautology
    "R8": "G (error -> alarm)",               # diagnostics team
    "R9": "G (alarm -> !moving)",             # safety team
    "R10": "G (error -> !moving)",            # safety team
}

formulas = {rid: spot.formula(text) for rid, text in SUITE.items()}
aps = {rid: {str(ap) for ap in spot.atomic_prop_collect(f)}
       for rid, f in formulas.items()}

# The checker caches the automaton of each formula, which pays off when
# many pairs are compared. Its contains(left, right) has the same argument
# order as spot.contains: True iff L(right) is a subset of L(left).
lcc = spot.language_containment_checker()


def refines(strong, weak):
    """Test implication; callers must also check satisfiability."""
    return lcc.contains(weak, strong)


# Step 1: filter unsatisfiable and valid formulas (automata emptiness).
candidates = []
rejected = []
for rid, f in formulas.items():
    if spot.translate(f).is_empty():
        rejected.append(rid)
        print(f"{rid}: UNSATISFIABLE - fix it, never use it to cover others")
    elif spot.translate(spot.formula.Not(f)).is_empty():
        print(f"{rid}: VALID (tautology) - constrains nothing")
    else:
        candidates.append(rid)

# Individually satisfiable requirements may still contradict each other.
# Stop rather than use an inconsistent conjunction to infer redundancy.
candidate_conjunction = spot.formula.And([formulas[r] for r in candidates])
if spot.translate(candidate_conjunction).is_empty():
    raise ValueError("The remaining requirements are jointly inconsistent; review them.")

# Step 2: pairwise refinement. After step 1, a formula can only refine
# another one if both share at least one atomic proposition.
edges = set()
for a in candidates:
    for b in candidates:
        if a != b and aps[a] & aps[b] and refines(formulas[a], formulas[b]):
            edges.add((a, b))

# Step 3: equivalence = refinement in both directions. Keep one representative.
representative = {}
for rid in candidates:
    representative[rid] = next(
        r for r in candidates
        if r == rid or ((r, rid) in edges and (rid, r) in edges)
    )

# Step 4: a representative is redundant if a non-equivalent one refines it.
reps = sorted(set(representative.values()), key=candidates.index)
retained = [r for r in reps
            if not any((s, r) in edges and (r, s) not in edges for s in reps)]

print("\nRefinement relations (stronger => weaker):")
order = candidates.index
for a, b in sorted(edges, key=lambda e: (order(e[0]), order(e[1]))):
    if (b, a) in edges:
        if order(a) < order(b):
            print(f"  {a} is equivalent to {b}")
    else:
        print(f"  {a} refines {b}")

print("\nRetained after pairwise refinement:", ", ".join(retained))
for rid in candidates:
    if rid not in retained:
        covers = [r for r in retained if (r, rid) in edges]
        print(f"  {rid} is covered by {', '.join(covers)}")

# Optional extra step, beyond pairwise refinement: is a retained property
# implied by the conjunction of the others? This single pass can depend on
# the order and does not guarantee a set of minimum cardinality.
for rid in list(retained):
    others = [formulas[r] for r in retained if r != rid]
    if others and refines(spot.formula.And(others), formulas[rid]):
        retained.remove(rid)
        print(f"  {rid} is implied by the conjunction of {', '.join(retained)}")

print("\nProperties to model-check:", ", ".join(retained))
conjunction = spot.formula.And([formulas[r] for r in retained])
assert not spot.translate(conjunction).is_empty()
assert all(refines(conjunction, f) for rid, f in formulas.items() if rid not in rejected)
print("Check: the retained set is satisfiable and implies every non-rejected requirement.")

With Python 3.14 and Spot 2.14.5, the script produces:

R6: UNSATISFIABLE - fix it, never use it to cover others
R7: VALID (tautology) - constrains nothing

Refinement relations (stronger => weaker):
  R1 is equivalent to R2
  R3 refines R4
  R3 refines R5
  R4 refines R5

Retained after pairwise refinement: R1, R3, R8, R9, R10
  R2 is covered by R1
  R4 is covered by R3
  R5 is covered by R3
  R10 is implied by the conjunction of R1, R3, R8, R9

Properties to model-check: R1, R3, R8, R9
Check: the retained set is satisfiable and implies every non-rejected requirement.

Reading the output

• R6 is unsatisfiable. It requires every request to be served immediately and also requires an unserved request. It is reported for correction and excluded from the reduction analysis.
• R7 is a tautology. A trace either contains a grant or never does. Every trace satisfies it.
• R1 and R2 are equivalent. The script keeps R1 as their representative.
• R3 implies R4 and R5. Next-step service guarantees eventual service and, when requests occur infinitely often, infinitely many grants.
• R10 needs a joint check. No single property implies it, but R8 and R9 together do: an error raises the alarm, and an alarm prohibits movement.

The final assertions check that the retained conjunction is satisfiable and entails every requirement except the rejected contradiction. This establishes a reduction of the remaining suite. R6 still needs correction before the complete specification can be satisfied.

The command-line equivalent

Spot's ltlfilt can filter formulas by implication [9]. Here, the first input implies the filter formula and is printed. The second does not, so it produces no output:

# Print the formula only if it implies the --imply formula
ltlfilt -f 'G(request -> X grant)' --imply='G(request -> F grant)'
ltlfilt -f 'G(request -> F grant)' --imply='G(request -> X grant)'

G(request -> Xgrant)

From implication checks to a reduced suite

The example starts with the following requirements. The temporal and Boolean operators have the meanings introduced above.

Relations in the suite

Which checks remain?

After reporting R6 and setting aside the tautology R7, eight properties enter the pairwise analysis. Equivalence and refinement leave five checks: R1, R3, R8, R9 and R10. The additional joint-entailment step removes R10.

To see why the four remaining checks suffice, suppose a model satisfies all four. R1 gives R2 by equivalence. R3 gives R4, which gives R5. R8 and R9 ensure that every error coincides with an alarm and therefore with no movement, establishing R10. R7 holds independently. This argument establishes every original requirement except R6, which remains unresolved.

The method in the FSE 2026 paper

The paper places refinement analysis between formalization and model checking [1]:

1. Filter and partition. Construct automata, identify contradictions and tautologies, and group the remaining properties by connections through shared atomic propositions. These groups restrict which properties need comparison. They are distinct from groups of logically equivalent formulas.
2. Build refinement relations. Check language inclusion within each group and record the relations in a graph. Use transitivity to infer further relations. Mutual refinement identifies equivalent formulas.
3. Select representatives. Keep the most refined properties, choosing one representative from each selected equivalence class. In a graph oriented from stronger to weaker, these are the source components.

The shared-proposition partition is justified after filtering: if a satisfiable property implies a non-tautological property, the two must share at least one atomic proposition. The tutorial script uses this test to skip disjoint pairs, but compares the remaining ordered pairs directly rather than implementing the paper's full graph analysis.

What pairwise analysis can miss

The paper calls the selected set a minimal sufficient subset. For the pairwise construction, the practical guarantee is that every remaining candidate is implied by a selected property, and no selected representative is strictly refined by another selected representative. This does not by itself rule out redundancy caused by a conjunction.

R10 illustrates the distinction: neither R8 nor R9 implies it alone. A pairwise result can therefore contain a property that is redundant with respect to the rest of the set. Inclusion-minimality under arbitrary joint entailment and minimum cardinality are stronger requirements.

The script's optional final pass checks each property against the conjunction of the others. It performs one pass in a fixed order and does not guarantee a set of minimum cardinality. Although the number of checks is small, the conjunctions can make automata construction expensive. Exhaustively exploring combinations adds a separate combinatorial cost; see the discussion of subset-based analysis in the paper and Barnat et al. [1], [13].

Why not just simplify the formulas?

Simplification can make a formula easier to verify. Suite reduction asks which requirements need independent checks. Both can help, and they can be used together.

With Spot, syntactic uniqueness and simplification give different results:

# --unique removes exact duplicates only: both equivalent formulas survive
ltlfilt --unique -f 'G(moving -> !door_open)' -f 'G !(door_open & moving)'
# Simplifying a conjunction can absorb an implied conjunct ...
ltlfilt -r3 -f 'G(request -> X grant) & G(request -> F grant)'
# ... but the result is one rewritten formula, not a list of requirements
ltlfilt -r3 -f 'G(error -> alarm) & G(alarm -> !moving) & G(error -> !moving)'

G(moving -> !door_open)
G!(door_open & moving)
G(!request | Xgrant)
G((alarm | !error) & (!alarm | !moving))

--unique keeps both safety formulations because their syntax differs. Simplifying a conjunction may absorb implied conjuncts, but the output is one rewritten formula. To use that result in requirements management, a tool still needs to track the original requirement IDs and explain the dependencies. Refinement analysis records those relations explicitly.

Research: Property Refinement in Linear Temporal Logic (FSE 2026)

The paper develops the language-based semantics of LTL property refinement and its algebraic properties, including transitivity and equivalence. It then gives algorithms for specification partitioning and refinement analysis, and evaluates the resulting reduction in verification tasks [1]. The method described above summarizes the construction; the tutorial code is an independent illustration.

Reported results

The evaluation uses 141 benchmarks derived from BEEM [17], covering mutual exclusion, communication protocols, distributed algorithms, scheduling and other model-checking examples. Each model is checked with its original and reduced property suites using the Spot–LTSmin–DVE backend. Table 1 reports:

• Fewer tasks in 109 of 141 benchmarks. The reduction reaches 75%, with a mean of 35.95% and a median of 50%.
• A mean model-checking speedup of 1.63×. The median is 1.75× and the best case in Table 1c is 4.2×.
• About 20.6 hours of gross verification time saved across the benchmarks, against roughly 12 minutes of refinement analysis.
• A median analysis overhead of 0.035% of baseline verification time. The mean is 2.22% and the worst case is 54.5%.

These figures describe the evaluated benchmarks and use the speedup metric reported in Table 1c. They are not performance guarantees for other models or property suites.

Costs and applicability

The benefit depends on the suite's redundancy and the cost of the checks avoided. Four benchmarks had a net loss: analysis of their property suites cost more than the verification time it saved. The same analysis can be reused when the model changes, provided the properties and their semantics remain unchanged.

LTL satisfiability and inclusion are PSPACE-complete [6], and the constructed automata can be exponential in the formula size. Caching and partitioning reduce repeated work but do not remove this worst-case cost. Most evaluated suites produced only one to three proposition-connected groups, so the evaluation gives limited evidence about partitioning benefits for more modular specifications.

Related papers: What Do We Really Need? Identifying Minimal Sufficient Temporal Properties via Refinement and Property Refinement in Computation Tree Logic. The research page collects this work on refinement and specification debt.

Assumptions and limitations

Check the implication direction

Verify the stronger property and use it to establish the weaker one. Spot's argument order is easy to reverse: spot.contains(a, b) tests whether b implies a. A small known example, such as always p implying eventually p, helps catch this error.

Check consistency as well as individual satisfiability

A contradiction must be reported and corrected. Also check whether individually satisfiable requirements can hold together: G p (“p always holds”) and F !p (“p is eventually false”) are each satisfiable but jointly inconsistent. Their conjunction implies everything vacuously. The example stops if the non-rejected requirements are jointly inconsistent.

Separate similarity from implication

Changing X to F can weaken a response requirement while leaving its text almost unchanged. Conversely, a Boolean rewrite can change the syntax without changing the meaning. Textual similarity can guide review, but it does not establish either equivalence or refinement.

Use a common interpretation

Proposition names must have the same meaning throughout the suite. If grant means “request accepted” in one source and “passenger served” in another, an implication between the formulas does not establish the intended requirement relation. Align the vocabulary, time-step interpretation, model variants and environment assumptions first.

Distinguish universal from model-dependent implication

The checks here range over all traces. Further implications may hold only under a model's constraints or explicit environment assumptions. Record those dependencies: such relations need to be reconsidered when the constraints change. D³ is related work on exploiting dependencies for model checking [14].

Keep the requirements and their coverage records

An implied requirement can still be useful for documentation, certification or communication with its owners. Record which retained properties cover it. Recompute the affected relations when a property changes, and report an omitted check as established only after its covering checks succeed. If a stronger check fails, a weaker requirement may still hold and may need a separate diagnostic check.

State what kind of reduction was computed

A pairwise reduction does not establish that no property follows from a combination of others. Likewise, an inclusion-minimal set need not have the fewest possible members. State the criterion used and avoid describing an arbitrary reduced set as globally optimal.

Handle expensive checks conservatively

Cache automata and measure preprocessing time. In a production workflow, use time limits and retain properties when an inclusion check is inconclusive. A timeout provides no proof of redundancy.

Using the reduced suite

For this example, verify R1, R3, R8 and R9, then record the implied requirements as covered if those checks pass. Keep R6 open as a specification defect. After it is corrected, rerun the analysis before treating the complete suite as verified.

For another suite, follow the same sequence: review the formalization, check consistency, establish implication relations, and keep a record of why each omitted check is covered. The useful output is a smaller verification suite together with an explanation of its coverage.

Further reading and citation

For the formal definitions, algorithms and evaluation, cite the FSE 2026 paper:

@article{brodo2026ltlrefinement,
  author    = {Brodo, Luca and Scalora, Giuseppe and Henkler, Stefan},
  title     = {Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification},
  journal   = {Proceedings of the ACM on Software Engineering},
  volume    = {3},
  number    = {FSE},
  articleno = {FSE120},
  numpages  = {22},
  year      = {2026},
  month     = jul,
  publisher = {Association for Computing Machinery},
  doi       = {10.1145/3808127},
  url       = {https://doi.org/10.1145/3808127}
}

References

1. Luca Brodo, Giuseppe Scalora, and Stefan Henkler. 2026. Property Refinement in Linear Temporal Logic: Formal Semantics and Algorithms for Software Verification. Proceedings of the ACM on Software Engineering, 3, FSE, Article FSE120, 2698–2719 (FSE 2026). doi:10.1145/3808127
2. Amir Pnueli. 1977. The Temporal Logic of Programs. 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), IEEE, 46–57. doi:10.1109/SFCS.1977.32
3. Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking., MIT Press.
4. Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. 1999. Model Checking., MIT Press.
5. Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification. Proceedings of the First Symposium on Logic in Computer Science (LICS 1986), IEEE Computer Society, 332–344.
6. A. Prasad Sistla and Edmund M. Clarke. 1985. The Complexity of Propositional Linear Temporal Logics. Journal of the ACM, 32, 3, 733–749. doi:10.1145/3828.3837
7. Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard, and Henrich Lauko. 2022. From Spot 2.0 to Spot 2.10: What’s New?. Computer Aided Verification (CAV 2022), LNCS 13372, Springer, 174–187. doi:10.1007/978-3-031-13188-2_9
8. Spot developers. Spot documentation: Testing for language inclusion and equivalence (contains.ipynb).. Accessed October 2026.
9. Spot developers. Spot documentation: ltlfilt.. Accessed October 2026.
10. Spot developers. Spot documentation: Installing Spot.. Accessed October 2026.
11. Fabio Somenzi and Roderick Bloem. 2000. Efficient Büchi Automata from LTL Formulae. Computer Aided Verification (CAV 2000), LNCS 1855, Springer, 248–263. doi:10.1007/10722167_21
12. Orna Kupferman and Moshe Y. Vardi. 2003. Vacuity Detection in Temporal Model Checking. International Journal on Software Tools for Technology Transfer, 4, 2, 224–233. doi:10.1007/s100090100062
13. Jiří Barnat, Petr Bauch, Nikola Beneš, Luboš Brim, Jan Beran, and Tomáš Kratochvíla. 2016. Analysing Sanity of Requirements for Avionics Systems. Formal Aspects of Computing, 28, 1, 45–63. doi:10.1007/s00165-015-0348-9
14. Rohit Dureja and Kristin Yvonne Rozier. 2018. More Scalable LTL Model Checking via Discovering Design-Space Dependencies (D³). Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018), LNCS 10805, Springer, 309–327. doi:10.1007/978-3-319-89960-2_17
15. Gianpiero Cabodi and Sergio Nocco. 2011. Optimized Model Checking of Multiple Properties. Design, Automation & Test in Europe (DATE 2011), IEEE, 1–4. doi:10.1109/DATE.2011.5763279
16. Elmar Juergens, Florian Deissenboeck, Martin Feilkas, Benjamin Hummel, Bernhard Schaetz, Stefan Wagner, Christoph Domann, and Jonathan Streit. 2010. Can Clone Detection Support Quality Assessments of Requirements Specifications?. Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering (ICSE 2010), Vol. 2, ACM, 79–88. doi:10.1145/1810295.1810308
17. Radek Pelánek. 2007. BEEM: Benchmarks for Explicit Model Checkers. Model Checking Software (SPIN 2007), LNCS 4595, Springer, 263–267. doi:10.1007/978-3-540-73370-6_17