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 hybrid zone is formalized for the representation and manipulation of rectangular automata state-spaces. Hybrid zones are proved to be closed over symbolic reachability operations of rectangular 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 difference constraint matrix is defined. These enable us to deal with the symbolic algorithmic analysis of rectangular hybrid systems in an e±cient way. Electronic supplementary material  The online version of this article (doi: ) contains supplementary material, which is available to authorized users. This research is supported by the National Natural Science Foundation of China under Grant Nos. 60433010 and 60873018, the Specialized Research Foundation for the Doctoral Program of Chinese Higher Education under Grant No. 200807010012, and the Defense Pre-Research Project of China under Grant No. 51315050105.