
Probabilistic Model Checking with PCTL
Finite Automata
Modelling real-world systems can be done with something called finite automata, a mathematical object in which we have a collection of labelled states, with transitions between them. For example, below is an automaton representing a UK traffic light, labelled with the colour the light is in a given state, with arrows representing the transitions between the states. Note that we’re modelling with discrete time-steps rather than continuous time. The labelling of states is done with so-called ‘atomic propositions’, these are basically low-level properties that we know hold in a given state.
We are allowed to have multiple outgoing transitions from a state, in which case the choice is non-deterministic. This allows us to model uncertain real-world behaviour, such as the fact that when the traffic light is red there is a non-zero probability that it will explode!
So, while this tells us which transitions could possibly be taken, it says nothing about the probability of those transitions. We can extend our definition of an automaton so that each transition has a probability of being taken. For this to make sense, the probabilities of all of a node’s outgoing edges must sum to one. This new type of automaton is called a Markov chain or Markov process.
The probability of taking a particular path through the automaton, i.e. a particular sequence of connected states, is the product of the probabilities of the connecting transitions that we take along the way.
Probabilistic Computation Tree Logic (PCTL)
While this structure allows us to model real-world systems with quantified uncertainty, we would then like to be able to answer complex probabilistic questions about these systems. For example, when considering a communication protocol, we may want to verify that “There is at least a 95% probability that within 5 time-steps of sending a message, we receive an acknowledgement”. To formally express statements like these, we use a logic called Probabilistic Computation Tree Logic (PCTL). This logic has a branching model of time where in a given state there may be multiple outgoing paths into future states, creating a tree structure that expands outwards as time progresses.
PCTL has the standard logical operators like negation, conjunction, implication, etc., but the fundamental temporal building block of PCTL is the ‘until’ operator:
which says that with a probability of at least
Let us create a model of a hungry frog who wants to eat a fly, but is very inaccurate. The frog begins in its initial state as being hungry. It tries to eat the fly, with a 10% probability of success and a 90% probability of failure. If it succeeds then the frog is satisfied, if it fails then the frog is still hungry, but is now sad as well. In this state, the fly has a 50% probability of making its escape, and so the frog stays permanently hungry and sad. Otherwise the frog gets another chance at eating it.
We may want to claim that there is at least a 10% probability that within 10 time-steps, the frog is satisfied (i.e. it has eaten the fly), which we would formulate as:
(The formula
It’s all well and good to claim that this formula holds in our model, but how do we validate our claim? This is where model checking comes in, which is a way to automatically verify whether a temporal logic formula holds in a given model.
Model Checking
We solve our problem from the bottom-up, finding solutions for each of the constituent parts of our formula, and then combining these solutions together in a compositional way so that we eventually get the answer for the full formula.
This algorithm operates by ‘labelling’ states with sub-formulae, with the labelling of a complex formulae being dependent on which states are labelled with its constituent sub-formulae. As an example, let’s check the formula
in the model
We start with the left sub-formula
As an introduction to this idea we can first consider the case where
We can compute this recursively in a top-down manner, starting in the starting state and recursing on each outgoing edge to the neighbouring states. In each state, if the state is labelled with
As this is a property of states, and we may compose together multiple temporal operators, we must perform this state exploration algorithm independently from every state, so that at the end each state is either labelled with
Below is listed the labelling of each state in the model with this
We now cover the case of model checking when
This says that if we are in a state
As above, we compute
Below is
Assuming that the starting state of the model is
Links
Code
- PCTL GitHub repository (link).