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.
MSC:
| 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 |
Software:
Charon; OpenModelica; SystemModeler; GitHub; KeYmaera; VNODE; ValEncIA-IVP; Haskell; Cosy; ValEncIA; SpaceExReferences:
| [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.: 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.: 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. Solving Ordinary Differential Equations. II, Springer Series in Computational Mathematics, vol. 14 (1996), Springer-Verlag: Springer-Verlag Berlin) · Zbl 0859.65067 |
| [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 |
| [11] | Moreau, J., Unilateral contact and dry friction in finite freedom dynamics, (Moreau, J.; Panagiotopoulos, P., Nonsmooth Mechanics and Applications. 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: 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: 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. Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC’11 (2011), ACM: 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 |
| [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) · Zbl 1107.68385 |
| [26] | Alur, R.; Grosu, R.; Hur, Y.; Kumar, V.; Lee, I., Modular specification of hybrid systems in CHARON, (Hybrid Systems: Computation and Control. Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 1790 (2000), Springer), 6-19 · Zbl 0992.93040 |
| [28] | Nilsson, H.; Courtney, A.; Peterson, J., Functional reactive programming, continued, (Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell. Proceedings of the 2002 ACM SIGPLAN Workshop on Haskell, Haskell’02 (2002), ACM: 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) |
| [33] | Brogliato, B., Nonsmooth Mechanics, Communications and Control Engineering (1999), Springer Verlag: Springer Verlag London · Zbl 0917.73002 |
| [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 |
| [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. 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) |
| [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. Computer Aided Verification, Lecture Notes in Computer Science, vol. 6806 (2011), Springer: 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. Hybrid Systems: Computation and Control, Lecture Notes in Computer Science, vol. 3414 (2005), Springer: 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. Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science, vol. 3921 (2006), Springer: 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. Programming Languages and Systems, Lecture Notes in Computer Science, vol. 4960 (2008), Springer: 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 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: 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 · Zbl 1023.65037 |
| [59] | Moore, R. E.; Kearfott, R. B.; Cloud, M. J., Introduction to Interval Analysis (2009), Society for Industrial and Applied Mathematics: 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 University Press Princeton, NJ · Zbl 1231.65077 |
| [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. Computer Aided Verification, Lecture Notes in Comput. Sci., vol. 6806 (2011), Springer: 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. Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC’12 (2012), ACM: 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. Proceedings of the 2012 IEEE 33rd Real-Time Systems Symposium, RTSS’12 (2012), IEEE Computer Society: 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 |
| [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 |
| [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. 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. 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.
