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

Abstract

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.

Cited by in corpus (17)

• Complexity Hierarchies Beyond Elementary
• What's decidable about parametric timed automata?
• The Power of Well-Structured Systems
• Model Checking One-clock Priced Timed Automata
• The Power of Priority Channel Systems
• Real-Time Specification Patterns and Tools
• A Boyer-Moore Type Algorithm for Timed Pattern Matching
• MTL-Model Checking of One-Clock Parametric Timed Automata is Undecidable
• Timed Context-Free Temporal Logics
• Model checking: the interval way
• Bounded Variability of Metric Temporal Logic
• Determinisability of register and timed automata
• Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground
• Real-Time Synthesis is Hard!
• Revisiting Timed Logics with Automata Modalities
• Undecidability of future timeline-based planning over dense temporal domains
• Model checking memoryful linear-time logics over one-counter automata