Guaranteed Error Bounds on Approximate Model Abstractions through Reachability Analysis
Luca Cardelli, Mirco Tribastone, Max Tschaikowski, and Andrea Vandin

TL;DR
This paper introduces approximate differential equivalence for nonlinear ODEs, enabling robust model abstraction with guaranteed error bounds through reachability analysis, and demonstrates its application to electric circuit models.
Contribution
It develops algorithms for computing approximate differential equivalence, constructing quotient models, and providing formal error bounds for nonlinear ODE abstractions.
Findings
Algorithms for approximate differential equivalence and error bounds.
Application to symmetric electric circuit models.
Formal certification of approximation quality.
Abstract
It is well known that exact notions of model abstraction and reduction for dynamical systems may not be robust enough in practice because they are highly sensitive to the specific choice of parameters. In this paper we consider this problem for nonlinear ordinary differential equations (ODEs) with polynomial derivatives. We introduce approximate differential equivalence as a more permissive variant of a recently developed exact counterpart, allowing ODE variables to be related even when they are governed by nearby derivatives. We develop algorithms to (i) compute the largest approximate differential equivalence; (ii) construct an approximate quotient model from the original one via an appropriate parameter perturbation; and (iii) provide a formal certificate on the quality of the approximation as an error bound, computed as an over-approximation of the reachable set of the perturbed…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Numerical methods for differential equations · Low-power high-performance VLSI design
