Probabilistic Computation Tree Logic (PCTL) is an extension of computation tree logic (CTL) that 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.
YouTube Encyclopedic
-
1/5
Views:5 010
14 226
308
1 813 666
16 377
-
EE 101/20 - Controlling Variable Equations (CTL), a tutorial.
-
Applying the central limit theorem to find probability example 1
-
Finding probability using the CLT
-
Central limit theorem | Inferential statistics | Probability and Statistics | Khan Academy
-
Probability Independent Events Rolling a Die & Flipping a Coin
PCTL syntax
A possible syntax of PCTL can be defined as follows:
Therein, is a comparison operator and is a probability threshold.
Formulas of PCTL are interpreted over discrete Markov chains. An interpretation structure
is a quadruple , where
- is a finite set of states,
- is an initial state,
- is a transition probability function, , such that for all we have , and
- is a labeling function, , assigning atomic propositions to states.
A path from a state is an infinite sequence of states
. The n-th state of the path is denoted as
and the prefix of of length is denoted as .
Probability measure
A probability measure on the set of paths with a common prefix of length is given by the product of transition probabilities along the prefix of the path:
For the probability measure is equal to .
Satisfaction relation
The satisfaction relation is inductively defined as follows:
- if and only if ,
- if and only if not ,
- if and only if or ,
- if and only if and ,
- if and only if , and
- if and only if .
See also
References
- ^ Hansson, Hans, and Bengt Jonsson. "A logic for reasoning about time and reliability." Formal aspects of computing 6.5 (1994): 512-535.
This page was last edited on 11 June 2023, at 19:24