{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,20]],"date-time":"2024-09-20T16:31:26Z","timestamp":1726849886890},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030206512"},{"type":"electronic","value":"9783030206529"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-20652-9_12","type":"book-chapter","created":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:03:25Z","timestamp":1558998205000},"page":"186-203","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Towards a Two-Layer Framework for Verifying Autonomous Vehicles"],"prefix":"10.1007","author":[{"given":"Rong","family":"Gu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raluca","family":"Marinescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cristina","family":"Seceleanu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kristina","family":"Lundqvist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,5,28]]},"reference":[{"issue":"3","key":"12_CR1","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/MRA.2011.942115","volume":"18","author":"A Bhatia","year":"2011","unstructured":"Bhatia, A., Maly, M.R., Kavraki, L.E., Vardi, M.Y.: Motion planning with complex goals. IEEE Rob. Autom. Mag. 18(3), 55\u201364 (2011)","journal-title":"IEEE Rob. Autom. Mag."},{"key":"12_CR2","first-page":"2012","volume":"18","author":"PE Black","year":"2006","unstructured":"Black, P.E.: Manhattan distance. Dictionary Algorithms Data Struct. 18, 2012 (2006)","journal-title":"Dictionary Algorithms Data Struct."},{"issue":"2","key":"12_CR3","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"RH Bordini","year":"2006","unstructured":"Bordini, R.H., Fisher, M., Visser, W., Wooldridge, M.: Verifying multi-agent programs by model checking. Auton. Agent. Multi-Agent Syst. 12(2), 239\u2013256 (2006)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"issue":"1","key":"12_CR4","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1109\/9.654885","volume":"43","author":"MS Branicky","year":"1998","unstructured":"Branicky, M.S., Borkar, V.S., Mitter, S.K.: A unified framework for hybrid control: model and optimal control theory. IEEE Trans. Autom. Control 43(1), 31\u201345 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-28717-6_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P Bulychev","year":"2012","unstructured":"Bulychev, P., et al.: Monitor-based statistical model checking for weighted metric temporal logic. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 168\u2013182. Springer, Heidelberg (2012). \n                    https:\/\/doi.org\/10.1007\/978-3-642-28717-6_15"},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"533","DOI":"10.1613\/jair.2994","volume":"39","author":"K Daniel","year":"2010","unstructured":"Daniel, K., Nash, A., Koenig, S., Felner, A.: Theta*: any-angle path planning on grids. J. Artif. Intell. Res. 39, 533\u2013579 (2010)","journal-title":"J. Artif. Intell. Res."},{"key":"12_CR7","unstructured":"David, A., et al.: Statistical model checking for stochastic hybrid systems. arXiv preprint \n                    arXiv:1208.3856\n                    \n                   (2012)"},{"issue":"1","key":"12_CR8","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","volume":"19","author":"LA Dennis","year":"2012","unstructured":"Dennis, L.A., Fisher, M., Webster, M.P., Bordini, R.H.: Model checking agent programming languages. Autom. Softw. Eng. 19(1), 5\u201363 (2012)","journal-title":"Autom. Softw. Eng."},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-319-67531-2_11","volume-title":"Runtime Verification","author":"A Desai","year":"2017","unstructured":"Desai, A., Dreossi, T., Seshia, S.A.: Combining model checking and runtime verification for safe robotics. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 172\u2013189. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-67531-2_11"},{"key":"12_CR10","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, pp. 239\u2013248. ACM (2017)","DOI":"10.1145\/3055004.3055022"},{"issue":"3","key":"12_CR11","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/s10458-009-9079-8","volume":"19","author":"P Doherty","year":"2009","unstructured":"Doherty, P., Kvarnstr\u00f6m, J., Heintz, F.: A temporal logic-based planning and execution monitoring framework for unmanned aircraft systems. Auton. Agent. Multi-Agent Syst. 19(3), 332\u2013377 (2009)","journal-title":"Auton. Agent. Multi-Agent Syst."},{"key":"12_CR12","unstructured":"Fainekos, G.E., Kress-Gazit, H., Pappas, G.J.: Temporal logic motion planning for mobile robots. In: Proceedings of the 2005 IEEE International Conference on Robotics and Automation, ICRA 2005, pp. 2020\u20132025. IEEE (2005)"},{"issue":"1","key":"12_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1111\/j.1467-8640.2007.00295.x","volume":"23","author":"M Fisher","year":"2007","unstructured":"Fisher, M., Bordini, R.H., Hirsch, B., Torroni, P.: Computational logics and agents: a road map of current technologies and future trends. Comput. Intell. 23(1), 61\u201391 (2007)","journal-title":"Comput. Intell."},{"issue":"9","key":"12_CR14","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/2500468.2494558","volume":"56","author":"M Fisher","year":"2013","unstructured":"Fisher, M., Dennis, L., Webster, M.: Verifying autonomous systems. Commun. ACM 56(9), 84\u201393 (2013)","journal-title":"Commun. ACM"},{"key":"12_CR15","unstructured":"Gat, E., Slack, M.G., Miller, D.P., Firby, R.J.: Path planning and execution monitoring for a planetary rover. In: Proceedings of the IEEE International Conference on Robotics and Automation, pp. 20\u201325 (1990)"},{"issue":"3","key":"12_CR16","doi-asserted-by":"publisher","first-page":"1280","DOI":"10.1109\/LRA.2017.2665682","volume":"2","author":"Y Golan","year":"2017","unstructured":"Golan, Y., Edelman, S., Shapiro, A., Rimon, E.: Online robot navigation using continuously updated artificial temperature gradients. IEEE Rob. Autom. Lett. 2(3), 1280\u20131287 (2017)","journal-title":"IEEE Rob. Autom. Lett."},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Gu, R., Marinescu, R., Seceleanu, C., Lundqvist, K.: Formal verification of an autonomous wheel loader by model checking. In: Proceedings of the 6th Conference on Formal Methods in Software Engineering, pp. 74\u201383. ACM (2018)","DOI":"10.1145\/3193992.3193999"},{"key":"12_CR18","doi-asserted-by":"crossref","unstructured":"Jafari, A., Nair, J.J.S., Baumgart, S., Sirjani, M.: Safe and efficient fleet operation for autonomous machines: an actor-based approach. In: Proceedings of the 33rd Annual ACM Symposium on Applied Computing, pp. 423\u2013426. ACM (2018)","DOI":"10.1145\/3167132.3167382"},{"key":"12_CR19","doi-asserted-by":"crossref","unstructured":"Ke, X., Sierszecki, K., Angelov, C.: COMDES-II: a component-based framework for generative development of distributed real-time control systems. In: 13th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications, pp. 199\u2013208. IEEE (2007)","DOI":"10.1109\/RTCSA.2007.29"},{"issue":"4","key":"12_CR20","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1007\/s10626-013-0162-6","volume":"24","author":"M Kloetzer","year":"2014","unstructured":"Kloetzer, M., Mahulea, C.: A petri net based approach for multi-robot path planning. Discrete Event Dyn. Syst. 24(4), 417\u2013445 (2014)","journal-title":"Discrete Event Dyn. Syst."},{"issue":"1\u20132","key":"12_CR21","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132), 134\u2013152 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"12_CR22","volume-title":"Introduction to Embedded Systems: A Cyber-Physical Systems Approach","author":"EA Lee","year":"2016","unstructured":"Lee, E.A., Seshia, S.A.: Introduction to Embedded Systems: A Cyber-Physical Systems Approach. MIT Press, Cambridge (2016)"},{"key":"12_CR23","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":"12_CR24","doi-asserted-by":"crossref","unstructured":"Luo, C., et al.: Runtime verification of robots collision avoidance case study. In: 2018 IEEE 42nd Annual Computer Software and Applications Conference (COMPSAC), pp. 204\u2013212. IEEE (2018)","DOI":"10.1109\/COMPSAC.2018.00033"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Miloradovi\u0107, B., C\u00fcr\u00fckl\u00fc, B., Ekstr\u00f6m, M., Papadopoulos, A.: Extended colored traveling salesperson for modeling multi-agent mission planning problems. In: Proceedings of the 8th International Conference on Operations Research and Enterprise Systems - Volume 1, ICORES, pp. 237\u2013244, INSTICC. SciTePress (2019). \n                    https:\/\/doi.org\/10.5220\/0007309002370244","DOI":"10.5220\/0007309002370244"},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Quottrup, M.M., Bak, T., Zamanabadi, R.: Multi-robot planning: a timed automata approach. In: 2004 IEEE International Conference on Robotics and Automation, Proceedings, ICRA 2004, vol. 5, pp. 4417\u20134422. IEEE (2004)","DOI":"10.1109\/ROBOT.2004.1302413"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Sirigineedi, G., Tsourdos, A., White, B.A., Zbikowski, R.: Modelling and verification of multiple UAV mission using SMV. arXiv preprint \n                    arXiv:1003.0381\n                    \n                   (2010)","DOI":"10.4204\/EPTCS.20.3"},{"issue":"14","key":"12_CR28","doi-asserted-by":"publisher","first-page":"1695","DOI":"10.1177\/0278364911417911","volume":"30","author":"SL Smith","year":"2011","unstructured":"Smith, S.L., Tumova, J., Belta, C., Rus, D.: Optimal path planning for surveillance with temporal-logic constraints. Int. J. Rob. Res. 30(14), 1695\u20131708 (2011)","journal-title":"Int. J. Rob. Res."},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Trinh, L.A., Ekstr\u00f6m, M., C\u00fcr\u00fckl\u00fc, B.: Toward shared working space of human and robotic agents through dipole flow field for dependable path planning. Front. Neurorob. 12 (2018)","DOI":"10.3389\/fnbot.2018.00028"},{"issue":"3\u20134","key":"12_CR30","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10846-012-9685-6","volume":"68","author":"L Valbuena","year":"2012","unstructured":"Valbuena, L., Tanner, H.G.: Hybrid potential field based control of differential drive mobile robots. J. Intell. Rob. Syst. 68(3\u20134), 307\u2013322 (2012)","journal-title":"J. Intell. Rob. Syst."}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-20652-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T23:15:32Z","timestamp":1558998932000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-20652-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030206512","9783030206529"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-20652-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 May 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Houston, TX","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 May 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 May 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/robonaut.jsc.nasa.gov\/R2\/pages\/nfm2019.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}