Top

Published in:

2017 | OriginalPaper | Chapter

Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems

Authors : Arvind Adimoolam, Thao Dang

Published in: Formal Modeling and Analysis of Timed Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Zonotopes are a useful set representation for bounded time reach set computation of affine hybrid systems because of their closure under Minkowski sum and matrix multiplication operations. For unbounded time reach set approximation of arbitrarily switched affine hybrid systems, template complex zonotopes and a corresponding invariant computation procedure were introduced, which utilized the possibly complex eigenstructure of the affine maps. But a major hurdle in extending the technique for computing invariants of more general affine hybrid systems, where switching is state dependent and controlled by linear constraints, is that the class of template complex zonotopes is not closed under intersection with linear constraints. In this paper, we use a more expressive set representation called augmented complex zonotopes, for which we propose an algebraic over-approximation of the intersection with linear constraints. This over-approximation is then used to derive a set of second order conic constraints for computing an augmented complex zonotopic positive invariant for discrete time affine hybrid systems with additive disturbance input and linear safety constraints. We demonstrate the efficiency of this approach by experimenting on some benchmark examples.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Optimal Control for Multi-mode Systems with Discrete Costs

next chapter Conic Abstractions for Hybrid Systems

http://cps-vo.org/node/15096.

Adimoolam, A., Dang, T.: Template complex zonotopes for stability and invariant computation. In: American Control Conference (ACC). IEEE (2017)

Adimoolam, A.S., Dang, T.: Using complex zonotopes for stability verification. In: American Control Conference (ACC), pp. 4269–4274. IEEE (2016)

Adjé, A.: Coupling policy iterations with piecewise quadratic lyapunov functions. In: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control (HSCC 2017), Pittsburgh, 18–20 April 2017, pp. 143–152 (2017)

Adjé, A., Garoche, P., Werey, A.: Quadratic zonotopes - an extension of zonotopes to quadratic arithmetics. In: Proceedings of the 13th Asian Symposium on Programming Languages and Systems (APLAS 2015), pp. 127–145 (2015)

Allamigeon, X., Gaubert, S., Goubault, É.: Inferring min and max invariants using max-plus polyhedra. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 189–204. Springer, Heidelberg (2008). doi:10.1007/978-3-540-69166-2_13 CrossRef

Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control (HSCC 2013), pp. 173–182 (2013)

Bagnara, R., Rodríguez-Carbonell, E., Zaffanella, E.: Generation of basic semi-algebraic invariants using convex polyhedra. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 19–34. Springer, Heidelberg (2005). doi:10.1007/11547662_4 CrossRef

Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. Form. Methods Syst. Des. 15(1), 75–92 (1999)CrossRef

Bouissou, O., Goubault, E., Putot, S., Tekkal, K., Vedrine, F.: HybridFluctuat: a static analyzer of numerical programs within a continuous environment. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 620–626. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_46 CrossRef

10.

Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_39 CrossRef

11.

Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Tucson, pp. 84–97 (1978)

12.

Dang, T., Gawlitza, T.M.: Template-based unbounded time verification of affine hybrid automata. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 34–49. Springer, Heidelberg (2011). doi:10.1007/978-3-642-25318-8_6 CrossRef

13.

Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_30 CrossRef

14.

Ghorbal, K., Goubault, E., Putot, S.: The zonotope abstract domain Taylor1+. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 627–633. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_47 CrossRef

15.

Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31954-2_19 CrossRef

16.

Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 1–3. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38856-9_1 CrossRef

17.

Heinz, T., Oehlerking, J., Woehrle, M.: Benchmark: reachability on a model with holes. In: ARCH@ CPSWeek, pp. 31–36 (2014)

18.

Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_52 CrossRef

19.

Kurzhanski, A., Varaiya, P.: Ellipsoidal techniques for reachability analysis: internal approximation. Syst. Control Lett. 41(3), 201–211 (2000)MathSciNetCrossRefMATH

20.

Maïga, M., Combastel, C., Ramdani, N., Travé-Massuyès, L.: Nonlinear hybrid reachability using set integration and zonotopic enclosures. In: European Control Conference (ECC 2014), Strasbourg, 24–27 June 2014, pp. 234–239 (2014)

21.

Makhlouf, I.B., Kowalewski, S.: Networked cooperative platoon of vehicles for testing methods and verification tools. In: ARCH@ CPSWeek, pp. 37–42 (2014)

22.

Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31–100 (2006)CrossRefMATH

23.

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). doi:10.1007/978-3-540-24743-2_32 CrossRef

24.

Rakovic, S., Grieder, P., Kvasnica, M., Mayne, D., Morari, M.: Computation of invariant sets for piecewise affine discrete time systems subject to bounded disturbances. In: 43rd IEEE Conference on Decision and Control (CDC 2004), vol. 2, pp. 1418–1423. IEEE (2004)

25.

Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007)MathSciNetCrossRefMATH

26.

Rodríguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 590–605. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31954-2_38 CrossRef

27.

Roux, P., Garoche, P.-L.: Computing quadratic invariants with min- and max-policy iterations: a practical comparison. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 563–578. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_38 CrossRef

28.

Roux, P., Jobredeaux, R., Garoche, P., Feron, E.: A generic ellipsoid abstract domain for linear time invariant systems. In: Hybrid Systems: Computation and Control (part of CPS Week 2012) (HSCC 2012), Beijing, 17–19 April 2012, pp. 105–114 (2012)

29.

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). doi:10.1007/978-3-540-78800-3_14 CrossRef

30.

Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 539–554. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_36 CrossRef

31.

Sassi, M.A.B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: 53rd IEEE Conference on Decision and Control (CDC 2014), Los Angeles, 15–17 December 2014, pp. 6348–6353 (2014)

32.

Scott, J.K., Raimondo, D.M., Marseglia, G.R., Braatz, R.D.: Constrained zonotopes: a new tool for set-based estimation and fault detection. Automatica 69, 126–136 (2016)MathSciNetCrossRefMATH

33.

Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 268–288. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_13 CrossRef

34.

Tiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001). doi:10.1007/3-540-45319-9_9 CrossRef

Title: Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems
Authors: Arvind Adimoolam
Thao Dang
Publisher: Springer International Publishing
Book: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-319-65764-6

Electronic ISBN: 978-3-319-65765-3

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-319-65765-3_6

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner