|
Abstract : |
Abstract. A unified approach to decidability questions for verification algorithms of hybrid systems 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. In this paper, we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal structure. We prove that o-minimal hybrid systems always admit finite bisimulations. We then present a list of o-minimal structures which captures most hybrid systems known to admit finite bisimulations as well as present new classes of hybrid systems with more complex dynamics for which finite bisimulations exist., |
