Probabilistic Model Checking

Discrete-time Markov Chains

$P$ is a stochastic matrix:
- $P(s,s’) \in [0,1]$ for all $s, s’ \in S$ and $\sum_{s’ \in S} P(s,s’) = 1$ for all $s \in S$
$P$ is a sub-stochastic matrix:
- $P(s,s’) \in [0,1]$ for all $s, s’ \in S$ and $\sum_{s’ \in S} P(s,s’) \leq 1$ for all $s \in S$
An absorbing state is a state for $s$ for which:
- $P(s,s) = 1$ and $P(s,s’) = 0$ for all $s \not = s’$
- the transition from $s$ to itself is also called a self-loop.
Since we assume $P$ is stochastic:
- every state has at least one outgoing transition
- i.e. no deadlocks in model checking terminology

Probabilistic reachability
- probability of a path reaching a state in some target set $T \in S$
Dual of reachability: invariance
- probability of remaining within some class of states
Other variants of reachability
- time-bounded

Derive a linear equation system
- solve for all states simultaneously
Least fixed point characterisation
- This yields a simple iterative algorithm to approximate ProbReach(T)
- using the power mehtod
  - which is guaranteed to converge
- also yields step-bounded reachability probabilities

$\pi_{s,k} = \pi_{s,k-1} \cdot P = \pi_{s, 0} \cdot P^k$
$k^{th} matrix power: P^k$
- $p$ gives one-step transition probabilities
- $p^k$ gives probabilities of $k$-step transition probabilities
- i.e. $P^k(s,s’) = \pi_{s,k}(s’)$

Two possible views:
- Discrete time steps model time accurately
- Time-abstract model
In both cases, often beneficial to study long-run behaviour

Consider the limit
- if this limit exists, is called the limiting distribution
- steady-state of the model
Questions:
- when does this limit exist?
- does it depend on the initial state/distribution?

Markov chain is irreducible if all its states belong to a single BSCC, otherwise reducible

For a finite, irreducible, aperiodic DTMC (a.k.a, ergodic)
- limiting distribution always exists
- and is independent of initial state/disbribution
These are known as steady-state probabilities
- or equilibrium probabilities
- effect of initial distribution has disappeared, denoted $\pi$
These probabilities can be computed as the unique solution of the linear equation system:
- $\pi \cdot P = \pi$ and $\sum_{s \in S} \pi (s) = 1$
- known as balance equations
General case: reducible DTMC
- there are multiple solutions of steady-state equation
- number of solution = number of BSCCs
- limiting distribution obtained by iterations exists
- limiting distribution depends on initial one
- compute BSCCs for DTMC; then two cases to consider:
  - s is in a BSCC T
    - compute steady-state probabilities x in sub-DTMC for T
    - $\pi_s (s’) = x(s’)$ if $s’$ in $T$
    - $\pi_s (s’) = 0$, otherwise
  - s is not in any BSCC
    - compute steady-state probabilities $x_T$ for sub-DTMC of each BSCC T and combine with reachability probabilities to BSCCs
    - $\pi_s (s’) = ProbReach(s,T) \cdot x_T(s’)$ if $s’$ is in BSCC T
    - $\pi_s (s’) = 0$, otherwise