Journal article

### On the decidability of Metric Temporal Logic

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 f...

Publication status:
Published

### Authors

Ouaknine, J More by this author
More by this author
Institution:
University of Oxford
Department:
Oxford, MPLS, Computer Science
Soc, IEEEC More by this author
Journal:
LICS 2005: 20th Annual IEEE Symposium on Logic in Computer Science - Proceedings
Pages:
188-197
Publication date:
2005
ISSN:
1043-6871
URN:
uuid:510c8a5e-2ccf-4b49-ae77-64eaeae10371
Source identifiers:
282469
Local pid:
pubs:282469
Language:
English