Theory and computation of discrete state space decompositions for hybrid systems

The problem of verifying whether properties such as reachability and safety hold for a hybrid system can be simplified, for example by using bisimulation. In this paper, we introduce a novel decomposition method to simplify the problem of verifying also other important properties such as stabilizability and detectability. To do so, we characterize general properties of a hybrid system and derive structural decompositions with respect to the characterization, which reduce the verification problem to a set of simpler verification problems on the elements of the decomposition.