On the decidability and complexity of Metric Temporal Logic over finite words
<|reference_start|>On the decidability and complexity of Metric Temporal Logic over finite words: 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.<|reference_end|>
@article{ouaknine2007on,
    title={On the decidability and complexity of Metric Temporal Logic over finite
  words},
    author={Joel Ouaknine and James Worrell},
    journal={Logical Methods in Computer Science, Volume 3, Issue 1 (February
  28, 2007) lmcs:2230},
    year={2007},
    doi={10.2168/LMCS-3(1:8)2007},
    archivePrefix={arXiv},
    eprint={cs/0702120},
    primaryClass={cs.LO cs.CC}
}