Hybrid systems: From verification to falsification by combining motion planning and discrete search. (English) Zbl 1192.68692
Summary: We propose HyDICE, Hybrid Discrete Continuous Exploration, a multi-layered approach for hybrid-system falsification that combines motion planning with discrete search and discovers safety violations by computing witness trajectories to unsafe states. The discrete search uses discrete transitions and a state-space decomposition to guide the motion planner during the search for witness trajectories. Experiments on a nonlinear hybrid robotic system with over one million modes and experiments with an aircraft conflict-resolution protocol with high-dimensional continuous state spaces demonstrate the effectiveness of HyDICE. Comparisons to related work show computational speedups of up to two orders of magnitude.
MSC:
| 68T40 | Artificial intelligence for robotics |
| 68T20 | Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) |
Keywords:
hybrid system; safety properties; robot motion planning; discrete search; sampling-based planning; decomposition; nonlinear dynamicsReferences:
| [1] | Alur R, Courcoubetis C, Halbwachs N, Henzinger TA, Ho PH, Nicollin X, Olivero A, Sifakis J, Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138(1):3–34 · Zbl 0874.68206 · doi:10.1016/0304-3975(94)00202-T |
| [2] | Alur R, Henzinger TA, Lafferriere G, Pappas G (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971–984 · doi:10.1109/5.871304 |
| [3] | Alur R, Dang T, Ivančić F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250–271 · Zbl 1088.68096 · doi:10.1016/j.tcs.2005.11.026 |
| [4] | Asarin E, Dang T, Maler O (2002) The d/dt tool for verification of hybrid systems. In: Int conf on computer aided verification. LNCS. Springer, Berlin, pp 365–370 · Zbl 1010.68796 |
| [5] | Behrmann G, David A, Larsen KG, Möller O, Pettersson P, Yi W (2001) Uppaal–present and future. In: IEEE conf on decision and control, vol 3, pp 2881–2886 |
| [6] | Belta C, Esposito J, Kim J, Kumar V (2005) Computational techniques for analysis of genetic network dynamics. Int J Robot Res 24(2–3):219–235 · doi:10.1177/0278364905050359 |
| [7] | Bhatia A, Frazzoli E (2004) Incremental search methods for reachability analysis of continuous and hybrid systems. In: Hybrid systems: Computation and control. LNCS, vol 2993. Springer, Berlin, pp 142–156 · Zbl 1135.93316 |
| [8] | Botchkarev O, Tripakis S (2000) Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Hybrid systems: Computation and control. LNCS, vol 1790. Springer, Berlin, pp 73–88 · Zbl 1037.93510 |
| [9] | Branicky MS, Curtiss MM, Levine J, Morgan S (2006) Sampling-based planning, control, and verification of hybrid systems. Control Theory Appl 153(5):575–590 · doi:10.1049/ip-cta:20050152 |
| [10] | Burch J, Clarke E, McMillan K, Dill D, Hwang L (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170 · Zbl 0753.68066 · doi:10.1016/0890-5401(92)90017-A |
| [11] | Choset H, Lynch KM, Hutchinson S, Kantor G, Burgard W, Kavraki LE, Thrun S (2005) Principles of robot motion: Theory, algorithms, and implementations. MIT Press, Cambridge · Zbl 1081.68700 |
| [12] | Chutinan C, Krogh BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64–75 · Zbl 1364.93457 · doi:10.1109/TAC.2002.806655 |
| [13] | Clarke EM, Bierea A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7–34 · Zbl 0985.68038 · doi:10.1023/A:1011276507260 |
| [14] | Clarke EM, Grumberg O, Peled DA (2001) Model checking. MIT Press, Cambridge |
| [15] | Copty F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi M (2001) Benefits of bounded model checking at an industrial setting. In: Int conf on computer aided verification. LNCS, vol 2102. Springer, Berlin, pp 436–453 · Zbl 0991.68637 |
| [16] | de Berg M, van Kreveld M, Overmars MH (1997) Computational geometry: Algorithms and applications. Springer, Berlin |
| [17] | Edelkamp S, Jabbar S (2006) Large-scale directed model checking LTL. In: Int SPIN work on model checking software. LNCS, vol 3925. Springer, Berlin, pp 1–18 · Zbl 1178.68339 |
| [18] | Esposito J, Kumar V, Pappas G (2001) Accurate event detection for simulation of hybrid systems. In: Hybrid systems: Computation and control. LNCS. Springer, Berlin, pp 204–217 · Zbl 0991.93525 |
| [19] | Esposito JM, Kim J, Kumar V (2004) Adaptive RRTs for validating hybrid robotic control systems. In: Workshop on algorithmic foundations of robotics. Zeist, Netherlands, pp 107–132 |
| [20] | Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. In: Hybrid systems: Computation and control. LNCS, vol 2993. Springer, Berlin, pp 326–341 · Zbl 1135.93324 |
| [21] | Galassi M, Davies J, Theiler J, Gough B, Jungman G, Booth M, Rossi F (2006) GNU scientific library reference manual, 2 edn. Network Theory Ltd |
| [22] | George PL, Borouchaki H (1998) Delaunay triangulation and meshing: Application to finite elements. Hermes Science Publications · Zbl 0908.65143 |
| [23] | Giorgetti N, Pappas GJ, Bemporad A (2005) Bounded model checking for hybrid dynamical systems. In: IEEE conf on decision and control. Seville, Spain, pp 672–677 |
| [24] | Glover W, Lygeros J (2004) A stochastic hybrid model for air traffic control simulation. In: Hybrid systems: Computation and control. LNCS, vol 2993. Springer, Berlin, pp 372–386 · Zbl 1135.93374 |
| [25] | Henzinger T (1996) The theory of hybrid automata. In: Symp on logic in computer science, pp 278–292 |
| [26] | Henzinger T, Kopke P, Puri A, Varaiya P (1995) What’s decidable about hybrid automata? In: ACM symp on theory of computing, pp 373–382 · Zbl 0978.68534 |
| [27] | Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: A model checker for hybrid systems. Softw Tools Technol Transfer 1:110–122 · Zbl 1060.68603 · doi:10.1007/s100090050008 |
| [28] | Hsu D, Kindel R, Latombe, JC, Rock S (2002) Randomized kinodynamic motion planning with moving obstacles. Int J Robot Res 21(3):233–255 · doi:10.1177/027836402320556421 |
| [29] | Johansson R, Rantzer A (2002) Nonlinear and hybrid, systems in automotive, control. Springer, New York · Zbl 1098.00007 |
| [30] | Julius AA, Fainekos GE, Anand M, Lee I, Pappas GJ (2007) Robust test generation and coverage for hybrid systems. In: Hybrid systems: Computation and control. LNCS, vol 4416. Springer, Berlin, pp 329–342 · Zbl 1221.93076 |
| [31] | Kavraki LE, Švestka P, Latombe JC, Overmars MH (1996) Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Trans Robot Autom 12(4):566–580 · doi:10.1109/70.508439 |
| [32] | Kim J, Esposito JM, Kumar V (2005) An RRT-based algorithm for testing and validating multi-robot controllers. In: Robotics: Science and systems. Boston, MA, pp 249–256 |
| [33] | Kruskal JB (1956) On the shortest spanning subtree of a graph and the traveling salesman problem. Proc Am Math Soc 7(1):48–50 · Zbl 0070.18404 · doi:10.1090/S0002-9939-1956-0078686-7 |
| [34] | Ladd AM (2006) Motion planning for physical simulation. PhD thesis, Rice University, Houston, TX |
| [35] | Ladd AM, Kavraki LE (2005) Motion planning in the presence of drift, underactuation and discrete system changes. In: Robotics: Science and systems. Boston, MA, pp 233–241 |
| [36] | Lafferriere G, Pappas G, Yovine S (1999) A new class of decidable hybrid systems. In: Hybrid systems: Computation and control. LNCS, vol 1569. Springer, Berlin, pp 137–151 · Zbl 0926.93036 |
| [37] | LaValle SM (2006) Planning algorithms. Cambridge University Press, Cambridge · Zbl 1100.68108 |
| [38] | LaValle SM, Kuffner JJ (2001) Rapidly-exploring random trees: Progress and prospects. In: Workshop on algorithmic foundations of robotics, pp 293–308 · Zbl 0986.68151 |
| [39] | Livadas C, Lynch N (1998) Formal verification of safety-critical hybrid systems. In: Hybrid systems: Computation and control. LNCS, vol 1386. Springer, Berlin, pp 253–272 |
| [40] | Mitchell IM (2007) Comparing forward and backward reachability as tools for safety analysis. In: Hybrid systems: Computation and control. LNCS, vol 4416. Springer, Berlin, pp 428–443 · Zbl 1221.93029 |
| [41] | Nahhal T, Dang T (2007) Test coverage for continuous and hybrid systems. In: Int conf on computer aided verification. LNCS, vol 4590. Springer, Berlin, pp 449–462 · Zbl 1135.68346 |
| [42] | Pepyne D, Cassandras C (2000) Optimal control of hybrid systems in manufacturing. Proc IEEE 88(7):1108–1123 · doi:10.1109/5.871312 |
| [43] | Piazza C, Antoniotti M, Mysore V, Policriti A, Winkler F, Mishra B (2005) (2005) Algorithmic algebraic model checking I: Challenges from systems biology. In: Int conf computer aided verification. LNCS, vol 3576. Springer, Berlin, pp 5–19 · Zbl 1081.68056 |
| [44] | Plaku E, Bekris KE, Chen BY, Ladd AM, Kavraki LE (2005) Sampling-based roadmap of trees for parallel motion planning. IEEE Trans Robot 21(4):597–608 · doi:10.1109/TRO.2005.847599 |
| [45] | Plaku E, Kavraki LE, Vardi MY (2007) Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science and systems. Atlanta, Georgia |
| [46] | Plaku E, Kavraki LE, Vardi MY (2007) Hybrid systems: From verification to falsification. In: Int conf on computer aided verification. LNCS, vol 4590. Springer, Berlin, pp 468–481 · Zbl 1135.68479 |
| [47] | Plaku E, Kavraki LE, Vardi MY (2007) A motion planner for a hybrid robotic system with kinodynamic constraints. In: IEEE int conf on robotics and automation. Rome, Italy, pp 692–697 |
| [48] | Puri A (1995) Theory of hybrid systems and discrete event systems. PhD thesis, University of California, Berkeley |
| [49] | Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8 · doi:10.1145/1210268.1210276 |
| [50] | Sánchez G, Latombe JC (2002) On delaying collision checking in PRM planning: Application to multi-robot coordination. Int J Robot Res 21(1):5–26 · doi:10.1177/027836402320556458 |
| [51] | Silva BI, Krogh BH (2000) Formal verification of hybrid systems using CheckMate: A case study. In: American control conference, pp 1679–1683 |
| [52] | Stursberg O, Krogh BH (2003) Efficient representation and computation of reachable sets for hybrid systems. In: Hybrid systems: Computation and control. LNCS, vol 2623. Springer, Berlin, pp 482–497 · Zbl 1032.93037 |
| [53] | Tomlin CJ, Pappas GJ, Sastry SS (1998) Conflict resolution for air traffic management: A case study in multi-agent hybrid systems. IEEE Trans Autom Control 43(4):509–521 · Zbl 0904.90113 · doi:10.1109/9.664154 |
| [54] | Tomlin CJ, Mitchell I, Bayen A, Oishi M (2003) Computational techniques for the verification and control of hybrid systems. Proc IEEE 91(7):986–1001 · doi:10.1109/JPROC.2003.814621 |
| [55] | Yovine S (1997) Kronos: A verification tool for real-time systems. Int J Softw Tools Technol Transf 1:123–133 · Zbl 1060.68606 · doi:10.1007/s100090050009 |
| [56] | Zhang W (2006) State-space search: Algorithms, complexity, extensions, and applications. Springer, New York |
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.
