Abstract. The theory of formal verification is one of the main approaches to hybrid system analysis. Decidability questions for verification algorithms are obtained by constructing finite, reachability preserving quotient systems called bisimulations. In this paper, we use recent results from stratification theory, subanalytic sets, and model theory in order to extend the state-of-the-art results on the existence of bisimulations for certain classes of planar hybrid systems.
Gerardo Lafferriere, George J. Pappas, Shankar Sas