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_0: The most natural, compositional, way of modeling real-time systems uses a dense domain for time. The satisfiability of timing constraints that are capable of expressing punctuality in this model, however, is known to be undecidable. We introduce a temporal language that can constrain the time difference between events only with finite, yet arbitrary, precision and show the resulting logic to be EXPSPACE-complete. This result allows us to develop an algorithm for the verification of timing properties of real-time systems with a dense semantics.
@cite_9: A monadic second-order language, denoted by ( L d ), is introduced for the specification of sets of timed state sequences. A fragment of ( L d ), denoted by , is proved to be expressively complete for timed automata (Alur and Dill), i.e., every timed regular language is definable by a -formula and every -formula defines a timed regular language. As a consequence the satisfiability problem for is decidable.
@cite_15: 
@cite_12: A unifying framework for the study of real-time logics is developed. In analogy to the untimed case, the underlying classical theory of timed state sequences is identified, it is shown to be nonelementarily decidable, and its complexity and expressiveness are used as a point of reference. Two orthogonal extensions of PTL (timed propositional temporal logic and metric temporal logic) that inherit its appeal are defined: they capture elementary, yet expressively complete, fragments of the theory of timed state sequences, and thus are excellent candidates for practical real-time specification languages.
Existing decidability results for MTL involve placing restrictions on the semantics or the syntax of the logic to circumvent the problem of punctuality. Alur and Henzinger @cite_12 showed that the satisfiability and model-checking problems for MTL relative to a discrete-time semantics are EXPSPACE-complete. Alur, Feder, and Henzinger @cite_15 @cite_0 introduced as a fragment of MTL in which the temporal operators may only be constrained by intervals. They showed that the satisfiability and model-checking problems for MITL relative to a dense-time semantics are also EXPSPACE-complete. Wilke @cite_9 considered MTL over a dense-time semantics with , i.e., the semantics is parameterised by a bound @math on the number of events per unit time interval. He showed that the satisfiability problem is decidable in this semantics and that MTL with existential quantification over propositions is equally expressive as Alur-Dill timed automata.