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.
@cite_22: We introduce timed alternating tree automata as a natural extension of timed automata for the purpose of solving the model checking problem for timed computation tree logic (TCTL) following the automata-theoretic approach. This settles a problem posed by Henzinger, Kupferman, and Vardi
A class of timed alternating tree automata has been defined by Dickh " o fer and Wilke @cite_22 in the context of model checking a real-time version of Computation Tree Logic, called TCTL @. The language-emptiness problem for these automata is undecidable in general. However, TCTL model checking reduces to a special case of language emptiness, which is shown in @cite_22 to be decidable using Alur and Dill's clock regions construction. In contrast, bounded-dimension clock regions do not suffice in the present paper: we combine clock regions with the notion of well-quasi-orders.