Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties. (English) Zbl 1485.93277

Summary: What if we designed a tool to automatically generate a dynamical transition system for the formal specification of mechanical systems subject to multiple impacts, contacts and discontinuous friction? Such a tool would represent an advance in the description and simulation of these complex systems. This is precisely what this paper offers: Dyverse Rigid Body Toolbox (DyverseRBT). This tool requires a sufficiently expressive computational model that can accurately describe the behaviour of the system as it evolves over time. For this purpose, we propose an alternative abstraction of multi-rigid-body (MRB) mechanical systems with multiple contacts as an extended version of the classical hybrid automaton, which we call MRB hybrid automaton. One of the chief characteristics of the MRB hybrid automaton is the inclusion of computation nodes to encode algorithms to calculate the contact forces. The computation nodes consist of a set of non-dynamical discrete locations, discrete transitions and guards between these locations, and resets on transitions. They can account for the energy transfer not explicitly considered within the rigid-body formalism. The proposed modelling framework is well suited for the automated verification of dynamical properties of realistic mechanical systems. We show this by the falsification of safety properties over the transition system generated by DyverseRBT.


93C30 Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems)
70Q05 Control of mechanical systems
92-08 Computational methods for problems pertaining to biology
Full Text: DOI


[1] Alur, R.; Courcoubetis, C.; Henzinger, T. A.; Ho, P. H.; Grossman, R. L.; Nerode, A.; Ravn, A. P.; Rischel, H., Hybrid Automata: an Algorithmic Approach to the Specification and Verification of Hybrid Systems, in Hybrid Systems, 736 (1993), Springer
[2] Henzinger, T., The theory of hybrid automata, 1, 278-292 (1996)
[3] Johansson, K. H.; Egerstedt, M.; Lygeros, J.; Sastry, S., On the regularization of Zeno hybrid automata, Syst. Control. Lett., 38, 141-150 (1999)
[4] Lygeros, J.; Johansson, K. H.; Simic, S. N.; Sastry, S. S., Dynamical properties of hybrid automata, IEEE Trans Automat Contr, 48, 2-17 (2003)
[5] Acary, V.; Brogliato, B., Numerical Methods for Nonsmooth Dynamical Systems (2008), Springer-Verlag Heidelberg
[6] Alart, P.; Curnier, A., A mixed formulation for fictional contact problems prone to newton like solution methods, Methods Appl. Mechanics Eng., 92, 353-375 (1991)
[7] Bayo, E.; Laursen, R., Augmented lagrangian and mass-orthogonal projection methods for constrained multibody dynamics, Nonlinear Dyn., 9, 113-130 (1996)
[8] Blumentals, A.; Brogliato, B.; Bertails-Descoubes, F., The contact problem in Lagrangian systems subject to bilateral and unilateral constraints, with or without sliding Coulomb’s friction: a tutorial, Multibody Syst. Dyn., 38, 43-76 (2016)
[9] Brogliato, B., Nonsmooth Mechanics: models, Dynamics and Control (1999), Springer-Verlag
[10] Hurmuzlu, Y.; Marghitu, D., Rigid body collisioons of planar kinematic chains with multiple contact points, Int. J. Rob. Res., 13, 82-92 (1994)
[11] Leine, R.; Van De Wouw, N., Stability and Convergence of Mechanical Systems with Unilateral Constraints (2008), Springer-Verlag
[12] Nguyen, N.; Brogliato, B., Multiple Impacts in Dissipative Granular Chains (2014), Springer-Verlag
[13] Pfeiffer, F., Mechanical Systems Dynamics (2008), Springer Heidelberg
[14] Studer, C., Numerics of Unilateral Contacts and Friction (2009), Springer-Verlag Heidelberg
[15] Kress-Gazit, H., Robot challenges: toward development of verification and synthesis techniques [from the guest editors], IEEE Robotics and Automation Magazine, 18, 22-23 (2011)
[16] Kress-Gazit, H.; Wongpiromsarn, T.; Topcu, U., Correct, reactive, high-level robot control: mitigating the state explosion problem of temporal logic synthesis, IEEE Robotics and Automation Magazine, 18, 65-74 (2011)
[17] Bhatia, A.; Maly, M.; Kavraki, E.; Vardi, M., Motion planning with complex goals, Robotics Automation Magazine, IEEE, 18, 55-64 (2011)
[18] Ding, X.; Kloetzer, M.; Chen, Y.; Belta, C., Automatic deployment of robotic teams, IEEE Robotics Automation Magazine, 18, 75-86 (2011)
[19] Verma, R.; Del Vecchio, D., Semi-autonomous multi-vehicle safety, Robotics and Automation Magazine, IEEE, 18, 44-54 (2011)
[20] Navarro-López, E.; Celikok, U.; Sengör, N.; El Hady, A., Hybrid systems neuroscience, 1, 113-129 (2016), Academic Press
[21] Goebel, R.; Sanfelice, R.; Teel, A., Hybrid dynamical systems. robust stability and control for systems that combine continuous-time and discrete-time dynamics, 28-93 (2009)
[22] Simo, J.; Laursen, T., An augmented lagrangian treatment of contact problems involving friction, Comput. Struct., 42, 91-116 (1992)
[23] O’Toole, M. D.; Navarro-López, E. M., A hybrid automaton for a class of multi-Contact rigid-body systems with friction and impacts, 299-306 (2012), Eindhoven, The Netherlands
[24] Navarro-López, E.; Carter, R., Hybrid automata: an insight into the discrete abstraction of discontinuous systems, Int. J. Syst. Sci., 42, 1883-1898 (2011)
[25] Nishida, T.; Doshita, S., Reasoning about discontinuous change, 2, 643-648 (1987), AAAI Press
[26] Mosterman, P.; Biswas, G., A theory of discontinuities in physical system models, J. Franklin Inst., 335, 401-439 (1998)
[27] Mosterman, P.; Biswas, G., A comprehensive methodology for building hybrid models of physical systems, Artif. Intell., 121, 171-209 (2000)
[28] Navarro-López, E.; Zander, J.; Mosterman, P. J., DYVERSE: from formal verification to biologically-inspired real-time self-organising systems, 303-348 (2013), CRC Press/Taylor & Francis
[29] Brockett, R., On the computer control of movement, 1, 534-540 (1988), New York, USA
[30] Forbus, K., Qualitative process theory, Artif. Intell., 24, 85-168 (1984)
[31] Kuipers, B., Qualitative simulation, Artif. Intell., 29, 298-338 (1986)
[32] Egerstedt, M.; Brockett, R., Feedback can reduce the specification complexity of motor programs, IEEE Trans Automat Contr, 48, 213-223 (2003)
[33] Woods, E., The hybrid phenomena theory, 1, 71-76 (1991)
[34] Acary, V., Projected event-capturing time-stepping schemes for nonsmooth mechanical systems with unilateral contact and Coulomb’s friction, Comput. Methods Appl. Mechanical Eng., 256, 224-250 (2013)
[35] Stewart, D.; Trinkle, J., An implicit time-stepping scheme for rigid body dynamics with inelastic collisions and Coulomb friction, Int. J. Numer. Methods Eng., 39, 2673-2691 (1996)
[36] Filippov, A., Differential Equations with Discontinuous Right-Hand Sides (1988), Kluwer Academic Publishers: Kluwer Academic Publishers, Dordrecht
[37] Utkin, V., Sliding Modes in Control Optimization (1992), Springer-Verlag: Springer-Verlag, Berlin
[38] Elmqvist, H.; Cellier, F.; Otter, M., Object-oriented modeling of hybrid systems, 1, 31-41 (1993)
[39] Mattsson, S., On object-oriente dmodelling of relays and sliding mode behaviour, 1, 259-264 (1996)
[40] Bliudze, S.; Furic, S., An operational semantics for hybrid systems involving behavioral abstraction, 1, 693-706 (2014)
[41] Liu, J.; Lee, E., A component-based approach to modeling and simulating mixed-signal and hybrid systems, ACM Trans. Model Comput. Simul., 12, 343-368 (2002)
[42] Lee, E.; Zheng, H.; Morari, M.; Thiele, L., Operational semantics of hybrid systems, 3414, 25-53 (2005), LNCS, Springer-Verlag
[43] Mosterman, P.; Zhao, F.; Biswas, G., Sliding mode model semantics and simulation for hybrid systems, 1567, 218-237 (1999), LNCS, Springer-Verlag
[44] Mosterman, P.; Vangheluwe, H., Computer automated multi-paradigm modeling: an introduction, Simulation, 80, 433-450 (2004)
[45] Navarro-López, E., Hybrid-automaton models for simulating systems with sliding motion: still a challenge, 1, 322-327 (2009), Zaragoza, Spain
[46] Navarro-López, E., Hybrid modelling of a discontinuous dynamical system including switching control, 1 (2009), CHAOS09: CHAOS09, London, UK
[47] Eker, J.; Janneck, J.; Lee, E.; Liu, J.; Liu, X.; Ludvig, J.; Neuendorffer, S.; Sachs, S.; Xiong, Y., Taming heterogeneity: the ptolemy approach, Proc. IEEE, 91, 127-144 (2003)
[48] Frehse, G.; Guernic, C.; Donzé, A.; Cotton, S.; Ray, R.; Lebeltel, O.; Ripado, R.; Girard, A.; Dang, T.; Maler, O.; Gopalakrishnan, G.; Qadeer, S., Spaceex: scalable Verification of Hybrid Systems, in Computer Aided Verification, 6806, 379-395 (2011), LNCS, Springer-Verlag
[49] Girard, A.; Julius, A.; Pappas, G., Approximate simulation relations for hybrid systems, Discrete Event Dyn Syst, 18, 163-179 (2008)
[50] Girard, A., Controller synthesis for safety and reachability via approximate bisimulation, Automatica, 48, 947-953 (2012)
[51] Pola, G.; Tabuada, P., Symbolic models for nonlinear control systems: alternating approximate bisimulations, SIAM J Control Optimization, 48, 719-733 (2009)
[52] Tabuada, P., An approximate simulation approach to symbolic control, IEEE Trans Automat Contr, 53, 1406-1418 (2008)
[53] Mosterman, P.; Zander, J.; Hamon, G.; Denckla, B., A computational model of time for stiff hybrid systems applied to control synthesis, Control Eng Pract, 20, 2-13 (2012)
[54] The MathWorks, Inc., Stateflow and Stateflow Coder User’s Guide, For Complex Logic and State Diagram Modeling (2008)
[55] Fritzson, P., Introduction to Modeling and Simulation of Technical and Physical Systems with Modelica (2011), Wiley-IEEE Press
[56] Brooks, C.; Lee, E.; Lorenzetti, D.; Nouidui, T.; Wetter, M., Demo: cyPhySim A Cyber-Physical Systems Simulator, 1, 301-302 (2015), HSCC: HSCC, Seattle, Washington, USA
[57] Bhatia, A.; Frazzoli, E., Resolution-complete safety falsification of continuous time systems, 1, 3297-3302 (2006), CDC: CDC, San Diego, CA, USA
[58] Bhatia, A.; Frazzoli, E.; Egerstedt, M.; Mishra, B., Sampling-based resolution-complete algorithms for safety falsification of linear systems, 4981, 606-609 (2008), HSCC, LNCS, Springer-Verlag
[59] Cheng, P.; Kumar, V., Sampling-Based Falsification and Verification of Controllers for Continuous Dynamic Systems (2006), Workshop on Algorithmic Foundations of Robotics VII
[60] Sankaranarayanan, S.; Fainekos, G., Falsification of temporal properties of hybrid systems using the cross-entropy method, 125-134 (2012)
[61] Bhatia, A.; Frazzoli, E.; Alur, R.; Pappas, G., Hybrid Systems: computation and Control, 2993, Incremental search methods for reachability analysis of continuous and hybrid systems, 142-156 (2004), HSCC, LNCS, Springer-Verlag
[62] Bhatia, A.; Frazzoli, E., Sampling-based resolution-complete safety falsification of linear hybrid systems, 1, 3405-3411 (2007), CDC: CDC, New Orleans, LA, USA
[63] Plaku, E.; Kavraki, L.; Vardi, M., Hybrid systems: from verification to falsification by combining motion planning and discrete search, Formal Methods Syst. Des., 34, 157-182 (2009)
[64] Plaku, E.; Kavraki, L.; Vardi, M., Falsification of LTL safety properties in hybrid systems, 2009, 368-382 (2009), TACAS
[65] Zutshi, A.; Sankaranarayanan, S.; Deshmukh, J.; Kapinski, J., A trajectory splicing approach to concretizing counterexamples for hybrid systems, 3918-3925 (2013)
[66] Annpureddy, Y.; Liu, C.; Fainekos, G.; Sankaranarayanan, S., S-TaLiRo: A tool for temporal logic falsification for hybrid systems, 6605, 254-257 (2011), Springer
[67] Biere, A.; Cimatti, A.; Clarke, E.; Zhu, Y., Symbolic model checking without BDDs, 1579, 193-207 (1999), Springer
[68] Copty, F.; Fix, L.; Fraer, R.; Giunchiglia, E.; Kamhi, G.; Tacchella, A.; Vardi, M., Benefits of bounded model checking at an industrial setting, 2102, 436-453 (2001), Springer
[69] Fränzle, M.; Herde, C., HySAT: an efficient proof engine for bounded model checking of hybrid systems, Formal Methods Syst. Des., 30, 179-198 (2007)
[70] Prasad, M.; Biere, A.; Gupta, A., A survey of recent advances in sat-based formal verification, Int J Software Tools Technol Transfer, 7, 156-173 (2005)
[71] Nuzzo, P.; Puggelli, A.; Seshia, S.; Sangiovanni-Vincentelli, A., CalCS: SMT Solving for Non-linear Convex Constraints, 71-80 (2010), FMCAD: FMCAD, Lugano, Switzerland
[72] Griggio, A.; Fondazione, B.; Kessler, I.; Sommarive, V., A practical approach to satisfiability modulo linear integer arithmetic, J. Satisfiability Boolean Modeling and Computation, 1-27 (2012)
[73] Rushby, J., Harnessing disruptive innovation in formal verification, 2006, 21-30 (2006), SEF M
[74] Sebastiani, R., Lazy satisfiability modulo theories, Journal on Satisfiability, Boolean Modeling Computat, 3, 141-224 (2007)
[75] Fränzle, M.; Herde, C.; Teige, T.; Ratschan, S.; Schubert, T., Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure, Journal on Satisfiability, Boolean Modeling Computat, 1, 209-236 (2007)
[76] Eggers, A.; Kalinnik, N.; Kupferschmid, S.; Teige, T., Challenges in constraint-based analysis of hybrid systems, 5655, 51-65 (2009), Springer
[77] Audemard, G.; Bozzano, M.; Cimatti, A.; Sebastiani, R., Verifying industrial hybrid systems with mathsat, Electron. Notes Theor. Compu. Sci, 119, 17-32 (2005)
[78] Bauer, A.; Pister, M.; Tautschnig, M., Tool-support for the analysis of hybrid systems and models, Proceedings of the Conference Design, Automation and Test in Europe, DATE, 2007, 924-929 (2007)
[79] Bauer, A.; Leucker, M.; Schallhart, C.; Tautschnig, M., Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers, Int J Software Tools Technol Transfer, 12, 23-37 (2010)
[80] Cimatti, A.; Mover, S.; Tonetta, S., Efficient scenario verification for hybrid automata, 6806, 317-332 (2011), Springer
[81] Bu, L.; Cimatti, A.; Li, X.; Mover, S.; Tonetta, S., Model checking of hybrid systems using shallow synchronization, 6117, 155-169 (2010), Springer
[82] Kong, S.; Gao, S.; Chen, W.; Clarke, E., dReach: -Reachability Analysis for Hybrid Systems, 2015 (2015), TACAS
[83] Gao, S.; Kong, S.; Clarke, E., dREal: an SMT solver for nonlinear theories over the reals, 7898, 208-214 (2013), Springer
[84] Gao, S.; Kong, S.; Clarke, E., Satisfiability Modulo ODEs, 105-112 (2013)
[85] Van Der Schaft, A.; Schumacher, H., An Introduction to Hybrid Dynamical Systems, Lecture Notes in Control and Information Sciences, 251 (2000), Springer-Verlag, London
[86] Pang, J. S.; Trinkle, J., Complementarity formulations and existence of solutions of dynamic multi-rigid-body contact problems with coulomb friction, Math. Programming, 73, 199-226 (1996)
[87] The NAG Library, The Numerical Algorithms Group (NAG) (2013), Oxford: Oxford, United Kingdom
[88] Studer, C.; Glocker, C., Solving normal cone inclusion problems in contact mechanics by iterative methods, J. Syst. Des. Dyn., 1, 458-467 (2007)
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.