An hybrid system roughly consists in finitely many continuous dynamical systems coupled with a finite automaton which governs the discrete transitions between the continuous dynamical systems. Behaviors of hybrid systems model air traffic control, flight behavior... The main decision problem for hybrid systems is the reachability problem: given a set I of initial states, a set F of final states and a set A of states to avoid, does the system securely behave on inputs from I, i.e. does the system always reach a final state, avoiding the set of prohibited states?
A first global approach to this question is to build finite bisimulations of the system. We will show how to prove existence of finite bisimulations when the hybrid system is definable in a o-minimal theory. This is joint work with Thomas Brihaye, Cedric Riviere and Christophe Troestler. Our results generalizes previous results of Lafferriere, Pappas and Sastry.
Recent advances on the effectivenesss of our construction have been obtained by Maragarita Korovina and Nicolai Vorobjov in the pfaffian case.