Metric interval temporal logic

In model checking, the Metric Interval Temporal Logic (MITL) is a fragment of Metric Temporal Logic (MTL). This fragment is often preferred to MTL because some problems which are undecidable for MTL becomes decidable for MITL.

Definition

A MITL formula is a MTL formula, as defined in the Metric temporal logic, such that each set of real used in subscript are intervals, which are not singletons, and whose bounds are either a natural number or the infinite.

Difference with MTL

MTL can express a statement such as "P holed exactly ten-time units ago". Let us call S this sentence. This is impossible in MITL. Instead, it can be said that "P holed between 9 and 10-time units ago". Let us call T this statement. Since MITL can express T but not S, in a sense, MITL is a restriction of MTL which allow only less precise statement.

Problems of MTL 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 time in a single time unit. Indeed, the truth value of this statement change as many time 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 or a signal automaton, which want to know at each instant whether S holds or not. This system should recall everything which occurred in the last 10 time units. As seen above, it means that it must recall an arbitrarily great number of event. Which means that this can not be implemented by a system with finite memory and clocks.

Bounded variability

One of the main advantages of MITL is that each operator has the bounded variability property. We are first given an example before explaining what it means.

Consider now the statement T defined above. Note that each time the truth value of T switch from false to true, it remains true for at least a time unit. We now prove this statement. At a time t where T becomes true, it means both:

• that between 9 and 10 time units ago, P was true.
• and that just before time t, P was false.

Hence, P was true exactly 9 time units ago. It follows that, for each $t'\in [0,1]$, at time $t+t'$, P was true $9+t'$ time units ago. Since $9+t'\in [9,10]$, at time $t'$, T holds.

As in the previous section, consider a system which, at each instant, wants to know the value of T. As explained above, this system must recall what did occur during the last ten unit of times. However, thanks to the bounded variability property, we know that it has to recall at most 10 times when T becomes true. And hence 11 times when T becomes false. Thus this system would need to recall at most 21 events, hence can be implemented as a timed automaton or a signal automaton.

Examples

We now give some example of MITL formulas.

• $\square \diamond _{(0,1)}p$ states that there the letter $p$ appears at least one in each open interval of length 1.
• $\triangleright _{\{i\}}p$ where $\triangleright _{\{i\}}p$ is the prophecy operator defined as $\square _{(0,i)}\neg p\land \diamond _{(0,i]}p$ and which states that the first occurrence of $p$ in the future is in $i$ time unit.
• $p\land \square (p\implies \triangleright _{\{1\}}p)$ states that $p$ holds exactly at each integral time and not anytime else.

Fragments of MITL

Safety-MTL_0,∞

The fragment Safety-MTL_0,v is defined as the subset of MITL_0,∞ containing only formulas in positive normal form where the interval of every until operators has an upper bound. For example, the formula $\Box (a\implies \Diamond _{(0,1]}b)$ which states that each $a$ is followed, less than one time unit later, by a $b$, belongs to this logic.

Open and closed MITL

The fragment Open-MTL contains the formula in positive normal form such that:

• for each ${\mathcal {U}}_{I}$, $I$ is open, and
• for each ${\mathcal {R}}_{I}$, $I$ is closed.

The fragment Closed-MITL contains the negation of formulas of Open-MITL.

Flat and Coflat MITL

The fragment Flat-MTL contains the formula in positive normal form such that

• for each $\phi _{1}{\mathcal {U}}_{I}\phi _{2}$, if $I$ is unbounded, then $\phi _{1}$ is a LTL-formula
• for each $\phi _{1}{\mathcal {R}}_{I}\phi _{2}$, if $I$ is unbounded, then $\phi _{2}$ is a LTL-formula

The fragment Coflat-MITL contains the negation of formulas of Flat-MITL.

Non-strict variant

Given any fragment L, the fragment L^ns is the restriction of L in which only non strict operators are used.

MITL_0,∞ and MITL₀

Given any fragment L, the fragment L_0,∞ is the subset of L where the lower bound of each interval is 0 or the upper bound is infinity. Similarly we denote by L₀ (respectively, L_∞) the subset of L such that the lower bound of each interval is 0 (respectively, the upper bound of each interval is ∞).

Expressiveness over signals

Over signals, MITL₀ is as expressive as MITL. This can be proven by applying the following rewriting rules to a MITL formula.

• $\phi {\mathcal {U}}_{(a,b)}\psi$ is equivalent to $\Box _{(0,a]}\phi {\mathcal {U}}\psi \land \Diamond _{(a,b)}\psi$ (the construction for half-closed and closed intervals is similar).
• $\Diamond _{(a,b)}\phi$ is equivalent to $\Diamond _{(2a-b,a)}\Box _{(0,b-a)}\Diamond _{(0,b-a)}\phi$ if $2a-b\geq 0$.
• $\Diamond _{(a,b)}\phi$ is equivalent to $\Diamond _{(a,b-a)}\Diamond _{(0,a)}\phi$ if $a<b$.
• $\Diamond _{(a,+\infty )}\phi$ is equivalent to $\Box _{(0,a)}\Diamond \phi$.

It should be noted that applying those rewriting rules exponentially increase the size of the formula. Indeed, the numbers $a$ and $b$ are traditionally written in binary, and those rules should be applied $O\left({\frac {b}{b-a}}\right)$ times.

Expressiveness over timed words

Contrary to the case of signals, MITL is strictly more expressive than MITL_0,∞. The rewriting rules given above do not apply in the case of timed words because, in order to rewrite $\Diamond _{(a,b)}$ there assume that some event occurs between times 0 and $a$, which is not necessarily the case anymore.

Advisability problem

The problem of deciding whether a MITL formula is satisfiable over a signal is in PSPACE-complete.