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.
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
x\simc
x\inX
c
\sim
x.\phi
\phi
X\cup\{x\}
Furthermore, for
I=(a,b)
x\inI
x>a\landx<b
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]
Let
T\subseteqR+
\gamma:T\tolP(AP)
t\inT
\gamma
\gamma
T
Let
T
\gamma
X
\nu:X\toR\ge0
X
We are now going to explain what it means for a TPTL formula
\phi
t
\nu
\gamma,t,\nu\models\phi
\phi
\psi
X
\xi
X\cup\{y\}
x\inX
l\inAP
c
\sim
\gamma,t,\nu\modelsl
l\in\gamma(t)
\gamma,t,\nu\models\neg\phi
\gamma,t,\nu\not\models\phi
\gamma,t,\nu\models\phi\lor\psi
\gamma,t,\nu\models\phi
\gamma,t,\nu\models\psi
\gamma,t,\nu\models\phinlU\psi
t<t''
\gamma,t'',\nu\models\psi
t<t'<t''
\gamma,t',\nu\models\phi
\gamma,t,\nu\models\phinlS\psi
t''<t
\gamma,t'',\nu\models\psi
t''<t'<t
\gamma,t',\nu\models\phi
\gamma,t,\nu\modelsx\simc
t-\nu(y)\simc
\gamma,t,\nu\modelsy.\xi
\gamma,t,\nu[y\tot]\models\phi
Metric temporal logic is another extension of LTL that allows measurement of time. Instead of adding variables, it adds an infinity of operators
lUI
lSI
I
\phinl{UI}\psi
t
\phinlU\psi
t''
\psi
t+I
TPTL is as least as expressive as MTL. Indeed, the MTL formula
\phinl{UI}\psi
x.\phil(x\inI\land\psi)
x
It follows that any other operator introduced in the page MTL, such as
\Box
\Diamond
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)))
x.\Diamond(a\landx\le1\land\Box(x\le1\implies\negb))
a
A standard (untimed) infinite word
w=a0,a1,...,
N
A
T=N
\gamma(i)=ai
\phi
w,i\models\phi
\gamma,i,\nu\models\phi
\phi
\nu