Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point. (English) Zbl 1336.93085

Summary: Even simple hybrid automata like the classic bouncing ball can exhibit Zeno behavior. The existence of this type of behavior has so far forced a large class of simulators to either ignore some events or risk looping indefinitely. This in turn forces modelers to either insert ad-hoc restrictions to circumvent Zeno behavior or to abandon hybrid automata. To address this problem, we take a fresh look at event detection and localization. A key insight that emerges from this investigation is that an enclosure for a given time interval can be valid independent of the occurrence of a given event. Such an event can then even occur an unbounded number of times. This insight makes it possible to handle some types of Zeno behavior. If the post-Zeno state is defined explicitly in the given model of the hybrid automaton, the computed enclosure covers the corresponding trajectory that starts from the Zeno point through a restarted evolution.


93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
93B40 Computational methods in systems theory (MSC2010)
37N35 Dynamical systems in control
Full Text: DOI


[1] Darulova, E.; Kuncak, V., Trustworthy numerical computation in scala, (Lopes, C. V.; Fisher, K., OOPSLA, (2011), ACM), 325-344
[2] Escardó, M. H., PCF extended with real numbers, Theoret. Comput. Sci., 162, 1, 79-115, (1996) · Zbl 0871.68034
[3] Cellier, F. E.; Kofman, E., Continuous system simulation, (2006), Springer-Verlag New York, Inc. Secaucus, NJ, USA · Zbl 1112.93004
[4] Hairer, E.; Nørsett, S. P.; Wanner, G., Solving ordinary differential equations I (2nd revised. ed.): nonstiff problems, (1993), Springer-Verlag New York, Inc. New York, NY, USA · Zbl 0789.65048
[5] Hairer, E.; Wanner, G., Stiff and differential-algebraic problems, (Solving Ordinary Differential Equations. II, Springer Series in Computational Mathematics, vol. 14, (1996), Springer-Verlag Berlin) · Zbl 0859.65067
[6] F. Zhang, M. Yeddanapudi, P. Mosterman, Zero-crossing location and detection algorithms for hybrid system simulation, in: IFAC World Congress, 2008, pp. 7967-7972.
[7] A. Ames, H. Zheng, R. Gregg, S. Sastry, Is there life after Zeno? Taking executions past the breaking (Zeno) point, in: 25th American Control Conference, 2006, Minneapolis, MN, 2006, pp. 2652-2657.
[8] K. Johansson, J. Lygeros, S. Sastry, M. Egerstedt, Simulation of zeno hybrid automata, in: Proceedings of the 38th IEEE Conference on Decision and Control, 1999. Vol. 4, 1999, pp. 3538-3543. · Zbl 0948.93031
[9] Zhang, J.; Johansson, K. H.; Lygeros, J.; Sastry, S., Zeno hybrid systems, Internat. J. Robust Nonlinear Control, 11, 5, 435-451, (2001) · Zbl 0977.93047
[10] M. Konečný, W. Taha, J. Duracz, A. Duracz, A. Ames, Enclosing the behavior of a hybrid system up to and beyond a zeno point, in: 2013 IEEE 1st International Conference on Cyber-Physical Systems, Networks, and Applications, CPSNA, 2013, pp. 120-125. · Zbl 1336.93085
[11] Moreau, J., Unilateral contact and dry friction in finite freedom dynamics, (Moreau, J.; Panagiotopoulos, P., Nonsmooth Mechanics and Applications, International Centre for Mechanical Sciences, vol. 302, (1988), Springer Vienna), 1-82 · Zbl 0703.73070
[12] Marques, Manuel Duque Pereira Monteiro, Differential inclusions in nonsmooth mechanical problems: shocks and dry friction, (1993), Birkhäuser Boston, MA · Zbl 0802.73003
[13] Stewart, D. E., A dynamics with inequalities: impacts and hard constraints, (2011), Society for Industrial and Applied Mathematics Philadelphia, PA, USA · Zbl 1241.37003
[14] Schumacher, J. M., Time-scaling symmetry and Zeno solutions, Automatica J. IFAC, 45, 5, 1237-1242, (2009) · Zbl 1173.37026
[15] Shen, J.; Pang, J.-S., Linear complementarity systems: Zeno states, SIAM J. Control Optim., 44, 3, 1040-1066, (2005), (electronic) · Zbl 1092.90052
[16] Thuan, L. Q.; Camlibel, M. K., Continuous piecewise affine dynamical systems do not exhibit Zeno behavior, IEEE Trans. Automat. Control, 56, 8, 1932-1936, (2011) · Zbl 1368.93284
[17] Acary, V.; Brogliato, B., Numerical methods for nonsmooth dynamical systems: applications in mechanics and electronics, vol. 35, (2008), Springer Science & Business Media · Zbl 1173.74001
[18] Ames, A. D., Characterizing knee-bounce in bipedal robotic walking: A Zeno behavior approach, (Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC’11, (2011), ACM New York, NY, USA), 163-172 · Zbl 1364.70016
[19] Or, Y.; Teel, A., Zeno stability of the set-valued bouncing ball, IEEE Trans. Automat. Control, 56, 2, 447-452, (2011) · Zbl 1368.93606
[20] Lamperski, A.; Ames, A. D., On the existence of Zeno behavior in hybrid systems with non-isolated Zeno equilibria, (47th IEEE Conference on Decision and Control, 2008, (2008), IEEE), 2776-2781
[21] Or, Y.; Ames, A., Stability and completion of Zeno equilibria in Lagrangian hybrid systems, IEEE Trans. Automat. Control, 56, 6, 1322-1336, (2011) · Zbl 1368.93476
[22] H. Zheng, E.A. Lee, A.D. Ames, Beyond zeno: Get on with it!, in: Hybrid Systems: Computation and Control, 9th International Workshop, HSCC 2006, Santa Barbara, CA, USA, 2006, pp. 568-582. · Zbl 1178.93079
[23] Carloni, L. P.; Passerone, R.; Pinto, A.; Angiovanni-Vincentelli, A. L., Languages and tools for hybrid systems design, Found. Trends Electron. Des. Autom., 1, 1-2, 1-193, (2006)
[24] Wolfram, SystemModeler, 2012. http://wolfram.com/system-modeler.
[25] P. Fritzson, P. Aronsson, A. Pop, H. Lundvall, K. Nystrom, L. Saldamli, D. Broman, A. Sandholm, OpenModelica—A free open-source environment for system modeling, simulation, and teaching, in: Computer Aided Control System Design, 2006 IEEE International Conference on Control Applications, 2006 IEEE International Symposium on Intelligent Control, 2006, pp. 1588-1595.
[26] Alur, R.; Grosu, R.; Hur, Y.; Kumar, V.; Lee, I., Modular specification of hybrid systems in CHARON, (Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 1790, (2000), Springer), 6-19 · Zbl 0992.93040
[27] Z. Wan, P. Hudak, Functional reactive programming from first principles, in: ACM SIGPLAN Conference on Programming Language Design and Implementation, 2000, pp. 242-252.
[28] Nilsson, H.; Courtney, A.; Peterson, J., Functional reactive programming, continued, (Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell’02, (2002), ACM New York, NY, USA), 51-64
[29] Makino, K.; Berz, M., New applications of Taylor model methods, (Automatic Differentiation of Algorithms: From Simulation to Optimization, (2002), Springer), 359-364, (Chapter 43)
[30] N. Nedialkov, M. von Mohrenschildt, Rigorous simulation of hybrid dynamic systems with symbolic and interval methods, in: Proceedings of the 2002 American Control Conference, Vol. 1, 2002, pp. 140-147.
[31] A. Rauh, E. Hofer, E. Auer, ValEncIA-IVP: A comparison with other initial value problem solvers, in: Scientific Computing, Computer Arithmetic and Validated Numerics, 2006. SCAN 2006. 12th GAMM—IMACS International Symposium on, 2006, pp. 36-36.
[32] J. Lygeros, Lecture notes on hybrid systems, in: Notes for an ENSIETA Workshop, 2004.
[33] Brogliato, B., Nonsmooth mechanics, communications and control engineering, (1999), Springer Verlag London
[34] Moreau, J. J., Numerical aspects of the sweeping process, Comput. Methods Appl. Mech. Engrg., 177, 3, 329-349, (1999) · Zbl 0968.70006
[35] Acary, V.; Pérignon, F., Siconos: A software platform for modeling, simulation, analysis and control of nonsmooth dynamical systems, Simul. News Europe, 17, 3-4, 19-26, (2007)
[36] Acary, V.; Brogliato, B.; Goeleven, D., Higher order moreau’s sweeping process: mathematical formulation and numerical simulation, Math. Program., 113, 1, 133-217, (2008) · Zbl 1148.93003
[37] A. Ames, A. Abate, S. Sastry, Sufficient conditions for the existence of Zeno behavior in a class of nonlinear hybrid systems via constant approximations, in: 46th IEEE Conference on Decision and Control, 2007, pp. 4033-4038.
[38] Lamperski, A.; Ames, A., Lyapunov theory for Zeno stability, IEEE Trans. Automat. Control, 58, 1, 100-112, (2013) · Zbl 1369.93534
[39] Alur, R.; Dill, D. L., A theory of timed automata, Theoret. Comput. Sci., 126, 2, 183-235, (1994) · Zbl 0803.68071
[40] Henzinger, T. A., The theory of hybrid automata, (LICS, (1996), IEEE Computer Society), 278-292
[41] Platzer, A., Differential dynamic logic for hybrid systems, J. Automat. Reason., 41, 2, 143-189, (2008) · Zbl 1181.03035
[42] Platzer, A.; Quesel, J.-D., Keymaera: A hybrid theorem prover for hybrid systems, (Armando, A.; Baumgartner, P.; Dowek, G., IJCAR, LNCS, vol. 5195, (2008), Springer), 171-178 · Zbl 1165.68469
[43] Ishii, D.; Ueda, K.; Hosobe, H., An interval-based sat modulo ODE solver for model checking nonlinear hybrid systems, Int. J. Softw. Tools Technol. Trans., 13, 5, 449-461, (2011)
[44] Ishii, D., Simulation and verification of hybrid systems based on interval analysis and constraint programming, (2010), Waseda University, (Ph.D. thesis)
[45] N.S. Nedialkov, VNODE-LP—A validated solver for initial value problems in ordinary differential equations, Department of Computing and Software, McMaster University, Hamilton, Ontario, Canada, L8S 4K1, Technical Report CAS-06-06-NN, November 2006. Retrieved from: http://www.cas.mcmaster.ca/ nedialk/vnodelp.
[46] Chen, X.; Abrahám, E.; Sankaranarayanan, S., Taylor model flowpipe construction for non-linear hybrid systems, (Real-Time Systems Symposium (RTSS), 2012 IEEE 33rd, (2012), IEEE), 183-192
[47] Frehse, G.; Le Guernic, C.; Donzé, A.; Cotton, S.; Ray, R.; Lebeltel, O.; Ripado, R.; Girard, A.; Dang, T.; Maler, O., Spaceex: scalable verification of hybrid systems, (Gopalakrishnan, G.; Qadeer, S., Computer Aided Verification, Lecture Notes in Computer Science, vol. 6806, (2011), Springer Berlin, Heidelberg), 379-395
[48] Guernic, C. L.; Girard, A., Reachability analysis of linear systems using support functions, Nonlinear Anal. Hybrid Syst., 4, 2, 250-262, (2010) · Zbl 1201.93018
[49] Lee, E.; Zheng, H., Operational semantics of hybrid systems, (Morari, M.; Thiele, L., Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 3414, (2005), Springer Berlin, Heidelberg), 25-53 · Zbl 1078.93535
[50] Edalat, A.; Pattinson, D., Denotational semantics of hybrid automata, (Aceto, L.; Ingólfsdóttir, A., Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 3921, (2006), Springer Berlin, Heidelberg), 231-245 · Zbl 1168.68417
[51] Bouissou, O.; Martel, M., A hybrid denotational semantics for hybrid systems, (Drossopoulou, S., Programming Languages and Systems, Lecture Notes in Computer Science, vol. 4960, (2008), Springer Berlin, Heidelberg), 63-77 · Zbl 1133.68369
[52] Schrammel, P.; Jeannet, B., From hybrid data-flow languages to hybrid automata: A complete translation, (Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, (2012), ACM), 167-176 · Zbl 1362.68184
[53] Benveniste, A.; Caillaud, B.; Pouzet, M., The fundamentals of hybrid systems modelers, (2010 49th IEEE Conference on Decision and Control (CDC), (2010), IEEE), 4180-4185
[54] Bliudze, S.; Furic, S., An operational semantics for hybrid systems involving behavioral abstraction, (Proceedings of the 10th International Modelica Conference, Linköping Electronic Conference Proceedings, (2014), Linköping University Electronic Press Linköping), 693-706
[55] Bliudze, S.; Krob, D., Modelling of complex systems: systems as dataflow machines, Fund. Inform., 91, 2, 251-274, (2009) · Zbl 1176.68081
[56] Suenaga, K.; Sekine, H.; Hasuo, I., Hyperstream processing systems: nonstandard modeling of continuous-time signals, (ACM SIGPLAN Notices, Vol. 48, (2013), ACM), 417-430 · Zbl 1301.68105
[57] Moore, R. E., Interval analysis, vol. 4, (1966), Prentice-Hall Englewood Cliffs · Zbl 0176.13301
[58] Jaulin, L., Applied interval analysis: with examples in parameter and state estimation, robust control and robotics, vol. 1, (2001), Springer Science & Business Media
[59] Moore, R. E.; Kearfott, R. B.; Cloud, M. J., Introduction to interval analysis, (2009), Society for Industrial and Applied Mathematics Philadelphia, PA, USA · Zbl 1168.65002
[60] Tucker, W., Validated numerics, A short introduction to rigorous computations, (2011), Princeton University Press Princeton, NJ · Zbl 1231.65077
[61] A. Ames, S. Sastry, Characterization of Zeno behavior in hybrid systems using homological methods, in: Proceedings of the American Control Conference, Vol. 2, 2005, pp. 1160-1165.
[62] Frehse, G.; Le Guernic, C.; Donze, A.; Cotton, S.; Ray, R.; Lebeltel, O.; Ripado, R.; Girard, A.; Dang, T.; Maler, O., Spaceex: scalable verification of hybrid systems, (Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 6806, (2011), Springer Heidelberg), 379-395
[63] Althoff, M.; Krogh, B. H., Avoiding geometric intersection operations in reachability analysis of hybrid systems, (Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC’12, (2012), ACM New York, NY, USA), 45-54 · Zbl 1362.93012
[64] Chen, X.; Abraham, E.; Sankaranarayanan, S., Taylor model flowpipe construction for non-linear hybrid systems, (Proceedings of the 2012 IEEE 33rd Real-Time Systems Symposium, RTSS’12, (2012), IEEE Computer Society Washington, DC, USA), 183-192
[65] Ramdani, N.; Nedialkov, N. S., Computing reachable sets for uncertain nonlinear hybrid systems using interval constraint-propagation techniques, Nonlinear Anal. Hybrid Syst., 5, 2, 149-162, (2011) · Zbl 1225.93026
[66] N. Ramdani, L. Trave-Massuyes, A fast method for solving guard set intersection in nonlinear hybrid reachability, Decision and Control, CDC, IEEE, 2013, pp. 508-513.
[67] Makino, K.; Berz, M., Cosy infinity version 9, Nucl. Instrum. Methods Phys. Res. A, 558, 1, 346-350, (2006)
[68] Edalat, A.; Pattinson, D., A domain-theoretic account of picard’s theorem, LMS J. Comput. Math., 10, 83-118, (2007) · Zbl 1112.65065
[69] M. Konečný, J. Duracz, A. Farjudian, W. Taha, Picard method for enclosing ODEs with uncertain initial values, in: 11th International Conference on Computability and Complexity in Analysis, Darmstadt, Germany, 2014, pp. 41-42.
[70] M. Konečný, A Library for Approximating Exact Real Numbers and Functions (AERN), A branch dedicated to experiments reported in this paper, https://github.com/michalkonecny/aern/tree/nahs2015-plots.
[71] Or, Y.; Ames, A. D., Stability and completion of Zeno equilibria in Lagrangian hybrid systems, IEEE Trans. Automat. Control, 56, 1322-1336, (2011) · Zbl 1368.93476
[72] Asarin, E.; Dang, T.; Maler, O.; Testylier, R., Using redundant constraints for refinement, (Automated Technology for Verification and Analysis, (2010), Springer), 37-51 · Zbl 1305.68117
[73] Carlson, B.; Gupta, V., Hybrid CC and interval constraints, (Henzinger, T. A.; Sastry, S., Hybrid Systems 98: Computation and Control, Lecture notes in computer science, vol. 1386, (1998), Springer Verlag), 80-94
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.