2018/07/18 by Luca Cardelli, Mirco Tribastone, Cardelli, Luca +5
Computer Science · Engineering · Mathematics · #Formal Methods in Verification #Low-power high-performance VLSI design #Numerical methods for differential equations
paper · pdf · doi:10.48550/arxiv.1807.06888
It is well known that exact notions of model abstraction and reduction for\ndynamical systems may not be robust enough in practice because they are highly\nsensitive to the specific choice of parameters. In this paper we consider this\nproblem for nonlinear ordinary differential equations (ODEs) with polynomial\nderivatives. We introduce approximate differential equivalence as a more\npermissive variant of a recently developed exact counterpart, allowing ODE\nvariables to be related even when they are governed by nearby derivatives. We\ndevelop algorithms to (i) compute the largest approximate differential\nequivalence; (ii) construct an approximate quotient model from the original one\nvia an appropriate parameter perturbation; and (iii) provide a formal\ncertificate on the quality of the approximation as an error bound, computed as\nan over-approximation of the reachable set of the perturbed model. Finally, we\napply approximate differential equivalences to study the effect of parametric\ntolerances in models of symmetric electric circuits.\n