Metric temporal logic explained

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 linear-time logic that assumes both the interleaving and fictitious-clock abstractions. It is defined over a point-based weakly-monotonic integer-time semantics.

MTL has been described as a prominent specification formalism for real-time systems.[1] Full MTL over infinite timed words is undecidable.[2]

Syntax

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:

When the subscript is omitted, it is implicitly equal to

[0,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.

Past and Future

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] 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.

Model

Let

T\subseteqR+

intuitively represent a setof points in time. Let

\gamma:T\toA

a function which associates a letter toeach moment

t\inT

. A model of a MTL formula issuch a function

\gamma

. Usually,

\gamma

iseither a timed word or a signal. Inthose cases,

T

is either a discrete subset or an intervalcontaining 0.

Semantics

Let

T

and

\gamma

as above and let

t\in T

some fixed time. We are now going to explain what it meansthat a MTL formula

\phi

holds at time

t

,which is denoted

\gamma,t\models\phi

.

Let

I\subseteqR+

and

\phi,\psi\in MTL

. We first consider the formula

\phil UI\psi

. We saythat

\gamma,t\models\philUI\psi

if and only ifthere exists some time

t'\inI+t

such that:

\gamma,t'\models\psi

and

t''\inT

with

t<t''< t'

,

\gamma,t''\models\phi

.

We now consider the formula

\phil SI\psi

(pronounced "

\phi

sincein

I

\psi

.") We saythat

\gamma,t\models\philSI\psi

if and only ifthere exists some time

t'\inI-t

such that:

\gamma,t'\models\psi

and

t''\inT

with

t'<t''< t

,

\gamma,t''\models\phi

.

The definitions of

\gamma,t\models\phi

for the valuesof

\phi

not considered above is similar as the definitionin the LTL case.

Operators defined from basic MTL operators

Some formulas are so often used that a new operator is introduced forthem. These operators are usually not considered to belong to thedefinition of MTL, but are syntactic sugar which denote morecomplex MTL formula. We first consider operators which also exists in LTL. Inthis section, we fix

\phi,\psi

MTL formulasand

I\subseteqR+

.

Operators similar to the ones of LTL

Release and Back to

We denote by

\philRI\psi

(pronounced "

\phi

releasein

I

,

\psi

") theformula

\neg\philUI\neg\psi

. This formula holdsat time

t

if either:

t'\int+I

such that

\phi

holds, and

\psi

hold in the interval

(t,t')\cap(t+I)

.

t'\int+I

,

\phi

holds.

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

\phi

should always hold,unless

\psi

releases it.

The past counterpart of release is denote by

\philBI\psi

(pronounced "

\phi

back toin

I

,

\psi

") and is equal to theformula

\neg\philSI\neg\psi

.

Finally and Eventually

We denote by

\DiamondI\phi

or

l FI\phi

(pronounced "Finallyin

I

,

\phi

", or "Eventuallyin

I

,

\phi

") the formula

\topl UI\phi

. Intuitively, this formula holds at time

t

if there is some time

t'\int+I

suchthat

\phi

holds.

We denote by

\BoxI\phi

or

l GI\phi

(pronounced "Globallyin

I

,

\phi

",) theformula

\neg\DiamondI\neg\phi

. Intuitively, this formulaholds at time

t

if for all time

t'\in t+I

,

\phi

holds.

We denote by

\overleftarrow\BoxI\phi

and

\overleftarrow\DiamondI\phi

the formula similarto

\BoxI\phi

and

\DiamondI\phi

,where

lU

is replaced by

l S

. Both formula has intuitively the same meaning, but when weconsider the past instead of the future.

Next and previous

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

\gamma

considered.

We denote by

circI\phi

or

lNI\phi

(pronounced "Next in

I

,

\phi

") theformula

\botlUI\phi

. Similarly, we denote by

\ominusI\phi

[3] (pronounced "Previously in

I

,

\phi

) the formula

\botlSI\phi

. The following discussion about the Next operator also holds for the Previously operator, by reversing the past and the future.

\gamma:T\to A

, this formulameans that both:

T

, the formula

\phi

will holds.

I

.

\gamma

, the notion of next time doesnot makes sense. Instead, "next" means "immediately after". Moreprecisely

\gamma,t\models\circ\phi

means:

I

contains an interval of the form

(0,\epsilon)

and

t'\in(t,t+\epsilon)

,

\gamma,t'\models\phi

.

Other operators

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

Fall and Rise

We denote by

\uparrow\phi

(pronounced "rise

\phi

"), a formula which holds when

\phi

becomes true. More precisely, either

\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

\uparrow\phi

is defined as

(\phi\land(\neg\philS\top))\lor(\neg\phi\land(\philU\top))

.[4]

Over timed words, this formula always hold. Indeed

\philU\top

and

\neg\philS\top

always hold. Thus the formula is equivalent to

\phi\lor\neg\phi

, hence is true.

By symmetry, we denote by

\downarrow\phi

(pronounced "Fall

\phi

), a formula which holds when

\phi

becomes false. Thus, it is defined as

(\neg\phi\land(\philS\top))\land(\phi\land(\neg\philU\top))

.

History and Prophecy

We now introduce the prophecy operator, denoted by

\triangleright

. We denote by

\trianglerightI\phi

[5] the formula

\neg\philUI\phi

. This formula asserts that there exists a first moment in the future such that

\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=\mida,b\mid'

where

\mid

and

\mid'

represents either open or closed bounds. Let

\gamma

a timed word and

t

in its domain of definition. Over timed words, the formula

\gamma,t\models\trianglerightI\phi

holds if and only if

\gamma,t\models\Box]0,b[\setminus\neg\phi\land\DiamondI\phi

also holds. That is, this formula simply assert that, in the future, until the interval

t+I

is met,

\phi

should not hold. Furthermore,

\phi

should hold sometime in the interval

t+I

. Indeed, given any time

t''\int+I

such that

\gamma,t''\models\phi

hold, there exists only a finite number of time

t'\int+I

with

t'<t''

and

\gamma,t'\models\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'

, due to the fact that the domain of definition of a signal is continuous. Thus, the formula

\trianglerightI\phi

also ensures that the first interval in which

\phi

holds is closed on the left.

By temporal symmetry, we define the history operator, denoted by

\triangleleft

. We define

\triangleleftI\phi

as

\neg\philSI\phi

. This formula asserts that there exists a last moment in the past such that

\phi

held. And the time since this first moment belongs to

I

.

Non-strict operator

The semantic of operators until and since introduced do not consider the current time. That is, in order for

\phi1l{U}\phi2

to holds at some time

t

, neither

\phi1

nor

\phi2

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

\overline{lU}

, which consider the current time.

We denote by

\phi1\overline{lU}I\phi2

and

\phi1\overline{lS}I\phi2

either:

\phi2\lor(\phi1\land(\phi1lUI\phi2))

and

\phi2\lor(\phi1\land(\phi1lSI\phi2))

if

0\inI

, and

\phi1\land(\phi1lUI\phi2)

and

\phi1\land(\phi1lSI\phi2)

otherwise.

For any of the operators

lO

introduced above, we denote

\overline{lO}

the formula in which non-strict untils and sinces are used. For example

\overline\Diamondp

is an abbreviation for

\top\overline{lU}p

.

Strict operator can not be defined using non-strict operator. That is, there is no formula equivalent to

circIp

which uses only non-strict operator. This formula is defined as

\botlUIp

. This formula can never hold at a time

t

if it is required that

\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.

\Box(p\implies\Diamond\{1\

}q) states that each letter

p

is followed exactly one time unit later by a letter

q

.

\Box(p\implies\neg\Diamond\{1\

}p) states that no two successive occurrences of

p

can occur at exactly one time unit from each other.

Comparison with LTL

A standard (untimed) infinite word

w=a0,a1,...,

is afunction from

N

to

A

. We canconsider such a word using the set of time

T=N

,and the function

\gamma(i)=ai

. In this case,for

\phi

an arbitrary LTLformula,

w,i\models\phi

if and onlyif

\gamma,i\models\phi

, where

\phi

isconsidered as a MTL formula with non-strict operator and

[0,infty)

subscript. In this sense, MTL is an extension of LTL.

For this reason, a formula using only non-strict operator with

[0,infty)

subscript is called an LTL formula. This is because the

Algorithmic complexity

The satisfiability of ECL over signals is EXPSPACE-complete.[5]

Fragments of MTL

We now consider some fragments of MTL.

MITL

See main article: Metric interval temporal logic. An important subset of MTL is the Metric Interval Temporal Logic (MITL). This is defined similarly to MTL, with therestriction that the sets

I

, used in

l U

and

lS

, are intervals which are notsingletons, and whose bounds are natural numbers or infinity.

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

Future Fragments

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

Event-Clock Temporal Logic

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

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

If

I

is not a singleton and

\phi

is a MITL formula,

\trianglerightI\phi

is defined as a MITL formula. If

I=\{i\}

is a singleton, then

\trianglerightI\phi

is equivalent to

\Box]0,i[\neg\phi\land\Diamond]0,i]\phi

which is a MITL-formula. Reciprocally, for

\psi

an ECL-formula, and

I

an interval whose lower bound is 0,

\BoxI\psi

is equivalent to the ECL-formula

\neg\trianglerightI\neg\psi

.

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

Positive normal form

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

Any MTL formula is equivalent to formula in normal form. This can be shown by an easy induction on formulas. For example, the formula

\neg(\philUS\psi)

is equivalent to the formula

(\neg\phi)lRS(\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.

See also

Notes and References

  1. J. Ouaknine and J. Worrell, "On the decidability of metric temporal logic," 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), 2005, pp. 188-197.
  2. Ouaknine J., Worrell J. (2006) On Metric Temporal Logic and Faulty Turing Machines. In: Aceto L., Ingólfsdóttir A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg
  3. Book: Maler . Oded . Nickovic . Dejan . Pnueli . Amir . 478 . Pillars of computer science . Checking temporal properties of discrete, timed and continuous behaviors . 2008 . ACM . 978-3-540-78126-4.
  4. Nickovic . Dejan . 31 August 2009 . Checking Timed and Hybrid Properties: Theory and Applications . 3 . https://tel.archives-ouvertes.fr/tel-00411957/en/ .
  5. Book: Henzinger . T.A. . Raskin . J.F. . Schobbens . P.-Y. . Automata, Languages and Programming . The regular real-time languages . Lecture Notes in Computer Science . 1998 . 1443 . 590 . 10.1007/BFb0055086. 978-3-540-64781-2 .