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.
MTL has been described as a prominent specification formalism for real-time systems.
[1] Full MTL over infinite timed words is undecidable.
[2] The full metric temporal logic is defined similarly to linear temporal logic, where a set of non-negative real number is added to temporal modal operators U and S. Formally, MTL is built up from: When the subscript is omitted, it is implicitly equal to
Note that the next operator N is not considered to be a part of MTL syntax.
The past fragment of metric temporal logic, denoted as past-MTL is defined as the restriction of the full metric temporal logic without the until operator.
Similarly, the future fragment of metric temporal logic, denoted as future-MTL is defined as the restriction of the full metric temporal logic without the since operator.
In order to avoid ambiguity, this article uses the names full-MTL, past-MTL and future-MTL.
When the statements holds for the three logic, MTL will simply be used.
if either: The name "release" come from the LTL case, where this formula simply means that
Both formula has intuitively the same meaning, but when we consider the past instead of the future.
This case is slightly different from the previous ones, because the intuitive meaning of the "Next" and "Previously" formulas differs depending on the kind of function
This formula asserts that there exists a first moment in the future such that
holds, and the time to wait for this first moment belongs to
We now consider this formula over timed words and over signals.
That is, this formula simply assert that, in the future, until the interval
The equivalence mentioned above does not hold anymore over signal.
This is due to the fact that, using the variables introduced above, there may exists an infinite number of correct values for
, due to the fact that the domain of definition of a signal is continuous.
By temporal symmetry, we define the history operator, denoted by
The semantic of operators until and since introduced do not consider the current time.
Some more example can be found on article of fragments of MITL, such as metric interval temporal logic.
[clarification needed] For this reason, a formula using only non-strict operator with
This is because the[further explanation needed] The satisfiability of ECL over signals is EXPSPACE-complete.
An important subset of MTL is the Metric Interval Temporal Logic (MITL).
, are intervals which are not singletons, and whose bounds are natural numbers or infinity.
The fragment Event-Clock Temporal Logic[6] of MTL, denoted EventClockTL or ECL, allows only the following operators: Over signals, ECL is as expressive as MITL and as MITL0.
Similarly, conjunctions and disjunctions can be considered using De Morgan's laws.
Strictly speaking, the set of formulas in positive normal form is not a fragment of MTL.