Timed propositional temporal logic

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 ${\displaystyle X}$ of clocks, MTL is built up from:

• a finite set of propositional variables AP,
• the logical operators ¬ and ∨, and
• the temporal modal operator U,
• a clock comparison ${\displaystyle x\sim c}$, with ${\displaystyle x\in X}$, ${\displaystyle c}$ a number and ${\displaystyle \sim }$ being a comparison operator such as <, ≤, =, ≥ or >.
• a freeze quantification operator ${\displaystyle x.\phi }$, for ${\displaystyle \phi }$ a TPTL formula with set of clocks ${\displaystyle X\cup \{x\}}$.

Furthermore, for ${\displaystyle I=(a,b)}$ an interval, ${\displaystyle x\in I}$ is considered as an abbreviation for ${\displaystyle x>a\land x<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

• the temporal modal operator S.

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 ${\displaystyle T\subseteq \mathbb {R} _{+}}$ it intuitively represents a set of time. Let ${\displaystyle \gamma :T\to {\mathcal {P}}(AP)}$ a function which associate to each moment ${\displaystyle t\in T}$ a set of propositions from AP. A model of a TPTL formula is such a function ${\displaystyle \gamma }$. Usually, ${\displaystyle \gamma }$ is either a timed word or a signal. In those cases, ${\displaystyle T}$ is either a discrete subset or an interval containing 0.

Let ${\displaystyle T}$ and ${\displaystyle \gamma }$ as above. Let ${\displaystyle X}$ a set of clocks. Let ${\displaystyle \nu :X\to \mathbb {R} _{\geq 0}}$ a clock valuation over ${\displaystyle X}$.

We are now going to explain what it means that a TPTL formula ${\displaystyle \phi }$ holds at time ${\displaystyle t}$ for a valuation ${\displaystyle \nu }$. This is denoted by ${\displaystyle \gamma ,t,\nu \models \phi }$. Let ${\displaystyle \phi }$ and ${\displaystyle \psi }$ be two formulas over the set of clocks ${\displaystyle X}$, ${\displaystyle \xi }$ a formula over the set of clocks ${\displaystyle X\cup \{y\}}$, ${\displaystyle x\in X}$, ${\displaystyle l\in {\mathtt {AP}}}$, ${\displaystyle c}$ a number and ${\displaystyle \sim }$ being a comparison operator such as <, ≤, =, ≥ or >: We first consider formulas whose main operator also belongs to LTL:

• ${\displaystyle \gamma ,t,\nu \models l}$ holds if ${\displaystyle l\in \gamma (t)}$,
• ${\displaystyle \gamma ,t,\nu \models \neg \phi }$ holds if either ${\displaystyle \gamma ,t,\nu \models \phi }$ or ${\displaystyle \gamma ,t,\nu \models \psi }$
• ${\displaystyle \gamma ,t,\nu \models \phi \lor \psi }$ holds if either ${\displaystyle \gamma ,t,\nu \models \phi }$ or ${\displaystyle \gamma ,t,\nu \models \psi }$
• ${\displaystyle \gamma ,t,\nu \models \phi {\mathcal {U}}\psi }$ holds if there exists ${\displaystyle t<t''}$ such that ${\displaystyle \gamma ,t'',\nu \models \psi }$ and such that for each ${\displaystyle t<t'<t''}$, ${\displaystyle \gamma ,t',\nu \models \phi }$,
• ${\displaystyle \gamma ,t,\nu \models \phi {\mathcal {S}}\psi }$ holds if there exists ${\displaystyle t''<t}$ such that ${\displaystyle \gamma ,t'',\nu \models \psi }$ and such that for each ${\displaystyle t''<t'<t}$, ${\displaystyle \gamma ,t',\nu \models \phi }$,
• ${\displaystyle \gamma ,t,\nu \models y.\xi }$ holds if ${\displaystyle \gamma ,t,\nu [y\to t]\models \phi }$ holds,
• ${\displaystyle \gamma ,t,\nu \models x\sim c}$ holds if ${\displaystyle t-\nu (y)\sim c}$.

Metric temporal logic is another extension of LTL which allow to measure time. Instead of adding variables, it adds an infinity of operators ${\displaystyle {\mathcal {U}}_{I}}$ and ${\displaystyle {\mathcal {S}}_{I}}$ for ${\displaystyle I}$ an interval of non-negative number. The semantic of the formula ${\displaystyle \phi {\mathcal {U}}_{I}\psi }$ at some time ${\displaystyle t}$ is essentially the same than the semantic of the formula ${\displaystyle \phi {\mathcal {U}}\psi }$, with the constraints that the time ${\displaystyle t''}$ at which ${\displaystyle \psi }$ must hold occurs in the interval ${\displaystyle t+I}$.

TPTL is as least as expressive as MTL. Indeed, the MTL formula ${\displaystyle \phi {\mathcal {U}}_{I}\psi }$ is equivalent to the TPTL formula ${\displaystyle x.\phi {\mathcal {(}}x\in I\land \psi )}$ where ${\displaystyle x}$ is a new variable.[2]

It follows that any other operator introduced in the page MTL, such as ${\displaystyle \Box }$ and ${\displaystyle \Diamond }$ can also be defined as TPTL formulas.

TPTL is strictly more expressive than MTL[1]^:2 both over timed words and over signals. Over timed words, no MTL formula is equivalent to ${\displaystyle \Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))}$. Over signal, there are no MTL formula equivalent to ${\displaystyle x.\Diamond (a\land x\leq 1\land \Box (x\leq 1\implies \neg b))}$, which states that the last atomic proposition before time point 1 is an ${\displaystyle a}$.

A standard (untimed) infinite word ${\displaystyle w=a_{0},a_{1},\dots ,}$ is a function from ${\displaystyle \mathbb {N} }$ to ${\displaystyle A}$. We can consider such a word using the set of time ${\displaystyle T=\mathbb {N} }$, and the function ${\displaystyle \gamma (i)=a_{i}}$. In this case, for ${\displaystyle \phi }$ an arbitrary LTL formula, ${\displaystyle w,i\models \phi }$ if and only if ${\displaystyle \gamma ,i,\nu \models \phi }$, where ${\displaystyle \phi }$ is considered as a TPTL formula with non-strict operator, and ${\displaystyle \nu }$ is the only function defined on the empty set.