A Geometric Approach to Bisimulation and Verification of Hybrid Systems

An approximate verification method for hybrid systems in which sets of the automaton are over-approximated, while leaving the vector fields intact, is presented. The method is based on a geometricallyinspired approach, using tangential and transversal foliations, to obtain bisimulations. Exterior differential systems provide a natural setting to obtain an analytical representation of the bisimulation, and to obtain the bisimulation under parallel composition. We define the symbolic execution theory and give applications to coordinated aircraft and robots.