Probabilistic CTL

From Wikipedia, the free encyclopedia

There are very few or no other articles that link to this one.
Please help introduce links in articles on related topics. After links have been created, remove this message.
This article has been tagged since November 2006.

Probabilistic Computational Tree Logic is an extension of CTL which allows for probabilistic quantification of described properties. It has been defined in the paper by Hansson and Jonsson. PCTL is a useful logic for stating soft deadline properties, e.g. "after a request for a service, there is at least a 98% probability that the service will be carried out within 2 seconds". Akin CTL suitability for model-checking PCTL extension is widely used as a property specification language for probabilistic model checkers.

One of the possible syntax of PCTL is defined as follows:

$\phi ::= p | \neg p | \phi \lor \phi | \phi \land \phi | \mathcal{P}_{\sim\lambda}(\phi \mathcal{U} \phi) | \mathcal{P}_{\sim\lambda}(\square\phi)$

Therein, $\sim \in \{ <, \leq, =, \geq, > \}$ is comparison operator and $λ$ is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure is a quadruple $K = \langle S, s^i, \mathcal{T}, L \rangle$ , where

$S$ is a finite set of states,
$s^i \in S$ is an initial state,
$\mathcal{T}$ is a transition probability function, $\mathcal{T} : S \times S \to [0,1]$ , such that for all $s \in S$ we have $\sum_{s'\in S} \mathcal{T}(s,s')=1$ , and
$L$ is a labeling function, $L:S\to2^A$ , assigning atomic propositions to states.

A path $σ$ from a state $s 0$ is an inifite sequence of states $s_0 \to s_1 \to \dots \to s_n \to \dots$ . The n-th state of the path is denoted as $σ[n]$ and the prefix of $σ$ of length $n$ is denoted as $\sigma\uparrow n$ .

A probability measure $μ m$ of the set of path with the common prefix of length $n$ is equal to the product of transitions probabilitites along the prefix of the path:

$\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)$

For $n = 0$ the probability measure is equal to $\mu_m(\{\sigma \in X : \sigma\uparrow 0 = s_0 \}) = 1$ .

Satisfaction relations $s \models_K f$ , $\sigma \models_K f$ are inductively defined as follows:

$s \models_K a$ if and only if $a \in L(s)$ ,
$s \models_K \neg f$ if and only if not $s \models_K f$ ,
$s \models_K f_1 \lor f_2$ if and only if $s \models_K f_1$ or $s \models_K f_2$ ,
$s \models_K f_1 \land f_2$ if and only if $s \models_K f_1$ and $s \models_K f_2$ ,
$s \models_K \mathcal{P}_{\sim\lambda}(f_1 \mathcal{U} f_2)$ if and only if $\mu_m(\{\sigma : \sigma[0] = s \land (\exists i)\sigma[i] \models_K f_2 \land (\forall 0 \leq j < i) \sigma[i] \models_K f_2\}) \sim \lambda$ , and
$s \models_K \mathcal{P}_{\sim\lambda}(\square f)$ if and only if $\mu_m(\{\sigma : \sigma[0] = s \land (\forall i \geq 0)\sigma[i] \models_K f\}) \sim \lambda$ .