Skip to main content
SpringerLink
Log in

Non-Standard Zeno-Free Simulation Semantics for Hybrid Dynamical Systems

  • Conference paper
  • First Online:
Verification and Evaluation of Computer and Communication Systems (VECoS 2019)

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

Abstract

Geometric-Zeno behavior is one of the most challenging problems in the analysis and simulation of hybrid systems. Geometric-Zeno solutions involve an accumulation of an infinite number of discrete events occurring in a finite amount of time. In models that exhibit geometric-Zeno, discrete events occur at an increasingly smaller distance in time, converging to a limit point according to a geometric series. In practice, simulating models of hybrid systems exhibiting geometric-Zeno is highly challenging, in that the simulation either halts or produces faulty results, as the time interval lengths are decreasing to arbitrary small positive numbers. Although many simulation tools for hybrid systems have been developed in the past years, none of them have a Zeno-free semantic model. All of them produce faulty results when simulating geometric-Zeno models. In this paper, we propose a non-standard Zeno-free mathematical formalism for detecting and eliminating geometric-Zeno during simulation. We derive sufficient conditions for the existence of geometric-Zeno behavior based on the existence of a non-standard contraction map in a complete metric space. We also provide methods for carrying solutions from pre-Zeno to post-Zeno. We illustrate the concepts with examples throughout the paper.

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

