Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Probabilistic CTL
open-in-new
<h2 id="pctl-syntax">PCTL syntax</h2> <p>A possible syntax of PCTL can be defined as follows: </p> <p> ϕ ::= p ∣ ¬ ϕ ∣ ϕ ∨ ϕ ∣ ϕ ∧ ϕ ∣ P ∼ λ ( ϕ U ϕ ) ∣ P ∼ λ ( ◻ ϕ ) {\displaystyle \phi ::=p\mid \neg \phi \mid \phi \lor \phi \mid \phi \land \phi \mid {\mathcal {P}}_{\sim \lambda }(\phi {\mathcal {U}}\phi )\mid {\mathcal {P}}_{\sim \lambda }(\square \phi )} </p> <p>Therein, ∼∈ { < , ≤ , ≥ , > } {\displaystyle \sim \in \{<,\leq ,\geq ,>\}} is a comparison operator and λ {\displaystyle \lambda } is a probability threshold. Formulas of PCTL are interpreted over discrete <a href="/facts/Markov_chains/5oP5hntk">Markov chains</a>. An interpretation structure is a quadruple K = ⟨ S , s i , T , L ⟩ {\displaystyle K=\langle S,s^{i},{\mathcal {T}},L\rangle } , where </p> <ul><li> S {\displaystyle S} is a <a href="/facts/Finite_set/za1newlP">finite set</a> of states,</li> <li> s i ∈ S {\displaystyle s^{i}\in S} is an initial state,</li> <li> T {\displaystyle {\mathcal {T}}} is a transition probability function, T : S × S → [ 0 , 1 ] {\displaystyle {\mathcal {T}}:S\times S\to [0,1]} , such that for all s ∈ S {\displaystyle s\in S} we have ∑ s ′ ∈ S T ( s , s ′ ) = 1 {\displaystyle \sum _{s'\in S}{\mathcal {T}}(s,s')=1} , and</li> <li> L {\displaystyle L} is a labeling function, L : S → 2 A {\displaystyle L:S\to 2^{A}} , assigning atomic propositions to states.</li></ul> <p> A path σ {\displaystyle \sigma } from a state s 0 {\displaystyle s_{0}} is an infinite sequence of states s 0 → s 1 → ⋯ → s n → … {\displaystyle s_{0}\to s_{1}\to \dots \to s_{n}\to \dots } . The n-th state of the path is denoted as σ [ n ] {\displaystyle \sigma [n]} and the prefix of σ {\displaystyle \sigma } of length n {\displaystyle n} is denoted as σ ↑ n {\displaystyle \sigma \uparrow n} . </p> <h2 id="probability-measure">Probability measure</h2> <p>A probability measure μ m {\displaystyle \mu _{m}} on the set of paths with a common prefix of length n {\displaystyle n} is given by the product of transition probabilities along the prefix of the path: </p> μ m ( { σ ∈ X : σ ↑ n = s 0 → ⋯ → s n } ) = T ( s 0 , s 1 ) × ⋯ × T ( s n − 1 , s n ) {\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow n=s_{0}\to \dots \to s_{n}\})={\mathcal {T}}(s_{0},s_{1})\times \dots \times {\mathcal {T}}(s_{n-1},s_{n})} <p>For n = 0 {\displaystyle n=0} the probability measure is equal to μ m ( { σ ∈ X : σ ↑ 0 = s 0 } ) = 1 {\displaystyle \mu _{m}(\{\sigma \in X:\sigma \uparrow 0=s_{0}\})=1} . </p> <h2 id="satisfaction-relation">Satisfaction relation</h2> <p>The satisfaction relation s ⊨ K f {\displaystyle s\models _{K}f} is inductively defined as follows: </p> <ul><li> s ⊨ K a {\displaystyle s\models _{K}a} if and only if a ∈ L ( s ) {\displaystyle a\in L(s)} ,</li> <li> s ⊨ K ¬ f {\displaystyle s\models _{K}\neg f} <a href="/facts/If_and_only_if/bYSxGJ66">if and only if</a> not s ⊨ K f {\displaystyle s\models _{K}f} ,</li> <li> s ⊨ K f 1 ∨ f 2 {\displaystyle s\models _{K}f_{1}\lor f_{2}} if and only if s ⊨ K f 1 {\displaystyle s\models _{K}f_{1}} or s ⊨ K f 2 {\displaystyle s\models _{K}f_{2}} ,</li> <li> s ⊨ K f 1 ∧ f 2 {\displaystyle s\models _{K}f_{1}\land f_{2}} if and only if s ⊨ K f 1 {\displaystyle s\models _{K}f_{1}} and s ⊨ K f 2 {\displaystyle s\models _{K}f_{2}} ,</li> <li> s ⊨ K P ∼ λ ( f 1 U f 2 ) {\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(f_{1}{\mathcal {U}}f_{2})} if and only if μ m ( { σ : σ [ 0 ] = s ∧ ( ∃ i ) σ [ i ] ⊨ K f 2 ∧ ( ∀ 0 ≤ j < i ) σ [ j ] ⊨ K f 1 } ) ∼ λ {\displaystyle \mu _{m}(\{\sigma :\sigma [0]=s\land (\exists i)\sigma [i]\models _{K}f_{2}\land (\forall 0\leq j<i)\sigma [j]\models _{K}f_{1}\})\sim \lambda } , and</li> <li> s ⊨ K P ∼ λ ( ◻ f ) {\displaystyle s\models _{K}{\mathcal {P}}_{\sim \lambda }(\square f)} if and only if μ m ( { σ : σ [ 0 ] = s ∧ ( ∀ i ≥ 0 ) σ [ i ] ⊨ K f } ) ∼ λ {\displaystyle \mu _{m}(\{\sigma :\sigma [0]=s\land (\forall i\geq 0)\sigma [i]\models _{K}f\})\sim \lambda } .</li></ul> <h2 id="see-also">See also</h2> <ul><li><a href="/facts/Computation_tree_logic/h04gVzsL">Computation tree logic</a></li> <li><a href="/facts/Temporal_logic/vANP39lc">Temporal logic</a></li></ul> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>Hansson, Hans, and Bengt Jonsson. "A logic for reasoning about time and reliability." Formal aspects of computing 6.5 (1994): 512-535. <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> </ol>