Discrete Dynamics of Two-Dimensional Nonlinear Hybrid Automata

In this paper, we develop an algorithm to compute under- and over-approximations to the discrete dynamics of a hybrid automaton. We represent the approximations to the dynamics as \emph{sofic shifts}, which can be generated by a discrete automaton. We restrict to two-dimensional systems, since these give rise to one-dimensional return maps, which are significantly easier to study. Given generic non-degeneracy conditions, the under- and over-approximations computed by our algorithm converge to the discrete dynamics of the hybrid automaton. We apply the algorithms to two simple nonlinear hybrid systems, an affine switching system with hysteresis, and the singularly forced van der Pol oscillator.