Ouaknine, Joel and Worrell, James - 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
On the decidability and complexity of Metric Temporal Logic over finite words

Authors: Ouaknine, Joel and Worrell, James

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.


Source : oai:arXiv.org:cs/0702120
DOI : 10.2168/LMCS-3(1:8)2007
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 91 times.
This article's PDF has been downloaded 39 times.