[1]KOPKE P, HENZINGER T A, PURL, A, et al. What's decidable about hybrid automata?[J]. Journal of Computer and System Sciences, 1995,57(1): 94-124.[2]LAFFERRIERE G, PAPPAS G, YOVINE S. A new class of decidable hybrid systems[C]// Hybrid Systems: Computation and Control, LNCS 1569. Berlin: Springer, 1999: 137-151.[3]ZHANG H B, DUAN Z H. Symbolic algorithmic analysis of rectangular hybrid systems[J]. Journal of Computer Science and Technology, 2009, 24(3): 531-543.[4]HARTMANNS A, HERMANNS H. A modest approach to checking probabilistic timed automata[C]// Proceedings of the 6th International Conference on Quantitative Evaluation of Systems. Washington, DC: IEEE Computer Society, 2009: 187-196.[5]COLLINS P. Continuity and computability of reachable sets [J]. Theoretical Computer Science, 2005, 341(1): 162-195.[6]ASARIN E, BOURNEZ O, DANG T, et al. Approximate reachability analysis of piecewise linear dynamical systems[C]// Hybrid Systems: Computation and Control, LNCS 1790. London: Springer, 2000: 21-31.[7]KURZHANSKIY A, VARAIYA P. Ellipsoidal techniques for reachability analysis of discrete-time linear systems[J]. IEEE Transactions on Automatic Control, 2007, 52(1): 26-38.[8]THOMAS S, ASHISH T. Verification and synthesis using real quantifier elimination[C]// The 36th International Symposium on Symbolic and Algebraic Computation. New York: ACM, 2011: 329-336.[9]COLAS L G, ANTOINE G. Reachability analysis of hybrid systems using support functions[C]// Proceedings of the 21th International Conference on Computer Aided Verification, LNCS 5643. Berlin: Springer, 2009: 540-554.[10]FREHSE G. PHAVer: algorithmic verification of hybrid systems past HyTech[J]. International Journal on Software Tools for Technology Transfer, 2008, 10(3): 263-279.[11]SILVA B, RICHESON K, KROGH B, et al. Modeling and verifying hybrid dynamic systems using CheckMate[C]// Proceedings of the 4th International Conference on Automation of Mixed Processes. Dortmund: Shaker, 2000: 323-328.[12]FREHSE G, GUERNIC C L, DONZE A, et al. SpaceEx: Scalable verification of hybrid systems[C]// Proceedings of the 23th International Conference on Computer Aided Verification, LNCS 6806. Berlin: Springer, 2011: 379-395.[13]EUGENE A, THAO D, ODED M. The d/dt tool for verification of hybrid systems[C]// Proceedings of the 14th International Conference on Computer Aided Verification, LNCS 2404. Berlin: Springer, 2002: 365-370.[14]EUGENE A, THAO D, ANTOINE G. Reachability analysis of nonlinear systems using conservative approximation[C]// Proceedings of the 6th ACM International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2003: 20-35.[15]ASARIN E, DANG T, GIRARD A. Hybridization methods for the analysis of nonlinear systems[J]. Acta Informatica, 2007, 43(7): 451-476.[16]DANG T, MALER O, TESTYLIER R. Accurate hybridization of nonlinear systems[C]// Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control. New York: ACM, 2010: 11-20.[17]HENZINGER T A, WONG-TOI H. Linear phase-portrait approximations for nonlinear hybrid systems[C]// Hybrid Systems Ⅲ: Verication and Control, LNCS 1066. Berlin: Springer, 1996: 377-388.[18]YANG L, ZHOU C, ZHAN N, et al. Recent advances in program verification through computer algebra[J]. Frontiers of Computer Science in China, 2010, 4(1): 1-16.[19]XIA B. DISCOVERER: A tool for solving semi-algebraic systems[J]. ACM Communications in Computer Algebra, 2007, 41(3): 102-103.[20]HONG H, EI DIN M S. Variant real quantifier elimination: algorithm and application[C]// Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation. New York: ACM, 2009: 183-190.[21]BROWN C W. QEPCAD B - a program for computing with semi-algebraic sets using CADs[J]. ACM SIGSAM Bulletin, 2003, 37(4): 97-108.[22]STURM T. REDLOG online resources for applied quantifier elimination[J]. Acta Academiae Aboensis, 2007, 67(2): 177-191.[23]RATSCHAN S, SHE Z. Safety verification of hybrid systems by constraint propagation-based abstraction refinement[J]. ACM Transactions on Embedded Computing Systems, 2007,6(1): Article No. 8. |