{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,31]],"date-time":"2026-07-31T02:35:53Z","timestamp":1785465353641,"version":"3.56.0"},"reference-count":185,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T00:00:00Z","timestamp":1568332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/R026084,EP\/R026173, EP\/R026092"],"award-info":[{"award-number":["EP\/R026084,EP\/R026173, EP\/R026092"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Comput. Surv."],"published-print":{"date-parts":[[2020,9,30]]},"abstract":"<jats:p>Autonomous robotic systems are complex, hybrid, and often safety critical; this makes their formal specification and verification uniquely challenging. Though commonly used, testing and simulation alone are insufficient to ensure the correctness of, or provide sufficient evidence for the certification of, autonomous robotics. Formal methods for autonomous robotics have received some attention in the literature, but no resource provides a current overview. This article systematically surveys the state of the art in formal specification and verification for autonomous robotics. Specially, it identifies and categorizes the challenges posed by, the formalisms aimed at, and the formal approaches for the specification and verification of autonomous robotics.<\/jats:p>","DOI":"10.1145\/3342355","type":"journal-article","created":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T12:28:56Z","timestamp":1568377736000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":248,"title":["Formal Specification and Verification of Autonomous Robotic Systems"],"prefix":"10.1145","volume":"52","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6444-9312","authenticated-orcid":false,"given":"Matt","family":"Luckcuck","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7708-3877","authenticated-orcid":false,"given":"Marie","family":"Farrell","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Louise A.","family":"Dennis","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0875-3862","authenticated-orcid":false,"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Liverpool, Liverpool, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,9,13]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2012.09.005"},{"key":"e_1_2_1_2_1","volume-title":"Modeling in Event-B: System and Software Engineering","author":"Abrial Jean-Raymond","unstructured":"Jean-Raymond Abrial . 2010. Modeling in Event-B: System and Software Engineering . Cambridge University Press . 1--586 pages. Jean-Raymond Abrial. 2010. Modeling in Event-B: System and Software Engineering. Cambridge University Press. 1--586 pages."},{"key":"e_1_2_1_3_1","first-page":"120","article-title":"Rule-based dynamic safety monitoring for mobile robots","author":"Adam Sorin","year":"2016","unstructured":"Sorin Adam , Morten Larsen , Kjeld Jensen , and Ulrik Pagh Schultz . 2016 . Rule-based dynamic safety monitoring for mobile robots . J. Softw. Eng. Robot. 7 , July (2016), 120 -- 141 . Sorin Adam, Morten Larsen, Kjeld Jensen, and Ulrik Pagh Schultz. 2016. Rule-based dynamic safety monitoring for mobile robots. J. Softw. Eng. Robot. 7, July (2016), 120--141.","journal-title":"J. Softw. Eng. Robot. 7"},{"key":"e_1_2_1_4_1","first-page":"120","article-title":"Rule-based dynamic safety monitoring for mobile robots","volume":"7","author":"Adam Sorin","year":"2016","unstructured":"Sorin Adam , Morten Larsen , Kjeld Jensen , and Ulrik Pagh Schultz . 2016 . Rule-based dynamic safety monitoring for mobile robots . J. Softw. Eng. Robot. 7 , 1 (2016), 120 -- 141 . Sorin Adam, Morten Larsen, Kjeld Jensen, and Ulrik Pagh Schultz. 2016. Rule-based dynamic safety monitoring for mobile robots. J. Softw. Eng. Robot. 7, 1 (2016), 120--141.","journal-title":"J. Softw. Eng. Robot."},{"key":"e_1_2_1_5_1","first-page":"45","article-title":"Design of a robotic software manager for using heterogeneous components of different frameworks","volume":"8","author":"Ahn Ho Seok","year":"2017","unstructured":"Ho Seok Ahn , Min Ho Lee , and Bruce MacDonald . 2017 . Design of a robotic software manager for using heterogeneous components of different frameworks . J. Softw. Eng. Robot. 8 , 1 (2017), 45 -- 64 . Ho Seok Ahn, Min Ho Lee, and Bruce MacDonald. 2017. Design of a robotic software manager for using heterogeneous components of different frameworks. J. Softw. Eng. Robot. 8, 1 (2017), 45--64.","journal-title":"J. Softw. Eng. Robot."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2006.08.005"},{"key":"e_1_2_1_7_1","first-page":"35","article-title":"Contribution to the formal specification and verification of a multi-agent robotic system","volume":"117","author":"Akhtar Nadeem","year":"2014","unstructured":"Nadeem Akhtar . 2014 . Contribution to the formal specification and verification of a multi-agent robotic system . Eur. J. Sci. Res. 117 , 1 (2014), 35 -- 55 . Retrieved from http:\/\/www.europeanjournalofscientificresearch.com. Nadeem Akhtar. 2014. Contribution to the formal specification and verification of a multi-agent robotic system. Eur. J. Sci. Res. 117, 1 (2014), 35--55. Retrieved from http:\/\/www.europeanjournalofscientificresearch.com.","journal-title":"Eur. J. Sci. Res."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1177\/027836499801700402"},{"key":"e_1_2_1_9_1","first-page":"85","article-title":"Provably safe motions strategies for mobile robots in dynamic domains. In Auton. Navig","volume":"35","author":"Alami Rachid","year":"2007","unstructured":"Rachid Alami , K. Madhava Krishna , and Thierry Sim\u00e9on . 2007 . Provably safe motions strategies for mobile robots in dynamic domains. In Auton. Navig . Dyn. Environ.STAR , Vol. 35. Spring er, 85 -- 106 . Rachid Alami, K. Madhava Krishna, and Thierry Sim\u00e9on. 2007. Provably safe motions strategies for mobile robots in dynamic domains. In Auton. Navig. Dyn. Environ.STAR, Vol. 35. Springer, 85--106.","journal-title":"Dyn. Environ.STAR"},{"key":"e_1_2_1_10_1","volume-title":"Robot. Autom","author":"Alexandrova Sonya","unstructured":"Sonya Alexandrova , Zachary Tatlock , and Maya Cakmak . 2015. RoboFlow: A flow-based visual programming language for mobile manipulation tasks . In Robot. Autom . IEEE , 5537--5544. Sonya Alexandrova, Zachary Tatlock, and Maya Cakmak. 2015. RoboFlow: A flow-based visual programming language for mobile manipulation tasks. In Robot. Autom. IEEE, 5537--5544."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.rcim.2009.12.001"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/IVS.2010.5548121"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89076-8_12"},{"key":"e_1_2_1_14_1","first-page":"79","article-title":"Towards the verification of safety-critical autonomous systems in dynamic environments","volume":"232","author":"Aniculaesei Adina","year":"2016","unstructured":"Adina Aniculaesei , Daniel Arnsberger , Falk Howar , and Andreas Rausch . 2016 . Towards the verification of safety-critical autonomous systems in dynamic environments . Theor. Comput. Sci. 232 (2016), 79 -- 90 . Adina Aniculaesei, Daniel Arnsberger, Falk Howar, and Andreas Rausch. 2016. Towards the verification of safety-critical autonomous systems in dynamic environments. Theor. Comput. Sci. 232 (2016), 79--90.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_2_1_15_1","volume-title":"Symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms (LNCS)","author":"Antu\u00f1a Laura","unstructured":"Laura Antu\u00f1a , Dejanira Araiza-Illan , S\u00e9rgio Campos , and Kerstin Eder . 2015. Symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms (LNCS) , Vol. 9287 . Springer , 26--37. Laura Antu\u00f1a, Dejanira Araiza-Illan, S\u00e9rgio Campos, and Kerstin Eder. 2015. Symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms (LNCS), Vol. 9287. Springer, 26--37."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2011.2173265"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2011.27"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.27"},{"key":"e_1_2_1_20_1","first-page":"631","article-title":"Incremental component-based construction and verification of a robotic system","volume":"178","author":"Basu Ananda","year":"2008","unstructured":"Ananda Basu , Matthieu Gallien , Charles Lesire , Thanh-Hung Nguyen , Saddek Bensalem , F\u00e9lix Ingrand , and Joseph Sifakis . 2008 . Incremental component-based construction and verification of a robotic system . In Front. Artif. Intell. Appl. , Vol. 178. 631 -- 635 . Ananda Basu, Matthieu Gallien, Charles Lesire, Thanh-Hung Nguyen, Saddek Bensalem, F\u00e9lix Ingrand, and Joseph Sifakis. 2008. Incremental component-based construction and verification of a robotic system. In Front. Artif. Intell. Appl., Vol. 178. 631--635.","journal-title":"Front. Artif. Intell. Appl."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0253-8"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2007.339624"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30552-1_1"},{"key":"e_1_2_1_24_1","volume-title":"Andreas Griesmayer, F\u00e9lix Ingrand, Axel Legay, and Rongjie Yan.","author":"Bensalem Saddek","year":"2011","unstructured":"Saddek Bensalem , Lavindra De Silva , Andreas Griesmayer, F\u00e9lix Ingrand, Axel Legay, and Rongjie Yan. 2011 . A formal approach for incremental construction with an application to autonomous robotic systems. In Softw. Compos. (LNCS), Vol. 6708 . Springer , 116--132. Saddek Bensalem, Lavindra De Silva, Andreas Griesmayer, F\u00e9lix Ingrand, Axel Legay, and Rongjie Yan. 2011. A formal approach for incremental construction with an application to autonomous robotic systems. In Softw. Compos. (LNCS), Vol. 6708. Springer, 116--132."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2008.931631"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1986308.1986344"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00170-007-1288-1"},{"key":"e_1_2_1_28_1","volume-title":"Intell. Robot. Syst","author":"Biggs Geoffrey","unstructured":"Geoffrey Biggs and Bruce MacDonald . 2006. Specifying robot reactivity in procedural languages . In Intell. Robot. Syst . IEEE , 3735--3740. Geoffrey Biggs and Bruce MacDonald. 2006. Specifying robot reactivity in procedural languages. In Intell. Robot. Syst. IEEE, 3735--3740."},{"key":"e_1_2_1_29_1","volume-title":"Robot. Biomechatronics","author":"Bonfe Marcello","unstructured":"Marcello Bonfe , Fabrizio Boriero , Riccardo Dodi , Paolo Fiorini , Angelica Morandi , Riccardo Muradore , Liliana Pasquale , Alberto Sanna , and Cristian Secchi . 2012. Towards automated surgical robotics: A requirements engineering approach . In Biomed. Robot. Biomechatronics . IEEE , 56--61. Marcello Bonfe, Fabrizio Boriero, Riccardo Dodi, Paolo Fiorini, Angelica Morandi, Riccardo Muradore, Liliana Pasquale, Alberto Sanna, and Cristian Secchi. 2012. Towards automated surgical robotics: A requirements engineering approach. In Biomed. Robot. Biomechatronics. IEEE, 56--61."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514095.1514169"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10514-011-9258-8"},{"key":"e_1_2_1_32_1","volume-title":"Int. Jt. Conf. Artif. Intell., Toby Walsh NICTA of NSW and University (Eds.)","volume":"11","author":"Bozzano Marco","year":"2011","unstructured":"Marco Bozzano , Alessandro Cimatti , Marco Roveri , and Andrei Tchaltsev . 2011 . A comprehensive approach to on-board autonomy verification and validation . In Int. Jt. Conf. Artif. Intell., Toby Walsh NICTA of NSW and University (Eds.) , Vol. 11 . Barcelona, Catalonia, Spain, 2398--2403. Marco Bozzano, Alessandro Cimatti, Marco Roveri, and Andrei Tchaltsev. 2011. A comprehensive approach to on-board autonomy verification and validation. In Int. Jt. Conf. Artif. Intell., Toby Walsh NICTA of NSW and University (Eds.), Vol. 11. Barcelona, Catalonia, Spain, 2398--2403."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2016.7759280"},{"key":"e_1_2_1_34_1","volume-title":"Intell. Robot. Syst","author":"Braman Julia","unstructured":"Julia Braman , Richard Murray , and David Wagner . 2007. Safety verification of a fault tolerant reconfigurable autonomous goal-based robotic control system . In Intell. Robot. Syst . IEEE , 853--858. Julia Braman, Richard Murray, and David Wagner. 2007. Safety verification of a fault tolerant reconfigurable autonomous goal-based robotic control system. In Intell. Robot. Syst. IEEE, 853--858."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2700318"},{"key":"e_1_2_1_36_1","volume-title":"Mauro Birattari, and Marco Dorigo.","author":"Brambilla Manuele","year":"2012","unstructured":"Manuele Brambilla , Carlo Pinciroli , Mauro Birattari, and Marco Dorigo. 2012 . Property-driven design for swarm robotics. In Auton. Agents Multiagent Syst. Retrieved from http:\/\/iridia.ulb.ac.be\/ mbrambilla\/pdf\/Bra-aamas2012.pdf. Manuele Brambilla, Carlo Pinciroli, Mauro Birattari, and Marco Dorigo. 2012. Property-driven design for swarm robotics. In Auton. Agents Multiagent Syst. Retrieved from http:\/\/iridia.ulb.ac.be\/ mbrambilla\/pdf\/Bra-aamas2012.pdf."},{"key":"e_1_2_1_37_1","volume-title":"Unmanned Untethered Submers. Technol.","author":"Brutzman Donald","unstructured":"Donald Brutzman , Duane Davis , George Lucas , and Robert McGhee . 2013. Run-time ethics checking for autonomous unmanned vehicles: Developing a practical approach . In Unmanned Untethered Submers. Technol. Monterey, CA : Naval Postgraduate School. Retrieved from http:\/\/calhoun.nps.edu\/handle\/10945\/37443. Donald Brutzman, Duane Davis, George Lucas, and Robert McGhee. 2013. Run-time ethics checking for autonomous unmanned vehicles: Developing a practical approach. In Unmanned Untethered Submers. Technol. Monterey, CA: Naval Postgraduate School. Retrieved from http:\/\/calhoun.nps.edu\/handle\/10945\/37443."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480693"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSMC.2007.4413960"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2011.2163434"},{"key":"e_1_2_1_41_1","volume-title":"Alin Stefanescu, and Calin Belta.","author":"Chen Yushan","year":"2013","unstructured":"Yushan Chen , Xu Chu Ding , Alin Stefanescu, and Calin Belta. 2013 . A formal approach to deployment of robotic teams in an urban-like environment. In Distrib. Auton. Robot. Syst., Alcherio Martinoli, Francesco Mondada, Nikolaus Correll, Gr\u00e9gory Mermoud, Magnus Egerstedt, M. Ani Hsieh, Lynne E. Parker, and Kasper St\u00f8y (Eds.). Vol. STAR 83 . Springer , Berlin, Heidelberg, 313--327. Yushan Chen, Xu Chu Ding, Alin Stefanescu, and Calin Belta. 2013. A formal approach to deployment of robotic teams in an urban-like environment. In Distrib. Auton. Robot. Syst., Alcherio Martinoli, Francesco Mondada, Nikolaus Correll, Gr\u00e9gory Mermoud, Magnus Egerstedt, M. Ani Hsieh, Lynne E. Parker, and Kasper St\u00f8y (Eds.). Vol. STAR 83. Springer, Berlin, Heidelberg, 313--327."},{"key":"e_1_2_1_42_1","volume-title":"Models@run.time (LNCS)","author":"Cheng Betty","unstructured":"Betty Cheng , Kerstin Eder , Martin Gogolla , Lars Grunske , Marin Litoiu , Hausi M\u00fcller , Patrizio Pelliccione , Anna Perini , Nauman Qureshi , Bernhard Rumpe , Daniel Schneider , Frank Trollmann , and Norha Villegas . 2014. Using models at runtime to address assurance for self-adaptive systems . In Models@run.time (LNCS) , Vol. 8378 . Springer , 101--136. Betty Cheng, Kerstin Eder, Martin Gogolla, Lars Grunske, Marin Litoiu, Hausi M\u00fcller, Patrizio Pelliccione, Anna Perini, Nauman Qureshi, Bernhard Rumpe, Daniel Schneider, Frank Trollmann, and Norha Villegas. 2014. Using models at runtime to address assurance for self-adaptive systems. In Models@run.time (LNCS), Vol. 8378. Springer, 101--136."},{"key":"e_1_2_1_43_1","first-page":"5","article-title":"Translating AADL into BIP-application to the verification of real-time systems. In Model Driven","volume":"5421","author":"Chkouri Mohamed Yassin","year":"2008","unstructured":"Mohamed Yassin Chkouri , Anne Robert , Marius Bozga , and Joseph Sifakis . 2008 . Translating AADL into BIP-application to the verification of real-time systems. In Model Driven Eng. Lang. Syst. (LNCS) , Vol. 5421. Spring er, 5 -- 19 . Mohamed Yassin Chkouri, Anne Robert, Marius Bozga, and Joseph Sifakis. 2008. Translating AADL into BIP-application to the verification of real-time systems. In Model Driven Eng. Lang. Syst. (LNCS), Vol. 5421. Springer, 5--19.","journal-title":"Eng. Lang. Syst. (LNCS)"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207721.2013.793890"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03240-0_11"},{"key":"e_1_2_1_48_1","volume-title":"Int. Conf. Robot. Autom., Savvas Loizou and Vijay Kumar (Eds.)","volume":"30","author":"Correll Nikolaus","year":"2007","unstructured":"Nikolaus Correll and Alcherio Martinoli . 2007 . Modeling and designing self-organized aggregation in a swarm of miniature robots . In Int. Conf. Robot. Autom., Savvas Loizou and Vijay Kumar (Eds.) , Vol. 30 . Rome, Italy, 6. Nikolaus Correll and Alcherio Martinoli. 2007. Modeling and designing self-organized aggregation in a swarm of miniature robots. In Int. Conf. Robot. Autom., Savvas Loizou and Vijay Kumar (Eds.), Vol. 30. Rome, Italy, 6."},{"key":"e_1_2_1_49_1","volume-title":"Thomas C. Henderson and Edward Grant (Eds.)","volume":"41","author":"Costelha Hugo","year":"2008","unstructured":"Hugo Costelha and Pedro Lima . 2008 . Modelling, analysis and execution of multi-robot tasks using petri nets. In Auton. Agents Multiagent Syst ., Thomas C. Henderson and Edward Grant (Eds.) , Vol. 41 . IEEE, 1187--1190. Hugo Costelha and Pedro Lima. 2008. Modelling, analysis and execution of multi-robot tasks using petri nets. In Auton. Agents Multiagent Syst., Thomas C. Henderson and Edward Grant (Eds.), Vol. 41. IEEE, 1187--1190."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/HUMANOIDS.2012.6651538"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2724719"},{"key":"e_1_2_1_52_1","volume-title":"Automating the generation of heterogeneous aviation safety cases","author":"Denney Ewen","year":"2011","unstructured":"Ewen Denney , Ganesh Pai , and Josef Pohl . 2011. Automating the generation of heterogeneous aviation safety cases . IEEE Trans. Reliab. 63, NASA\/CR- 2011 -215983 (2011), 1--20. Ewen Denney, Ganesh Pai, and Josef Pohl. 2011. Automating the generation of heterogeneous aviation safety cases. IEEE Trans. Reliab. 63, NASA\/CR-2011-215983 (2011), 1--20."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2008.4526576"},{"key":"e_1_2_1_54_1","volume-title":"Gwendolen: A BDI language for verifiable agents. Log. Simul. Interact. Reason.","author":"Dennis Louise","year":"2008","unstructured":"Louise Dennis and Berndt Farwer . 2008 . Gwendolen: A BDI language for verifiable agents. Log. Simul. Interact. Reason. (2008), 16--23. Louise Dennis and Berndt Farwer. 2008. Gwendolen: A BDI language for verifiable agents. Log. Simul. Interact. Reason. (2008), 16--23."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2015.11.012"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0088-x"},{"key":"e_1_2_1_57_1","volume-title":"Towards verifiably ethical robot behaviour. Artif. Intell. Ethics abs\/1504.0","author":"Dennis Louise","year":"2014","unstructured":"Louise Dennis , Michael Fisher , and Alan Winfield . 2015. Towards verifiably ethical robot behaviour. Artif. Intell. Ethics abs\/1504.0 , 2014 (2015), 1--11. arxiv:1504.03592 http:\/\/arxiv.org\/abs\/1504.03592 Louise Dennis, Michael Fisher, and Alan Winfield. 2015. Towards verifiably ethical robot behaviour. Artif. Intell. Ethics abs\/1504.0, 2014 (2015), 1--11. arxiv:1504.03592 http:\/\/arxiv.org\/abs\/1504.03592"},{"key":"e_1_2_1_58_1","volume-title":"Runtime Verif. (LNCS)","author":"Desai Ankush","unstructured":"Ankush Desai , Tommaso Dreossi , and Sanjit Seshia . 2017. Combining model checking and runtime verification for safe robotics . In Runtime Verif. (LNCS) , Vol. 10548 . Springer , 172--189. Ankush Desai, Tommaso Dreossi, and Sanjit Seshia. 2017. Combining model checking and runtime verification for safe robotics. In Runtime Verif. (LNCS), Vol. 10548. Springer, 172--189."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AGNT.0000019688.11109.19"},{"key":"e_1_2_1_60_1","volume-title":"The fridge door is open","author":"Dixon Clare","unstructured":"Clare Dixon , Matt Webster , Joe Saunders , Michael Fisher , and Kerstin Dautenhahn . 2014. \u201c The fridge door is open \u201d - Temporal verification of a robotic assistant\u2019s behaviours (LNAI), Vol. 8717 . Springer , 97--108. Clare Dixon, Matt Webster, Joe Saunders, Michael Fisher, and Kerstin Dautenhahn. 2014. \u201cThe fridge door is open\u201d - Temporal verification of a robotic assistant\u2019s behaviours (LNAI), Vol. 8717. Springer, 97--108."},{"key":"e_1_2_1_61_1","volume-title":"Towards temporal verification of emergent behaviours in swarm robotic systems (LNAI)","author":"Dixon Clare","unstructured":"Clare Dixon , Alan Winfield , and Michael Fisher . 2011. Towards temporal verification of emergent behaviours in swarm robotic systems (LNAI) , Vol. 6856 . Springer , 336--347. Clare Dixon, Alan Winfield, and Michael Fisher. 2011. Towards temporal verification of emergent behaviours in swarm robotic systems (LNAI), Vol. 6856. Springer, 336--347."},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2012.03.003"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:AURO.0000034008.48988.2b"},{"key":"e_1_2_1_64_1","doi-asserted-by":"crossref","unstructured":"Frank Dylla Alexander Ferrein Gerhard Lakemeyer Jan Murray Oliver Obst Thomas R\u00f6fer Stefan Schiffer Frieder Stolzenburg Ubbo Visser and Th Wagner. 2008. In Comput. Sport. Vol. 32. WIT Press 161--185.  Frank Dylla Alexander Ferrein Gerhard Lakemeyer Jan Murray Oliver Obst Thomas R\u00f6fer Stefan Schiffer Frieder Stolzenburg Ubbo Visser and Th Wagner. 2008. In Comput. Sport. Vol. 32. WIT Press 161--185.","DOI":"10.2495\/978-1-84564-064-4\/06"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEAMS.2009.5069083"},{"key":"e_1_2_1_66_1","series-title":"Lecture Notes in Computer Science","volume-title":"Runtime verification of component-based systems","author":"Falcone Yli\u00e8s","unstructured":"Yli\u00e8s Falcone , Mohamad Jaber , Thanh-hung Nguyen, Marius Bozga , and Saddek Bensalem . 2011. Runtime verification of component-based systems . In Softw. Eng. Form. Methods, G. Barthe, A. Pardo, and G. Schneider (Eds.). Lecture Notes in Computer Science , Vol. 7041 . Springer , 204--220. Yli\u00e8s Falcone, Mohamad Jaber, Thanh-hung Nguyen, Marius Bozga, and Saddek Bensalem. 2011. Runtime verification of component-based systems. In Softw. Eng. Form. Methods, G. Barthe, A. Pardo, and G. Schneider (Eds.). Lecture Notes in Computer Science, Vol. 7041. Springer, 204--220."},{"key":"e_1_2_1_67_1","volume-title":"Integr. Form. Methods (LNCS)","author":"Farrell Marie","year":"1805","unstructured":"Marie Farrell , Matt Luckcuck , and Michael Fisher . 2018. Robotics and integrated formal methods: Necessity meets opportunity . In Integr. Form. Methods (LNCS) , C. Furia and K. Winter (Eds.), Vol. 11023 . Springer , 161--171. arxiv: 1805 .11996 http:\/\/arxiv.org\/abs\/1805.11996 Marie Farrell, Matt Luckcuck, and Michael Fisher. 2018. Robotics and integrated formal methods: Necessity meets opportunity. In Integr. Form. Methods (LNCS), C. Furia and K. Winter (Eds.), Vol. 11023. Springer, 161--171. arxiv:1805.11996 http:\/\/arxiv.org\/abs\/1805.11996"},{"key":"e_1_2_1_68_1","volume-title":"Fvav","author":"Fernandes Lucas","year":"2017","unstructured":"Lucas Fernandes , Vinicius Custodio , Gleifer Alves , and Michael Fisher . 2017. A rational agent controlling an autonomous vehicle: Implementation and formal verification. Theor. Comput. Sci. 257 , Fvav ( 2017 ), 35--42. Lucas Fernandes, Vinicius Custodio, Gleifer Alves, and Michael Fisher. 2017. A rational agent controlling an autonomous vehicle: Implementation and formal verification. Theor. Comput. Sci. 257, Fvav (2017), 35--42."},{"key":"e_1_2_1_69_1","volume-title":"Auton. Agents Multiagent Syst. IFAAMAS\/ACM","author":"Ferrando Angelo","year":"2018","unstructured":"Angelo Ferrando , Louise Dennis , Davide Ancona , Michael Fisher , and Viviana Mascardi . 2018 . Recognising assumption violations in autonomous systems verificaion . In Auton. Agents Multiagent Syst. IFAAMAS\/ACM , Stockholm, Sweden , 1933--1935. http:\/\/dl.acm.org\/citation.cfm?id&equals;3238028 Angelo Ferrando, Louise Dennis, Davide Ancona, Michael Fisher, and Viviana Mascardi. 2018. Recognising assumption violations in autonomous systems verificaion. In Auton. Agents Multiagent Syst. IFAAMAS\/ACM, Stockholm, Sweden, 1933--1935. http:\/\/dl.acm.org\/citation.cfm?id&equals;3238028"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2012.6426027"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/2494558"},{"key":"e_1_2_1_72_1","first-page":"7","article-title":"A generic approach for automatic model composition. In Model","volume":"5002","author":"Fleurey Franck","year":"2007","unstructured":"Franck Fleurey , Benoit Baudry , Robert France , and Sudipto Ghosh . 2007 . A generic approach for automatic model composition. In Model . Softw. Eng. (LNCS) , Vol. 5002. Spring er, 7 -- 15 . Franck Fleurey, Benoit Baudry, Robert France, and Sudipto Ghosh. 2007. A generic approach for automatic model composition. In Model. Softw. Eng. (LNCS), Vol. 5002. Springer, 7--15.","journal-title":"Softw. Eng. (LNCS)"},{"key":"e_1_2_1_73_1","volume-title":"Intell. Robot. Syst.","volume":"2","author":"Fleury Sara","year":"1997","unstructured":"Sara Fleury , Matthieu Herrb , and Raja Chatila . 1997 . GenoM: A tool for the specification and the implementation of operating modules in a distributed robot architecture . In Intell. Robot. Syst. , Vol. 2 . IEEE, 842--849. Sara Fleury, Matthieu Herrb, and Raja Chatila. 1997. GenoM: A tool for the specification and the implementation of operating modules in a distributed robot architecture. In Intell. Robot. Syst., Vol. 2. IEEE, 842--849."},{"key":"e_1_2_1_74_1","volume-title":"Automating verification of state machines with reactive designs and Isabelle\/UTP. arXiv Prepr. arXiv1807.08588","author":"Foster Simon","year":"2018","unstructured":"Simon Foster , James Baxter , Ana Cavalcanti , Alvaro Miyazawa , and Jim Woodcock . 2018. Automating verification of state machines with reactive designs and Isabelle\/UTP. arXiv Prepr. arXiv1807.08588 ( 2018 ). Simon Foster, James Baxter, Ana Cavalcanti, Alvaro Miyazawa, and Jim Woodcock. 2018. Automating verification of state machines with reactive designs and Isabelle\/UTP. arXiv Prepr. arXiv1807.08588 (2018)."},{"key":"e_1_2_1_75_1","series-title":"Lecture Notes in Computer Science","volume-title":"F\u00e9lix Ingrand, and Anthony Mallet.","author":"Foughali Mohammed","year":"2016","unstructured":"Mohammed Foughali , Bernard Berthomieu , Silvano Dal Zilio , F\u00e9lix Ingrand, and Anthony Mallet. 2016 . Model checking real-time properties on the functional layer of autonomous robots. In Form. Methods Softw. Eng. Kazuhiro Ogata, Mark Lawford, and Shaoying Liu (Eds.), Lecture Notes in Computer Science , Vol. 10009 . Springer International Publishing , Cham, 383--399. Mohammed Foughali, Bernard Berthomieu, Silvano Dal Zilio, F\u00e9lix Ingrand, and Anthony Mallet. 2016. Model checking real-time properties on the functional layer of autonomous robots. In Form. Methods Softw. Eng. Kazuhiro Ogata, Mark Lawford, and Shaoying Liu (Eds.), Lecture Notes in Computer Science, Vol. 10009. Springer International Publishing, Cham, 383--399."},{"key":"e_1_2_1_76_1","volume-title":"CRutoN: Automatic verification of a robotic assistant\u2019s behaviours","author":"Gainer Paul","unstructured":"Paul Gainer , Clare Dixon , Kerstin Dautenhahn , Michael Fisher , Ullrich Hustadt , Joe Saunders , and Matt Webster . 2017. CRutoN: Automatic verification of a robotic assistant\u2019s behaviours . In Int. Work. Form. Methods Ind. Crit. Syst., Laure Petrucci, Cristina Seceleanu, and Ana Cavalcanti (Eds.), LNCS, Vol . 10471. Springer International Publishing , Cham, 119--133. Paul Gainer, Clare Dixon, Kerstin Dautenhahn, Michael Fisher, Ullrich Hustadt, Joe Saunders, and Matt Webster. 2017. CRutoN: Automatic verification of a robotic assistant\u2019s behaviours. In Int. Work. Form. Methods Ind. Crit. Syst., Laure Petrucci, Cristina Seceleanu, and Ana Cavalcanti (Eds.), LNCS, Vol. 10471. Springer International Publishing, Cham, 119--133."},{"key":"e_1_2_1_77_1","volume-title":"Contemporary Planetary Robotics: An Approach Toward Autonomous Systems","author":"Gao Yang","unstructured":"Yang Gao . 2016. Contemporary Planetary Robotics: An Approach Toward Autonomous Systems . Wiley , Germany , 10--410 pages. Yang Gao. 2016. Contemporary Planetary Robotics: An Approach Toward Autonomous Systems. Wiley, Germany, 10--410 pages."},{"key":"e_1_2_1_78_1","volume-title":"Natl. Conf. Artif. Intell.","volume":"87","author":"Georgeff Michael","year":"1987","unstructured":"Michael Georgeff and Amy Lansky . 1987 . Reactive reasoning and planning . In Natl. Conf. Artif. Intell. , Vol. 87 . 677--682. Retrieved from http:\/\/scholar.google.com\/scholar?hl&equals;en8btnG&equals;Search8q&equals;intitle:Reactive+reasoning+and+planning#0. Michael Georgeff and Amy Lansky. 1987. Reactive reasoning and planning. In Natl. Conf. Artif. Intell., Vol. 87. 677--682. Retrieved from http:\/\/scholar.google.com\/scholar?hl&equals;en8btnG&equals;Search8q&equals;intitle:Reactive+reasoning+and+planning#0."},{"key":"e_1_2_1_79_1","first-page":"187","article-title":"FDR3 - A modern model checker for CSP. In Tools Algorithms Constr","volume":"8413","author":"Gibson-Robinson Thomas","year":"2014","unstructured":"Thomas Gibson-Robinson , Philip Armstrong , Alexandre Boulgakov , and Andrew Roscoe . 2014 . FDR3 - A modern model checker for CSP. In Tools Algorithms Constr . Anal. Syst. (LNCS) , Vol. 8413. Spring er, 187 -- 201 . Retrieved from http:\/\/www.cs.ox.ac.uk\/projects\/fdr\/manual\/. Thomas Gibson-Robinson, Philip Armstrong, Alexandre Boulgakov, and Andrew Roscoe. 2014. FDR3 - A modern model checker for CSP. In Tools Algorithms Constr. Anal. Syst. (LNCS), Vol. 8413. Springer, 187--201. Retrieved from http:\/\/www.cs.ox.ac.uk\/projects\/fdr\/manual\/.","journal-title":"Anal. Syst. (LNCS)"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34281-3_7"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/SASO.2008.66"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2017.04.004"},{"key":"e_1_2_1_83_1","volume-title":"Robot. Autom","author":"Guo Meng","unstructured":"Meng Guo , Karl Johansson , and Dimos Dimarogonas . 2013. Revising motion planning under linear temporal logic specifications in partially known workspaces . In Robot. Autom . IEEE , 5025--5032. Meng Guo, Karl Johansson, and Dimos Dimarogonas. 2013. Revising motion planning under linear temporal logic specifications in partially known workspaces. In Robot. Autom. IEEE, 5025--5032."},{"key":"e_1_2_1_84_1","first-page":"1","article-title":"On methodology for the verification of reconfigurable timed net condition\/event systems","volume":"99","author":"Hafidi Yousra","year":"2018","unstructured":"Yousra Hafidi , La\u00efd Kahloul , Mohamed Khalgui , Zhiwu Li , Khalid Alnowibet , and Ting Qu . 2018 . On methodology for the verification of reconfigurable timed net condition\/event systems . IEEE Trans. Syst. Man Cybernetics: Syst. 99 (2018), 1 -- 15 . Yousra Hafidi, La\u00efd Kahloul, Mohamed Khalgui, Zhiwu Li, Khalid Alnowibet, and Ting Qu. 2018. On methodology for the verification of reconfigurable timed net condition\/event systems. IEEE Trans. Syst. Man Cybernetics: Syst. 99 (2018), 1--15.","journal-title":"IEEE Trans. Syst. Man Cybernetics: Syst."},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2013.05.008"},{"key":"e_1_2_1_86_1","volume-title":"Form. Methods Softw. Eng","author":"Halder Raju","unstructured":"Raju Halder , Jos\u00e9 Proen\u00e7a , Nuno MacEdo , and Andr\u00e9 Santos . 2017. Formal verification of ROS-based robotic applications using timed-automata . In Form. Methods Softw. Eng . IEEE , 44--50. Raju Halder, Jos\u00e9 Proen\u00e7a, Nuno MacEdo, and Andr\u00e9 Santos. 2017. Formal verification of ROS-based robotic applications using timed-automata. In Form. Methods Softw. Eng. IEEE, 44--50."},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"e_1_2_1_88_1","volume-title":"Intell. Robot. Syst","author":"He\u00df Daniel","unstructured":"Daniel He\u00df , Matthias Althoff , and Thomas Sattel . 2014. Formal verification of maneuver automata for parameterized motion primitives . In Intell. Robot. Syst . IEEE , 1474--1481. Daniel He\u00df, Matthias Althoff, and Thomas Sattel. 2014. Formal verification of maneuver automata for parameterized motion primitives. In Intell. Robot. Syst. IEEE, 1474--1481."},{"key":"e_1_2_1_89_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194007003392"},{"key":"e_1_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081180.1081196"},{"key":"e_1_2_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_92_1","doi-asserted-by":"publisher","DOI":"10.1145\/1562764.1562779"},{"key":"e_1_2_1_93_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-32582-8_7"},{"key":"e_1_2_1_94_1","doi-asserted-by":"publisher","DOI":"10.1109\/ETFA.2016.7733579"},{"key":"e_1_2_1_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_20"},{"key":"e_1_2_1_96_1","volume-title":"Comput. Aided Verif. (LNCS)","author":"Huang Xiaowei","unstructured":"Xiaowei Huang , Marta Kwiatkowska , Sen Wang , and Min Wu. 2017. Safety verification of deep neural networks . In Comput. Aided Verif. (LNCS) , Vol. 10426 . Springer , 3--29. Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017. Safety verification of deep neural networks. In Comput. Aided Verif. (LNCS), Vol. 10426. Springer, 3--29."},{"key":"e_1_2_1_97_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.91.4"},{"key":"e_1_2_1_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593929.2593944"},{"key":"e_1_2_1_99_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2016.7799031"},{"key":"e_1_2_1_100_1","doi-asserted-by":"publisher","DOI":"10.4218\/etrij.10.1510.0138"},{"key":"e_1_2_1_101_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.05.006"},{"key":"e_1_2_1_102_1","volume-title":"Modular verification of vehicle platooning with respect to decisions, space and time. (apr","author":"Kamali Maryam","year":"2018","unstructured":"Maryam Kamali , Sven Linker , and Michael Fisher . 2018. Modular verification of vehicle platooning with respect to decisions, space and time. (apr 2018 ), 17. arXiv:1804.06647 http:\/\/arxiv.org\/abs\/1804.06647 Maryam Kamali, Sven Linker, and Michael Fisher. 2018. Modular verification of vehicle platooning with respect to decisions, space and time. (apr 2018), 17. arXiv:1804.06647 http:\/\/arxiv.org\/abs\/1804.06647"},{"key":"e_1_2_1_103_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23820-3_7"},{"key":"e_1_2_1_104_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2009.5400278"},{"key":"e_1_2_1_105_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1160055"},{"key":"e_1_2_1_106_1","volume-title":"Proc. of the IEEE Int. Conf. Robot. Autom.","volume":"2005","author":"Kim Moonzoo","year":"2005","unstructured":"Moonzoo Kim , Kyo Chul Kang , and Hyoungki Lee . 2005 . Formal verification of robot movements - A case study on home service robot SHR100 . In Proc. of the IEEE Int. Conf. Robot. Autom. , Vol. 2005 . IEEE, 4739--4744. Moonzoo Kim, Kyo Chul Kang, and Hyoungki Lee. 2005. Formal verification of robot movements - A case study on home service robot SHR100. In Proc. of the IEEE Int. Conf. Robot. Autom., Vol. 2005. IEEE, 4739--4744."},{"key":"e_1_2_1_107_1","unstructured":"Barbara Kitchenham and Stuart Charters. 2007. Guidelines for performing systematic literature reviews in software engineering. 65 pages. https:\/\/www.elsevier.com\/__data\/promis_misc\/525444systematicreviewsguide.pdf.  Barbara Kitchenham and Stuart Charters. 2007. Guidelines for performing systematic literature reviews in software engineering. 65 pages. https:\/\/www.elsevier.com\/__data\/promis_misc\/525444systematicreviewsguide.pdf."},{"key":"e_1_2_1_108_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2011.6160478"},{"key":"e_1_2_1_109_1","unstructured":"John Knight Colleen Dejong Matthew Gibble and Lu\u00eds Nakano. 1997. Why are formal methods not used more widely? In NASA Form. Methods. Virginia Univ. 12.  John Knight Colleen Dejong Matthew Gibble and Lu\u00eds Nakano. 1997. Why are formal methods not used more widely? In NASA Form. Methods. Virginia Univ. 12."},{"key":"e_1_2_1_110_1","volume-title":"Swarm Intell. (LNCS)","author":"Konur Savas","unstructured":"Savas Konur , Clare Dixon , and Michael Fisher . 2010. Formal verification of probabilistic swarm behaviours . In Swarm Intell. (LNCS) , Vol. 6234 . Springer , 440--447. Savas Konur, Clare Dixon, and Michael Fisher. 2010. Formal verification of probabilistic swarm behaviours. In Swarm Intell. (LNCS), Vol. 6234. Springer, 440--447."},{"key":"e_1_2_1_111_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2011.10.005"},{"key":"e_1_2_1_112_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33600-8_13"},{"key":"e_1_2_1_113_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461369"},{"key":"e_1_2_1_114_1","doi-asserted-by":"publisher","DOI":"10.5555\/3171642.3171684"},{"key":"e_1_2_1_115_1","doi-asserted-by":"publisher","DOI":"10.1109\/ROBOT.2007.363946"},{"key":"e_1_2_1_116_1","doi-asserted-by":"publisher","DOI":"10.1109\/MRA.2011.942116"},{"key":"e_1_2_1_117_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-009-0096-1"},{"key":"e_1_2_1_118_1","volume-title":"Proc. Towar. Auton. Robot. Syst. 25--32","author":"Liu Wenguo","year":"2007","unstructured":"Wenguo Liu , Alan Winfield , and Jin Sa . 2007 . Modelling swarm robotic systems: A case study in collective foraging . In Proc. Towar. Auton. Robot. Syst. 25--32 . Wenguo Liu, Alan Winfield, and Jin Sa. 2007. Modelling swarm robotic systems: A case study in collective foraging. In Proc. Towar. Auton. Robot. Syst. 25--32."},{"key":"e_1_2_1_119_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_55"},{"key":"e_1_2_1_120_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11721-016-0119-0"},{"key":"e_1_2_1_121_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2015.22"},{"key":"e_1_2_1_122_1","doi-asserted-by":"publisher","DOI":"10.1109\/HASE.2015.15"},{"key":"e_1_2_1_123_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11721-013-0079-6"},{"key":"e_1_2_1_124_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICAS.2006.19"},{"key":"e_1_2_1_125_1","volume-title":"On provably safe obstacle avoidance for autonomous robotic ground vehicles","author":"Mitsch Stefan","unstructured":"Stefan Mitsch , Khalil Ghorbal , and Andr\u00e9 Platzer . 2013. On provably safe obstacle avoidance for autonomous robotic ground vehicles . In Robot. Sci. Syst. IX, Paul Newman, Dieter Fox, and David Hsu (Eds.). Robotics : Science and Systems Foundation, Berlin, Germany , 8. Stefan Mitsch, Khalil Ghorbal, and Andr\u00e9 Platzer. 2013. On provably safe obstacle avoidance for autonomous robotic ground vehicles. In Robot. Sci. Syst. IX, Paul Newman, Dieter Fox, and David Hsu (Eds.). Robotics: Science and Systems Foundation, Berlin, Germany, 8."},{"key":"e_1_2_1_126_1","doi-asserted-by":"publisher","DOI":"10.1177\/0278364917733549"},{"key":"e_1_2_1_127_1","volume-title":"Intell. Robot. Syst","author":"Miyazawa Alvaro","unstructured":"Alvaro Miyazawa , Pedro Ribeiro , Wei Li , Ana Cavalcanti , and Jon Timmis . 2017. Automatic property checking of robotic applications . In Intell. Robot. Syst . IEEE , 3869--3876. Alvaro Miyazawa, Pedro Ribeiro, Wei Li, Ana Cavalcanti, and Jon Timmis. 2017. Automatic property checking of robotic applications. In Intell. Robot. Syst. IEEE, 3869--3876."},{"key":"e_1_2_1_128_1","volume-title":"Multi-Robot Multi-Agent Syst","author":"Moarref Salar","unstructured":"Salar Moarref and Hadas Kress-Gazit . 2017. Decentralized control of robotic swarms from high-level temporal logic specifications . In Multi-Robot Multi-Agent Syst . IEEE , 17--23. Salar Moarref and Hadas Kress-Gazit. 2017. Decentralized control of robotic swarms from high-level temporal logic specifications. In Multi-Robot Multi-Agent Syst. IEEE, 17--23."},{"key":"e_1_2_1_129_1","volume-title":"Ocean. 2009 - Eur","author":"Molnar Levente","unstructured":"Levente Molnar and Sandor Veres . 2009. System verification of autonomous underwater vehicles by model checking . In Ocean. 2009 - Eur . IEEE , 1--10. Levente Molnar and Sandor Veres. 2009. System verification of autonomous underwater vehicles by model checking. In Ocean. 2009 - Eur. IEEE, 1--10."},{"key":"e_1_2_1_130_1","unstructured":"Jeremy Morse Dejanira Araiza-Illan Jonathan Lawry Arthur Richards and Kerstin Eder. 2016. Formal Specification and Analysis of Autonomous Systems under Partial Compliance. 15 pages. arxiv:1603.01082. Retrieved from https:\/\/www.researchgate.net\/profile\/Kerstin_Eder\/publication\/301841477_Towards_the_Specification_of_Adaptive_Robotic_Systems\/links\/5737a84108ae9ace840bf752\/Towards-the-Specification-of-Adaptive-Robotic-Systems.pdf http:\/\/arxiv.org\/abs\/1603.01082  Jeremy Morse Dejanira Araiza-Illan Jonathan Lawry Arthur Richards and Kerstin Eder. 2016. Formal Specification and Analysis of Autonomous Systems under Partial Compliance. 15 pages. arxiv:1603.01082. Retrieved from https:\/\/www.researchgate.net\/profile\/Kerstin_Eder\/publication\/301841477_Towards_the_Specification_of_Adaptive_Robotic_Systems\/links\/5737a84108ae9ace840bf752\/Towards-the-Specification-of-Adaptive-Robotic-Systems.pdf http:\/\/arxiv.org\/abs\/1603.01082"},{"key":"e_1_2_1_131_1","first-page":"75","article-title":"A survey on domain-specific languages in robotics","author":"Nordmann Arne","year":"2016","unstructured":"Arne Nordmann , Nico Hochgeschwender , Dennis Wigand , and Sebastian Wrede . 2016 . A survey on domain-specific languages in robotics . J. Softw. Eng. Robot. 7 , July (2016), 75 -- 99 . Arne Nordmann, Nico Hochgeschwender, Dennis Wigand, and Sebastian Wrede. 2016. A survey on domain-specific languages in robotics. J. Softw. Eng. Robot. 7, July (2016), 75--99.","journal-title":"J. Softw. Eng. Robot. 7"},{"key":"e_1_2_1_132_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11900-7_39"},{"key":"e_1_2_1_133_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2007.909810"},{"key":"e_1_2_1_134_1","volume-title":"Runtime Verif. (LNCS)","author":"Phan Dung","unstructured":"Dung Phan , Junxing Yang , Denise Ratasich , Radu Grosu , Scott Smolka , and Scott Stoller . 2015. Collision avoidance for mobile robots with limited sensing and limited information about the environment . In Runtime Verif. (LNCS) , Vol. 9333 . Springer , 201--215. Dung Phan, Junxing Yang, Denise Ratasich, Radu Grosu, Scott Smolka, and Scott Stoller. 2015. Collision avoidance for mobile robots with limited sensing and limited information about the environment. In Runtime Verif. (LNCS), Vol. 9333. Springer, 201--215."},{"key":"e_1_2_1_135_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73099-6_17"},{"key":"e_1_2_1_136_1","volume-title":"Integr. Form. Methods (LNCS)","author":"Podorozhny Rodion","unstructured":"Rodion Podorozhny , Sarfraz Khurshid , Dewayne Perry , and Xiaoqin Zhang . 2007. Verification of multi-agent negotiations using the alloy analyzer . In Integr. Form. Methods (LNCS) , Vol. 4591 . Springer , 501--517. Rodion Podorozhny, Sarfraz Khurshid, Dewayne Perry, and Xiaoqin Zhang. 2007. Verification of multi-agent negotiations using the alloy analyzer. In Integr. Form. Methods (LNCS), Vol. 4591. Springer, 501--517."},{"key":"e_1_2_1_137_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2013.04.005"},{"key":"e_1_2_1_138_1","unstructured":"Martin Proetzsch and Karsten Berns. 2007. Formal verification of safety behaviours of the outdoor robot ravon. In Informatics Control. Autom. Robot. 157--164. Retrieved from http:\/\/es.informatik.uni-kl.de\/publications\/datarsg\/PBSS07.pdf.  Martin Proetzsch and Karsten Berns. 2007. Formal verification of safety behaviours of the outdoor robot ravon. In Informatics Control. Autom. Robot. 157--164. Retrieved from http:\/\/es.informatik.uni-kl.de\/publications\/datarsg\/PBSS07.pdf."},{"key":"e_1_2_1_139_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74565-5_48"},{"key":"e_1_2_1_140_1","volume-title":"ROS: An open-source robot operating system. In ICRA Work. open source Softw.","author":"Quigley Morgan","year":"2009","unstructured":"Morgan Quigley , Ken Conley , Brian Gerkey , Josh Faust , Tully Foote , Jeremy Leibs , Rob Wheeler , and Andrew Ng . 2009 . ROS: An open-source robot operating system. In ICRA Work. open source Softw. , Kazuhiro Kosuge and Katsushi Ikeuchi (Eds.), Vol. 3 . IEEE ICRA, Kobe , Japan , 5. Morgan Quigley, Ken Conley, Brian Gerkey, Josh Faust, Tully Foote, Jeremy Leibs, Rob Wheeler, and Andrew Ng. 2009. ROS: An open-source robot operating system. In ICRA Work. open source Softw., Kazuhiro Kosuge and Katsushi Ikeuchi (Eds.), Vol. 3. IEEE ICRA, Kobe, Japan, 5."},{"key":"e_1_2_1_141_1","volume-title":"Comput. Aided Verif","author":"Raman Vasumathi","unstructured":"Vasumathi Raman and Hadas Kress-Gazit . 2011. Analyzing unsynthesizable specifications for high-level robot behavior using LTLMoP . In Comput. Aided Verif . Springer , 663--668. Vasumathi Raman and Hadas Kress-Gazit. 2011. Analyzing unsynthesizable specifications for high-level robot behavior using LTLMoP. In Comput. Aided Verif. Springer, 663--668."},{"key":"e_1_2_1_142_1","volume-title":"Icmas","volume":"95","author":"Rao Anand","year":"1995","unstructured":"Anand Rao and Michael Georgeff . 1995 . BDI agents: From theory to practice . In Icmas , Vol. 95 . San Francisco, USA, 312--319. Anand Rao and Michael Georgeff. 1995. BDI agents: From theory to practice. In Icmas, Vol. 95. San Francisco, USA, 312--319."},{"key":"e_1_2_1_143_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90030-8"},{"key":"e_1_2_1_144_1","volume-title":"Integr. Form. Methods (LNCS)","author":"Ribeiro Pedro","unstructured":"Pedro Ribeiro , Alvaro Miyazawa , Wei Li , Ana Cavalcanti , and Jon Timmis . 2017. Modelling and verification of timed robotic controllers . In Integr. Form. Methods (LNCS) , Vol. 10510 . Springer , 18--33. Pedro Ribeiro, Alvaro Miyazawa, Wei Li, Ana Cavalcanti, and Jon Timmis. 2017. Modelling and verification of timed robotic controllers. In Integr. Form. Methods (LNCS), Vol. 10510. Springer, 18--33."},{"key":"e_1_2_1_145_1","first-page":"33","article-title":"Code generator composition for model-driven engineering of robotics component 8 connector systems","volume":"6","author":"Ringert Jan Oliver","year":"2015","unstructured":"Jan Oliver Ringert , Alexander Roth , Bernhard Rumpe , and Andreas Wortmann . 2015 . Code generator composition for model-driven engineering of robotics component 8 connector systems . J. Softw. Eng. Robot. 6 , 1 (2015), 33 -- 57 . Retrieved from http:\/\/www.se-rwth.de\/%0Ahttp:\/\/www.cs.tau.ac.il\/. Jan Oliver Ringert, Alexander Roth, Bernhard Rumpe, and Andreas Wortmann. 2015. Code generator composition for model-driven engineering of robotics component 8 connector systems. J. Softw. Eng. Robot. 6, 1 (2015), 33--57. Retrieved from http:\/\/www.se-rwth.de\/%0Ahttp:\/\/www.cs.tau.ac.il\/.","journal-title":"J. Softw. Eng. Robot."},{"key":"e_1_2_1_146_1","unstructured":"Max Risler and Oskar von Stryk. 2008. Formal behavior specification of multi-robot systems using hierarchical state machines in XABSL. In Form. Model. Methods Multi-Robot Syst. Citeseer.  Max Risler and Oskar von Stryk. 2008. Formal behavior specification of multi-robot systems using hierarchical state machines in XABSL. In Form. Model. Methods Multi-Robot Syst. Citeseer."},{"key":"e_1_2_1_147_1","volume-title":"Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/HOL (LNCS)","author":"Rizaldi Albert","unstructured":"Albert Rizaldi , Jonas Keinholz , Monika Huber , Jochen Feldle , Fabian Immler , Matthias Althoff , Eric Hilgendorf , and Tobias Nipkow . 2017. Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/HOL (LNCS) , Vol. 10510 . Springer , 50--66. Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, and Tobias Nipkow. 2017. Formalising and monitoring traffic rules for autonomous vehicles in Isabelle\/HOL (LNCS), Vol. 10510. Springer, 50--66."},{"key":"e_1_2_1_148_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-6205-y"},{"key":"e_1_2_1_150_1","unstructured":"Christopher Rouff Amy Vanderbilt Walter Truszkowski James Rash and Michael Hinchey. 2004. Formal methods for autonomic and swarm-based systems. In Leveraging Appl. Form. Methods. 100--102.  Christopher Rouff Amy Vanderbilt Walter Truszkowski James Rash and Michael Hinchey. 2004. Formal methods for autonomic and swarm-based systems. In Leveraging Appl. Form. Methods. 100--102."},{"key":"e_1_2_1_151_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.1999.811709"},{"key":"e_1_2_1_152_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCVE.2014.7297637"},{"key":"e_1_2_1_153_1","volume-title":"Int. Conf. Machine Learning","volume":"70","author":"Selsam Daniel","year":"2017","unstructured":"Daniel Selsam , Percy Liang , and David L Dill . 2017 . Developing bug-free machine learning systems with formal mathematics . In Int. Conf. Machine Learning , Vol. 70 . JMLR, 4661--4670. Daniel Selsam, Percy Liang, and David L Dill. 2017. Developing bug-free machine learning systems with formal mathematics. In Int. Conf. Machine Learning, Vol. 70. JMLR, 4661--4670."},{"key":"e_1_2_1_154_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.1998.703255"},{"key":"e_1_2_1_155_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377576.2377592"},{"key":"e_1_2_1_156_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2000.893218"},{"key":"e_1_2_1_157_1","unstructured":"Olivier Simonin and Jacques Ferber. 2000. Modeling self satisfaction and altruism to handle action selection and reactive cooperation. Simul. Adapt. Behav. from Anim. to Animat. 314--323. Retrieved from https:\/\/www.researchgate.net\/publication\/246850928  Olivier Simonin and Jacques Ferber. 2000. Modeling self satisfaction and altruism to handle action selection and reactive cooperation. Simul. Adapt. Behav. from Anim. to Animat. 314--323. Retrieved from https:\/\/www.researchgate.net\/publication\/246850928"},{"key":"e_1_2_1_158_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_21"},{"key":"e_1_2_1_159_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_6"},{"key":"e_1_2_1_160_1","volume-title":"Can robot navigation bugs be found in simulation? An exploratory study","author":"Sotiropoulos Thierry","unstructured":"Thierry Sotiropoulos , H\u00e9l\u00e8ne Waeselynck , J\u00e9r\u00e9mie Guiochet , and F\u00e9lix Ingrand . 2017. Can robot navigation bugs be found in simulation? An exploratory study . In Softw. Qual. Reliab. Secur., Mladen Vouk, Irena Bojanova, Manuel Nu\u00f1ez, Tadashi Dohi, and Xiaoying Bai (Eds.). IEEE , 150--159. Thierry Sotiropoulos, H\u00e9l\u00e8ne Waeselynck, J\u00e9r\u00e9mie Guiochet, and F\u00e9lix Ingrand. 2017. Can robot navigation bugs be found in simulation? An exploratory study. In Softw. Qual. Reliab. Secur., Mladen Vouk, Irena Bojanova, Manuel Nu\u00f1ez, Tadashi Dohi, and Xiaoying Bai (Eds.). IEEE, 150--159."},{"key":"e_1_2_1_161_1","first-page":"3","article-title":"The SmartMDSD toolchain: An integrated MDSD workflow and IDE for robotics software","author":"Stampfer Dennis","year":"2016","unstructured":"Dennis Stampfer . 2016 . The SmartMDSD toolchain: An integrated MDSD workflow and IDE for robotics software . J. Softw. Eng. Robot. 1 , July (2016), 3 -- 19 . Dennis Stampfer. 2016. The SmartMDSD toolchain: An integrated MDSD workflow and IDE for robotics software. J. Softw. Eng. Robot. 1, July (2016), 3--19.","journal-title":"J. Softw. Eng. Robot. 1"},{"key":"e_1_2_1_162_1","volume-title":"Merk","author":"Steinberg Dave","year":"2008","unstructured":"Dave Steinberg , Frank Budinsky , Marcelo Paternostro , and Ed Merk . 2008 . Eclipse Modeling Framework (2nd ed.). Addison-Wesley . 744 pages. Dave Steinberg, Frank Budinsky, Marcelo Paternostro, and Ed Merk. 2008. Eclipse Modeling Framework (2nd ed.). Addison-Wesley. 744 pages."},{"key":"e_1_2_1_163_1","volume-title":"Verification and Control of Hybrid Systems: A Symbolic Approach","author":"Tabdada Paulo","unstructured":"Paulo Tabdada . 2009. Verification and Control of Hybrid Systems: A Symbolic Approach . Springer . 1--202. Paulo Tabdada. 2009. Verification and Control of Hybrid Systems: A Symbolic Approach. Springer. 1--202."},{"key":"e_1_2_1_164_1","doi-asserted-by":"publisher","DOI":"10.1109\/IROS.2014.6942970"},{"key":"e_1_2_1_165_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33678-2_18"},{"key":"e_1_2_1_166_1","doi-asserted-by":"publisher","DOI":"10.5555\/1732643.1732745"},{"key":"e_1_2_1_167_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-51100-9_34"},{"key":"e_1_2_1_168_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"e_1_2_1_169_1","series-title":"Lecture Notes in Computer Science","volume-title":"Logics Concurr. - Struct. versus Autom","author":"Vardi Moshe","unstructured":"Moshe Vardi . 1996. An automata-theoretic approach to linear temporal logic . In Logics Concurr. - Struct. versus Autom . Lecture Notes in Computer Science , Vol. 1043 . Springer , 238--266. Moshe Vardi. 1996. An automata-theoretic approach to linear temporal logic. In Logics Concurr. - Struct. versus Autom. Lecture Notes in Computer Science, Vol. 1043. Springer, 238--266."},{"key":"e_1_2_1_170_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_1_171_1","first-page":"33","article-title":"The ArmarX statechart concept: Graphical programing of robot behavior","author":"W\u00e4chter Mirko","year":"2016","unstructured":"Mirko W\u00e4chter , Simon Ottenhaus , Manfred Kr\u00f6hnert , Nikolaus Vahrenkamp , and Tamim Asfour . 2016 . The ArmarX statechart concept: Graphical programing of robot behavior . Front. Robot. AI 3 , June (2016), 33 . Mirko W\u00e4chter, Simon Ottenhaus, Manfred Kr\u00f6hnert, Nikolaus Vahrenkamp, and Tamim Asfour. 2016. The ArmarX statechart concept: Graphical programing of robot behavior. Front. Robot. AI 3, June (2016), 33.","journal-title":"Front. Robot. AI 3"},{"key":"e_1_2_1_172_1","volume-title":"Experiences in applying formal verification in robotics (LNCS)","author":"Walter Dennis","unstructured":"Dennis Walter , Holger T\u00e4ubig , and Christoph L\u00fcth . 2010. Experiences in applying formal verification in robotics (LNCS) , Vol. 6351 . Springer , 347--360. Dennis Walter, Holger T\u00e4ubig, and Christoph L\u00fcth. 2010. Experiences in applying formal verification in robotics (LNCS), Vol. 6351. Springer, 347--360."},{"key":"e_1_2_1_173_1","first-page":"1","article-title":"Generating certification evidence for autonomous unmanned aircraft using model checking and simulation","volume":"11","author":"Webster Matt","year":"2014","unstructured":"Matt Webster , Neil Cameron , Michael Fisher , and Mike Jump . 2014 . Generating certification evidence for autonomous unmanned aircraft using model checking and simulation . J. Aerosp. Inf. Syst. 11 , 5 (2014), 1 -- 31 . Matt Webster, Neil Cameron, Michael Fisher, and Mike Jump. 2014. Generating certification evidence for autonomous unmanned aircraft using model checking and simulation. J. Aerosp. Inf. Syst. 11, 5 (2014), 1--31.","journal-title":"J. Aerosp. Inf. Syst."},{"key":"e_1_2_1_174_1","volume-title":"Kheng Lee Koay, and Kerstin Dautenhahn","author":"Webster Matt","year":"2014","unstructured":"Matt Webster , Clare Dixon , Michael Fisher , Maha Salem , Joe Saunders , Kheng Lee Koay, and Kerstin Dautenhahn . 2014 . Formal verification of an autonomous personal robotic assistant. In AAAI FVHMS, 74--79. Retrieved from http:\/\/www.aaai.org\/ocs\/index.php\/SSS\/SSS14\/paper\/download\/7734\/7762. Matt Webster, Clare Dixon, Michael Fisher, Maha Salem, Joe Saunders, Kheng Lee Koay, and Kerstin Dautenhahn. 2014. Formal verification of an autonomous personal robotic assistant. In AAAI FVHMS, 74--79. Retrieved from http:\/\/www.aaai.org\/ocs\/index.php\/SSS\/SSS14\/paper\/download\/7734\/7762."},{"key":"e_1_2_1_175_1","doi-asserted-by":"publisher","DOI":"10.1109\/THMS.2015.2425139"},{"key":"e_1_2_1_176_1","volume-title":"Formal methods for the certification of autonomous unmanned aircraft systems (LNCS)","author":"Webster Matt","unstructured":"Matt Webster , Michael Fisher , Neil Cameron , and Mike Jump . 2011. Formal methods for the certification of autonomous unmanned aircraft systems (LNCS) , Vol. 6894 . Springer , 228--242. Matt Webster, Michael Fisher, Neil Cameron, and Mike Jump. 2011. Formal methods for the certification of autonomous unmanned aircraft systems (LNCS), Vol. 6894. Springer, 228--242."},{"key":"e_1_2_1_177_1","doi-asserted-by":"publisher","DOI":"10.1145\/2347583.2347592"},{"key":"e_1_2_1_178_1","doi-asserted-by":"publisher","DOI":"10.1145\/1809049.1809078"},{"key":"e_1_2_1_179_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168260.2168268"},{"key":"e_1_2_1_180_1","doi-asserted-by":"publisher","DOI":"10.1109\/RE.2009.36"},{"key":"e_1_2_1_181_1","volume-title":"The case for an ethical black box (LNAI)","author":"Winfield Alan","unstructured":"Alan Winfield and Marina Jirotka . 2017. The case for an ethical black box (LNAI) , Vol. 10454 . Springer , 262--273. Alan Winfield and Marina Jirotka. 2017. The case for an ethical black box (LNAI), Vol. 10454. Springer, 262--273."},{"key":"e_1_2_1_182_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11721-008-0018-0"},{"key":"e_1_2_1_183_1","doi-asserted-by":"publisher","DOI":"10.1504\/IJMIC.2006.008645"},{"key":"e_1_2_1_184_1","doi-asserted-by":"publisher","DOI":"10.5772\/5769"},{"key":"e_1_2_1_185_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_2_1_186_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-010-9146-1"},{"key":"e_1_2_1_187_1","volume-title":"Swarm Robot., Erol \u015eahin and William M","author":"\u015eahin Erol","unstructured":"Erol \u015eahin . 2005. Swarm robotics: From sources of inspiration to domains of application . In Swarm Robot., Erol \u015eahin and William M . Spears (Eds.). Springer Berlin Heidelberg, Berlin , Heidelberg , 10--20. Erol \u015eahin. 2005. Swarm robotics: From sources of inspiration to domains of application. In Swarm Robot., Erol \u015eahin and William M. Spears (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 10--20."}],"container-title":["ACM Computing Surveys"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3342355","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3342355","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:02Z","timestamp":1750206362000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3342355"}},"subtitle":["A Survey"],"short-title":[],"issued":{"date-parts":[[2019,9,13]]},"references-count":185,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,9,30]]}},"alternative-id":["10.1145\/3342355"],"URL":"https:\/\/doi.org\/10.1145\/3342355","relation":{},"ISSN":["0360-0300","1557-7341"],"issn-type":[{"value":"0360-0300","type":"print"},{"value":"1557-7341","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,9,13]]},"assertion":[{"value":"2018-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2019-09-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}