O-Minimal Hybrid Reachability Games

In this paper, we consider reachability games over general hybrid systems,and distinguish between two possible observation frameworks for those games:either the precise dynamics of the system is seen by the players (this is theperfect observation framework), or only the starting point and the delays areknown by the players (this is the partial observation framework). In the firstmore classical framework, we show that time-abstract bisimulation is notadequate for solving this problem, although it is sufficient in the case oftimed automata . That is why we consider an other equivalence, namely thesuffix equivalence based on the encoding of trajectories through words. We showthat this suffix equivalence is in general a correct abstraction for games. Weapply this result to o-minimal hybrid systems, and get decidability andcomputability results in this framework. For the second framework which assumesa partial observation of the dynamics of the system, we propose anotherabstraction, called the superword encoding, which is suitable to solve thegames under that assumption. In that framework, we also provide decidabilityand computability results