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 words

Authors: Joel Ouaknine ; James Worrell

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


Share

Consultation statistics

This page has been seen 379 times.
This article's PDF has been downloaded 180 times.