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

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TASE.2010.18

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

CITATIONS

SEARCH