Skip to main content
SpringerLink
Log in

Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10419))

  • 482 Accesses

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.

This research work is partially supported by ANR project MALTHY.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

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

References

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

    Google Scholar 

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

    Google Scholar 

  3. 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)

    Google Scholar 

  4. 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)

    Google Scholar 

  5. 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

    Chapter  Google Scholar 

  6. 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)

    Google Scholar 

  7. 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

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  9. 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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

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

    Google Scholar 

  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

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Google Scholar 

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

    Google Scholar 

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

    Article  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verimag, Grenoble, France

    Arvind Adimoolam & Thao Dang

Authors
  1. Arvind Adimoolam
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Thao Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Arvind Adimoolam .

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, United Kingdom

    Alessandro Abate

  2. Dept. d’Informatique, Université Libre de Bruxelles, Brussels, Belgium

    Gilles Geeraerts

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Adimoolam, A., Dang, T. (2017). Augmented Complex Zonotopes for Computing Invariants of Affine Hybrid Systems. In: Abate, A., Geeraerts, G. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2017. Lecture Notes in Computer Science(), vol 10419. Springer, Cham. https://doi.org/10.1007/978-3-319-65765-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-65765-3_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-65764-6

  • Online ISBN: 978-3-319-65765-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation