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

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.