2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering (2010)
Aug. 25, 2010 to Aug. 27, 2010
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2010.18
To deal with the model checking issue of rectangular hybrid systems, a constraint system called hybrid zone is introduced for the representation and manipulation of rectangular hybrid automata state-spaces. Model checking procedures for rectangular hybrid systems based on timed computation tree logic are given. The hybrid zone is proved to be closed to the operations required in these model checking procedures, which enables it to be used as the basis for the infinite state-space exploring of rectangular hybrid automata. To represent hybrid zones, a data structure difference constraint matrix is introduced.
hybrid systems, rectangular automata, model checking, timed computing tree logic
L. Zhang, H. Zhang, B. Huang, X. Wang and Z. Duan, "Model Checking Rectangular Hybrid Systems with Timed Computation Tree Logic," 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering(TASE), Taipei, Taiwan, 2010, pp. 126-131.