Metric temporal logic

From Wikipedia, the free encyclopedia
  (Redirected from Metric Temporal Logic)
Jump to navigation Jump to search

Metric temporal logic (MTL) is a special case of temporal logic. It is an extension of temporal logic in which temporal operators are replaced by time-constrained versions like until, next, since and previous operators. It is linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly-monotonic integer-time semantics. For MTL, the exact complexity of the satisfiability problems is known and independent of interval-based or point-based, synchronous (i.e., strictly-monotonic) or asynchronous (i.e., weakly-monotonic) interpretation: EXPSPACE-complete. [1]

MTL has been described as a prominent specification formalism for real-time systems.[2] The decidability of full MTL over infinite timed words is undecidable.[3]


  1. ^ Alur R., Henzinger T.A. (1992) Logics and models of real time: A survey. In: de Bakker J.W., Huizing C., de Roever W.P., Rozenberg G. (eds) Real-Time: Theory in Practice. REX 1991. Lecture Notes in Computer Science, vol 600. Springer, Berlin, Heidelberg
  2. ^ J. Ouaknine and J. Worrell, "On the decidability of metric temporal logic," 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005, pp. 188-197.
  3. ^ Ouaknine J., Worrell J. (2006) On Metric Temporal Logic and Faulty Turing Machines. In: Aceto L., Ingólfsdóttir A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg