{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,20]],"date-time":"2026-07-20T18:32:29Z","timestamp":1784572349369,"version":"3.55.0"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319675305","type":"print"},{"value":"9783319675312","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-67531-2_11","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:33:37Z","timestamp":1504604017000},"page":"172-189","source":"Crossref","is-referenced-by-count":61,"title":["Combining Model Checking and Runtime Verification for Safe Robotics"],"prefix":"10.1007","author":[{"given":"Ankush","family":"Desai","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tommaso","family":"Dreossi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Marino, A., Parker, L., Antonelli, G., Caccavale, F.: Behavioral control for multi-robot perimeter patrol: a finite state automata approach. In: International Conference on Robotics and Automation, ICRA, pp. 831\u2013836. IEEE (2009)","DOI":"10.1109\/ROBOT.2009.5152710"},{"issue":"5","key":"11_CR2","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1002\/rob.20403","volume":"28","author":"A Barrientos","year":"2011","unstructured":"Barrientos, A., Colorado, J., del Cerro, J., Martinez, A., Rossi, C., Sanz, D., Valente, J.: Aerial remote sensing in agriculture: a practical approach to area coverage and path planning for fleets of mini aerial robots. J. Field Robot. 28(5), 667\u2013689 (2011)","journal-title":"J. Field Robot."},{"issue":"2","key":"11_CR3","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1109\/TASE.2014.2376492","volume":"12","author":"B Kehoe","year":"2015","unstructured":"Kehoe, B., Patil, S., Abbeel, P., Goldberg, K.: A survey of research on cloud robotics and automation. IEEE Trans. Autom. Sci. Eng. 12(2), 398\u2013409 (2015)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"1","key":"11_CR4","first-page":"1","volume":"15","author":"VK Omachonu","year":"2010","unstructured":"Omachonu, V.K., Einspruch, N.G.: Innovation in healthcare delivery systems: a conceptual framework. Publ. Sect. Innov. J. 15(1), 1\u201320 (2010)","journal-title":"Publ. Sect. Innov. J."},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Yamaguchi, T., Kaga, T., Donz\u00e9, A., Seshia, S.A.: Combining requirement mining, software model checking, and simulation-based verification for industrial automotive systems. In: Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2016","DOI":"10.1109\/FMCAD.2016.7886680"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Desai, A., Gupta, V., Jackson, E., Qadeer, S., Rajamani, S., Zufferey, D.: P: safe asynchronous event-driven programming. In: Programming Language Design and Implementation (PLDI), pp. 321\u2013332 (2013)","DOI":"10.1145\/2491956.2462184"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-540-30206-3_12","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"O Maler","year":"2004","unstructured":"Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS\/FTRTFT -2004. LNCS, vol. 3253, pp. 152\u2013166. Springer, Heidelberg (2004). doi:\n10.1007\/978-3-540-30206-3_12"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Koenig, N., Howard, A.: Design and use paradigms for gazebo, an open-source multi-robot simulator. In: Intelligent Robots and Systems, IROS, vol. 3, pp. 2149\u20132154. IEEE (2004)","DOI":"10.1109\/IROS.2004.1389727"},{"key":"11_CR9","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511546877","volume-title":"Planning Algorithms","author":"SM LaValle","year":"2006","unstructured":"LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Mellinger, D., Kumar, V.: Minimum snap trajectory generation and control for quadrotors. In: International Conference on Robotics and Automation (ICRA), pp. 2520\u20132525 (2011)","DOI":"10.1109\/ICRA.2011.5980409"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Automated composition of motion primitives for multi-robot systems from safe ltl specifications. In: Intelligent Robots and Systems, IROS, pp. 1525\u20131532. IEEE (2014)","DOI":"10.1109\/IROS.2014.6942758"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Desai, A., Saha, I., Yang, J., Qadeer, S., Seshia, S.A.: Drona: a framework for safe distributed mobile robotics. In: Proceedings of the 8th International Conference on Cyber-Physical Systems, ICCPS 2017, pp. 239\u2013248. ACM, New York (2017)","DOI":"10.1145\/3055004.3055022"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Karaman, S., Frazzoli, E.: Incremental sampling-based algorithms for optimal motion planning. In: Robotics Science and Systems VI, vol. 104 (2010)","DOI":"10.15607\/RSS.2010.VI.034"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Model checking for programming languages using verisoft. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174\u2013186. ACM (1997)","DOI":"10.1145\/263699.263717"},{"key":"11_CR15","volume-title":"Applied Linear Statistical Models","author":"J Neter","year":"1996","unstructured":"Neter, J., Kutner, M.H., Nachtsheim, C.J., Wasserman, W.: Applied Linear Statistical Models, vol. 4. Irwin, Chicago (1996)"},{"issue":"3","key":"11_CR16","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s10009-012-0247-9","volume":"15","author":"O Maler","year":"2013","unstructured":"Maler, O., Ni\u010dkovi\u0107, D.: Monitoring properties of analog and mixed-signal circuits. Int. J. Softw. Tools Technol. Transf. 15(3), 247\u2013268 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-319-11164-3_15","volume-title":"Runtime Verification","author":"H-M Ho","year":"2014","unstructured":"Ho, H.-M., Ouaknine, J., Worrell, J.: Online monitoring of metric temporal logic. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 178\u2013192. Springer, Cham (2014). doi:\n10.1007\/978-3-319-11164-3_15"},{"key":"11_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-11164-3_19","volume-title":"Runtime Verification","author":"A Dokhanchi","year":"2014","unstructured":"Dokhanchi, A., Hoxha, B., Fainekos, G.: On-line monitoring for temporal logic robustness. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 231\u2013246. Springer, Cham (2014). doi:\n10.1007\/978-3-319-11164-3_19"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-23820-3_4","volume-title":"Runtime Verification","author":"JV Deshmukh","year":"2015","unstructured":"Deshmukh, J.V., Donz\u00e9, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. In: Bartocci, E., Majumdar, R. (eds.) RV 2015. LNCS, vol. 9333, pp. 55\u201370. Springer, Cham (2015). doi:\n10.1007\/978-3-319-23820-3_4"},{"key":"11_CR20","unstructured":"P Github (2017). \nhttps:\/\/github.com\/p-org\/P"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"Desai, A., Qadeer, S., Seshia, S.A.: Systematic testing of asynchronous reactive systems. In: Foundations of Software Engineering (FSE), pp. 73\u201383 (2015)","DOI":"10.1145\/2786805.2786861"},{"key":"11_CR22","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1109\/MRA.2012.2205651","volume":"19","author":"IA \u015eucan","year":"2012","unstructured":"\u015eucan, I.A., Moll, M., Kavraki, L.E.: The open motion planning library. IEEE Robot. Autom. Mag. 19, 72\u201382 (2012). \nhttp:\/\/ompl.kavrakilab.org","journal-title":"IEEE Robot. Autom. Mag."},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-14295-6_17","volume-title":"Computer Aided Verification","author":"A Donz\u00e9","year":"2010","unstructured":"Donz\u00e9, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167\u2013170. Springer, Heidelberg (2010). doi:\n10.1007\/978-3-642-14295-6_17"},{"key":"11_CR24","unstructured":"3D Robotics (2017). \nhttps:\/\/3dr.com\/"},{"key":"11_CR25","unstructured":"PX4 Autopilot (2017). \nhttps:\/\/pixhawk.org\/"},{"issue":"3","key":"11_CR26","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"issue":"6","key":"11_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.E., 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":"11_CR28","doi-asserted-by":"crossref","unstructured":"Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Implan: scalable incremental motion planning for multi-robot systems. In: International Conference on Cyber-Physical Systems (ICCPS), pp. 1\u201310. IEEE (2016)","DOI":"10.1109\/ICCPS.2016.7479105"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Fainekos, G.E., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for mobile robots. In: International Conference on Robotics and Automation, ICRA, pp. 2020\u20132025. IEEE (2005)","DOI":"10.1109\/ROBOT.2005.1570410"},{"issue":"2","key":"11_CR30","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/j.automatica.2008.08.008","volume":"45","author":"GE Fainekos","year":"2009","unstructured":"Fainekos, G.E., Girard, A., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for dynamic robots. Automatica 45(2), 343\u2013352 (2009)","journal-title":"Automatica"},{"key":"11_CR31","doi-asserted-by":"crossref","unstructured":"Saha, I., Ramaithitima, R., Kumar, V., Pappas, G.J., Seshia, S.A.: Automated composition of motion primitives for multi-robot systems from safe ltl specifications. In: International Conference on Intelligent Robots and Systems (IROS), pp. 1525\u20131532. IEEE (2014)","DOI":"10.1109\/IROS.2014.6942758"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22110-1_30"},{"key":"11_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-39799-8_18"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Dreossi, T.: Sapo: reachability computation and parameter synthesis of polynomial dynamical systems. In: Hybrid Systems: Computation and Control, HSCC, HSCC 2017, pp. 29\u201334 (2017)","DOI":"10.1145\/3049797.3049824"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-662-46681-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"PS Duggirala","year":"2015","unstructured":"Duggirala, P.S., Mitra, S., Viswanathan, M., Potok, M.: C2E2: a verification tool for stateflow models. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 68\u201382. Springer, Heidelberg (2015). doi:\n10.1007\/978-3-662-46681-0_5"},{"key":"11_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-17524-9_10","volume-title":"NASA Formal Methods","author":"T Dreossi","year":"2015","unstructured":"Dreossi, T., Dang, T., Donz\u00e9, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 127\u2013142. Springer, Cham (2015). doi:\n10.1007\/978-3-319-17524-9_10"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-642-19835-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Annpureddy","year":"2011","unstructured":"Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254\u2013257. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-19835-9_21"},{"key":"11_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing monitors for safety properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 342\u2013356. Springer, Heidelberg (2002). doi:\n10.1007\/3-540-46002-0_24"},{"key":"11_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-642-29860-8_15","volume-title":"Runtime Verification","author":"SD Stoller","year":"2012","unstructured":"Stoller, S.D., Bartocci, E., Seyster, J., Grosu, R., Havelund, K., Smolka, S.A., Zadok, E.: Runtime verification with state estimation. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 193\u2013207. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-29860-8_15"},{"key":"11_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-35632-2_18","volume-title":"Runtime Verification","author":"E Bartocci","year":"2013","unstructured":"Bartocci, E., Grosu, R., Karmarkar, A., Smolka, S.A., Stoller, S.D., Zadok, E., Seyster, J.: Adaptive runtime verification. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 168\u2013182. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-35632-2_18"},{"key":"11_CR41","doi-asserted-by":"crossref","unstructured":"Gat, E., Slack, M.G., Miller, D.P., Firby, R.J.: Path planning and execution monitoring for a planetary rover. In: Robotics and Automation, pp. 20\u201325. IEEE (1990)","DOI":"10.1109\/ROBOT.1990.125939"},{"issue":"2","key":"11_CR42","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/j.robot.2005.09.004","volume":"53","author":"O Pettersson","year":"2005","unstructured":"Pettersson, O.: Execution monitoring in robotics: a survey. Robot. Auton. Syst. 53(2), 73\u201388 (2005)","journal-title":"Robot. Auton. Syst."},{"key":"11_CR43","doi-asserted-by":"crossref","unstructured":"Lotz, A., Steck, A., Schlegel, C.: Runtime monitoring of robotics software components: increasing robustness of service robotic systems. In: 2011 15th International Conference on Advanced Robotics (ICAR), pp. 285\u2013290. IEEE (2011)","DOI":"10.1109\/ICAR.2011.6088591"},{"key":"11_CR44","unstructured":"Lee, I., Ben-Abdallah, H., Kannan, S., Kim, M., Sokolsky, O., Viswanathan, M.: A monitoring and checking framework for run-time correctness assurance (1998)"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:36:35Z","timestamp":1504604195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}