Computing Invariants for Hybrid Systems

Abstract:

This paper address the problem of generating invariants of hybrid systems. We present a new approach, for generating polynomial inequality invariants of hybrid systems through solving semi-algebraic systems and quantifier elimination. From the preliminary experiment results, we demonstrate the feasibility of our approach.

• Periodical: Applied Mechanics and Materials (Volumes 380-384)
• Pages: 556-561
• DOI: https://doi.org/10.4028/www.scientific.net/AMM.380-384.556
• Online since: August 2013
• Authors: Bin Wu, Xiao Guang Zou
• Keywords: Hybrid System, Invariant Generation, Program Verification, Semi-Algebraic Systems

References

[1] A. Tiwari, Approximate reachability for linear systems, " in HSCC, 2003: Hybrid Systems: Computation and Control, O. Maler and A. Pnueli, Eds., vol. 2623 of LNCS. Prague, The Czech Republic: Springer-Verlag, 2003, p.514–525.

DOI: 10.1007/3-540-36580-x

[2] N. Halbwachs, Y. erick Proy, and P. Roumanoff, Verification of real-time systems using linear relation analysis, Formal Methods in System Design, vol. 11, no. 2, p.157–185, (1997).

DOI: 10.1023/a:1008678014487

[3] S. Sankaranarayanan, H. Sipma, and Z. Manna, Constructing invariants for hybrid systems, " in HSCC, 2004: Hybrid Systems: Computation and Control, R. Alur and G. J. Pappas, Eds., vol. 2993 of LNCS. Philadelphia, PA, USA: Springer-Verlag, 2004, p.539.

DOI: 10.1007/978-3-540-24743-2_36

[4] E. Rodr´ıguez-Carbonell and A. Tiwari, Generating polynomial invariants for hybrid systems, " in HSCC, 2005: Hybrid Systems: Computation and Control, M. Morari and L. Thiele, Eds., vol. 3414 of LNCS. Zurich, Switzerland: Springer-Verlag, 2005, p.590.

DOI: 10.1007/978-3-540-31954-2_38

[5] S. Gulwani and A. Tiwari, Constraint-based approach for analysis of hybrid systems, " in CAV, 2008: 20th International Conference on Computer Aided Verification, A. Gupta and S. Malik, Eds., vol. 5123 of LNCS. Princeton, NJ, USA: Springer-Verlag, 2008, p.190.

DOI: 10.1007/978-3-540-70545-1

[6] A. Platzer and E. M. Clarke, Computing differential invariants of hybrid systems as fixedpoints, " in CAV, 2008: 20th International Conference on Computer Aided Verification, A. Gupta and S. Malik, Eds., vol. 5123 of LNCS. Princeton, NJ, USA: Springer-Verlag, 2008, p.176.

DOI: 10.1007/978-3-540-70545-1

[7] P. A. Parrilo, Semidefinite programming relaxations for semialgebraic problems, Mathematical Programming Series B, vol. 96, no. 2, p.293–320, (2003).

DOI: 10.1007/s10107-003-0387-5

[8] S. Prajna and A. Jadbabaie, Safety verification of hybrid systems using barrier certificates, " in HSCC, 2004: Hybrid Systems: Computation and Control, R. Alur and G. J. Pappas, Eds., vol. 2993 of LNCS. Philadelphia, PA, USA: Springer-Verlag, 2004, p.477.

DOI: 10.1007/978-3-540-24743-2_32

[9] B. Wu and Y. Fu, Generating invariants for hybrid systems by computing vanishing ideals of sample points, International Journal of Digital Content Technology & its Applic, vol. 6, no. 4, 2012, pp.252-269.

DOI: 10.4156/jdcta.vol6.issue4.31

[10] T. A. Henzinger, The theory of hybrid automata, " in LICS, 1996: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, 1996, p.278–292.

DOI: 10.1109/lics.1996.561342

[11] L. Yang, X. Hou, and B. Xia, A complete algorithm for automated discovering of a class of inequality-type theorems, Sci. China, (Ser. F. ), vol. 44, no. 1, 2001, p.33–49.

DOI: 10.1007/bf02713938

[12] L. Yang and B. Xia, Real solution classifications of a class of parametric semialgebraic systems, In Proc. of Intl Conf. on Algorithmic Algebra and Logic, 2005, p.281–289.

[13] C. Brown, QEPCAD B: A program for computing with semi-algebraic sets using CADs, ACM SIGSAM Bulletin, vol. 37, no. 4, 2003, pp.97-108.

DOI: 10.1145/968708.968710