💻 computer science

Robust Probabilistic Bisimilarity for Labelled Markov Chains

This paper addresses the lack of robustness in standard probabilistic bisimilarity under small perturbations of transition probabilities by introducing a new notion of robust probabilistic bisimilarity that ensures continuity and providing an efficient algorithm to compute it.

Original authors: Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, Franck van Breugel

Published 2026-06-26

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Syyeda Zainab Fatmi, Stefan Kiefer, David Parker, Franck van Breugel

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are trying to sort a massive pile of mixed-up toys into boxes based on how they behave. Some toys look different but act exactly the same (like two different-looking remote controls that do the exact same thing). In the world of computer science, specifically for systems that involve chance (like a robot flipping a coin to decide where to go next), we call this sorting process "probabilistic bisimilarity."

For a long time, computer scientists have used this method to simplify complex systems. If two states (or "toy positions") are "bisimilar," they can be merged into one, making the system easier to check and verify.

The Problem: The "House of Cards" Effect
The paper points out a major flaw in the traditional method: it's incredibly fragile. Imagine building a house of cards. If the probabilities are perfect, the cards stand. But if you blow just a tiny breath of air (a tiny error in the data, like a coin that is 50.1% heads instead of exactly 50%), the whole house collapses.

In the real world, we rarely know the exact probabilities of a system. We usually estimate them from experiments or data, which always have tiny errors. The old method says: "If the coin is 50/50, these two states are identical. If it's 50.1/49.9, they are completely different." This creates a "jump" or a discontinuity. A tiny, harmless error in measurement causes the computer to think the system has completely changed its behavior. This makes the verification unreliable for real-world applications where data is never perfect.

The Solution: "Robust" Bisimilarity
The authors introduce a new concept called Robust Probabilistic Bisimilarity.

Think of the old method as a strict judge who says, "You are either 100% identical or 0% identical."
The new method is like a wise mentor who says, "You are identical, and even if we nudge the rules slightly, you will still act almost the same."

How it Works (The Analogy of the Safe Path)
To understand how they define this "robustness," imagine two people, Alice and Bob, walking through a maze.

Old Method: If they take the exact same path, they are "bisimilar." If the map changes slightly and they take a different path, they are no longer similar.
New Method (Robust): We ask, "Is there a strategy where Alice and Bob can always find a way to end up in the same 'safe zone' together, even if the maze walls shift slightly?"
- If the answer is yes, they are robustly bisimilar. They are "stuck together" in a way that survives small changes.
- If the answer is no (meaning a tiny shift in the maze sends them to totally different destinations), they are not robustly bisimilar, even if they looked identical on the perfect map.

The Algorithm: A Smart Filter
The paper doesn't just define this; they built a tool (an algorithm) to find these robust pairs.

Start: They begin with all the pairs that the old method says are identical.
Filter: They run a test to see which of these pairs can survive a "stress test" (a strategy that keeps them together despite potential changes).
Prune: They remove the pairs that fail the test.
Repeat: They keep refining the list until they are left with only the pairs that are truly robust.

The Results: It Works!
The authors tested this new tool on many standard computer models (like traffic lights, coin tossers, and network protocols).

Speed: It takes a bit more time to run than the old method (like checking a map more carefully), but it's still fast enough to be useful.
Safety: In many cases, the old method would merge two states that look the same but actually behave very differently if the data is slightly off. The new method correctly identifies these as "unsafe to merge" and keeps them separate.
Continuity: Most importantly, the new method ensures that if you change the probabilities slightly, the "distance" between states changes smoothly, rather than jumping wildly.

In Summary
This paper gives us a way to check computer systems that are "tougher" against real-world imperfections. Instead of breaking when the data isn't perfect, the new "Robust" method ensures that our understanding of the system remains stable and reliable, even when the numbers are just a little bit fuzzy.

Technical Summary: Robust Probabilistic Bisimilarity for Labelled Markov Chains

Problem Statement

Probabilistic bisimilarity is a foundational concept in the verification of probabilistic systems, allowing for the minimization of state spaces by merging behaviorally indistinguishable states. However, standard probabilistic bisimilarity lacks robustness under minute perturbations of transition probabilities. While the probabilistic bisimilarity distance function (a behavioral pseudometric) quantifies the similarity between states, it is often discontinuous. This means that arbitrarily small changes in transition probabilities can cause the distance between two states to jump abruptly from 0 (bisimilar) to a large value (e.g., 1), or vice versa.

