Labelled Markov Processes

Prakash Panangaden · 2009 · Imperial College Press

Prereqs: 🍞 Fritz 2020 (Markov kernels, composition). Basic probability.

Two stochastic systems are behaviorally equivalent if no experiment can tell them apart. Bisimulation makes this precise. The bisimulation metric measures how different two systems are — a continuous relaxation of the binary same-or-different question.

Labelled Markov processes

A labelled Markov process (LMP) is a state space with labelled probabilistic transitions. From state s, action a leads to a distribution over next states. It's a Markov decision process viewed through the lens of process algebra.

Scheme

; LMP: states + labelled transitions
; transition(state, label) -> distribution over states

(define (transition state label)
  (cond
    ((and (eq? state 's0) (eq? label 'a))
     '((s1 . 0.7) (s2 . 0.3)))
    ((and (eq? state 's1) (eq? label 'a))
     '((s0 . 0.5) (s1 . 0.5)))
    ((and (eq? state 's2) (eq? label 'a))
     '((s2 . 1.0)))
    (else '())))

(display "s0 --a--> ") (display (transition 's0 'a)) (newline)
(display "s1 --a--> ") (display (transition 's1 'a)) (newline)
(display "s2 --a--> ") (display (transition 's2 'a)) (newline)
; s2 is absorbing: once you're there, you stay

Bisimulation — behavioral equivalence

Two states are bisimilar if they can't be distinguished by any sequence of observations. Formally: s ~ t if for every label a, the distributions transition(s,a) and transition(t,a) assign the same total probability to every equivalence class of ~.

Scheme

; Bisimulation: s ~ t iff no experiment distinguishes them
; Check: do s and t assign same probability to each class?

; Two systems: one with 3 states, one with 2
; System 1: s0 --a--> (s1: 0.5, s2: 0.5)
; System 2: t0 --a--> (t1: 0.5, t1: 0.5) = (t1: 1.0)
; s1 and s2 might be bisimilar (both absorbing)

(define (absorbing? state trans label)
  (let ((d (trans state label)))
    (and (= (length d) 1)
         (eq? (caar d) state))))

(define (trans1 s l)
  (cond ((eq? s 's1) '((s1 . 1.0)))
        ((eq? s 's2) '((s2 . 1.0)))
        (else '())))

(display "s1 absorbing? ")
(display (absorbing? 's1 trans1 'a)) (newline)
(display "s2 absorbing? ")
(display (absorbing? 's2 trans1 'a)) (newline)
; Both absorbing — bisimilar. No experiment tells them apart.
; They can be merged into one equivalence class.

Bisimulation metric

Instead of binary (same or different), measure how far apart two states are. The bisimulation metric d(s,t) is the maximum difference in expected reward over all experiments. d(s,t) = 0 iff s ~ t. This is the Kantorovich lifting of the metric to distributions.

Scheme

; Bisimulation metric: iterative fixed point
; d_{n+1}(s,t) = max_label Kantorovich(d_n)(trans(s,l), trans(t,l))
; Kantorovich distance lifts d to distributions

(define (kantorovich-1d d-prev dist1 dist2)
  ; Simplified: total variation for 2-state case
  (let ((states '(s0 s1 s2)))
    (apply + (map (lambda (s)
      (let ((p1 (let ((e (assoc s dist1))) (if e (cdr e) 0)))
            (p2 (let ((e (assoc s dist2))) (if e (cdr e) 0))))
        (abs (- p1 p2))))
    states))))

; s0 --a--> (s1: 0.7, s2: 0.3)
; s1 --a--> (s0: 0.5, s1: 0.5)
(define d1 '((s1 . 0.7) (s2 . 0.3)))
(define d2 '((s0 . 0.5) (s1 . 0.5)))

(display "TV distance(s0->a, s1->a) = ")
(display (kantorovich-1d '() d1 d2))
; Nonzero — s0 and s1 are behaviorally different

Logical characterization

The metric has a logical counterpart: two states are distance d apart iff there exists a formula in a quantitative logic that evaluates to values differing by d on the two states. Behavioral distance = logical distance. This is the quantitative analogue of the Hennessy-Milner theorem.

Scheme

; Logical characterization: distance = max formula difference
; Formula: "probability of reaching absorbing state within 2 steps"

(define (prob-reach trans state label target steps)
  (if (= steps 0)
    (if (eq? state target) 1.0 0.0)
    (let ((dist (trans state label)))
      (apply + (map (lambda (p)
        (* (cdr p)
           (prob-reach trans (car p) label target (- steps 1))))
      dist)))))

(define (trans s l)
  (cond ((eq? s 's0) '((s1 . 0.7) (s2 . 0.3)))
        ((eq? s 's1) '((s0 . 0.5) (s1 . 0.5)))
        ((eq? s 's2) '((s2 . 1.0)))
        (else '())))

(display "P(reach s2 in 2 from s0) = ")
(display (prob-reach trans 's0 'a 's2 2)) (newline)
(display "P(reach s2 in 2 from s1) = ")
(display (prob-reach trans 's1 'a 's2 2)) (newline)
; Difference in this formula witnesses behavioral distance

Notation reference

Paper	Scheme	Meaning
(S, {τ_a})	(transition state label)	LMP: states + labelled transitions
s ~ t	; bisimilar (no experiment distinguishes)	Bisimulation relation
d(s,t)	(kantorovich-1d ...)	Bisimulation metric
K(d)	; Kantorovich lifting	Lift metric to distributions
L	; set of labels (actions)	Action alphabet

Neighbors

Other paper pages

🍞 Fritz 2020 — the category where these kernels compose
🍞 Sato 2023 — divergences as distances between distributions
🍞 Baez, Fritz, Leinster 2011 — information loss (related to behavioral distance)

Foundations (Wikipedia)

Translation notes

All examples use finite state spaces with explicit transition tables. Panangaden works with labelled Markov processes over analytic spaces — continuous state spaces with σ-algebras, where bisimulation is defined via measurable partitions and the metric uses the Kantorovich (Wasserstein-1) distance on probability measures. For example: the bisimulation metric on this page computes total variation between finite distributions. In the book, the Kantorovich metric lifts an arbitrary pseudometric on states to distributions over those states, and the bisimulation metric is the greatest fixed point of this lifting. The iterative structure is the same; the measure-theoretic foundations are not.

Every example is Simplified.

Ready for the real thing? The book is published by Imperial College Press (2009). Start at Chapter 4 for bisimulation, Chapter 7 for the metric, Chapter 8 for the logical characterization.

← Di Lavore 2025 · 17 of 21 by june.kim Cho, Jacobs 2015 · 19 of 21 →