Abstract
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
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
Alur R, Henzinger TA, Lafferriere G, Pappas G (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971–984
Alur R, Dang T, Ivančić F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250–271
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
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
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
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
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
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
Burch J, Clarke E, McMillan K, Dill D, Hwang L (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142–170
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
Chutinan C, Krogh BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64–75
Clarke EM, Bierea A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7–34
Clarke EM, Grumberg O, Peled DA (2001) Model checking. MIT Press, Cambridge
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
de Berg M, van Kreveld M, Overmars MH (1997) Computational geometry: Algorithms and applications. Springer, Berlin
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
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
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
Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. In: Hybrid systems: Computation and control. LNCS, vol 2993. Springer, Berlin, pp 326–341
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
George PL, Borouchaki H (1998) Delaunay triangulation and meshing: Application to finite elements. Hermes Science Publications
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
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
Henzinger T (1996) The theory of hybrid automata. In: Symp on logic in computer science, pp 278–292
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
Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: A model checker for hybrid systems. Softw Tools Technol Transfer 1:110–122
Hsu D, Kindel R, Latombe, JC, Rock S (2002) Randomized kinodynamic motion planning with moving obstacles. Int J Robot Res 21(3):233–255
Johansson R, Rantzer A (2002) Nonlinear and hybrid, systems in automotive, control. Springer, New York
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
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
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
Kruskal JB (1956) On the shortest spanning subtree of a graph and the traveling salesman problem. Proc Am Math Soc 7(1):48–50
Ladd AM (2006) Motion planning for physical simulation. PhD thesis, Rice University, Houston, TX
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
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
LaValle SM (2006) Planning algorithms. Cambridge University Press, Cambridge
LaValle SM, Kuffner JJ (2001) Rapidly-exploring random trees: Progress and prospects. In: Workshop on algorithmic foundations of robotics, pp 293–308
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
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
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
Pepyne D, Cassandras C (2000) Optimal control of hybrid systems in manufacturing. Proc IEEE 88(7):1108–1123
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
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
Plaku E, Kavraki LE, Vardi MY (2007) Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science and systems. Atlanta, Georgia
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
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
Puri A (1995) Theory of hybrid systems and discrete event systems. PhD thesis, University of California, Berkeley
Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8
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
Silva BI, Krogh BH (2000) Formal verification of hybrid systems using CheckMate: A case study. In: American control conference, pp 1679–1683
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
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
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
Yovine S (1997) Kronos: A verification tool for real-time systems. Int J Softw Tools Technol Transf 1:123–133
Zhang W (2006) State-space search: Algorithms, complexity, extensions, and applications. Springer, New York
Author information
Authors and Affiliations
Corresponding author
Additional information
Work supported in part by NSF CNS 0615328 (EP, LK, MV), NSF 0713623 (EP, LK), a Sloan Fellowship (LK), and NSF CCF 0613889 (MV). Equipment supported by NSF CNS 0454333 and NSF CNS 0421109 in partnership with Rice, AMD, and Cray.
A preliminary version of this work was published in the Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007). Lecture Notes in Computer Science, eds. W. Damm and H. Hermanns, vol. 4590, pp. 468–481. This work contains substantial improvements to the overall computational method introduced in the preliminary work and new experiments that were not included in the preliminary work.
Rights and permissions
About this article
Cite this article
Plaku, E., Kavraki, L.E. & Vardi, M.Y. Hybrid systems: from verification to falsification by combining motion planning and discrete search. Form Methods Syst Des 34, 157–182 (2009). https://doi.org/10.1007/s10703-008-0058-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-008-0058-5