{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T18:40:17Z","timestamp":1739040017587,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642007675"},{"type":"electronic","value":"9783642007682"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-00768-2_31","type":"book-chapter","created":{"date-parts":[[2009,3,27]],"date-time":"2009-03-27T01:16:10Z","timestamp":1238116570000},"page":"368-382","source":"Crossref","is-referenced-by-count":33,"title":["Falsification of LTL Safety Properties in Hybrid Systems"],"prefix":"10.1007","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","reference":[{"issue":"7","key":"31_CR1","doi-asserted-by":"publisher","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. of IEEE\u00a091(7), 986\u20131001 (2003)","journal-title":"Proc. of IEEE"},{"issue":"1","key":"31_CR2","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0138(1), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"31_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"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-540-71493-4_34","volume-title":"Hybrid Systems: Computation and Control","author":"I.M. Mitchell","year":"2007","unstructured":"Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 428\u2013443. Springer, Heidelberg (2007)"},{"issue":"7","key":"31_CR5","doi-asserted-by":"publisher","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. of IEEE\u00a088(7), 971\u2013984 (2000)","journal-title":"Proc. of IEEE"},{"issue":"4","key":"31_CR6","doi-asserted-by":"publisher","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. Intl. J. of Foundations of Computer Science\u00a014(4), 583\u2013604 (2003)","journal-title":"Intl. J. of Foundations of Computer Science"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"Giorgetti, N., Pappas, G.J., Bemporad, A.: Bounded model checking for hybrid dynamical systems. In: Conf. on Decision & Control, Seville, Spain, pp. 672\u2013677 (2005)","DOI":"10.1109\/CDC.2005.1582233"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 142\u2013156. Springer, Heidelberg (2004)"},{"key":"31_CR9","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 & Systems, Boston, MA, pp. 249\u2013256 (2005)","DOI":"10.15607\/RSS.2005.I.033"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-540-73368-3_47","volume-title":"Computer Aided Verification","author":"T. Nahhal","year":"2007","unstructured":"Nahhal, T., Dang, T.: Test coverage for continuous and hybrid systems. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 449\u2013462. Springer, Heidelberg (2007)"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-540-73368-3_48","volume-title":"Computer Aided Verification","author":"E. Plaku","year":"2007","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: From verification to falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 463\u2013476. Springer, Heidelberg (2007)"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: From verification to falsification by combining motion planning and discrete search. Formal Methods in System Design (2008)","DOI":"10.1007\/s10703-008-0058-5"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"issue":"5","key":"31_CR14","doi-asserted-by":"publisher","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. Intl. J. of Robotics Research\u00a020(5), 378\u2013400 (2001)","journal-title":"Intl. J. of Robotics Research"},{"key":"31_CR15","volume-title":"Model Checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., M\u00f6ller, O., Pettersson, P., Yi, W.: Uppaal present and future. In: Conf. on Decision & Control, Orlando, FL, pp. 2881\u20132886 (2001)","DOI":"10.1109\/CDC.2001.980713"},{"key":"31_CR17","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Kress-Gazit, H., Pappas, G.: Temporal logic motion planning for mobile robots. In: IEEE Intl. Conf. on Robotics & Automation, Barcelona, Spain, pp. 2020\u20132025 (2005)","DOI":"10.1109\/ROBOT.2005.1570410"},{"key":"31_CR18","doi-asserted-by":"publisher","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. of Automatic Control\u00a053, 215\u2013229 (2008)","journal-title":"IEEE Trans. of Automatic Control"},{"issue":"1","key":"31_CR19","doi-asserted-by":"publisher","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. Intl. J. of Foundations of Computer Science\u00a018(1), 63\u201386 (2007)","journal-title":"Intl. J. of Foundations of Computer Science"},{"issue":"3","key":"31_CR20","doi-asserted-by":"publisher","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 in System Design\u00a019(3), 291\u2013314 (2001)","journal-title":"Formal methods in System Design"},{"key":"31_CR21","doi-asserted-by":"crossref","unstructured":"Armoni, R., Egorov, S., Fraer, R., Korchemny, D., Vardi, M.: Efficient LTL compilation for SAT-based model checking. In: Intl. Conf. on Computer-Aided Design, San Jose, CA, pp. 877\u2013884 (2005)","DOI":"10.1109\/ICCAD.2005.1560185"},{"key":"31_CR22","doi-asserted-by":"publisher","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 of Computing\u00a06, 495\u2013511 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"31_CR23","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":"31_CR24","doi-asserted-by":"publisher","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":"31_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: Accurate event detection for simulation of hybrid systems. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 204\u2013217. Springer, Heidelberg (2001)"},{"key":"31_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-540-71493-4_27","volume-title":"Hybrid Systems: Computation and Control","author":"A.A. Julius","year":"2007","unstructured":"Julius, A.A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 329\u2013342. Springer, Heidelberg (2007)"},{"key":"31_CR27","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 & Systems, Atlanta, GA (2007)","DOI":"10.15607\/RSS.2007.III.040"},{"key":"31_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 326\u2013341. Springer, Heidelberg (2004)"},{"key":"31_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-44829-2_5","volume-title":"Model Checking Software","author":"T. Latvala","year":"2003","unstructured":"Latvala, T.: Efficient model checking of safety properties. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 74\u201388. Springer, Heidelberg (2003)"},{"key":"31_CR30","unstructured":"Ladd, A.M.: Motion Planning for Physical Simulation. PhD thesis, Rice University, Houston, TX (2006)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-00768-2_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,8]],"date-time":"2025-02-08T18:24:45Z","timestamp":1739039085000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-00768-2_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642007675","9783642007682"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-00768-2_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}