Joel Ouaknine ; James Worrell - On the decidability and complexity of Metric Temporal Logic over finite words

lmcs:2230 - Logical Methods in Computer Science, February 28, 2007, Volume 3, Issue 1 - https://doi.org/10.2168/LMCS-3(1:8)2007
On the decidability and complexity of Metric Temporal Logic over finite wordsArticle

Authors: Joel Ouaknine ; James Worrell ORCID

    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.


    Volume: Volume 3, Issue 1
    Published on: February 28, 2007
    Submitted on: May 15, 2006
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Computational Complexity,F.4.1

    66 Documents citing this article

    Consultation statistics

    This page has been seen 1350 times.
    This article's PDF has been downloaded 395 times.