Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Timed propositional temporal logic
open-in-new
<h2 id="syntax">Syntax</h2> <p>The future fragment of TPTL is defined similarly to <a href="/facts/Linear_temporal_logic/Gh5yxXK7">linear temporal logic</a>, in which furthermore, <a href="/facts/Clock_(model_checking)/3q9X8trL">clock</a> variables can be introduced and compared to constants. Formally, given a set X {\displaystyle X} of clocks, MTL[<i>clarify</i>] is built up from: </p> <ul><li>a finite set of <a href="/facts/Propositional_variable/NtAz1rfI">propositional variables</a> <i>AP</i>,</li> <li>the <a href="/facts/Logical_connective/VkPhUs6M">logical operators</a> ¬ and ∨, and</li> <li>the <a href="/facts/Temporal_logic/vANP39lc">temporal</a> <a href="/facts/Modal_operator/UHtpPLuH">modal operator</a> U,</li> <li>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 >.</li> <li>a freeze quantification operator x . ϕ {\displaystyle x.\phi } , for ϕ {\displaystyle \phi } a TPTL formula with set of clocks X ∪ { x } {\displaystyle X\cup \{x\}} .</li></ul> <p>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. </p><p>The logic TPTL+Past<a class="footnote-ref" id="fnref:1" href="#fn:1"><sup>1</sup></a> is built as the future fragment of TLS[<i>clarify</i>] and also contains </p> <ul><li>the temporal modal operator S.</li></ul> <p>The next operator N[<i>clarify</i>] is not considered to be a part of MTL[<i>clarify</i>] syntax. It will instead be defined from other operators. </p><p>A closed formula is a formula over an empty set of clocks.<a class="footnote-ref" id="fnref:2" href="#fn:2"><sup>2</sup></a> </p> <h2 id="models">Models</h2> <p>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 <i>AP</i>. A model of a TPTL formula is such a function γ {\displaystyle \gamma } . Usually, γ {\displaystyle \gamma } is either a <a href="/facts/Timed_word/HkB4W242">timed word</a> or a <a href="/facts/Signal_(model_checking)/c5wUJVoA">signal</a>. In those cases, T {\displaystyle T} is either a discrete subset or an interval containing 0. </p> <h2 id="semantics">Semantics</h2> <p>Let T {\displaystyle T} and γ {\displaystyle \gamma } be as above. Let X {\displaystyle X} be a set of <a href="/facts/Clock_(model_checking)/3q9X8trL">clocks</a>. Let ν : X → R ≥ 0 {\displaystyle \nu :X\to \mathbb {R} _{\geq 0}} (a <i>clock valuation</i> over X {\displaystyle X} ). </p><p>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: </p> <ul><li> γ , t , ν ⊨ l {\displaystyle \gamma ,t,\nu \models l} holds if l ∈ γ ( t ) {\displaystyle l\in \gamma (t)} ,</li> <li> γ , t , ν ⊨ ¬ ϕ {\displaystyle \gamma ,t,\nu \models \neg \phi } holds if γ , t , ν ⊭ ϕ {\displaystyle \gamma ,t,\nu \not \models \phi } </li> <li> γ , 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</li> <li> γ , t , ν ⊨ ϕ U ψ {\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {U}} \psi } holds if there exists t ″ {\displaystyle t''} such that t < t ″ {\displaystyle t<t''} and γ , t ″ , ν ⊨ ψ {\displaystyle \gamma ,t'',\nu \models \psi } and for each t ′ {\displaystyle t'} with t < t ′ < t ″ {\displaystyle t<t'<t''} , γ , t ′ , ν ⊨ ϕ {\displaystyle \gamma ,t',\nu \models \phi } ,</li> <li> γ , t , ν ⊨ ϕ S ψ {\displaystyle \gamma ,t,\nu \models \phi \mathbin {\mathcal {S}} \psi } holds if there exists t ″ {\displaystyle t''} such that t ″ < t {\displaystyle t''<t} and γ , t ″ , ν ⊨ ψ {\displaystyle \gamma ,t'',\nu \models \psi } and for each t ′ {\displaystyle t'} with t ″ < t ′ < t {\displaystyle t''<t'<t} , γ , t ′ , ν ⊨ ϕ {\displaystyle \gamma ,t',\nu \models \phi } ,</li> <li> γ , t , ν ⊨ x ∼ c {\displaystyle \gamma ,t,\nu \models x\sim c} holds if t − ν ( y ) ∼ c {\displaystyle t-\nu (y)\sim c} ,</li> <li> γ , t , ν ⊨ y . ξ {\displaystyle \gamma ,t,\nu \models y.\xi } holds if γ , t , ν [ y → t ] ⊨ ϕ {\displaystyle \gamma ,t,\nu [y\to t]\models \phi } holds.</li></ul> <h2 id="metric-temporal-logic">Metric temporal logic</h2> <p><a href="/facts/Metric_temporal_logic/9ctsX0YX">Metric temporal logic</a> is another extension of LTL that allows measurement of time. Instead of adding variables, it adds an infinity of operators U I {\displaystyle {\mathcal {U}}_{I}} and S I {\displaystyle {\mathcal {S}}_{I}} for I {\displaystyle I} an interval of non-negative numbers. The semantics of the formula ϕ U I ψ {\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi } at some time t {\displaystyle t} is essentially the same than the semantics of the formula ϕ U ψ {\displaystyle \phi \mathbin {\mathcal {U}} \psi } , with the constraints that the time t ″ {\displaystyle t''} at which ψ {\displaystyle \psi } must hold occurs in the interval t + I {\displaystyle t+I} . </p><p>TPTL is as least as expressive as MTL. Indeed, the MTL formula ϕ U I ψ {\displaystyle \phi \mathbin {\mathcal {U_{I}}} \psi } is equivalent to the TPTL formula x . ϕ ( x ∈ I ∧ ψ ) {\displaystyle x.\phi {\mathcal {(}}x\in I\land \psi )} where x {\displaystyle x} is a new variable.<a class="footnote-ref" id="fnref:3" href="#fn:3"><sup>3</sup></a> </p><p>It follows that any other operator introduced in the page <a href="/facts/Metric_temporal_logic/9ctsX0YX">MTL</a>, such as ◻ {\displaystyle \Box } and ◊ {\displaystyle \Diamond } can also be defined as TPTL formulas. </p><p>TPTL is strictly more expressive than MTL<a class="footnote-ref" id="fnref:4" href="#fn:4"><sup>4</sup></a>: 2 both over timed words and over signals. Over timed words, no MTL formula is equivalent to ◻ ( a ⟹ x . ◊ ( b ∧ ◊ ( c ∧ x ≤ 5 ) ) ) {\displaystyle \Box (a\implies x.\Diamond (b\land \Diamond (c\land x\leq 5)))} . Over signal, there are no MTL formula equivalent to x . ◊ ( a ∧ x ≤ 1 ∧ ◻ ( x ≤ 1 ⟹ ¬ b ) ) {\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 a {\displaystyle a} . </p> <h2 id="comparison-with-ltl">Comparison with LTL</h2> <p>A standard (untimed) infinite word w = a 0 , a 1 , … , {\displaystyle w=a_{0},a_{1},\dots ,} is a function from N {\displaystyle \mathbb {N} } to A {\displaystyle A} . We can consider such a word using the set of time T = N {\displaystyle T=\mathbb {N} } , and the function γ ( i ) = a i {\displaystyle \gamma (i)=a_{i}} . In this case, for ϕ {\displaystyle \phi } an arbitrary LTL formula, w , i ⊨ ϕ {\displaystyle w,i\models \phi } if and only if γ , i , ν ⊨ ϕ {\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. </p> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Bouyer, Patricia; Chevalier, Fabrice; Markey, Nicolas (2005). "Developments in Data Structure Research During the First 25 Years of FSTTCS". FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science. Vol. 3821. p. 436. doi:10.1007/11590156_3. ISBN 978-3-540-30495-1. {{cite book}}: |journal= ignored (help) <a href="978-3-540-30495-1" target="_blank">978-3-540-30495-1</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Alur, Rajeev; Henzinger, Thomas A. (Jan 1994). "A really temporal logic". Journal of the ACM. 41 (1): 181–203. doi:10.1145/174644.174651. <a href="/wiki/Rajeev_Alur" target="_blank">/wiki/Rajeev_Alur</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Alur, Rajeev; Henzinger, Thomas A. (Jan 1994). "A really temporal logic". Journal of the ACM. 41 (1): 181–203. doi:10.1145/174644.174651. <a href="/wiki/Rajeev_Alur" target="_blank">/wiki/Rajeev_Alur</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>Bouyer, Patricia; Chevalier, Fabrice; Markey, Nicolas (2005). "Developments in Data Structure Research During the First 25 Years of FSTTCS". FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science. Vol. 3821. p. 436. doi:10.1007/11590156_3. ISBN 978-3-540-30495-1. {{cite book}}: |journal= ignored (help) <a href="978-3-540-30495-1" target="_blank">978-3-540-30495-1</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></p></li> </ol>