Symbolic Algorithmic Analysis of Rectangular Hybrid Systems

This paper investigates symbolic algorithmic analysis of rectangular hybrid systems. To deal with the symbolic reachability problem, a restricted constraint system called \emphhybrid zone is formalized for the representation and manipulation of rec\-tangular automata state-spaces. Hybrid zones are proved to be closed over symbolic reachability operations of rec\-tangular hybrid systems. They are also applied to model-checking procedures for verifying some important classes of timed computation tree logic formulas. To represent hybrid zones, a data structure called \emphdifference constraint matrix is defined. These enable us to deal with the symbolic algorithmic analysis of rectangular hybrid systems in an efficient way.