Title: Compile-Time Extensions to Hybrid ODEs,
Abstract: 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.