{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:14Z","timestamp":1776333494537,"version":"3.51.2"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,5,23]],"date-time":"2012-05-23T00:00:00Z","timestamp":1337731200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2013,8]]},"DOI":"10.1007\/s10009-012-0233-2","type":"journal-article","created":{"date-parts":[[2012,7,9]],"date-time":"2012-07-09T01:33:02Z","timestamp":1341797582000},"page":"305-320","source":"Crossref","is-referenced-by-count":36,"title":["Falsification of LTL safety properties in hybrid systems"],"prefix":"10.1007","volume":"15","author":[{"given":"Erion","family":"Plaku","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lydia E.","family":"Kavraki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,5,23]]},"reference":[{"issue":"7","key":"233_CR1","doi-asserted-by":"crossref","first-page":"986","DOI":"10.1109\/JPROC.2003.814621","volume":"91","author":"C.J. Tomlin","year":"2003","unstructured":"Tomlin C.J., Mitchell I., Bayen A., Oishi M.: Computational techniques for the verification and control of hybrid systems. Proc. IEEE 91(7), 986\u20131001 (2003)","journal-title":"Proc. IEEE"},{"issue":"1","key":"233_CR2","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 T.A., Ho P.H., Nicollin X., Olivero A., Sifakis J., Yovine S.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"233_CR3","doi-asserted-by":"crossref","unstructured":"Henzinger, T., Kopke, P., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? In: ACM Symp on Theory of Computing, pp. 373\u2013382 (1995)","DOI":"10.1145\/225058.225162"},{"issue":"1","key":"233_CR4","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/TAC.2002.806655","volume":"48","author":"C. Chutinan","year":"2003","unstructured":"Chutinan C., Krogh B.H.: Computational techniques for hybrid system verification. IEEE Trans. Autom. Control 48(1), 64\u201375 (2003)","journal-title":"IEEE Trans. Autom. Control"},{"key":"233_CR5","doi-asserted-by":"crossref","unstructured":"Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Hybrid Systems: Computation and Control. LNCS, vol. 4416, pp. 428\u2013443 (2007)","DOI":"10.1007\/978-3-540-71493-4_34"},{"issue":"7","key":"233_CR6","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R. Alur","year":"2000","unstructured":"Alur R., Henzinger T.A., Lafferriere G., Pappas G.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971\u2013984 (2000)","journal-title":"Proc. IEEE"},{"issue":"4","key":"233_CR7","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1142\/S012905410300190X","volume":"14","author":"E. Clarke","year":"2003","unstructured":"Clarke E., Fehnker A., Han Z., Krogh B., Ouaknine J., Stursberg O., Theobald M.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Int. J. Found. Comput. Sci. 14(4), 583\u2013604 (2003)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"233_CR8","doi-asserted-by":"crossref","unstructured":"Giorgetti, N., Pappas, G.J., Bemporad, A.: Bounded model checking for hybrid dynamical systems. In: Conference on Decision and Control, Seville, Spain, pp. 672\u2013677 (2005)","DOI":"10.1109\/CDC.2005.1582233"},{"issue":"1","key":"233_CR9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1016\/0304-3975(94)00147-B","volume":"138","author":"M. Branicky","year":"1995","unstructured":"Branicky M.: Universal computation and other capabilities of continuous and hybrid systems. Theor. Comput. Sci. 138(1), 67\u2013100 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"233_CR10","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1049\/ip-cta:20050152","volume":"153","author":"M.S. Branicky","year":"2006","unstructured":"Branicky M.S., Curtiss M.M., Levine J., Morgan S.: Sampling-based planning, control, and verification of hybrid systems. IEE Proc. Control Theory Appl. 153(5), 575\u2013590 (2006)","journal-title":"IEE Proc. Control Theory Appl."},{"key":"233_CR11","doi-asserted-by":"crossref","unstructured":"Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Hybrid Systems: Computation and Control. LNCS, vol. 2993, pp. 142\u2013156 (2004)","DOI":"10.1007\/978-3-540-24743-2_10"},{"key":"233_CR12","doi-asserted-by":"crossref","unstructured":"Esposito, J.M., Kim, J., Kumar, V.: Adaptive RRTs for validating hybrid robotic control systems. In: Workshop on Algorithmic Foundations of Robotics, Zeist, Netherlands, pp. 107\u2013132 (2004)","DOI":"10.1007\/10991541_9"},{"key":"233_CR13","doi-asserted-by":"crossref","unstructured":"Kim, J., Esposito, J.M., Kumar, V.: An RRT-based algorithm for testing and validating multi-robot controllers. In: Robotics: Science and Systems, Boston, pp. 249\u2013256 (2005)","DOI":"10.15607\/RSS.2005.I.033"},{"issue":"2","key":"233_CR14","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/s10703-009-0066-0","volume":"34","author":"T. Nahhal","year":"2009","unstructured":"Nahhal T., Dang T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Des. 34(2), 183\u2013213 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"233_CR15","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification. In: International Conference on Computer Aided Verification. LNCS, vol. 4590, pp. 468\u2013481 (2007)"},{"issue":"2","key":"233_CR16","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/s10703-008-0058-5","volume":"34","author":"E. Plaku","year":"2009","unstructured":"Plaku E., Kavraki L.E., Vardi M.Y.: Hybrid systems: from verification to falsification by combining motion planning and discrete search. Formal Methods Syst. Des. 34(2), 157\u2013182 (2009)","journal-title":"Formal Methods Syst. Des."},{"key":"233_CR17","doi-asserted-by":"crossref","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.: Benefits of bounded model checking at an industrial setting. In: International Conference on Computer Aided Verification. LNCS, vol. 2102, pp. 436\u2013453 (2001)","DOI":"10.1007\/3-540-44585-4_43"},{"issue":"11\u201312","key":"233_CR18","doi-asserted-by":"crossref","first-page":"1232","DOI":"10.1177\/0278364908097582","volume":"27","author":"P. Cheng","year":"2008","unstructured":"Cheng P., Kumar V.: Sampling-based falsification and verification of controllers for continuous dynamic systems. Int. J. Robot. Res. 27(11\u201312), 1232\u20131245 (2008)","journal-title":"Int. J. Robot. Res."},{"key":"233_CR19","doi-asserted-by":"crossref","unstructured":"Bhatia, A., Frazzoli, E.: Sampling-based resolution-complete safety falsification of linear hybrid systems. In: IEEE Conference on Decision and Control, New Orleans, pp. 3405\u20133411 (2007)","DOI":"10.1109\/CDC.2007.4434542"},{"key":"233_CR20","doi-asserted-by":"crossref","unstructured":"Bhatia, A., Frazzoli, E.: Sampling-based resolution-complete algorithms for safety falsification of linear systems. In: Hybrid Systems: Computation and Control. LNCS, vol. 4981, pp. 606\u2013609 (2008)","DOI":"10.1007\/978-3-540-78929-1_45"},{"issue":"5","key":"233_CR21","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1177\/02783640122067453","volume":"20","author":"S.M. LaValle","year":"2001","unstructured":"LaValle S.M., Kuffner J.J.: Randomized kinodynamic planning. Int. J. Robot. Res. 20(5), 378\u2013400 (2001)","journal-title":"Int. J. Robot. Res."},{"key":"233_CR22","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke E., Grumberg O., Peled D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"233_CR23","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Mller, O., Pettersson, P., Yi, W.: Uppaal\u2014present and future. In: Conference on Decision and Control, Orlando, Florida, pp. 2881\u20132886 (2001)","DOI":"10.1109\/CDC.2001.980713"},{"issue":"2","key":"233_CR24","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/j.automatica.2008.08.008","volume":"45","author":"G.E. Fainekos","year":"2009","unstructured":"Fainekos G.E., Girard A., Kress-Gazit H., Pappas G.J.: Temporal logic motion planning for dynamic mobile robots. Automatica 45(2), 343\u2013352 (2009)","journal-title":"Automatica"},{"key":"233_CR25","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Kress-Gazit, H., Pappas, G.: Temporal logic motion planning for mobile robots. In: IEEE International Conference on Robotics and Automation, Barcelona, Spain, pp. 2020\u20132025 (2005)","DOI":"10.1109\/ROBOT.2005.1570410"},{"issue":"1","key":"233_CR26","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1109\/TAC.2007.914952","volume":"53","author":"M. Kloetzer","year":"2008","unstructured":"Kloetzer M., Belta C.: A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Autom. Control 53(1), 287\u2013297 (2008)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"6","key":"233_CR27","doi-asserted-by":"crossref","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H. Kress-Gazit","year":"2009","unstructured":"Kress-Gazit H., Fainekos G., Pappas G.J.: Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robot. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Robot."},{"key":"233_CR28","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Topcu, U., Murray, R.M.: Receding horizon temporal logic planning for dynamical systems. In: IEEE Conference on Decision and Control, Shanghai, China, pp. 5997\u20136004 (2009)","DOI":"10.1109\/CDC.2009.5399536"},{"issue":"2","key":"233_CR29","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1109\/TRO.2006.889492","volume":"23","author":"M. Kloetzer","year":"2007","unstructured":"Kloetzer M., Belta C.: Temporal logic planning and control of robotic swarms by hierarchical abstractions. IEEE Trans. Robot. 23(2), 320\u2013331 (2007)","journal-title":"IEEE Trans. Robot."},{"key":"233_CR30","doi-asserted-by":"crossref","first-page":"215","DOI":"10.1109\/TAC.2007.911330","volume":"53","author":"G. Batt","year":"2008","unstructured":"Batt G., Belta C., Weiss R.: Temporal logic analysis of gene networks under parameter uncertainty. IEEE Trans. Autom. Control 53, 215\u2013229 (2008)","journal-title":"IEEE Trans. Autom. Control"},{"issue":"1","key":"233_CR31","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1142\/S0129054107004577","volume":"18","author":"W. Damm","year":"2007","unstructured":"Damm W., Pinto G., Ratschan S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. Int. J. Found. Comput. Sci. 18(1), 63\u201386 (2007)","journal-title":"Int. J. Found. Comput. Sci."},{"issue":"3","key":"233_CR32","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O. Kupferman","year":"2001","unstructured":"Kupferman O., Vardi M.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"233_CR33","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1007\/BF01211865","volume":"6","author":"A. Sistla","year":"1994","unstructured":"Sistla A.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6, 495\u2013511 (1994)","journal-title":"Formal Aspects Comput."},{"key":"233_CR34","doi-asserted-by":"crossref","unstructured":"Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Hybrid Systems: Computation and Control. LNCS, vol. 2993, pp. 326\u2013341 (2004)","DOI":"10.1007\/978-3-540-24743-2_22"},{"key":"233_CR35","doi-asserted-by":"crossref","unstructured":"Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi, M.: Efficient LTL compilation for SAT-based model checking. In: International Conference on Computer-Aided Design, San Jose, pp. 877\u2013884 (2005)","DOI":"10.1109\/ICCAD.2005.1560185"},{"key":"233_CR36","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern B., Schneider F.: Recognizing safety and liveness. Distrib. Comput. 2, 117\u2013126 (1987)","journal-title":"Distrib. Comput."},{"key":"233_CR37","volume-title":"Principles of Robot Motion: Theory, Algorithms, and Implementations","author":"H. Choset","year":"2005","unstructured":"Choset H., Lynch K.M., Hutchinson S., Kantor G., Burgard W., Kavraki L.E., Thrun S.: Principles of Robot Motion: Theory, Algorithms, and Implementations. MIT Press, Cambridge (2005)"},{"key":"233_CR38","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511546877","volume-title":"Planning Algorithms","author":"S.M. LaValle","year":"2006","unstructured":"LaValle S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)"},{"key":"233_CR39","doi-asserted-by":"crossref","unstructured":"Esposito, J., Kumar, V., Pappas, G.: Accurate event detection for simulation of hybrid systems. In: Hybrid Systems: Computation and Control. LNCS, pp. 204\u2013217 (2001)","DOI":"10.1007\/3-540-45351-2_19"},{"key":"233_CR40","doi-asserted-by":"crossref","unstructured":"Julius, A.A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Hybrid Systems: Computation and Control. LNCS, vol. 4416, pp. 329\u2013342 (2007)","DOI":"10.1007\/978-3-540-71493-4_27"},{"key":"233_CR41","doi-asserted-by":"crossref","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Discrete search leading continuous exploration for kinodynamic motion planning. In: Robotics: Science and Systems, Atlanta, Georgia, pp. 326\u2013333 (2007)","DOI":"10.15607\/RSS.2007.III.040"},{"key":"233_CR42","doi-asserted-by":"crossref","unstructured":"Latvala, T.: Efficient model checking of safety properties. In Ball, T., Rajamani, S., (eds.) Model Checking Software. LNCS, vol. 2648, pp. 74\u201388 (2003)","DOI":"10.1007\/3-540-44829-2_5"},{"key":"233_CR43","unstructured":"Ladd, A.M.: Motion planning for physical simulation. PhD thesis, Rice University, Houston (2006)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0233-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0233-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0233-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:19:53Z","timestamp":1743697193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0233-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,5,23]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,8]]}},"alternative-id":["233"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0233-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,5,23]]}}}