Metric temporal logic (original) (raw)

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 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. MTL has been described as a prominent specification formalism for real-time systems. Full MTL over infinite timed words is undecidable.