Hybrid Systems with Finite Bisimulations

摘要

The theory of formal verification is one of the main approaches to hybrid system analysis. A unified approach to decidability questions for verification algorithms is obtained by the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. This approach has had success in the reachability analysis of timed automata and initialized rectangular automata. 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 hybrid systems.