×

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.

MSC:

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
PDFBibTeX XMLCite
Full Text: DOI

References:

[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) · Zbl 0948.93031 · doi:10.1016/S0167-6911(99)00059-6
[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) · Zbl 1364.93503 · doi:10.1109/TAC.2002.806650
[5] Acary, V.; Brogliato, B., Numerical Methods for Nonsmooth Dynamical Systems (2008), Springer-Verlag Heidelberg · Zbl 1173.74001
[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) · Zbl 0825.76353 · doi:10.1016/0045-7825(91)90022-X
[7] Bayo, E.; Laursen, R., Augmented lagrangian and mass-orthogonal projection methods for constrained multibody dynamics, Nonlinear Dyn., 9, 113-130 (1996) · doi:10.1007/BF01833296
[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) · Zbl 1372.70044 · doi:10.1007/s11044-016-9527-6
[9] Brogliato, B., Nonsmooth Mechanics: models, Dynamics and Control (1999), Springer-Verlag · Zbl 0917.73002
[10] Hurmuzlu, Y.; Marghitu, D., Rigid body collisioons of planar kinematic chains with multiple contact points, Int. J. Rob. Res., 13, 82-92 (1994) · doi:10.1177/027836499401300106
[11] Leine, R.; Van De Wouw, N., Stability and Convergence of Mechanical Systems with Unilateral Constraints (2008), Springer-Verlag · Zbl 1143.70001
[12] Nguyen, N.; Brogliato, B., Multiple Impacts in Dissipative Granular Chains (2014), Springer-Verlag
[13] Pfeiffer, F., Mechanical Systems Dynamics (2008), Springer Heidelberg · Zbl 1155.37001
[14] Studer, C., Numerics of Unilateral Contacts and Friction (2009), Springer-Verlag Heidelberg · Zbl 1162.70002
[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) · doi:10.1109/MRA.2011.942486
[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) · doi:10.1109/MRA.2011.942116
[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) · doi:10.1109/MRA.2011.942117
[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) · Zbl 1395.93001
[22] Simo, J.; Laursen, T., An augmented lagrangian treatment of contact problems involving friction, Comput. Struct., 42, 91-116 (1992) · Zbl 0755.73085 · doi:10.1016/0045-7949(92)90540-G
[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) · Zbl 1260.93013 · doi:10.1080/00207721.2010.495189
[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) · Zbl 0900.93030 · doi:10.1016/S0016-0032(96)00126-3
[27] Mosterman, P.; Biswas, G., A comprehensive methodology for building hybrid models of physical systems, Artif. Intell., 121, 171-209 (2000) · Zbl 0948.68210 · doi:10.1016/S0004-3702(00)00032-1
[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) · doi:10.1016/0004-3702(84)90038-9
[31] Kuipers, B., Qualitative simulation, Artif. Intell., 29, 298-338 (1986) · Zbl 0624.68098 · doi:10.1016/0004-3702(86)90073-1
[32] Egerstedt, M.; Brockett, R., Feedback can reduce the specification complexity of motor programs, IEEE Trans Automat Contr, 48, 213-223 (2003) · Zbl 1364.93512 · doi:10.1109/TAC.2002.808466
[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) · Zbl 1352.74477 · doi:10.1016/j.cma.2012.12.012
[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) · Zbl 0882.70003 · doi:10.1002/(ISSN)1097-0207
[36] Filippov, A., Differential Equations with Discontinuous Right-Hand Sides (1988), Kluwer Academic Publishers: Kluwer Academic Publishers, Dordrecht · Zbl 0664.34001
[37] Utkin, V., Sliding Modes in Control Optimization (1992), Springer-Verlag: Springer-Verlag, Berlin · Zbl 0748.93044
[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) · doi:10.1145/643120
[42] Lee, E.; Zheng, H.; Morari, M.; Thiele, L., Operational semantics of hybrid systems, 3414, 25-53 (2005), LNCS, Springer-Verlag · Zbl 1078.93535
[43] Mosterman, P.; Zhao, F.; Biswas, G., Sliding mode model semantics and simulation for hybrid systems, 1567, 218-237 (1999), LNCS, Springer-Verlag · Zbl 0925.93432
[44] Mosterman, P.; Vangheluwe, H., Computer automated multi-paradigm modeling: an introduction, Simulation, 80, 433-450 (2004) · doi:10.1177/0037549704050532
[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) · doi:10.1109/JPROC.2002.805829
[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) · Zbl 1395.93113 · doi:10.1007/s10626-007-0029-9
[50] Girard, A., Controller synthesis for safety and reachability via approximate bisimulation, Automatica, 48, 947-953 (2012) · Zbl 1246.93045 · doi:10.1016/j.automatica.2012.02.037
[51] Pola, G.; Tabuada, P., Symbolic models for nonlinear control systems: alternating approximate bisimulations, SIAM J Control Optimization, 48, 719-733 (2009) · Zbl 1194.93020 · doi:10.1137/070698580
[52] Tabuada, P., An approximate simulation approach to symbolic control, IEEE Trans Automat Contr, 53, 1406-1418 (2008) · Zbl 1367.93220 · doi:10.1109/TAC.2008.925824
[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) · doi:10.1016/j.conengprac.2011.04.013
[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 · Zbl 1144.93309
[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) · Zbl 1362.68183
[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 · Zbl 1135.93316
[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) · Zbl 1192.68692 · doi:10.1007/s10703-008-0058-5
[64] Plaku, E.; Kavraki, L.; Vardi, M., Falsification of LTL safety properties in hybrid systems, 2009, 368-382 (2009), TACAS · Zbl 1234.68264
[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 · Zbl 1316.68069
[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 · Zbl 0991.68637
[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) · Zbl 1116.68048 · doi:10.1007/s10703-006-0031-0
[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) · doi:10.1007/s10009-004-0183-4
[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) · Zbl 1331.68207
[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) · Zbl 1145.68501
[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) · Zbl 1144.68371
[76] Eggers, A.; Kalinnik, N.; Kupferschmid, S.; Teige, T., Challenges in constraint-based analysis of hybrid systems, 5655, 51-65 (2009), Springer · Zbl 1248.68328
[77] Audemard, G.; Bozzano, M.; Cimatti, A.; Sebastiani, R., Verifying industrial hybrid systems with mathsat, Electron. Notes Theor. Compu. Sci, 119, 17-32 (2005) · Zbl 1272.68220 · doi:10.1016/j.entcs.2004.12.022
[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) · doi:10.1007/s10009-009-0133-2
[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 · Zbl 1381.68268
[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 · Zbl 0940.93004
[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) · Zbl 0854.70008 · doi:10.1007/BF02592103
[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) · doi:10.1299/jsdd.1.458
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.