Compile-Time Extensions to Hybrid ODEs

Yingfu Zeng
(Rice University)
Ferenc Bartha
(Rice University)
Walid Taha
(Halmstad University)

Reachability analysis for hybrid systems is an active area of development and has resulted in many promising prototype tools. Most of these tools allow users to express hybrid system as automata with a set of ordinary differential equations (ODEs) associated with each state, as well as rules for transitions between states. Significant effort goes into developing and verifying and correctly implementing those tools. As such, it is desirable to expand the scope of applicability tools of such as far as possible. With this goal, we show how compile-time transformations can be used to extend the basic hybrid ODE formalism traditionally supported in hybrid reachability tools such as SpaceEx or Flow*. The extension supports certain types of partial derivatives and equational constraints. These extensions allow users to express, among other things, the Euler-Lagrangian equation, and to capture practically relevant constraints that arise naturally in mechanical systems. Achieving this level of expressiveness requires using a binding time-analysis (BTA), program differentiation, symbolic Gaussian elimination, and abstract interpretation using interval analysis. Except for BTA, the other components are either readily available or can be easily added to most reachability tools. The paper therefore focuses on presenting both the declarative and algorithmic specifications for the BTA phase, and establishes the soundness of the algorithmic specifications with respect to the declarative one.

In Erika Ábrahám and Sergiy Bogomolov: Proceedings 3rd International Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR 2017), Uppsala, Sweden, 22nd April 2017, Electronic Proceedings in Theoretical Computer Science 247, pp. 52–70.
Published: 8th April 2017.

ArXived at: https://dx.doi.org/10.4204/EPTCS.247.5 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org