Systems Using Bisimulat ions
George J. Pappast, Shankar SastryS · 1998
A unified approach to decidability questions for the verification of hybrid systems is obtained by the construction of a bisimulation. These are finite state quotients whose reachability properties are equivalent to those of the original infinite state system. This approach has had some success in the reachability analysis of timed automata and linear hybrid automata. In this paper, we use results from stratification theory, subanalytic sets and model theory of fields in order to extend earlier results on the existence of bismimulations for certain classes of analytic vector fields.