Hybridization based reachability of uncertain planar affine systems

The behaviour verification of hybrid systems, for example for safety properties, is based on the computation of the reachable state space of a hybrid automaton modelling the system under study. In this paper we present a method for the computation of reachable set of uncertain hybrid affine systems. This method extends previous works which compute the reachable set of certain affine systems by abstracting the continuous dynamics by a linear hybrid automaton. We show that the calculus of the reachable space of the uncertain system may be deduced from the computation of the reachable sets of a finite number of certain systems