Reducing the wrapping effect in flowpipe construction using pseudo-invariants (work in progress)

The reachability problem for a nonlinear hybrid automaton is often decomposed into steps where continuous successors are computed, and steps where discrete transitions and reset maps are processed. In this paper, we will show one method which can reduce the wrapping effect in the continuous-successor computation stage. A reduction in the wrapping effect can lead to both reduced error and reduced computation time. The key insight behind the proposed method is that, when computing continuous successors, time need not be tracked precisely. We split an individual mode of a hybrid automaton into a pair of modes by introducing an artificial invariant (and associated transition) which we call a pseudo-invariant. The resultant hybrid automaton is a bisimulation of the original one, and thus their exact set of reachable states is identical. However, since time information is often dropped across discrete transitions, practical methods for overapproximating reachability can experience less wrapping-effect error when run on the constructed bisimulation. We demonstrate the advantage of the approach of pseudo-invariants by computing reachability for a nonlinear dynamical system using Flow∗, a state-of-the-art reachability tool.