Compile-Time Extensions to Hybrid ODEs

TL;DR

This paper introduces compile-time transformations that extend hybrid ODE formalism in reachability tools, enabling more expressive modeling of mechanical systems with derivatives and constraints, while ensuring soundness.

Contribution

It presents a novel compile-time approach to extend hybrid ODEs in reachability analysis tools, supporting derivatives and constraints with proven soundness.

Findings

Supports partial derivatives and equational constraints

Enables expression of Euler-Lagrangian equations

Ensures soundness of the extension

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.

Figures