# Existence and Synthesis of Multi-Resolution Approximate Bisimulations for Continuous-State Dynamical Systems

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Sep 2025.

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

- [Adaptive state-action abstractions via rate-distortion](https://mlsanity.com/paper/2606.06123/) (2026)

## Abstract (arXiv)

We present a fully automatic framework for synthesising compact, finite-state deterministic abstractions of deterministic, continuous-state autonomous systems under locally specified resolution requirements. Our approach builds on multi-resolution approximate bisimulations, a generalisation of classical ε-approximate bisimulations, that support state-dependent error bounds and subsumes both variable- and uniform-resolution relations. We show that some systems admit multi-resolution bisimulations but no ε-approximate bisimulation. We prove the existence of multi-resolution approximately bisimilar abstractions for all incrementally uniformly bounded (δ-UB) systems, thereby broadening the applicability of symbolic verification to a larger class of dynamics; as a trivial special case, this result also covers incrementally globally asymptotically stable (δ-GAS) systems. The Multi-resolution Abstraction Synthesis Problem (MRASP) is solved via a scalable Counterexample-Guided Inductive Synthesis (CEGIS) loop, combining mesh refinement with counterexample-driven refinement. This ensures soundness for all δ-UB systems, and ensures termination in certain special cases. Experiments on linear and nonlinear benchmarks, including non-δ-GAS and non-differentiable cases, demonstrate that our algorithm yields abstractions up to 50% smaller than Lyapunov-based grids while enforcing tighter, location-dependent error guarantees.