# Bisimulation Learning

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

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 8 of its 54 references that are in the map.
- First posted on arXiv 24 May 2024.

## Builds on (most cited first, 8 of 8)

- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [dtControl: Decision Tree Learning Algorithms for Controller Representation](https://mlsanity.com/paper/2002.04991/) (2020)
- [Neural Abstractions](https://mlsanity.com/paper/2301.11683/) (2023)
- [Strategy Representation by Decision Trees in Reactive Synthesis](https://mlsanity.com/paper/1802.00758/) (2018)
- [Symbolic control of stochastic systems via approximately bisimilar finite abstractions](https://mlsanity.com/paper/1302.3868/) (2013)
- [Closure Certificates](https://mlsanity.com/paper/2305.17519/) (2023)
- [Deciding Conditional Termination](https://mlsanity.com/paper/1302.2762/) (2013)
- [A linear parallel algorithm to compute bisimulation and relational coarsest partitions](https://mlsanity.com/paper/2105.11788/) (2021)

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

- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [Warm Starting State-Space Models with Automata Learning](https://mlsanity.com/paper/2603.05694/) (2026)
- [Robust Parameter Learning for Uncertain MDPs](https://mlsanity.com/paper/2605.01339/) (2026)
- [Transfer Learning for Control Systems via Neural Simulation Relations](https://mlsanity.com/paper/2412.01783/) (2024)
- [Value Functions as Supermartingale Certificates](https://mlsanity.com/paper/2605.31524/) (2026)

## Abstract (arXiv)

We introduce a data-driven approach to computing finite bisimulations for state transition systems with very large, possibly infinite state space. Our novel technique computes stutter-insensitive bisimulations of deterministic systems, which we characterize as the problem of learning a state classifier together with a ranking function for each class. Our procedure learns a candidate state classifier and candidate ranking functions from a finite dataset of sample states; then, it checks whether these generalise to the entire state space using satisfiability modulo theory solving. Upon the affirmative answer, the procedure concludes that the classifier constitutes a valid stutter-insensitive bisimulation of the system. Upon a negative answer, the solver produces a counterexample state for which the classifier violates the claim, adds it to the dataset, and repeats learning and checking in a counterexample-guided inductive synthesis loop until a valid bisimulation is found. We demonstrate on a range of benchmarks from reactive verification and software model checking that our method yields faster verification results than alternative state-of-the-art tools in practice. Our method produces succinct abstractions that enable an effective verification of linear temporal logic without next operator, and are interpretable for system diagnostics.