# On the Relationship between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context (Extended Version)

arXiv: https://arxiv.org/abs/1701.04547 · HTML: https://mlsanity.com/paper/1701.04547/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 17 Jan 2017.

## Built on by (most cited first, 3 of 3)

- [Bisimulation Metrics are Optimal Transport Distances, and Can be Computed Efficiently](https://mlsanity.com/paper/2406.04056/) (2024)
- [Mode Reduction for Markov Jump Systems](https://mlsanity.com/paper/2205.02697/) (2022)
- [Comparing Labeled Markov Chains: A Cantor-Kantorovich Approach](https://mlsanity.com/paper/2511.18103/) (2025)

## Abstract (arXiv)

This work introduces a notion of approximate probabilistic trace equivalence for labelled Markov chains, and relates this new concept to the known notion of approximate probabilistic bisimulation. In particular this work shows that the latter notion induces a tight upper bound on the approximation between finite-horizon traces, as expressed by a total variation distance. As such, this work extends corresponding results for exact notions and analogous results for non-probabilistic models. This bound can be employed to relate the closeness in satisfaction probabilities over bounded linear-time properties, and allows for probabilistic model checking of concrete models via abstractions. The contribution focuses on both finite-state and uncountable-state labelled Markov chains, and claims two main applications: firstly, it allows an upper bound on the trace distance to be decided for finite state systems; secondly, it can be used to synthesise discrete approximations to continuous-state models with arbitrary precision.