This discontinuity poses a significant reliability issue in practical applications where transition probabilities are derived from experimental data and are inherently approximate. As illustrated in the paper's examples, two states may be bisimilar in a nominal model ( $\varepsilon = 0$ ) but exhibit maximally different long-term behaviors (e.g., reachability properties) under infinitesimal perturbations ( $\varepsilon > 0$ ). Consequently, merging such states in a minimized model can be unsafe if the precise transition probabilities are unknown.

Methodology

The authors introduce robust probabilistic bisimilarity ( $\simeq$ ) as a stricter subset of standard probabilistic bisimilarity ( $\sim$ ). The core methodology involves:

Policy-Based Characterization: The paper utilizes the concept of policies (couplings) on the product space of states $S \times S$ . A policy $P$ maps pairs of states to distributions over $S \times S$ .
Definition of Robustness: Two states $s$ and $t$ are robustly bisimilar ( $s \simeq t$ ) if there exists a policy $P$ such that the pair $(s, t)$ reaches the diagonal set $S^2_\Delta = \{(s, s) \mid s \in S\}$ with probability 1 in the induced Markov chain $\langle S \times S, P \rangle$ .
Continuity Guarantee: The authors prove that if $s \simeq t$ , the probabilistic bisimilarity distance function $\delta(s, t)$ is continuous with respect to perturbations of the transition function $\tau$ . Specifically, for any sequence of transition functions $\tau_n$ converging to $\tau$ , if $s \simeq t$ , then $\lim_{n \to \infty} \delta_{\tau_n}(s, t) = 0$ . This contrasts with standard bisimilarity, where the limit may not equal the distance at the nominal point.
Algorithmic Computation: The paper presents a polynomial-time algorithm (Algorithm 1) to compute the greatest robust bisimulation. The algorithm iteratively refines an initial set of bisimilar states using three functions:
- Filter: Identifies pairs that can reach the diagonal $S^2_\Delta$ under some policy supported by the current relation.
- Prune: Ensures the relation remains symmetric and transitive with respect to the "neighborhood" defined by the Filter step.
- Bisim: Computes the largest bisimulation contained within the current relation.
  The algorithm terminates at the greatest fixed point of the composition of these functions.

Key Contributions

Formal Definition: The introduction of robust probabilistic bisimilarity, defined via policies that ensure almost-sure reachability of the diagonal in the product space.
Theoretical Guarantee: A proof (Theorem 2) that robust probabilistic bisimilarity is a sufficient condition for the continuity of the probabilistic bisimilarity distance function under arbitrary perturbations of transition probabilities.
Efficient Algorithm: The development of an $O(n^6)$ algorithm (where $n$ is the number of states) to compute robust probabilistic bisimilarity, making it feasible for large-scale verification tasks.
Empirical Validation: Implementation of the algorithm within the PRISM model checker and evaluation on benchmarks from the Quantitative Verification Benchmark Set (QVBS) and the jpf-probabilistic extension.

Experimental Results

The authors evaluated their implementation against 170 models. Key findings include:

Feasibility: Robust bisimilarity was successfully computed for 152 models (approx. 89%) in under one minute.
State Space Differences: In cases where the minimized models differed, the robust approach often resulted in significantly larger state spaces compared to traditional bisimilarity, correctly identifying pairs of states that should not be merged due to sensitivity.
Performance Overhead: While robust bisimilarity is slower than traditional bisimilarity (with average time increases ranging from 28% to over 140,000% depending on the benchmark, e.g., the crowds benchmark), the computation time remained practical for most standard models.
Limitations: For 10 models (approx. 6%), the robust algorithm failed due to memory constraints (OutOfMemoryError), whereas traditional bisimilarity succeeded. This was observed in specific instances of the nand and egl benchmarks.

Significance and Claims

The paper claims that robust probabilistic bisimilarity provides a more reliable method for determining state equivalence in probabilistic systems where transition probabilities are approximations. By ensuring the continuity of the distance function, the approach mitigates the risk of merging states that behave differently under slight parameter variations.

The authors position this work as a necessary step for practical applications, particularly in mission-critical systems requiring high precision. They note that while robust bisimilarity is a sufficient condition for continuity, they conjecture it may also be a necessary condition for bisimilar states. The paper concludes by identifying future directions, including logical characterizations of robust bisimilarity and investigating specific types of perturbations that preserve graph structure versus those that introduce new transitions.