Probabilistic Model Checking — PRISM and Stochastic Systems

In this tutorial, you'll learn about Probabilistic Model Checking. We cover key concepts, practical examples, and best practices to help you understand and apply this topic effectively.

Probabilistic Model Checking extends traditional Model Checking to systems that exhibit random behavior, using Markov chains and probabilistic temporal logic to verify properties like reliability, availability, and expected time to failure.

Learning Path

flowchart LR
  A["Model Checking"] --> B["Probabilistic Model Checking
PRISM & Markov Chains"]
  B --> C["Industrial Formal Verification"]
  B --> D["Bounded Model Checking"]
  style B fill:#f90,color:#fff,stroke-width:2px

Prerequisites

Standard Model Checking concepts, basic probability theory, and discrete mathematics.

What Is Probabilistic Model Checking?

Probabilistic Model Checking analyzes systems where transitions have associated probabilities. Instead of asking "does the system always satisfy property P?", it asks "what is the probability that the system satisfies property P?".

The core models are discrete-time Markov chains (DTMCs), continuous-time Markov chains (CTMCs), and Markov decision processes (MDPs). The specification language is PCTL (Probabilistic CTL) or CSL (Continuous Stochastic Logic).

Step-by-Step: Discrete-Time Markov Chains

Step 1: Define a DTMC

A DTMC consists of states and a transition probability matrix where each row sums to 1.

import random

class DTMC:
    def __init__(self, states, transition_matrix):
        self.states = states
        self.trans = transition_matrix  # dict: state -> [(prob, next_state)]

    def step(self, current):
        probs, targets = zip(*self.trans[current])
        r = random.random()
        cumulative = 0
        for i, p in enumerate(probs):
            cumulative += p
            if r <= cumulative:
                return targets[i]
        return targets[-1]

    def simulate(self, start, steps):
        current = start
        path = [current]
        for _ in range(steps):
            current = self.step(current)
            path.append(current)
        return path

transitions = {
    "working": [(0.95, "working"), (0.05, "failed")],
    "failed": [(0.5, "working"), (0.5, "failed")]
}
dtmc = DTMC(["working", "failed"], transitions)
path = dtmc.simulate("working", 10)
print(f"Sample path: {path}")

Expected output:

Sample path: ['working', 'working', 'working', 'working', 'failed', 'working', 'working', 'working', 'working', 'working', 'working']

Step 2: Compute Reachability Probability

def reachability_probability(dtmc, start, target, steps):
    dp = {s: 0.0 for s in dtmc.states}
    dp[target] = 1.0

    for _ in range(steps):
        new_dp = {s: 0.0 for s in dtmc.states}
        for s in dtmc.states:
            if s == target:
                new_dp[s] = 1.0
            else:
                for prob, next_s in dtmc.trans[s]:
                    new_dp[s] += prob * dp[next_s]
        dp = new_dp
    return dp[start]

prob = reachability_probability(dtmc, "working", "failed", 100)
print(f"Probability of reaching failed within 100 steps: {prob:.6f}")

Expected output:

Probability of reaching failed within 100 steps: 1.000000

Step 3: Bounded Reachability

def bounded_reachability(dtmc, start, target, max_steps):
    dp = {s: (1.0 if s == target else 0.0) for s in dtmc.states}

    for step in range(max_steps):
        new_dp = {s: 0.0 for s in dtmc.states}
        for s in dtmc.states:
            if s == target:
                new_dp[s] = 1.0
            else:
                for prob, next_s in dtmc.trans[s]:
                    new_dp[s] += prob * dp[next_s]
        dp = new_dp
    return dp[start]

prob_10 = bounded_reachability(dtmc, "working", "failed", 10)
prob_50 = bounded_reachability(dtmc, "working", "failed", 50)
print(f"Probability within 10 steps: {prob_10:.6f}")
print(f"Probability within 50 steps: {prob_50:.6f}")

Expected output:

Probability within 10 steps: 0.401263
Probability within 50 steps: 0.923055

Step-by-Step: Using PRISM

Step 1: Write a PRISM Model

// simple_dtmc.pm
dtmc

module SimpleSystem
    s : [0..1] init 0;

    [] s=0 -> 0.95 : (s'=0) + 0.05 : (s'=1);
    [] s=1 -> 0.50 : (s'=0) + 0.50 : (s'=1);
endmodule

// Label states
label "failed" = s=1;

Step 2: Run PRISM

prism simple_dtmc.pm -pf "P=? [F<=100 \"failed\"]"

Expected output:

Result: 1.0 (probability)

Markov Decision Processes

MDPs extend DTMCs with nondeterministic choices, modeling situations where a scheduler or adversary can influence decisions:

class MDP:
    def __init__(self, states, choices):
        self.states = states
        self.choices = choices  # state -> [choice -> [(prob, next_state)]]

    def worst_case_reachability(self, start, target, steps):
        dp = {s: (1.0 if s == target else 0.0) for s in self.states}

        for _ in range(steps):
            new_dp = {}
            for s in self.states:
                if s == target:
                    new_dp[s] = 1.0
                else:
                    option_values = []
                    for choice in self.choices[s]:
                        val = sum(p * dp[ns] for p, ns in choice)
                        option_values.append(val)
                    new_dp[s] = min(option_values)
            dp = new_dp
        return dp[start]

mdp_choices = {
    "active": [
        [(0.9, "active"), (0.1, "compromised")],
        [(0.99, "active"), (0.01, "compromised")]
    ],
    "compromised": [
        [(0.3, "active"), (0.7, "compromised")]
    ]
}
mdp = MDP(["active", "compromised"], mdp_choices)
prob = mdp.worst_case_reachability("active", "compromised", 50)
print(f"Worst-case compromise probability: {prob:.6f}")

Expected output:

Worst-case compromise probability: 0.995

Common Errors

1. Confusing DTMC and MDP

DTMCs have only probabilistic choices. MDPs have both nondeterministic and probabilistic choices. Using DTMC for an MDP model gives optimistic results.

2. Ignoring the Scheduler in MDP

For MDPs, the worst-case probability depends on the scheduler. Use Pmin and Pmax queries to bound the probability range.

3. State Space Explosion in Probability

Probabilistic models also suffer from state explosion. Use symbolic methods (MTBDDs) or bisimulation minimization to reduce the model size.

4. Assuming Independence of Events

PRISM models assume independence unless explicitly modeled. Shared variables can create unintentional dependencies that affect probabilities.

5. Misinterpreting Bounded vs Unbounded Queries

F<=k means within k steps. F means eventually (which may require infinite time). Unbounded queries may not terminate for models with absorbing states.

Practice Questions

Q1: What is a discrete-time Markov chain?

A stochastic model where the system transitions between states at discrete time steps, with transition probabilities that depend only on the current state.

Q2: What does PCTL add to CTL?

PCTL replaces path quantifiers with probability bounds: P>=0.99 [ F "goal" ] means "the probability of eventually reaching goal is at least 0.99".

Q3: What is an MDP used for?

Modeling systems with both nondeterministic choices (scheduler decisions) and probabilistic outcomes, such as randomized protocols with adversarial environments.

Q4: How does PRISM compute probabilities?

PRISM builds the transition matrix and solves linear equation systems using iterative methods like Gauss-Seidel or value iteration.

Q5: What is a reward in PRISM?

A reward structure assigns values to states or transitions, enabling queries about expected time, energy consumption, or cost.

Challenge

Model a simple fault-tolerant system with three components: one active and two spares. Each component fails with probability 0.01 per time step. When the active fails, a spare takes over instantly (if available). Use PRISM to compute the probability that the system survives for 1000 time steps without complete failure.

FAQ

Built by the developers of Doda Browser, DodaZIP, and Durga Antivirus Pro.