PaperlayerView exact revision on arXiv

Source-linked AI summary

On the decidability and complexity of Metric Temporal Logic over finite words

Joel Ouaknine, James Worrell

arXiv:cs/0702120v3cs.LOcs.CC

TL;DR

MTL expresses quantitative timing requirements, but its decidability has been unclear because dense-time semantics can support encodings associated with undecidability. This paper uses timed alternating automata to establish decidability for finite-word MTL problems and safety-fragment model checking over infinite words, while retaining non-primitive recursive complexity for finite-word satisfiability.

  • Problem

    Linear temporal logic abstracts away precise observation times, while dense-time MTL has been considered undecidable under state-based semantics, motivating the question of decidability with punctuality.

    Source: §1 · pp. 1–2

  • Method

    The paper translates MTL formulas into timed alternating automata and uses decidable emptiness for one-clock automata over finite timed words.

    Source: §1 · p. 3

  • Results

    Finite-word MTL satisfiability and model checking are decidable, with non-primitive recursive satisfiability complexity, and infinite-word safety-fragment model checking is decidable.

    Source: §1 · pp. 2–3, §9 · p. 25

  • Takeaways & Limitations

    The results establish decidability for these event-based MTL settings despite claims that punctuality necessarily entails undecidability.

    Source: §1 · p. 2, §9 · p. 25

    Event-based MTL becomes genuinely undecidable when past temporal operators are allowed.

    Source: §1 · p. 2

Abstract

from arXiv · show

Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether all words accepted by a given Alur-Dill timed automaton satisfy a given MTL formula. We show that this problem is decidable over finite words. Over infinite words, we show that model checking the safety fragment of MTL--which includes invariance and time-bounded response properties--is also decidable. These results are quite surprising in that they contradict various claims to the contrary that have appeared in the literature.

1. Introduction

MTL adds quantitative timing to temporal logic, but the paper argues that punctuality does not force undecidability under event-based semantics. It establishes decidability for finite timed words and for safety-fragment model checking over infinite words, while surveying prior approaches and related automata results.

1. Introduction

  • MTL extends linear temporal logic by constraining temporal operators with real-valued intervals, addressing the loss of quantitative timing in order-only executions.For example, ✸ ϕ requires ϕ within three to four time units.Source: §1 · pp. 1–2
  • State-based MTL is undecidable because dense time can encode Turing-machine configurations and formulas can enforce their propagation between unit intervals.In event-based semantics, the corresponding encoding may contain insertion errors and describe faulty machines instead.Source: §1 · p. 2
  • Event-based MTL satisfiability and model checking over finite timed words are decidable despite punctuality, while infinite-word safety-fragment model checking is also decidable.The finite-word satisfiability problem has non-primitive recursive complexity.Source: §1 · pp. 2–3
  • The decidability proof translates MTL into timed alternating automata and uses decidable one-clock language emptiness; model-checking extensions and a non-primitive-recursive lower bound are also established.The lower bound is obtained by encoding insertion channel machines and applying a reachability-complexity result for lossy channel machines.Source: §1 · pp. 2–3

1.1. Related Work.

  • Earlier decidability results restricted discrete time, used the nonsingular MITL fragment, or imposed bounded variability on dense-time MTL.The cited results include EXPSPACE-completeness for discrete-time MTL and dense-time MITL.Source: §1.1 · p. 3
  • Independent work also established decidable finite-word emptiness for one-clock timed alternating automata, but did not address timed logics; other related studies concern TCTL or different timed-process problems.The TCTL comparison combines clock regions with well-quasi-orders, while the timed-process problems are described as different.Source: §1.1 · p. 3

2. Timed Words and Timed Automata

The paper represents timed words as event sequences paired with nondecreasing real timestamps, requiring unbounded time progress for infinite sequences. It defines Alur-Dill timed automata through clock-constrained transitions and accepting runs.

2. Timed Words and Timed Automata

  • A timed word pairs a finite or infinite event sequence with equally long timestamps; timestamps are nondecreasing, and infinite sequences must be unbounded.No a priori bound is imposed on events per unit interval.Source: §2 · p. 4

2.1. Timed Automata.

  • An Alur-Dill timed automaton has finite locations, clocks, accepting locations, and edges guarded by clock constraints that may reset selected clocks.Clock values above the largest guard constant are represented by ⊤ because the constraints cannot distinguish them.Source: §2.1 · p. 4
  • Runs alternate delay steps, which advance clocks within a location, with event-labelled discrete steps; finite runs accept when their last location is accepting.The automaton's language comprises finite or infinite timed words with accepting runs, using the corresponding acceptance condition.Source: §2.1 · p. 5

