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.
of clocks, MTL[clarify] is built up from: Furthermore, for
; and similarly for every other kind of intervals.
The logic TPTL+Past[1] is built as the future fragment of TLS[clarify] and also contains The next operator N[clarify] is not considered to be a part of MTL[clarify] syntax.
, which intuitively represents a set of times.
a function that associates to each moment
a set of propositions from AP.
A model of a TPTL formula is such a function
is either a timed word or a signal.
is either a discrete subset or an interval containing 0.
We are now going to explain what it means for a TPTL formula
γ , t , ν ⊨ ϕ
be two formulas over the set of clocks
a formula over the set of clocks
being a comparison operator such as <, ≤, =, ≥ or >: We first consider formulas whose main operator also belongs to LTL: Metric temporal logic is another extension of LTL that allows measurement of time.
Instead of adding variables, it adds an infinity of operators
an interval of non-negative numbers.
must hold occurs in the interval
[2] It follows that any other operator introduced in the page MTL, such as
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
Over signal, there are no MTL formula equivalent to
, which states that the last atomic proposition before time point 1 is an
A standard (untimed) infinite word
We can consider such a word using the set of time
γ , i , ν ⊨ ϕ
is considered as a TPTL formula with non-strict operator, and
is the only function defined on the empty set.