References

  1. https://www.mathworks.com/products/simulink.html

  2. https://openmodelica.org/

  3. https://ptolemy.berkeley.edu/hyvisual/

  4. http://www.scicos.org/

  5. http://www.acumen-language.org/

  6. http://zelus.di.ens.fr/

  7. DOMNA: a lite matlab simulator for zeno-free simulation of hybrid dynamical systems, with zeno detection and avoidance in run-time. https://bil.inria.fr/fr/software/view/2691/tab

  8. Sevama: A simulink toolbox and simulator for zeno-free simulation of hybrid dynamical systems, with zeno detection and avoidance in run-time. https://bil.inria.fr/fr/software/view/2679/tab

  9. Aljarbouh, A., Caillaudr, B.: Simulation for hybrid systems: chattering path avoidance. In: Proceedings of the 56th Conference on Simulation and Modelling (SIMS 56), Linkoping Electronic Conference Proceedings, vol. 119, pp. 175–185 (2015). https://doi.org/10.3384/ecp15119175

  10. Aljarbouh, A., Caillaudr, B.: Chattering-free simulation of hybrid dynamical systems with the functional mock-up interface 2.0. In: Proceedings of the First Japanese Modelica Conferences, Linkoping Electronic Conference Proceedings, vol. 124, pp. 95–105 (2016). https://doi.org/10.3384/ecp1612495

  11. Aljarbouh, A., Zeng, Y., Duracz, A., Caillaud, B., Taha, W.: Chattering-free simulation for hybrid dynamical systems semantics and prototype implementation. In: 2016 IEEE International Conference on Computational Science and Engineering (CSE) and IEEE International Conference on Embedded and Ubiquitous Computing (EUC) and 15th International Symposium on Distributed Computing and Applications for Business Engineering (DCABES), pp. 412–422, August 2016. https://doi.org/10.1109/CSE-EUC-DCABES.2016.217

  12. Aljarbouh, A., Caillaud, B.: On the regularization of chattering executions in real time simulation of hybrid systems. In: Cap, C. (ed.) Baltic Young Scientists Conference, p. 49. The 11th Baltic Young Scientists Conference, Universität Rostock, Tallinn, Estonia, July 2015. https://hal.archives-ouvertes.fr/hal-01246853

  13. Alur, R., et al.: Hybrid systems the algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3–34 (1995). https://doi.org/10.1016/0304-3975(94)00202-T. http://www.sciencedirect.com/science/article/pii/030439759400202T

    Article  MathSciNet  Google Scholar 

  14. Alur, R., Henzinger, T.A., Ho, P.H.: Automatic symbolic verification of embedded systems. IEEE Trans. Softw. Eng. 22(3), 181–201 (1996). https://doi.org/10.1109/32.489079

    Article  Google Scholar 

  15. Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 74–88. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63141-0_6

    Chapter  Google Scholar 

  16. Ames, A.D., Abate, A., Sastry, S.: Sufficient conditions for the existence of zeno behavior. In: Proceedings of the 44th IEEE Conference on Decision and Control, pp. 696–701, December 2005. https://doi.org/10.1109/CDC.2005.1582237

  17. Ames, A.D., Sastry, S.: Blowing up affine hybrid systems. In: 43rd IEEE Conference on Decision and Control, CDC, vol. 1, pp. 473–478, December 2004. https://doi.org/10.1109/CDC.2004.1428675

  18. Ames, A.D., Zheng, H., Gregg, R.D., Sastry, S.: Is there life after zeno? Taking executions past the breaking (zeno) point. In: 2006 American Control Conference, 6 pp., June 2006. https://doi.org/10.1109/ACC.2006.1656623

  19. Antsaklis, P.J.: Special issue on hybrid systems: theory and applications a brief introduction to the theory and applications of hybrid systems. Proc. IEEE 88(7), 879–887 (2000). https://doi.org/10.1109/JPROC.2000.871299

    Article  Google Scholar 

  20. Benveniste, A., Bourke, T., Caillaud, B., Pouzet, M.: Non-standard semantics of hybrid systems modelers. J. Comput. Syst. Sci. 78(3), 877–910 (2012). http://www.sciencedirect.com/science/article/pii/S0022000011001061. In Commemoration of Amir Pnueli

    Article  MathSciNet  Google Scholar 

  21. Bourke, T., Pouzet, M.: Zélus: a synchronous language with ODEs. In: Belta, C., Ivančić, F. (eds.) HSCC - Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 113–118, Calin Belta and Franjo Ivančić. ACM, Philadelphia, April 2013. https://doi.org/10.1145/2461328.2461348. https://hal.inria.fr/hal-00909029

  22. Cai, C., Goebel, R., Sanfelice, R.G., Teel, A.R.: Hybrid systems: limit sets and zero dynamics with a view toward output regulation. In: Astolfi, A., Marconi, L. (eds.) Analysis and Design of Nonlinear Control Systems, pp. 241–261. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74358-3_15

    Chapter  MATH  Google Scholar 

  23. Camlibel, M.K., Schumacher, J.M.: On the zeno behavior of linear complementarity systems. In: Proceedings of the 40th IEEE Conference on Decision and Control, vol. 124, pp. 346–351 (2001). https://doi.org/10.1109/.2001.980124

  24. Egerstedt, M., Johansson, K.H., Sastry, S., Lygeros, J.: On the regularization of Zeno hybrid automata. Syst. Control. Lett. 38, 141–150 (1999). https://control.ee.ethz.ch/index.cgi?page=publications;action=details;id=2985

  25. Eker, J., Janneck, J.W., Lee, E.A., Ludvig, J., Neuendorffer, S., Sachs, S.: Taming heterogeneity - the ptolemy approach. Proc. IEEE 91(1), 127–144 (2003). https://doi.org/10.1109/JPROC.2002.805829

    Article  Google Scholar 

  26. 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). https://doi.org/10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  27. Fritzson, P.: Introduction to Modeling and Simulation of Technical and Physical Systems with Modelica. Wiley-IEEE Press, Hoboken (2011)

    Book  Google Scholar 

  28. Goebel, R., Teel, A.R.: Lyapunov characterization of zeno behavior in hybrid systems. In: 47th IEEE Conference on Decision and Control, CDC 2008, pp. 2752–2757, December 2008. https://doi.org/10.1109/CDC.2008.4738864

  29. Goldblatt, R.: Lecture on the Hyperreals: An Introduction to Nonstandard Analysis. Springer, Heidelberg (1988)

    MATH  Google Scholar 

  30. Johansson, K.H., Lygeros, J., Sastry, S., Egerstedt, M.: Simulation of zeno hybrid automata. In: Proceedings of the 38th IEEE Conference on Decision and Control, vol. 4, pp. 3538–3543 (1999). https://doi.org/10.1109/CDC.1999.827900

  31. Lamperski, A., Ames, A.D.: Lyapunov-like conditions for the existence of zeno behavior in hybrid and Lagrangian hybrid systems. In: 2007 46th IEEE Conference on Decision and Control, pp. 115–120, December 2007. https://doi.org/10.1109/CDC.2007.4435003

  32. Lamperski, A., Ames, A.D.: On the existence of zeno behavior in hybrid systems with non-isolated zeno equilibria. In: 47th IEEE Conference on Decision and Control, CDC 2008, pp. 2776–2781, December 2008. https://doi.org/10.1109/CDC.2008.4739100

  33. Lamperski, A., Ames, A.D.: Lyapunov theory for zeno stability. IEEE Trans. Autom. Control 58(1), 100–112 (2013). https://doi.org/10.1109/TAC.2012.2208292

    Article  MathSciNet  MATH  Google Scholar 

  34. Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 25–53. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31954-2_2

    Chapter  Google Scholar 

  35. Lygeros, J., Tomlin, C., Sastry, S.: Hybrid systems: modeling, analysis and control. Lecture Notes on Hybrid Systems (2008). http://www-inst.cs.berkeley.edu/~ee291e/sp09/handouts/book.pdf

  36. Shen, J., Pang, J.S.: Linear complementarity systems: zeno states. SIAM J. Control Optim. 44(3), 1040–1066 (2005). https://doi.org/10.1137/040612270, http://dx.doi.org/10.1137/040612270

    Article  MathSciNet  Google Scholar 

  37. Thuan, L.Q.: Non-zenoness of piecewise affine dynamical systems and affine complementarity systems with inputs. Control Theory Technol. 12(1), 35–47 (2014). https://doi.org/10.1007/s11768-014-0074-5. http://dx.doi.org/10.1007/s11768-014-0074-5

    Article  MathSciNet  Google Scholar 

Download references

Acknowledgements

This work is supported by the European project ITEA3 MODRIO under contract No 6892, and the Grant ARED of Brittany Regional Council.

Author information

Authors and Affiliations

  1. Gipsa-lab, Grenoble INP, University of Grenoble Alpes, Grenoble, France

    Ayman Aljarbouh

Authors
  1. Ayman Aljarbouh
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ayman Aljarbouh .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute, Pozuelo de Alarcón, Spain

    Pierre Ganty

  2. Laboratory for Analysis and Architecture, Toulouse, France

    Mohamed Kaâniche

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Aljarbouh, A. (2019). Non-Standard Zeno-Free Simulation Semantics for Hybrid Dynamical Systems. In: Ganty, P., Kaâniche, M. (eds) Verification and Evaluation of Computer and Communication Systems. VECoS 2019. Lecture Notes in Computer Science(), vol 11847. Springer, Cham. https://doi.org/10.1007/978-3-030-35092-5_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-35092-5_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-35091-8

  • Online ISBN: 978-3-030-35092-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation