Timed propositional temporal logic explained

In model checking, a field of computer science, timed propositional temporal logic (TPTL) is an extension of propositional linear temporal logic (LTL) in which variables are introduced to measure times between two events. For example, while LTL allows to state that each event p is eventually followed by an event q, TPTL furthermore allows to give a time limit for q to occur.

Syntax

The future fragment of TPTL is defined similarly to linear temporal logic, in which furthermore, clock variables can be introduced and compared to constants. Formally, given a set

X

of clocks, MTL is built up from:

x\simc

, with

x\inX

,

c

a number and

\sim

a comparison operator such as <, ≤, =, ≥ or >.

x.\phi

, for

\phi

a TPTL formula with set of clocks

X\cup\{x\}

.

Furthermore, for

I=(a,b)

an interval,

x\inI

is considered as an abbreviation for

x>a\landx<b

; and similarly for every other kind of intervals.

The logic TPTL+Past[1] is built as the future fragment of TLS and also contains

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

A closed formula is a formula over an empty set of clocks.[2]

Models

Let

T\subseteqR+

, which intuitively represents a set of times. Let

\gamma:T\tolP(AP)

a function that associates to each moment

t\inT

a set of propositions from AP. A model of a TPTL formula is such a function

\gamma

. Usually,

\gamma

is either a timed word or a signal. In those cases,

T

is either a discrete subset or an interval containing 0.

Semantics

Let

T

and

\gamma

be as above. Let

X

be a set of clocks. Let

\nu:X\toR\ge0

(a clock valuation over

X

).

We are now going to explain what it means for a TPTL formula

\phi

to hold at time

t

for a valuation

\nu

. This is denoted by

\gamma,t,\nu\models\phi

.Let

\phi

and

\psi

be two formulas over the set of clocks

X

,

\xi

a formula over the set of clocks

X\cup\{y\}

,

x\inX

,

l\inAP

,

c

a number and

\sim

being a comparison operator such as <, ≤, =, ≥ or >:We first consider formulas whose main operator also belongs to LTL:

\gamma,t,\nu\modelsl

holds if

l\in\gamma(t)

,

\gamma,t,\nu\models\neg\phi

holds if

\gamma,t,\nu\not\models\phi

\gamma,t,\nu\models\phi\lor\psi

holds if either

\gamma,t,\nu\models\phi

or

\gamma,t,\nu\models\psi

\gamma,t,\nu\models\phinlU\psi

holds if there exists

t<t''

such that

\gamma,t'',\nu\models\psi

and such that for each

t<t'<t''

,

\gamma,t',\nu\models\phi

,

\gamma,t,\nu\models\phinlS\psi

holds if there exists

t''<t

such that

\gamma,t'',\nu\models\psi

and such that for each

t''<t'<t

,

\gamma,t',\nu\models\phi

,

\gamma,t,\nu\modelsx\simc

holds if

t-\nu(y)\simc

,

\gamma,t,\nu\modelsy.\xi

holds if

\gamma,t,\nu[y\tot]\models\phi

holds.

Metric temporal logic

Metric temporal logic is another extension of LTL that allows measurement of time. Instead of adding variables, it adds an infinity of operators

lUI

and

lSI

for

I

an interval of non-negative number. The semantics of the formula

\phinl{UI}\psi

at some time

t

is essentially the same than the semantics of the formula

\phinlU\psi

, with the constraints that the time

t''

at which

\psi

must hold occurs in the interval

t+I

.

TPTL is as least as expressive as MTL. Indeed, the MTL formula

\phinl{UI}\psi

is equivalent to the TPTL formula

x.\phil(x\inI\land\psi)

where

x

is a new variable.[2]

It follows that any other operator introduced in the page MTL, such as

\Box

and

\Diamond

can also be defined as TPTL formulas.

TPTL is strictly more expressive than MTL both over timed words and over signals. Over timed words, no MTL formula is equivalent to

\Box(a\impliesx.\Diamond(b\land\Diamond(c\landx\le5)))

. Over signal, there are no MTL formula equivalent to

x.\Diamond(a\landx\le1\land\Box(x\le1\implies\negb))

, which states that the last atomic proposition before time point 1 is an

a

.

Comparison with LTL

A standard (untimed) infinite word

w=a0,a1,...,

is a function from

N

to

A

. We can consider such a word using the set of time

T=N

, and the function

\gamma(i)=ai

. In this case, for

\phi

an arbitrary LTL formula,

w,i\models\phi

if and only if

\gamma,i,\nu\models\phi

, where

\phi

is considered as a TPTL formula with non-strict operator, and

\nu

is the only function defined on the empty set.

Notes and References

  1. Book: Bouyer . Patricia . Patricia Bouyer-Decitre. Chevalier . Fabrice . Markey . Nicolas . FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science . Developments in Data Structure Research During the First 25 Years of FSTTCS . Lecture Notes in Computer Science . Proceedings of the 25th Conference on Foundations of Software Technology and Theoretical Computer Science . 2005 . 3821 . 436 . 10.1007/11590156_3 . 978-3-540-30495-1 . https://hal.archives-ouvertes.fr/hal-01194615/document.
  2. Alur . Rajeev . Rajeev Alur. Henzinger . Thomas A. . Thomas Henzinger. A really temporal logic. Journal of the ACM. Jan 1994 . 41 . 1. 181–203 . 10.1145/174644.174651. free .