The Community for Technology Leaders
2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering (2010)
Taipei, Taiwan
Aug. 25, 2010 to Aug. 27, 2010
ISBN: 978-0-7695-4148-8
pp: 126-131
ABSTRACT
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.
INDEX TERMS
hybrid systems, rectangular automata, model checking, timed computing tree logic
CITATION

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.
doi:10.1109/TASE.2010.18
91 ms
(Ver 3.3 (11022016))