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 {\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 x ∼ c {\displaystyle x\sim c} , with x ∈ X {\displaystyle x\in X} , c {\displaystyle c} a number and ∼ {\displaystyle \sim } a comparison operator such as <, ≤, =, ≥ or >. a freeze quantification operator x . ϕ {\displaystyle x.\phi } , for ϕ {\displaystyle \phi } a TPTL formula with set of clocks X ∪ { x } {\displaystyle X\cup \{x\}} . Furthermore, for I = ( a , b ) {\displaystyle I=(a,b)} an interval, x ∈ I {\displaystyle x\in I} is considered as an abbreviation for x > a ∧ x < b {\displaystyle x>a\land x<b} ; and similarly for every other kind of intervals. The logic TPTL+Past is built as the future fragment of TLS and also contains
the temporal modal operator S. 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.
Models Let T ⊆ R + {\displaystyle T\subseteq \mathbb {R} _{+}} , which intuitively represents a set of times. Let γ : T → P ( A P ) {\displaystyle \gamma :T\to {\mathcal {P}}(AP)} a function that associates to each moment t ∈ T {\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, T {\displaystyle T} is either a discrete subset or an interval containing 0.
Semantics Let T {\displaystyle T} and γ {\displaystyle \gamma } be as above. Let X {\displaystyle X} be a set of clocks. Let ν : X → R ≥ 0 {\displaystyle \nu :X\to \mathbb {R} _{\geq 0}} (a clock valuation over X {\displaystyle X} ). We are now going to explain what it means for a TPTL formula ϕ {\displaystyle \phi } to hold at time t {\displaystyle t} for a valuation ν {\displaystyle \nu } . This is denoted by γ , t , ν ⊨ ϕ {\displaystyle \gamma ,t,\nu \models \phi } . Let ϕ {\displaystyle \phi } and ψ {\displaystyle \psi } be two formulas over the set of clocks X {\displaystyle X} , ξ {\displaystyle \xi } a formula over the set of clocks X ∪ { y } {\displaystyle X\cup \{y\}} , x ∈ X {\displaystyle x\in X} , l ∈ A P {\displaystyle l\in {\mathtt {AP}}} , c {\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:
γ , t , ν ⊨ l {\displaystyle \gamma ,t,\nu \models l} holds if l ∈ γ ( t ) {\displaystyle l\in \gamma (t)} ,
γ , t , ν ⊨ ¬ ϕ {\displaystyle \gamma ,t,\nu \models \neg \phi } holds if γ , t , ν ⊭ ϕ {\displaystyle \gamma ,t,\nu \not \models \phi }
γ , t , ν ⊨ ϕ ∨ ψ {\displaystyle \gamma ,t,\nu \models \phi \lor \psi } holds if either γ , t , ν ⊨ ϕ {\displaystyle \gamma ,t,\nu \models \phi } or γ , t , ν ⊨ ψ {\displaystyle \gamma ,t,\nu \models \psi } , or both
… excerpt ends here. Continue reading the full article.