3. Timed Alternating Automata

Timed alternating automata extend alternating automata with clocks, and the paper focuses on the one-clock case for representing MTL formulas. Their languages are closed under Boolean operations, including complement.

3. Timed Alternating Automata

  • Timed alternating automata extend alternating automata with clocks, and the paper focuses on one clock because that suffices to represent MTL formulas.The section considers finite timed words; virtually all decision problems, including emptiness, are undecidable with more than one clock.Source: §3 · p. 5, §3.1 · p. 5

3.1. One-clock Timed Alternating Automata.

  • Transitions use disjunction for existential branching and conjunction for universal branching, alongside clock constraints and a binding construct that resets the clock to zero.Automata configurations are finite sets of states, with acceptance determined by whether every location in the final configuration is accepting.Source: §3.1 · pp. 5–7
  • The example automaton accepts finite timed words in which no two events are separated by exactly one time unit, a language not expressible by an Alur-Dill automaton.Its transition creates a thread that rules out an event at exactly one time unit after the preceding event.Source: §3.1 · p. 6
  • A run advances configurations through alternating delays and discrete transitions, and accepts when its final configuration is accepting.The automaton accepts a word when there exists an accepting run.Source: §3.1 · p. 7

3.2. Duality and Complementation.

  • Timed alternating automata are closed under complement and, together with closure under union, under all Boolean operations.Complementation uses a dual transition function and the complement of the accepting locations.Source: §3.2 · pp. 8–9

4. Decidability of Language Emptiness

The section reduces one-clock timed alternating-automaton emptiness to reachability in an effective well-structured transition system, yielding decidable emptiness and language inclusion. It makes the reduction work by preserving behavior through a bisimulation abstraction and imposing a well-quasi-order on abstract configurations.

4.1. The Bisimulation Lemma.

  • The Bisimulation Lemma matches transitions between equivalent configurations, allowing the analysis to use rational configurations and discrete time-successor steps.Reachable configurations in the full transition system have equivalent rational representatives reachable in the reduced system.Source: §4.1 · pp. 10–11

4.2. Well-quasi-orders.

  • Abstract configurations encode locations and clock regions in fractional-part order; their equivalence classes correspond exactly to equal abstractions.The induced monotone domination order on these finite words is a well-quasi-order.Source: §4.2 · pp. 12–13

4.3. Well-Structured Transition Systems.

  • The reduced transition system WA is a well-structured transition system, enabling decidability of reachability to accepting configurations.Theorem 4.17 applies the WSTS result to emptiness and language inclusion.Source: §4.3 · pp. 13–14
  • Language emptiness for one-clock timed alternating automata and inclusion of an Alur-Dill automaton language in one are both decidable.The result follows from the well-structured transition system construction.Source: §4.3 · p. 14

5. Metric Temporal Logic

MTL extends linear temporal logic with real-time constraints on temporal operators, interpreted here over event-based timed words. Its event-based semantics differs materially from state-based semantics because temporal operators quantify over word positions rather than every instant of time.

Metric Temporal Logic

  • Event-based MTL refers to events and quantifies over the countable positions of a timed word, unlike state-based semantics, which quantifies over the whole time domain.The paper connects this distinction to why MTL is undecidable under state-based semantics but decidable over finite event-based words.Source: §5 · p. 14
  • MTL extends LTL with next and until operators constrained by real-valued intervals, with eventually and always available as derived operators.For example, eventually within [3,4] requires a formula to hold 3 to 4 time units later.Source: §5 · pp. 14–15
  • Satisfaction is evaluated at timed-word positions: next checks the following event's delay, while until requires a later witness and an intervening condition.The semantics define both finite and infinite model languages.Source: §5 · p. 15
  • Adding a fixed delay to every timestamp does not change satisfaction, since time is measured relative to the first event.The paper illustrates event-based specifications with timed lock-acquisition and release requirements.Source: §5 · p. 15

6. MTL over Finite Words

For finite timed words, MTL satisfiability and model checking are decidable, although both problems have non-primitive recursive complexity. The paper translates formulas to equivalent one-clock timed alternating automata and uses their decidable language problems.

