metric temporal logic

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:

• a finite set of propositional variables AP,
• the logical operators ¬ and ∨, and
• the temporal modal operator {{mvar|U_I}} (pronounced "{{mvar|φ}} until in {{mvar|I}} {{mvar|ψ}}."), with {{mvar|I}} an interval of non-negative numbers.
• the temporal modal operator {{mvar|S_I}} (pronounced "{{mvar|φ}} since in {{mvar|I}} {{mvar|ψ}}."), with {{mvar|I}} as above.

When the subscript is omitted, it is implicitly equal to $[0,\backslash infty)$.

Note that the next operator N is not considered to be a part of MTL syntax. It will instead be defined from other operators.

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.{{cite conference |last1=Bouyer |first1=Patricia |author1-link=Patricia Bouyer-Decitre|last2=Chevalier |first2=Fabrice |last3=Markey |first3=Nicolas |title=FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, Proceedings |chapter=On the Expressiveness of TPTL and MTL |series=Lecture Notes in Computer Science |date=2005 |volume=3821 |page=436| editor1 = Sundar Sarukkai | editor2= Sandeep Sen | conference =25th International Conference, Hyderabad, India, December 15–18, 2005 |doi = 10.1007/11590156_35 |isbn=978-3-540-32419-5|chapter-url=https://hal.archives-ouvertes.fr/hal-01194615/document}} 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.

Let $T\backslash subseteq\backslash mathbb\; R\_+$ intuitively represent a set

of points in time. Let $\backslash gamma:\; T\backslash to\; A$ a function which associates a letter to

each moment $t\backslash in\; T$. A model of a MTL formula is

such a function $\backslash gamma$. Usually, $\backslash gamma$ is

either a timed word or a signal. In

those cases, $T$ is either a discrete subset or an interval

containing 0.

Let $T$ and $\backslash gamma$ as above and let $t\backslash in$

T some fixed time. We are now going to explain what it means

that a MTL formula $\backslash phi$ holds at time $t$,

which is denoted $\backslash gamma,t\backslash models\backslash phi$.

Let $I\backslash subseteq\backslash mathbb\; R\_+$ and $\backslash phi,\backslash psi\backslash in$

MTL. We first consider the formula $\backslash phi\backslash mathcal$

U_I\psi. We say

that $\backslash gamma,t\backslash models\backslash phi\backslash mathcal\; U\_I\backslash psi$ if and only if

there exists some time $t\text{'}\backslash in\; I+t$ such that:

• $\backslash gamma,t\text{'}\backslash models\backslash psi$ and
• for each $t$\in T with <

t' , $\backslash gamma,t\text{'}\text{'}\backslash models\backslash phi$.

We now consider the formula $\backslash phi\backslash mathcal$

S_I\psi (pronounced "$\backslash phi$ since

in $I$ $\backslash psi$.") We say

that $\backslash gamma,t\backslash models\backslash phi\backslash mathcal\; S\_I\backslash psi$ if and only if

there exists some time $t\text{'}\backslash in\; I-t$ such that:

• $\backslash gamma,t\text{'}\backslash models\backslash psi$ and
• for each $t$\in T with <

t , $\backslash gamma,t\text{'}\text{'}\backslash models\backslash phi$.

The definitions of $\backslash gamma,t\backslash models\backslash phi$ for the values

of $\backslash phi$ not considered above is similar as the definition

in the LTL case.

Some formulas are so often used that a new operator is introduced for

them. These operators are usually not considered to belong to the

definition of MTL, but are syntactic sugar which denote more

complex MTL formula. We first consider operators which also exists in LTL. In

this section, we fix $\backslash phi,\backslash psi$ MTL formulas

and $I\backslash subseteq\backslash mathbb\; R\_+$.

We denote by $\backslash phi\backslash mathcal\; R\_I\backslash psi$

(pronounced "$\backslash phi$ release

in $I$, $\backslash psi$") the

formula $\backslash neg(\backslash neg\backslash phi\backslash mathcal\; U\_I\backslash neg\backslash psi)$. This formula holds

at time $t$ if either:

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

The name "release" come from the LTL case, where this formula simply

means that $\backslash psi$ should always hold,

unless $\backslash phi$ releases it.

The past counterpart of release is denote by $\backslash phi\backslash mathcal\; B\_I\backslash psi$

(pronounced "$\backslash phi$ back to

in $I$, $\backslash psi$") and is equal to the

formula $\backslash neg(\backslash neg\backslash phi\backslash mathcal\; S\_I\backslash neg\backslash psi)$.

We denote by $\backslash Diamond\_I\backslash phi$ or $\backslash mathcal$

F_I\phi (pronounced "Finally

in $I$, $\backslash phi$", or "Eventually

in $I$, $\backslash phi$") the formula $\backslash top\backslash mathcal$

U_I\phi. Intuitively, this formula holds at time $t$

if there is some time $t\text{'}\backslash in\; t+I$ such

that $\backslash phi$ holds.

We denote by $\backslash Box\_I\backslash phi$ or $\backslash mathcal$

G_I\phi (pronounced "Globally

in $I$, $\backslash phi$",) the

formula $\backslash neg\backslash Diamond\_I\backslash neg\backslash phi$. Intuitively, this formula

holds at time $t$ if for all time $t\text{'}\backslash in$

t+I, $\backslash phi$ holds.

We denote by $\backslash overleftarrow\backslash Box\_I\backslash phi$

and $\backslash overleftarrow\backslash Diamond\_I\backslash phi$ the formula similar

to $\backslash Box\_I\backslash phi$ and $\backslash Diamond\_I\backslash phi$,

where $\backslash mathcal\; U$ is replaced by $\backslash 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 $\backslash gamma$ considered.

We denote by $\backslash bigcirc\_I\backslash phi$ or $\backslash mathcal\; N\_I\backslash phi$

(pronounced "Next in $I$, $\backslash phi$") the

formula $\backslash bot\backslash mathcal\; U\_I\backslash phi$. Similarly, we denote by $\backslash ominus\_I\backslash phi${{cite book |last1=Maler |first1=Oded |last2=Nickovic |first2=Dejan |last3=Pnueli |first3=Amir |page=478 |title=Pillars of computer science |chapter=Checking temporal properties of discrete, timed and continuous behaviors |date=2008 |publisher=ACM |isbn=978-3-540-78126-4}} (pronounced "Previously in $I$, $\backslash phi$) the formula $\backslash bot\backslash mathcal\; S\_I\backslash 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 $\backslash gamma:T\backslash to$

A, this formula

means that both:

• at the next time in the domain of definition $T$, the formula $\backslash phi$ will holds.
• furthermore, the distance between this next time and the current time belong to the interval $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 $\backslash gamma$, the notion of next time does

not makes sense. Instead, "next" means "immediately after". More

precisely $\backslash gamma,t\backslash models\backslash circ\backslash phi$ means:

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

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

We denote by $\backslash uparrow\backslash phi$ (pronounced "rise $\backslash phi$"), a formula which holds when $\backslash phi$ becomes true. More precisely, either $\backslash 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 $\backslash uparrow\backslash phi$ is defined as $(\backslash phi\backslash land(\backslash neg\backslash phi\backslash mathcal\; S\backslash top))\backslash lor(\backslash neg\backslash phi\backslash land(\backslash phi\backslash mathcal\; U\backslash top))$.{{cite thesis |last=Nickovic |first=Dejan |date=31 August 2009 |title= Checking Timed and Hybrid Properties: Theory and Applications |chapter=3 |chapter-url=https://tel.archives-ouvertes.fr/tel-00411957/en/ }}

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

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

We now introduce the prophecy operator, denoted by $\backslash triangleright$. We denote by $\backslash triangleright\_I\backslash phi${{cite book |last1=Henzinger |first1=T.A. |last2=Raskin |first2=J.F. |last3=Schobbens |first3=P.-Y. |title=Automata, Languages and Programming |chapter=The regular real-time languages |series=Lecture Notes in Computer Science |date=1998 |volume=1443 |page=590 |doi=10.1007/BFb0055086|isbn=978-3-540-64781-2 }} the formula $\backslash neg\backslash phi\backslash mathcal\; U\_I\backslash phi$. This formula asserts that there exists a first moment in the future such that $\backslash phi$ holds, and the time to wait for this first moment belongs to $I$.

We now consider this formula over timed words and over signals. We consider timed words first. Assume that $I=\backslash mid\; a,b\backslash mid\text{'}$ where $\backslash mid$ and $\backslash mid\text{'}$ represents either open or closed bounds. Let $\backslash gamma$ a timed word and $t$ in its domain of definition.

Over timed words, the formula $\backslash gamma,t\backslash models\backslash triangleright\_I\backslash phi$ holds if and only if $\backslash gamma,t\backslash models\backslash Box\_\{]0,b[\backslash setminus\; I\}\backslash neg\backslash phi\backslash land\backslash Diamond\_I\backslash phi$ also holds. That is, this formula simply assert that, in the future, until the interval $t+I$ is met, $\backslash phi$ should not hold. Furthermore, $\backslash phi$ should hold sometime in the interval $t+I$. Indeed, given any time $t$\in t+I such that $\backslash gamma,t$\models\phi hold, there exists only a finite number of time $t\text{'}\backslash in\; t+I$ with and $\backslash gamma,t\text{'}\backslash models\backslash phi$. Thus, there exists necessarily a smaller such $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 $t\text{'}$, due to the fact that the domain of definition of a signal is continuous. Thus, the formula $\backslash triangleright\_I\backslash phi$ also ensures that the first interval in which $\backslash phi$ holds is closed on the left.

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

The semantic of operators until and since introduced do not consider the current time. That is, in order for $\backslash phi\_1\backslash mathcal\{U\}\backslash phi\_2$ to holds at some time $t$, neither $\backslash phi\_1$ nor $\backslash phi\_2$ has to hold at time $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 $\backslash overline\{\backslash mathcal\; U\}$, which consider the current time.

We denote by $\backslash phi\_1\backslash overline\{\backslash mathcal\; U\}\_\{I\}\backslash phi\_2$ and $\backslash phi\_1\backslash overline\{\backslash mathcal\; S\}\_\{I\}\backslash phi\_2$ either:

• the formulas $\backslash phi\_2\backslash lor(\backslash phi\_1\backslash land\; (\backslash phi\_1\backslash mathcal\; U\_\{I\}\backslash phi\_2))$ and $\backslash phi\_2\backslash lor(\backslash phi\_1\backslash land\; (\backslash phi\_1\backslash mathcal\; S\_\{I\}\backslash phi\_2))$ if $0\backslash in\; I$, and
• the formulas $\backslash phi\_1\backslash land(\backslash phi\_1\backslash mathcal\; U\_\{I\}\backslash phi\_2)$ and $\backslash phi\_1\backslash land(\backslash phi\_1\backslash mathcal\; S\_\{I\}\backslash phi\_2)$ otherwise.

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

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

== Example ==

We now give examples of MTL formulas. Some more example can be found on article of fragments of MITL, such as metric interval temporal logic.

• $\backslash Box(p\backslash implies\backslash Diamond\_\{\backslash \{1\backslash \}\}q)$ states that each letter $p$ is followed exactly one time unit later by a letter $q$.
• $\backslash Box(p\backslash implies\backslash neg\backslash Diamond\_\{\backslash \{1\backslash \}\}p)$ states that no two successive occurrences of $p$ can occur at exactly one time unit from each other.

A standard (untimed) infinite word $w=a\_0,a\_1,\backslash dots,$ is a

function from $\backslash mathbb\; N$ to $A$. We can

consider such a word using the set of time $T=\backslash mathbb\; N$,

and the function $\backslash gamma(i)=a\_i$. In this case,

for $\backslash phi$ an arbitrary LTL

formula, $w,i\backslash models\backslash phi$ if and only

if $\backslash gamma,i\backslash models\backslash phi$, where $\backslash phi$ is

considered as a MTL formula with non-strict operator and $[0,\backslash infty)$ subscript. In this sense, MTL is an extension of LTL.{{clarify|date=August 2019}}

For this reason, a formula using only non-strict operator with $[0,\backslash infty)$ subscript is called an LTL formula. This is because the

{{Explain|date=August 2019}}

The satisfiability of ECL over signals is EXPSPACE-complete.

We now consider some fragments of MTL.

{{Main|Metric interval temporal logic}}

An important subset of MTL is the Metric Interval Temporal Logic (MITL). This is defined similarly to MTL, with the

restriction that the sets $I$, used in $\backslash mathcal$

U and $\backslash 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{{r|ExpressivenesOfTPTLAndMtl|p=3}}.

=== Event-Clock Temporal Logic ===

The fragment Event-Clock Temporal Logic 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 $I$ is not a singleton and $\backslash phi$ is a MITL formula, $\backslash triangleright\_I\backslash phi$ is defined as a MITL formula. If $I=\backslash \{i\backslash \}$ is a singleton, then $\backslash triangleright\_I\backslash phi$ is equivalent to $\backslash Box\_\{]0,i[\}\backslash neg\backslash phi\backslash land\backslash Diamond\_\{]0,i]\}\backslash phi$ which is a MITL-formula. Reciprocally, for $\backslash psi$ an ECL-formula, and $I$ an interval whose lower bound is 0, $\backslash Box\_I\backslash psi$ is equivalent to the ECL-formula $\backslash neg\backslash triangleright\_I\backslash neg\backslash psi$.

The satisfiability of ECL over signals is PSPACE-complete.

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 $\backslash neg(\backslash phi\backslash mathcal\; U\_\{S\}\backslash psi)$ is equivalent to the formula $(\backslash neg\backslash phi)\backslash mathcal\; R\_\{S\}(\backslash neg\backslash 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.

• Timed propositional temporal logic, another extension of LTL in which time can be measured.

{{reflist}}

Category:Temporal logic

Category:Model checking