Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2509.17739 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916960690765824 |
|---|---|
| author | Coppola, Rudi Schnitzer, Yannik Giacobbe, Mirco Abate, Alessandro Mazo Jr, Manuel |
| author_facet | Coppola, Rudi Schnitzer, Yannik Giacobbe, Mirco Abate, Alessandro Mazo Jr, Manuel |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_17739 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Existence and Synthesis of Multi-Resolution Approximate Bisimulations for Continuous-State Dynamical Systems Coppola, Rudi Schnitzer, Yannik Giacobbe, Mirco Abate, Alessandro Mazo Jr, Manuel Systems and Control 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. |
| title | Existence and Synthesis of Multi-Resolution Approximate Bisimulations for Continuous-State Dynamical Systems |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2509.17739 |