{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T06:38:32Z","timestamp":1773470312353,"version":"3.50.1"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2008,10,25]],"date-time":"2008-10-25T00:00:00Z","timestamp":1224892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2009,4]]},"DOI":"10.1007\/s10703-008-0058-5","type":"journal-article","created":{"date-parts":[[2008,10,24]],"date-time":"2008-10-24T13:21:16Z","timestamp":1224854476000},"page":"157-182","source":"Crossref","is-referenced-by-count":45,"title":["Hybrid systems: from verification to falsification by\u00a0combining motion planning and discrete search"],"prefix":"10.1007","volume":"34","author":[{"given":"Erion","family":"Plaku","sequence":"first","affiliation":[]},{"given":"Lydia E.","family":"Kavraki","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2008,10,25]]},"reference":[{"issue":"1","key":"58_CR1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R Alur","year":"1995","unstructured":"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\u201334","journal-title":"Theor Comput Sci"},{"issue":"7","key":"58_CR2","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur R, Henzinger TA, Lafferriere G, Pappas G (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971\u2013984","journal-title":"Proc IEEE"},{"issue":"2","key":"58_CR3","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1016\/j.tcs.2005.11.026","volume":"354","author":"R Alur","year":"2006","unstructured":"Alur R, Dang T, Ivan\u010di\u0107 F (2006) Counterexample-guided predicate abstraction of hybrid systems. Theor Comput Sci 354(2):250\u2013271","journal-title":"Theor Comput Sci"},{"key":"58_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-45657-0_30","volume-title":"Int conf on computer aided verification","author":"E Asarin","year":"2002","unstructured":"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\u2013370"},{"key":"58_CR5","doi-asserted-by":"crossref","unstructured":"Behrmann G, David A, Larsen KG, M\u00f6ller O, Pettersson P, Yi W (2001) Uppaal\u2014present and future. In: IEEE conf on decision and control, vol 3, pp 2881\u20132886","DOI":"10.1109\/CDC.2001.980713"},{"issue":"2\u20133","key":"58_CR6","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1177\/0278364905050359","volume":"24","author":"C Belta","year":"2005","unstructured":"Belta C, Esposito J, Kim J, Kumar V (2005) Computational techniques for analysis of genetic network dynamics. Int J Robot Res 24(2\u20133):219\u2013235","journal-title":"Int J Robot Res"},{"key":"58_CR7","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-540-24743-2_10","volume-title":"Hybrid systems: Computation and control","author":"A Bhatia","year":"2004","unstructured":"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\u2013156"},{"key":"58_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/3-540-46430-1_10","volume-title":"Hybrid systems: Computation and control","author":"O Botchkarev","year":"2000","unstructured":"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\u201388"},{"issue":"5","key":"58_CR9","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1049\/ip-cta:20050152","volume":"153","author":"MS Branicky","year":"2006","unstructured":"Branicky MS, Curtiss MM, Levine J, Morgan S (2006) Sampling-based planning, control, and verification of hybrid systems. Control Theory Appl 153(5):575\u2013590","journal-title":"Control Theory Appl"},{"issue":"2","key":"58_CR10","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J Burch","year":"1992","unstructured":"Burch J, Clarke E, McMillan K, Dill D, Hwang L (1992) Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170","journal-title":"Inf Comput"},{"key":"58_CR11","volume-title":"Principles of robot motion: Theory, algorithms, and implementations","author":"H Choset","year":"2005","unstructured":"Choset H, Lynch KM, Hutchinson S, Kantor G, Burgard W, Kavraki LE, Thrun S (2005) Principles of robot motion: Theory, algorithms, and implementations. MIT\u00a0Press, Cambridge"},{"issue":"1","key":"58_CR12","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"C Chutinan","year":"2003","unstructured":"Chutinan C, Krogh BH (2003) Computational techniques for hybrid system verification. IEEE Trans Autom Control 48(1):64\u201375","journal-title":"IEEE Trans Autom Control"},{"issue":"1","key":"58_CR13","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Bierea A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7\u201334","journal-title":"Formal Methods Syst Des"},{"key":"58_CR14","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model checking","author":"EM Clarke","year":"2001","unstructured":"Clarke EM, Grumberg O, Peled DA (2001) Model checking. MIT Press, Cambridge"},{"key":"58_CR15","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Int conf on computer aided verification","author":"F Copty","year":"2001","unstructured":"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\u2013453"},{"key":"58_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03427-9","volume-title":"Computational geometry: Algorithms and applications","author":"M Berg de","year":"1997","unstructured":"de Berg M, van Kreveld M, Overmars MH (1997) Computational geometry: Algorithms and applications. Springer, Berlin"},{"key":"58_CR17","series-title":"LNCS","first-page":"1","volume-title":"Int SPIN work on model checking software","author":"S Edelkamp","year":"2006","unstructured":"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\u201318"},{"key":"58_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/3-540-45351-2_19","volume-title":"Hybrid systems: Computation and control","author":"J Esposito","year":"2001","unstructured":"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\u2013217"},{"key":"58_CR19","unstructured":"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\u2013132"},{"key":"58_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid systems: Computation and control","author":"A Fehnker","year":"2004","unstructured":"Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. In: Hybrid systems: Computation and control. LNCS, vol 2993. Springer, Berlin, pp 326\u2013341"},{"key":"58_CR21","unstructured":"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"},{"key":"58_CR22","unstructured":"George PL, Borouchaki H (1998) Delaunay triangulation and meshing: Application to finite elements. Hermes Science Publications"},{"key":"58_CR23","doi-asserted-by":"crossref","unstructured":"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\u2013677","DOI":"10.1109\/CDC.2005.1582233"},{"key":"58_CR24","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1007\/978-3-540-24743-2_25","volume-title":"Hybrid systems: Computation and control","author":"W Glover","year":"2004","unstructured":"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\u2013386"},{"key":"58_CR25","doi-asserted-by":"crossref","unstructured":"Henzinger T (1996) The theory of hybrid automata. In: Symp on logic in computer science, pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"58_CR26","doi-asserted-by":"crossref","unstructured":"Henzinger T, Kopke P, Puri A, Varaiya P (1995) What\u2019s decidable about hybrid automata? In: ACM symp on theory of computing, pp 373\u2013382","DOI":"10.1145\/225058.225162"},{"key":"58_CR27","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger TA, Ho PH, Wong-Toi H (1997) HyTech: A model checker for hybrid systems. Softw Tools Technol Transfer 1:110\u2013122","journal-title":"Softw Tools Technol Transfer"},{"issue":"3","key":"58_CR28","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1177\/027836402320556421","volume":"21","author":"D Hsu","year":"2002","unstructured":"Hsu D, Kindel R, Latombe, JC, Rock S (2002) Randomized kinodynamic motion planning with moving obstacles. Int J Robot Res 21(3):233\u2013255","journal-title":"Int J Robot Res"},{"key":"58_CR29","volume-title":"Nonlinear and hybrid, systems in automotive, control","author":"R Johansson","year":"2002","unstructured":"Johansson R, Rantzer A (2002) Nonlinear and hybrid, systems in automotive, control. Springer, New York"},{"key":"58_CR30","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1007\/978-3-540-71493-4_27","volume-title":"Hybrid systems: Computation and control","author":"AA Julius","year":"2007","unstructured":"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\u2013342"},{"issue":"4","key":"58_CR31","doi-asserted-by":"crossref","first-page":"566","DOI":"10.1109\/70.508439","volume":"12","author":"LE Kavraki","year":"1996","unstructured":"Kavraki LE, \u0160vestka P, Latombe JC, Overmars MH (1996) Probabilistic roadmaps for path planning in high-dimensional configuration spaces. IEEE Trans Robot Autom 12(4):566\u2013580","journal-title":"IEEE Trans Robot Autom"},{"key":"58_CR32","doi-asserted-by":"crossref","unstructured":"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\u2013256","DOI":"10.15607\/RSS.2005.I.033"},{"issue":"1","key":"58_CR33","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1090\/S0002-9939-1956-0078686-7","volume":"7","author":"JB Kruskal","year":"1956","unstructured":"Kruskal JB (1956) On the shortest spanning subtree of a graph and the traveling salesman problem. Proc Am Math Soc 7(1):48\u201350","journal-title":"Proc Am Math Soc"},{"key":"58_CR34","unstructured":"Ladd AM (2006) Motion planning for physical simulation. PhD thesis, Rice University, Houston, TX"},{"key":"58_CR35","unstructured":"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\u2013241"},{"key":"58_CR36","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-48983-5_15","volume-title":"Hybrid systems: Computation and control","author":"G Lafferriere","year":"1999","unstructured":"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\u2013151"},{"key":"58_CR37","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511546877","volume-title":"Planning algorithms","author":"SM LaValle","year":"2006","unstructured":"LaValle SM (2006) Planning algorithms. Cambridge University Press, Cambridge"},{"key":"58_CR38","unstructured":"LaValle SM, Kuffner JJ (2001) Rapidly-exploring random trees: Progress and prospects. In: Workshop on algorithmic foundations of robotics, pp 293\u2013308"},{"key":"58_CR39","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1007\/3-540-64358-3_44","volume-title":"Hybrid systems: Computation and control","author":"C Livadas","year":"1998","unstructured":"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\u2013272"},{"key":"58_CR40","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/978-3-540-71493-4_34","volume-title":"Hybrid systems: Computation and control","author":"IM Mitchell","year":"2007","unstructured":"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\u2013443"},{"key":"58_CR41","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/978-3-540-73368-3_47","volume-title":"Int conf on computer aided verification","author":"T Nahhal","year":"2007","unstructured":"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\u2013462"},{"issue":"7","key":"58_CR42","doi-asserted-by":"crossref","first-page":"1108","DOI":"10.1109\/5.871312","volume":"88","author":"D Pepyne","year":"2000","unstructured":"Pepyne D, Cassandras C (2000) Optimal control of hybrid systems in manufacturing. Proc IEEE 88(7):1108\u20131123","journal-title":"Proc IEEE"},{"key":"58_CR43","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/11513988_3","volume-title":"Int conf computer aided verification","author":"C Piazza","year":"2005","unstructured":"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\u201319"},{"issue":"4","key":"58_CR44","doi-asserted-by":"crossref","first-page":"597","DOI":"10.1109\/TRO.2005.847599","volume":"21","author":"E Plaku","year":"2005","unstructured":"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\u2013608","journal-title":"IEEE Trans Robot"},{"key":"58_CR45","doi-asserted-by":"crossref","unstructured":"Plaku E, Kavraki LE, Vardi MY (2007) Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science and systems. Atlanta, Georgia","DOI":"10.15607\/RSS.2007.III.040"},{"key":"58_CR46","series-title":"LNCS","first-page":"468","volume-title":"Int conf on computer aided verification","author":"E Plaku","year":"2007","unstructured":"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\u2013481"},{"key":"58_CR47","doi-asserted-by":"crossref","unstructured":"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\u2013697","DOI":"10.1109\/ROBOT.2007.363067"},{"key":"58_CR48","unstructured":"Puri A (1995) Theory of hybrid systems and discrete event systems. PhD thesis, University of California, Berkeley"},{"issue":"1","key":"58_CR49","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/1210268.1210276","volume":"6","author":"S Ratschan","year":"2007","unstructured":"Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8","journal-title":"ACM Trans Embed Comput Syst"},{"issue":"1","key":"58_CR50","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1177\/027836402320556458","volume":"21","author":"G S\u00e1nchez","year":"2002","unstructured":"S\u00e1nchez G, Latombe JC (2002) On delaying collision checking in PRM planning: Application to multi-robot coordination. Int J Robot Res 21(1):5\u201326","journal-title":"Int J Robot Res"},{"key":"58_CR51","doi-asserted-by":"crossref","unstructured":"Silva BI, Krogh BH (2000) Formal verification of hybrid systems using CheckMate: A case study. In: American control conference, pp 1679\u20131683","DOI":"10.1109\/ACC.2000.879487"},{"key":"58_CR52","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"482","DOI":"10.1007\/3-540-36580-X_35","volume-title":"Hybrid systems: Computation and control","author":"O Stursberg","year":"2003","unstructured":"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\u2013497"},{"issue":"4","key":"58_CR53","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/9.664154","volume":"43","author":"CJ Tomlin","year":"1998","unstructured":"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\u2013521","journal-title":"IEEE Trans Autom Control"},{"issue":"7","key":"58_CR54","doi-asserted-by":"crossref","first-page":"986","DOI":"10.1109\/JPROC.2003.814621","volume":"91","author":"CJ Tomlin","year":"2003","unstructured":"Tomlin CJ, Mitchell I, Bayen A, Oishi M (2003) Computational techniques for the verification and control of hybrid systems. Proc IEEE 91(7):986\u20131001","journal-title":"Proc IEEE"},{"key":"58_CR55","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S (1997) Kronos: A verification tool for real-time systems. Int J Softw Tools Technol Transf 1:123\u2013133","journal-title":"Int J Softw Tools Technol Transf"},{"key":"58_CR56","volume-title":"State-space search: Algorithms, complexity, extensions, and applications","author":"W Zhang","year":"2006","unstructured":"Zhang W (2006) State-space search: Algorithms, complexity, extensions, and applications. Springer, New York"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0058-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-008-0058-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-008-0058-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:03Z","timestamp":1559253663000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-008-0058-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,10,25]]},"references-count":56,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2009,4]]}},"alternative-id":["58"],"URL":"https:\/\/doi.org\/10.1007\/s10703-008-0058-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,10,25]]}}}