On the decidability and complexity of Metric Temporal Logic over finite words
Logic in Computer Science
2017-01-11 v3 Computational Complexity
Abstract
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.
Keywords
Cite
@article{arxiv.cs/0702120,
title = {On the decidability and complexity of Metric Temporal Logic over finite words},
author = {Joel Ouaknine and James Worrell},
journal= {arXiv preprint arXiv:cs/0702120},
year = {2017}
}