×

Synthesizing switching controllers for hybrid systems by generating invariants. (English) Zbl 1390.68316

Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 354-373 (2013).
Summary: We extend a template-based approach for synthesizing switching controllers for semi-algebraic hybrid systems, in which all expressions are polynomials. This is achieved by combining a QE (quantifier elimination)-based method for generating invariants with a qualitative approach for predefining templates. Our synthesis method is relatively complete with regard to a given family of predefined templates. Using qualitative analysis, we discuss heuristics to reduce the numbers of parameters appearing in the templates. To avoid too much human interaction in choosing templates as well as the high computational complexity caused by QE, we further investigate applications of the SOS (sum-of-squares) relaxation approach and the template polyhedra approach in invariant generation, which are both supported by modern numerical solvers.
For the entire collection see [Zbl 1269.68023].

MSC:

68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q25 Analysis of algorithms and problem complexity
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Alur, R.: Formal verification of hybrid systems. In: EMSOFT 2011, pp. 273–278. ACM (2011)
[2] Alur, R., Couroubetis, C., Henzinger, T., Ho, P.H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)
[3] Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995) · Zbl 0874.68206
[4] Asarin, E., Bournez, O., Dang, T., Maler, O., Pnueli, A.: Effective synthesis of switching controllers for linear systems. Proc. of the IEEE 88(7), 1011–1025 (2000)
[5] Blanchini, F.: Set invariance in control. Automatica 35(11), 1747–1767 (1999) · Zbl 0935.93005
[6] Brown, C.W.: QEPCAD B: A program for computing with semi-algebraic sets using CADs. SIGSAM Bulletin 37, 97–108 (2003) · Zbl 1083.68148
[7] Castelan, E., Hennet, J.: On invariant polyhedra of continuous-time linear systems. IEEE Trans. Autom. Control 38(11), 1680–1685 (1993) · Zbl 0790.93099
[8] Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 1–24. Springer, Heidelberg (2005) · Zbl 1111.68503
[9] Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1-2), 29–35 (1988) · Zbl 0663.03015
[10] Dolzmann, A., Seidl, A., Sturm, T.: Redlog User Manual (November 2006), http://redlog.dolzmann.de/downloads/ , edition 3.1, for redlog Version 3.06 (reduce 3.8)
[11] Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008) · Zbl 1155.68437
[12] Ho, P.H.: The algorithmic analysis of hybrid systems. Ph.D. thesis, Cornell University (1995) · Zbl 0874.68206
[13] Holmström, K., Göran, A.O., Edvall, M.M.: User’s Guide for TOMLAB/PENOPT. Tomlab Optimization (November 2006), http://tomopt.com/docs/TOMLAB_PENOPT.pdf
[14] Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Synthesizing switching logic for safety and dwell-time requirements. In: ICCPS 2010, pp. 22–31. ACM (2010)
[15] Kapur, D.: A quantifier-elimination based heuristic for automatically generating inductive assertions for programs. Journal of Systems Science and Complexity 19(3), 307–330 (2006) · Zbl 1115.68051
[16] Kapur, D.: Automatically Generating Loop Invariants Using Quantifier Elimination. Technical Report, Department of Computer Science, University of New Mexico, Albuquerque, USA (December 2003)
[17] Kapur, D., Shyamasundar, R.K.: Synthesizing controllers for hybrid systems. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 361–375. Springer, Heidelberg (1997)
[18] Kapur, D., Zhan, N., Zhao, H.: Synthesizing switching controllers for hybrid systems by continuous invariant generation. CoRR abs/1304.0825 (2013), http://arxiv.org/abs/1304.0825
[19] Kočvara, M., Stingl, M.: PENBMI User’s Guide (Version 2.1). PENOPT GbR (March 2006), http://www.penopt.com/doc/penbmi2_1.pdf
[20] Lin, W., Wu, M., Yang, Z., Zeng, Z.: Exact safety verification of hybrid systems using sums-of-squares representation. CoRR abs/1112.2328 (2011), http://arxiv.org/abs/1112.2328 · Zbl 1343.93051
[21] Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010) · Zbl 05825349
[22] Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: EMSOFT 2011, pp. 97–106. ACM (2011)
[23] Liu, J., Zhan, N., Zhao, H.: Automatically discovering relaxed Lyapunov functions for polynomial dynamical systems. Mathematics in Computer Science 6(4), 395–408 (2012) · Zbl 1261.93063
[24] Löfberg, J.: YALMIP: A toolbox for modeling and optimization in MATLAB. In: Proc. of the CACSD Conference, Taipei, Taiwan (2004), http://users.isy.liu.se/johanl/yalmip
[25] Löfberg, J.: Pre- and post-processing sum-of-squares programs in practice. IEEE Trans. Autom. Control 54(5), 1007–1011 (2009) · Zbl 1367.90002
[26] Parrilo, P.A.: Structured Semidefinite Programs and Semialgebraic Geometry Methods in Robustness and Optimization. Ph.D. thesis, California Institute of Technology, Pasadena, CA (May 2000), http://thesis.library.caltech.edu/1647/
[27] Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. and Comput. 20(1), 309–352 (2010) · Zbl 1191.03024
[28] Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176–189. Springer, Heidelberg (2008) · Zbl 1155.68445
[29] Platzer, A.: A differential operator approach to equational differential invariants. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 28–48. Springer, Heidelberg (2012) · Zbl 1360.68596
[30] Platzer, A.: The structure of differential invariants and differential cut elimination. Logical Methods in Computer Science 8(4), 1–38 (2012) · Zbl 1261.03112
[31] Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004) · Zbl 1135.93317
[32] Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Trans. Autom. Control 52(8), 1415–1428 (2007) · Zbl 1366.93711
[33] Prajna, S., Papachristodoulou, A., Seiler, P., Parrilo, P.: SOSTOOLS and its control applications. In: Henrion, D., Garulli, A. (eds.) Positive Polynomials in Control. LNCIS, vol. 312, pp. 273–292. Springer, Heidelberg (2005) · Zbl 1119.93302
[34] Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: POPL 2004 (2004) · Zbl 1325.68071
[35] Sankaranarayanan, S., Dang, T., Ivančić, F.: A policy iteration technique for time elapse over template polyhedra. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 654–657. Springer, Heidelberg (2008) · Zbl 1144.93327
[36] Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008) · Zbl 1134.68419
[37] Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005) · Zbl 1111.68514
[38] Sassi, M.A.B., Girard, A.: Computation of polytopic invariants for polynomial dynamical systems using linear programming. Automatica 48(12), 3114–3121 (2012) · Zbl 1256.93040
[39] Sturm, J.F.: Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization Methods and Software 11-12, 625–653 (1999) · Zbl 0973.90526
[40] Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: ISSAC 2011, pp. 329–336. ACM (2011) · Zbl 1323.68385
[41] Taly, A., Gulwani, S., Tiwari, A.: Synthesizing switching logic using constraint solving. International Journal on Software Tools for Technology Transfer 13, 519–535 (2011) · Zbl 1206.68191
[42] Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: FSTTCS 2009. LIPIcs, vol. 4, pp. 383–394 (2009) · Zbl 1248.68336
[43] Taly, A., Tiwari, A.: Switching logic synthesis for reachability. In: EMSOFT 2010, pp. 19–28. ACM (2010)
[44] Tarski, A.: A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley (1951) · Zbl 0044.25102
[45] Tomlin, C.J., Lygeros, J., Sastry, S.S.: A game theoretic approach to controller design for hybrid systems. Proc. of the IEEE 88(7), 949–970 (2000)
[46] VanAntwerp, J.G., Braatz, R.D.: A tutorial on linear and bilinear matrix inequalities. Journal of Process Control 10(4), 363–385 (2000)
[47] Vandenberghe, L., Boyd, S.: Semidefinite programming. SIAM Review 38(1), 49–95 (1996) · Zbl 0845.65023
[48] Yang, Z., Wu, M., Lin, W.: Exact safety verification of hybrid systems based on bilinear SOS representation. CoRR abs/1201.4219 (2012), http://arxiv.org/abs/1201.4219
[49] Zhao, H., Zhan, N., Kapur, D., Larsen, K.G.: A ”hybrid” approach for synthesizing optimal controllers of hybrid systems: A case study of the oil pump industrial example. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 471–485. Springer, Heidelberg (2012) · Zbl 1373.93125
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.