Discrete reachability of hybrid systems

This paper concerns hybrid systems subject to discrete-event supervisory control. It investigates the discrete reachability, where the hybrid system should be moved from a discrete initial state zinit into a given discrete goal state zgoal by a sequence of discrete inputs. The reachability analysis is carried out in three steps. First, a discrete-event model of the hybrid system is set up. Stochastic automata are used to describe all state sequences which may be generated by the hybrid system. Such a model is called complete. Second, methods for the reachability analysis of stochastic automata are elaborated which concern a weak and a strong condition for reachability. Third, these methods are applied to the hybrid system. It is shown that the reachability of the automaton implies the discrete reachability of the hybrid system, because the model is complete. Therefore, the weak and the strong condition for reachability of the stochastic automaton yield a necessary and a sufficient condition for discrete reachability of the hybrid system.