Probabilistic CTL

Probabilistic Computation Tree Logic (PCTL) is an extension of computation tree logic (CTL) which allows for probabilistic quantification of described properties. It has been defined in the paper by Hansson and Jonsson.[1]

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.

PCTL syntax

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 \lambda 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


A path \sigma from a state s_0 is an infinite 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 \sigma[n] and the prefix of \sigma of length n is denoted as \sigma\uparrow n.

Probability measure

A probability measure \mu_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

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

See also

References

  1. Hansson, Hans, and Bengt Jonsson. "A logic for reasoning about time and reliability." Formal aspects of computing 6.5 (1994): 512-535.
This article is issued from Wikipedia - version of the Wednesday, October 28, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.