Symbolic Reachability Analysis of Hybrid Systems

A restricted constraint system called hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces. Hybrid zones are proved to be closed over reachability operations of rectangular hybrid systems. In addition, rectangular hybrid systems are used to simulate nonlinear hybrid systems, which enables us to use hybrid zones for reachability analysis of nonlinear hybrid systems. After the hybrid zone has been converted to the canonical form, reachability operations for hybrid systems can be implemented straightforwardly. Hence, the main computation is the operation for obtaining the canonical form of hybrid zones. Finding the canonical form can be automated by an algorithm for linear programming.