{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T20:44:48Z","timestamp":1648673088297},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            As autonomous systems become more prevalent, methods for their verification will become more widely used. Model checking is a formal verification technique that can help ensure the safety of autonomous systems, but in most cases it cannot be applied by novices, or in its straight \u201coff-the-shelf\u201d form. In order to be more widely applicable it is crucial that more sophisticated techniques are used, and are presented in a way that is reproducible by engineers and verifiers alike. In this paper we demonstrate in detail two techniques that are used to increase the power of model checking using the model checker S\n            <jats:sc>pin<\/jats:sc>\n            . The first of these is the use of embedded C code within Promela specifications, in order to accurately reflect robot movement. The second is to use abstraction together with a simulation relation to allow us to verify multiple environments simultaneously. We apply these techniques to a fairly simple system in which a robot moves about a fixed circular environment and learns to avoid obstacles. The learning algorithm is inspired by the way that insects learn to avoid obstacles in response to pain signals received from their antennae. Crucially, we prove that our abstraction is sound for our example system\u2014a step that is often omitted but is vital if formal verification is to be widely accepted as a useful and meaningful approach.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0382-2","type":"journal-article","created":{"date-parts":[[2016,6,8]],"date-time":"2016-06-08T05:35:31Z","timestamp":1465364131000},"page":"1027-1056","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model checking learning agent systems using Promela with embedded C code and abstraction"],"prefix":"10.1145","volume":"28","author":[{"given":"Ryan","family":"Kirwan","sequence":"first","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alice","family":"Miller","sequence":"additional","affiliation":[{"name":"School of Computing Science, University of Glasgow, Glasgow, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Porr","sequence":"additional","affiliation":[{"name":"School of Engineering, University of Glasgow, Glasgow, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Alur R Courcoubetis C Halbwachs N Henzinger T Ho P-H Nicollin X Olivero A Sifakis J Yovine S (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138:3\u201334","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alur R Grosu R Lee I Sokolsky O (2001) Compositional refinement of hiererarchical hybrid systems. Vol. 2034 of Lecture Notes in Computer Science. Springer Berlin Heidelberg Rome pp 33\u201348.","DOI":"10.1007\/3-540-45351-2_7"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Antuna L Ilan D CAmpos S Eder K (2015) symmetry reduction enables model checking of more complex emergent behaviours of swarm navigation algorithms. In: Towards autonomous robotic systems vol. 9287 of Lecture Notes in Computing Science. Springer New York pp 26\u201337","DOI":"10.1007\/978-3-319-22416-9_4"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/2700318"},{"key":"e_1_2_1_2_5_2","volume-title":"Vehicles: experiments in synthetic psychology","author":"Braitenberg V","year":"1984"},{"key":"e_1_2_1_2_6_2","unstructured":"B\u00fcchi J (1960) On a decision method in restricted second order arithmetic. In: Proceedings of the International Congress on Logic Method and Philosophy of Science. Stanford University Press pp 1\u201312"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Cattel T (1994) Modeling and verification of a multiprocessor realtime OS kernel. In: Hogrefe D Leue S (eds) Proceedings of the 7th WG6.1 International Conference on Formal Description Techniques (FORTE \u201894) vol. 6 of International Federation For Information Processing. Chapman and Hall Berne Switzerland pp 55\u201370","DOI":"10.1007\/978-0-387-34878-0_4"},{"key":"e_1_2_1_2_8_2","unstructured":"Cimatti A Giunchiglia F Mingardi G Romano D Torielli F Traverso P (1997) Model checking safety critical software with SPIN: an application to a railway interlocking system. In: Langerak R (ed) Proceedings of the 3rd SPIN Workshop (SPIN\u201897). Twente University The Netherlands pp. 5\u201317"},{"key":"e_1_2_1_2_9_2","volume-title":"Model checking","author":"Clarke E","year":"1999"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.03.034"},{"key":"e_1_2_1_2_11_2","unstructured":"Dill D (1996) The Mur\u03d5 verification system. In: Alur R Henzinger T (eds) Proceedings of the 8th International Conference on Computer Aided Verification (CAV \u201896) vol. 1102 of Lecture Notes in Computer Science. Springer New Brunswick pp 390\u2013393"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2012.03.003"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/2494558"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.08.008"},{"key":"e_1_2_1_2_15_2","unstructured":"Guo M Johansson K Dimarogonas (2013) Revising motion planning under linear temporal logic specifications in partially known workspaces. In: IEEE international Conference Robotics and Automation"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Gallardo M Merino P Salmer\u00f3n A (2016) River basin management with SPIN. In: Proceedings of the 23rd International SPIN symposium on Model Checking of Software (SPIN 2016) (to appear)","DOI":"10.1007\/978-3-319-32582-8_5"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hoffman R Ireland M Miller A Norman G Veres S (2016) Autonomous agent behaviour modelled in PRISM. In: Proceedings of the 23rd International SPIN symposium on Model Checking of Software (SPIN 2016) (to appear)","DOI":"10.1007\/978-3-319-32582-8_7"},{"key":"e_1_2_1_2_18_2","first-page":"441","article-title":"Prism: a tool for automatic verification of probabilistic systems","volume":"3920","author":"Hinton A","year":"2006","journal-title":"LNCS"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (2003) Trends in software verification. In: Araki K Gnesi S Mandrioli D (eds) Proceedings of the International Symposium on Formal Methods Europe (FME 2006) vol. 2805 of Lecture Notes in Computer Science. Springer Pisa Italy pp 40\u201350","DOI":"10.1007\/978-3-540-45236-2_4"},{"key":"e_1_2_1_2_20_2","unstructured":"Holzmann G (2004) The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Pearson Education"},{"key":"e_1_2_1_2_21_2","unstructured":"(2002) Proceedings of the 5th International Workshop on Hybrid Systems: Computation and Control (HSCC \u201902) vol. 2289 of Lecture Notes in Computer Science. Springer Berlin Heidelberg Santa Barbara"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Humphrey L (2013) Model checking for verification in uav cooperative control applications. Vol. 444 of Lecture Notes in Computer Science. Springer New York pp 69\u2013117.","DOI":"10.1007\/978-3-642-37694-8_4"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Jeyaraman S Tsourdos A Zbikowski R White B (2006) Kripke modelling approaches of a multiple robots system with minimalist communication: a formal approach of choice. Int J Syst Sci 37(6):339\u2013349","DOI":"10.1080\/00207720500438472"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Kloetzer M Belta C (2006) Hierarchical abstractions for robotic swarms. In: Proceedings of the IEEE International Conference on Robotics and Automation (ICRA 2006) pp 952\u2013957","DOI":"10.1109\/ROBOT.2006.1641832"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2006.889492"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.robot.2011.10.005"},{"key":"e_1_2_1_2_27_2","unstructured":"Kirwan RF (2014) Applying model checking to agent-based learning systems. Ph.D. thesis University of Glasgow"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00422-010-0396-4"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Kumar S Li K (2002) Using model checking to debug device firmware. In: Proceedings of the 5th Symposium on Operating System Design and Implementation (OSDI 2002). USENIX Boston","DOI":"10.1145\/1060289.1060296"},{"key":"e_1_2_1_2_30_2","unstructured":"Kouvaros P Lomuscio A (2015) A counter abstraction technique for the verification of robot swarms. In: Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence. Austin pp 2081\u20132088"},{"key":"e_1_2_1_2_31_2","unstructured":"Kirwan R Miller A Porr B (2016). doi:10.5525\/gla.researchdata.310"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1162\/NECO_a_00493"},{"key":"e_1_2_1_2_33_2","first-page":"83","article-title":"Semantical considerations on modal logics","volume":"16","author":"Kripke S","year":"1963","journal-title":"Acta Philos Fenn"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"McMillan K (1993) Symbolic model checking. Boston","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_1_2_35_2","unstructured":"Merz S (2000) Model checking: a tutorial overview. In: Cassez F Jard C Rozoy B Ryan M (eds) Modeling and verification of parallel processes 4th Summer School MOVEP vol. 2067 of Lecture Notes in Computer Science. Springer Nantes"},{"key":"e_1_2_1_2_36_2","unstructured":"Milner R (1971) An algebraic definition of simulation between programs. In: Proceedings of the 2nd International Joint Conference on Artificial Intelligence pp 481\u2013489"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm M Schmidt D Steffen B (1999) Model-checking: a tutorial introduction. In: Cortesi A File G (eds) Proceedings of the 6th International Static Analysis Symposium (SAS\u201999) vol. 1694 of Lecture Notes in Computer Science (LNCS). Springer Venice pp 330\u2013354","DOI":"10.1007\/3-540-48294-6_22"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Porr B von Ferber C W\u00f6rg\u00f6tter F (2003) ISO-learning approximates a solution to the inverse-controller problem in an unsupervised behavioural paradigm. Neural Comput 15(4):865\u2013884","DOI":"10.1162\/08997660360581930"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1162\/neco.2006.18.6.1380"},{"key":"e_1_2_1_2_40_2","unstructured":"Sutton R Barto A (1987) A temporal-difference model of classical conditioning. In: Proceedings of the Ninth Annual Conference of the Cognitive Science Society. Seattle Washington pp 355\u2013378"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Stocker R Dennis L Dixon C Fisher M (2012) Verifiying Brahms human-robot teamwork models. In: Proceedings of the 13th European conference on logics in Artificial Intelligence (JELIA-2012) pp 385\u2013397","DOI":"10.1007\/978-3-642-33353-8_30"},{"key":"e_1_2_1_2_42_2","unstructured":"Sierhuis M (2001) Modeling and simulating work practice. BRAHMS: A multi-agent modeling and simulation language for work system analysis and design. Ph.D. thesis University of Amsterdam"},{"key":"#cr-split#-e_1_2_1_2_43_2.1","doi-asserted-by":"crossref","unstructured":"Sharma O Lewis J Miller A Dearle A Balasubramaniam D Morrison R Sventek J (2009) Towards verifying correctness of wireless sensor network applications using insense and spin. In: P\u0103sr\u0103eanu C","DOI":"10.1007\/978-3-642-02652-2_19"},{"key":"#cr-split#-e_1_2_1_2_43_2.2","unstructured":"(ed) Proceedings of the 16th International SPIN Workshop (SPIN 2009) Lecture Notes in Computer Science. Springer Grenoble pp 223-240"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Stauner T (2002) Discrete-time refinement of hybrid automata. In: Sta02 [hsc02] pp 407\u2013420","DOI":"10.1007\/3-540-45873-5_32"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Tiwari A Khanna G (2002) Series of abstractions for hybrid automata. In: TiwKha02 [hsc02] pp 465\u2013478","DOI":"10.1007\/3-540-45873-5_36"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Weissman M Bedenk S Buckl C Knoll A (2011) Model checking industrial robot systems. In: Groce A Musuvathi M (eds) Proceedings of the 18th International SPIN Workshop (SPIN 2009) vol. 6823 of Lecture Notes in Computer Science. Springer Snowbird pp 161\u2013176","DOI":"10.1007\/978-3-642-22306-8_11"},{"key":"e_1_2_1_2_47_2","first-page":"1","article-title":"Toward reliable autonomous robotic assistants through formal verification: a case study","volume":"99","author":"Webster M","year":"2015","journal-title":"IEEE Trans Human Mach Syst"},{"key":"#cr-split#-e_1_2_1_2_48_2.1","doi-asserted-by":"crossref","unstructured":"Yuen C Tjioe W (2001) Modeling and verifying a price model for congestion control in computer networks using Promela\/Spin. In: Dwyer MB","DOI":"10.1007\/3-540-45139-0_17"},{"key":"#cr-split#-e_1_2_1_2_48_2.2","unstructured":"(ed) Proceedings of the 8th International SPIN Workshop (SPIN 2001) vol. 2057 of Lecture Notes in Computer Science. Springer Toronto Canada pp 272-287"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0382-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0382-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0382-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0382-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:05:21Z","timestamp":1641485121000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0382-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":50,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["10.1007\/s00165-016-0382-2"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0382-2","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11]]}}}