What is Metric temporal logic?

Metric temporal logic 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 a 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 or asynchronous interpretation: EXPSPACE-complete.

MTL has been described as a prominent specification formalism for real-time systems. Full MTL over infinite timed words is undecidable.