In model checking, the Metric Interval Temporal Logic (MITL) is a fragment of Metric Temporal Logic (MTL).
A MITL formula is an MTL formula, such that each set of reals used in subscript are intervals, which are not singletons, and whose bounds are either a natural number or are infinite.
[citation needed] MTL can express a statement such as the sentence S: "P held exactly ten time units ago".
Instead, MITL can say T: "P held between 9 and 10 time units ago".
One reason to want to avoid a statement such as S is that its truth value may change an arbitrary number of times in a single time unit.
This system should recall everything that occurred in the last 10 time units.
As seen above, it means that it must recall an arbitrarily large number of events.
This can not be implemented by a system with finite memory and clocks.
One of the main advantage of MITL is that each operator has the bounded variability property.
However, thanks to the bounded variability property, it must recall at most 10 time units when T becomes true.
Examples of MITL formulas: The fragment Safety-MTL0,v is defined as the subset of MITL0,∞ containing only formulas in positive normal form where the interval of every until operator has an upper bound.
[1] The fragment Open-MTL contains the formula in positive normal form such that: The fragment Closed-MITL contains the negation of formulas of Open-MITL.
The fragment Flat-MTL contains the formula in positive normal form such that: The fragment Coflat-MITL contains the negation of formulas of Flat-MITL.
This can be proven by applying the following rewriting rules to a MITL formula.
[2] Applying those rewriting rules exponentially increases the size of the formula.
are traditionally written in binary, and those rules should be applied
Contrary to the case of signals, MITL is strictly more expressive than MITL0,∞.
the assumption must be that some event occurs between times 0 and
Logics and Models of Real-Time: A Survey.
REX Workshop, Real-time: Theory in Practice, pages 74–106.
It's about Time: Real-time Logics Reviewed.