Metric temporal logic

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.

Depending on the authors, MTL is either defined as the future fragment of MTL, in which case full-MTL is called MTL+Past.[1][3] Or MTL is defined as full-MTL.

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.

We denote by ${\displaystyle \phi {\mathcal {R}}_{I}\psi }$ (pronounced "${\displaystyle \phi }$ release in ${\displaystyle I}$, ${\displaystyle \psi }$") the formula ${\displaystyle \neg \phi {\mathcal {U}}_{I}\neg \psi }$. This formula holds at time ${\displaystyle t}$ if either:

• there is some time ${\displaystyle t'\in t+I}$ such that ${\displaystyle \phi }$ holds, and ${\displaystyle \psi }$ hold in the interval ${\displaystyle (t,t')\cap (t+I)}$.
• at each time ${\displaystyle t'\in t+I}$, ${\displaystyle \phi }$ holds.

The name "release" come from the LTL case, where this formula simply means that ${\displaystyle \phi }$ should always hold, unless ${\displaystyle \psi }$ releases it.

The past counterpart of release is denote by ${\displaystyle \phi {\mathcal {B}}_{I}\psi }$ (pronounced "${\displaystyle \phi }$ back to in ${\displaystyle I}$, ${\displaystyle \psi }$") and is equal to the formula ${\displaystyle \neg \phi {\mathcal {S}}_{I}\neg \psi }$.

We denote by ${\displaystyle \Diamond _{I}\phi }$ or ${\displaystyle {\mathcal {F}}_{I}\phi }$ (pronounced "Finally in ${\displaystyle I}$, ${\displaystyle \phi }$", or "Eventually in ${\displaystyle I}$, ${\displaystyle \phi }$") the formula ${\displaystyle \top {\mathcal {U}}_{I}\phi }$. Intuitively, this formula holds at time ${\displaystyle t}$ if there is some time ${\displaystyle t'\in t+I}$ such that ${\displaystyle \phi }$ holds.

We denote by ${\displaystyle \Box _{I}\phi }$ or ${\displaystyle {\mathcal {G}}_{I}\phi }$ (pronounced "Globally in ${\displaystyle I}$, ${\displaystyle \phi }$",) the formula ${\displaystyle \neg \Diamond _{I}\neg \phi }$. Intuitively, this formula holds at time ${\displaystyle t}$ if for all time ${\displaystyle t'\in t+I}$, ${\displaystyle \phi }$ holds.

We denote by ${\displaystyle {\overleftarrow {\Box }}_{I}\phi }$ and ${\displaystyle {\overleftarrow {\Diamond }}_{I}\phi }$ the formula similar to ${\displaystyle \Box _{I}\phi }$ and ${\displaystyle \Diamond _{I}\phi }$, where ${\displaystyle {\mathcal {U}}}$ is replaced by ${\displaystyle {\mathcal {S}}}$. 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 ${\displaystyle \gamma }$ considered.

We denote by ${\displaystyle \bigcirc _{I}\phi }$ or ${\displaystyle {\mathcal {N}}_{I}\phi }$ (pronounced "Next in ${\displaystyle I}$, ${\displaystyle \phi }$") the formula ${\displaystyle \bot {\mathcal {U}}_{I}\phi }$. Similarly, we denote by ${\displaystyle \ominus _{I}\phi }$[4] (pronounced "Previously in ${\displaystyle I}$, ${\displaystyle \phi }$) the formula ${\displaystyle \bot {\mathcal {S}}_{I}\phi }$. The following discussion about the Next operator also holds for the Previously operator, by reversing the past and the future.

When this formula is evaluated over a timed word ${\displaystyle \gamma :T\to A}$, this formula means that both:

• at the next time in the domain of definition ${\displaystyle T}$, the formula ${\displaystyle \phi }$ will holds.
• furthermore, the distance between this next time and the current time belong to the interval ${\displaystyle I}$.
• In particular, this next time holds, thus the current time is not the end of the word.

When this formula is evaluated over a signal ${\displaystyle \gamma }$, the notion of next time does not makes sense. Instead, "next" means "immediately after". More precisely ${\displaystyle \gamma ,t\models \circ \phi }$ means:

• ${\displaystyle I}$ contains an interval of the form ${\displaystyle (0,\epsilon )}$ and
• for each ${\displaystyle t'\in (t,t+\epsilon )}$, ${\displaystyle \gamma ,t'\models \phi }$.

We now consider operators which are not similar to any standard LTL operators.

We denote by ${\displaystyle \uparrow \phi }$ (pronounced "rise ${\displaystyle \phi }$"), a formula which holds when ${\displaystyle \phi }$ becomes true. More precisely, either ${\displaystyle \phi }$ did not hold in the immediate past, and holds at this time, or it does not hold and it holds in the immediate future. Formally ${\displaystyle \uparrow \phi }$ is defined as ${\displaystyle (\phi \land (\neg \phi {\mathcal {S}}\top ))\lor (\neg \phi \land (\phi {\mathcal {U}}\top ))}$.[5]

Over timed words, this formula always hold. Indeed ${\displaystyle \phi {\mathcal {U}}\top }$ and ${\displaystyle \neg \phi {\mathcal {S}}\top }$ always hold. Thus the formula is equivalent to ${\displaystyle \phi \lor \neg \phi }$, hence is true.

By symmetry, we denote by ${\displaystyle \downarrow \phi }$ (pronounced "Fall ${\displaystyle \phi }$), a formula which holds when ${\displaystyle \phi }$ becomes false. Thus, it is defined as ${\displaystyle (\neg \phi \land (\phi {\mathcal {S}}\top ))\land (\phi \land (\neg \phi {\mathcal {U}}\top ))}$.

We now introduce the prophecy operator, denoted by ${\displaystyle \triangleright }$. We denote by ${\displaystyle \triangleright _{I}\phi }$[6] the formula ${\displaystyle \neg \phi {\mathcal {U}}_{I}\phi }$. This formula asserts that there exists a first moment in the future such that ${\displaystyle \phi }$ holds, and the time to wait for this first moment belongs to ${\displaystyle I}$.

We now consider this formula over timed words and over signals. We consider timed words first. Assume that ${\displaystyle I=\mid a,b\mid '}$ where ${\displaystyle \mid }$ and ${\displaystyle \mid '}$ represents either open or closed bounds. Let ${\displaystyle \gamma }$ a timed word and ${\displaystyle t}$ in its domain of definition. Over timed words, the formula ${\displaystyle \gamma ,t\models \triangleright _{I}\phi }$ holds if and only if ${\displaystyle \gamma ,t\models \Box _{]0,b[\setminus I}\neg \phi \land \Diamond _{I}\phi }$ also holds. That is, this formula simply assert that, in the future, until the interval ${\displaystyle t+I}$ is met, ${\displaystyle \phi }$ should not hold. Furthermore, ${\displaystyle \phi }$ should hold sometime in the interval ${\displaystyle t+I}$. Indeed, given any time ${\displaystyle t''\in t+I}$ such that ${\displaystyle \gamma ,t''\models \phi }$ hold, there exists only a finite number of time ${\displaystyle t'\in t+I}$ with ${\displaystyle t'<t''}$ and ${\displaystyle \gamma ,t'\models \phi }$. Thus, there exists necessarily a smaller such ${\displaystyle t''}$.

Let us now consider signal. 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 ${\displaystyle t'}$, due to the fact that the domain of definition of a signal is continuous. Thus, the formula ${\displaystyle \triangleright _{I}\phi }$ also ensures that the first interval in which ${\displaystyle \phi }$ holds is closed on the left.

By temporal symmetry, we define the history operator, denoted by ${\displaystyle \triangleleft }$. We define ${\displaystyle \triangleleft _{I}\phi }$ as ${\displaystyle \neg \phi {\mathcal {S}}_{I}\phi }$. This formula asserts that there exists a last moment in the past such that ${\displaystyle \phi }$ held. And the time since this first moment belongs to ${\displaystyle I}$.

The semantic of operators until and since introduced do not consider the current time. That is, in order for ${\displaystyle \phi _{1}{\overline {\mathcal {U}}}\phi _{2}}$ to holds at some time ${\displaystyle t}$, neither ${\displaystyle \phi _{1}}$ nor ${\displaystyle \phi _{2}}$ has to hold at time ${\displaystyle t}$. This is not always wanted, for example in the sentence "there is no bug until the system is turned-off", it may actually be wanted that there are no bug at current time. Thus, we introduce another until operator, called non-strict until, denoted by ${\displaystyle {\overline {\mathcal {U}}}}$, which consider the current time.

We denote by ${\displaystyle \phi _{1}{\overline {\mathcal {U}}}_{I}\phi _{2}}$ and ${\displaystyle \phi _{1}{\overline {\mathcal {S}}}_{I}\phi _{2}}$ either:

• the formulas ${\displaystyle \phi _{2}\lor (\phi _{1}\land (\phi _{1}{\mathcal {U}}_{I}\phi _{2}))}$ and ${\displaystyle \phi _{2}\lor (\phi _{1}\land (\phi _{1}{\mathcal {S}}_{I}\phi _{2}))}$ if ${\displaystyle 0\in I}$, and
• the formulas ${\displaystyle \phi _{1}\land (\phi _{1}{\mathcal {U}}_{I}\phi _{2})}$ and ${\displaystyle \phi _{1}\land (\phi _{1}{\mathcal {S}}_{I}\phi _{2})}$ otherwise.

For any of the operators ${\displaystyle {\mathcal {O}}}$ introduced above, we denote ${\displaystyle {\overline {\mathcal {O}}}}$ the formula in which non-strict untils and sinces are used. For example ${\displaystyle {\overline {\Diamond }}p}$ is an abbreviation for ${\displaystyle \top {\overline {\mathcal {U}}}p}$.

Strict operator can not be defined using non-strict operator. That is, there is no formula equivalent to ${\displaystyle \bigcirc _{I}p}$ which uses only non-strict operator. This formula is defined as ${\displaystyle \bot {\mathcal {U}}_{I}p}$. This formula can never hold at a time ${\displaystyle t}$ if it is required that ${\displaystyle \bot }$ holds at time ${\displaystyle t}$.

An important subset of MTL is the Metric Interval Temporal Logic (MITL). This is defined similarly to MTL, with the restriction that the sets ${\displaystyle I}$, used in ${\displaystyle {\mathcal {U}}}$ and ${\displaystyle {\mathcal {S}}}$, are intervals which are not singletons, and whose bounds are natural numbers or infinity.

Some other subsets of MITL are defined in the article MITL.

Future-MTL was already introduced above. Both over timed-words and over signals, it is less expressive than Full-MTL[3]^: 3.

The fragment Event-Clock Temporal Logic[6] of MTL, denoted EventClockTL or ECL, allows only the following operators:

• the boolean operators, and, or, not
• the untimed until and since operators.
• The timed prophecy and history operators.

Over signals, ECL is as expressive as MITL and as MITL₀. The equivalence between the two last logics is explained in the article MITL₀. We sketch the equivalence of those logics with ECL.

If ${\displaystyle I}$ is not a singleton and ${\displaystyle \phi }$ is a MITL formula, ${\displaystyle \triangleright _{I}\phi }$ is defined as a MITL formula. If ${\displaystyle I=\{i\}}$ is a singleton, then ${\displaystyle \triangleright _{I}\phi }$ is equivalent to ${\displaystyle \Box _{]0,i[}\neg \phi \land \Diamond _{]0,i]}\phi }$ which is a MITL-formula. Reciprocally, for ${\displaystyle \psi }$ an ECL-formula, and ${\displaystyle I}$ an interval whose lower bound is 0, ${\displaystyle \Box _{I}\psi }$ is equivalent to the ECL-formula ${\displaystyle \neg \triangleright _{I}\neg \psi }$.

The satisfiability of ECL over signals is PSPACE-complete.[6]

A MTL-formula in positive normal form is defined almost as any MTL formula, with the two following change:

• the operators Release and Back are introduced in the logical language and are not considered anymore to be notations for some other formulas.
• negations can only be applied to letters.

Any MTL formula is equivalent to formula in normal form. This can be shown by an easy induction on formulas. For example, the formula ${\displaystyle \neg (\phi {\mathcal {U}}_{S}\psi )}$ is equivalent to the formula ${\displaystyle (\neg \phi ){\mathcal {R}}_{S}(\neg \psi )}$. 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.