6. MTL over Finite Words

  • MTL satisfiability and model checking over finite words are decidable and have non-primitive recursive complexity.The decision procedure translates MTL formulas into equivalent one-clock timed alternating automata and invokes the automata result.Source: §6 · p. 16, §6.1 · p. 18

6.1. Translation to Automata.

  • For each MTL formula in negation normal form, the construction produces a one-clock alternating automaton with the same finite-word language.The translation handles Boolean and temporal connectives through its transition function.Source: §6.1 · pp. 16–17
  • A fresh clock tracks each temporal obligation as the automaton propagates it until its requirements are discharged.Automaton states pair a formula-closure location with a clock value.Source: §6.1 · p. 16
  • The automaton for a negated formula corresponds to the complement of the original automaton, establishing the converse language inclusion.The proof identifies matching transition functions under the bijection between formula locations and their duals.Source: §6.1 · p. 17

7. Complexity

The paper proves that MTL satisfiability and model checking over finite words have non-primitive recursive complexity. It obtains the lower bound by encoding dual control-state reachability for insertion-error channel machines as MTL satisfiability.

7. Complexity

  • MTL satisfiability and model checking over finite words have non-primitive recursive complexity.The satisfiability lower bound transfers to model checking by using a universal timed automaton and formula validity.Source: §7 · pp. 19–20
  • The reduction encodes channel-machine computations as timed words and makes satisfiability equivalent to dual control-state reachability.The formula enforces the initial and final control states and an empty final channel.Source: §7 · pp. 19–20
  • The channel formula matches every write with a same-message read one time unit later but permits unpaired reads, representing insertion errors.Strongly monotonic time prevents ambiguity in matching write and read events.Source: §7 · p. 19
  • Timestamps encode FIFO order by placing matching write-read pairs one time unit apart while maintaining intervening events within that interval.The construction chooses timestamps sequentially using the density of time.Source: §7 · p. 20
  • A universal Alur-Dill timed automaton turns model checking into formula validity, so its complexity follows from MTL satisfiability.Validity is tested by asking whether the negated formula is unsatisfiable.Source: §7 · p. 20

8. Infinite Words: Safety MTL

The section establishes decidability of infinite-word model checking for Safety MTL and explains how a one-clock alternating-automaton inclusion procedure achieves it. Safety MTL restricts constrained-until intervals in negation normal form to bounded length.

8. Infinite Words: Safety MTL

  • Safety MTL requires bounded-length intervals for constrained until in negation normal form, with no such restriction on dual-until.Source: §8 · p. 21
  • Safety MTL expresses time-bounded response properties but not arbitrary response formulas.The section contrasts one-time-unit response with a response formula requiring potentially unboundedly many clocks to find a counterexample.Source: §8 · p. 21
  • Every Safety MTL formula defines a safety property relative to divergence of time.Source: §8 · p. 21

8.1. The Model-Checking Procedure.

  • A word rejected by an all-accepting timed alternating automaton has a finite prefix rejected by its complement automaton.This finite bad-prefix characterization supports deciding infinite-word inclusion through finite reachability.Source: §8.1 · p. 22
  • The model-checking procedure reduces inclusion to reaching a doomed configuration in a well-structured transition system built from the automaton pair.Doomed configurations pair an empty alternating-automaton configuration with a state from which the Alur-Dill automaton can accept an infinite non-Zeno word.Source: §8.1 · pp. 23–25
  • Model checking Safety MTL over infinite words on Alur-Dill automata is decidable.The procedure decides whether Lω(B) ⊆ Lω(ϕ).Source: §8.1 · p. 25

9. Conclusion

The paper establishes decidability for MTL satisfiability over finite timed words, with non-primitive recursive complexity, and decidable model checking for Safety MTL over infinite words. Its proof strategy introduces one-clock timed alternating automata and uses well-quasi-orders for emptiness decidability.

9. Conclusion

  • MTL is decidable over finite timed words in dense-time point-based semantics, with non-primitive recursive complexity.Source: §9 · p. 25
  • One-clock timed alternating automata have decidable finite-word emptiness and are closed under Boolean operations, but lack finite untimed quotients.The termination proof uses a well-quasi-order derived from Higman's Lemma.Source: §9 · p. 25
  • For infinite-word satisfiability, Safety MTL is decidable, whereas MTL is undecidable.The conclusion states that restricting to safety properties is crucial to obtaining decidability.Source: §9 · p. 25
Loading cs/0702120v3…