Symbolic algorithm analysis of rectangular hybrid systems

This paper investigates symbolic algorithm analysis of rectangular hybrid systems. To deal with the symbolic reachability problem, a restricted constraint system called hybrid zone is formalized. Hybrid zones are also applied to a symbolic model-checking algorithm for verifying some important classes of timed computation tree logic formulas. To present hybrid zones, a data structure called difference constraint matrix is defined. Using this structure, all reachability operations and model checking algorithms for rectangular hybrid systems are implemented. These enable us to deal with the symbolic algorithm analysis of rectangular hybrid systems in an efficient way.