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

DOI10.2168/LMCS-3(1:8)2007zbMath1128.03008OpenAlexW2022782983MaRDI QIDQ5310684

Joël Ouaknine, James Worrell

Publication date: 11 October 2007

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2168/lmcs-3(1:8)2007

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Temporal logic (03B44)

Related Items (34)

Zeno, Hercules, and the Hydra ⋮ To drive or not to drive: a logical and computational analysis of European transport regulations ⋮ Timed hyperproperties ⋮ Adequacy and complete axiomatization for timed modal logic ⋮ Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\) ⋮ Time-Bounded Verification of CTMCs against Real-Time Specifications ⋮ Path Checking for MTL and TPTL over Data Words ⋮ Model Checking Real-Time Systems ⋮ Time-Bounded Verification ⋮ Metric propositional neighborhood logic with an equivalence relation ⋮ Bounded variability of metric temporal logic ⋮ A survey of timed automata for the development of real-time systems ⋮ Metric temporal answer set programming over timed traces ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Parameterized model checking of weighted networks ⋮ Mixing Lossy and Perfect Fifo Channels ⋮ Some Recent Results in Metric Temporal Logic ⋮ MTL with Bounded Variability: Decidability and Complexity ⋮ ``Most of leads to undecidability: failure of adding frequencies to LTL ⋮ Timeline-based planning over dense temporal domains ⋮ Timed modal logics for real-time systems. Specification, verification and control ⋮ Model checking memoryful linear-time logics over one-counter automata ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the termination and structural termination problems for counter machines with incrementing errors ⋮ The ω-Regular Post Embedding Problem ⋮ Robust Analysis of Timed Automata Via Channel Machines ⋮ Post Embedding Problem Is Not Primitive Recursive, with Applications to Channel Systems ⋮ Complexity Hierarchies beyond Elementary ⋮ Model-checking Timed Temporal Logics ⋮ Complexity issues for timeline-based planning over dense time under future and minimal semantics ⋮ Realizability of Real-Time Logics ⋮ Context-free timed formalisms: robust automata and linear temporal logics

This page was built for publication: On the decidability and complexity of Metric Temporal Logic over finite words