In
model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
, the Metric Interval Temporal Logic (MITL) is a fragment of
Metric Temporal Logic 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 linea ...
(MTL). This fragment is often preferred to MTL because some problems that are
undecidable for MTL become
decidable for MITL.
Definition
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.
Difference from MTL
MTL can express a statement such as the sentence S: "P held exactly ten time units ago". This is impossible in MITL. Instead, MITL can say T: "P held between 9 and 10 time units ago". Since MITL can express T but not S, in a sense, MITL is a restriction of MTL which allows only less precise statements.
Problems that MITL avoids
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. Indeed, the truth value of this statement may change as many times as the truth value of P change, and P itself may change an arbitrary number of time in a single time unit.
Let us now consider a system, such as a
timed automaton In automata theory, a timed automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a timed automaton, clock values increase all with the same speed. Along the transitions of the automaton, clock values can ...
or a
signal automaton
In automata theory, a field of computer science, a signal automaton is a finite automaton extended with a finite set of real-valued clocks. During a run of a signal automaton, clock values increase all with the same speed. Along the transitions of ...
, which want to know at each instant whether S holds or not. 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.
Bounded variability
One of the main advantage of MITL is that each operator has the bounded variability property. Example:
Given the statement T defined above. Each time the truth value of T switches from false to true, it remains true for at least one time unit. Proof: At a time t where T becomes true, it means that:
* between 9 and 10 time units ago, P was true.
* just before time t, P was false.
Hence, P was true exactly 9 time units ago. It follows that, for each