{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T14:40:09Z","timestamp":1777560009370,"version":"3.51.4"},"reference-count":123,"publisher":"SAGE Publications","issue":"4","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["AIC"],"published-print":{"date-parts":[[2022,9,20]]},"abstract":"<jats:p>The Autonomy and Verification group11 Part of a wider, international, Autonomy and Verification Network of activity: https:\/\/autonomy-and-verification.github.io sits within the Department of Computer Science22 https:\/\/www.cs.manchester.ac.uk at the University of Manchester. The group has a long history of research into agents and multi-agent systems (both at Manchester and, previously, at the University of Liverpool) particularly in the areas of formal specification and verification, multi-agent programming, ethical agent reasoning, and swarms, teams and organisations.<\/jats:p>","DOI":"10.3233\/aic-220115","type":"journal-article","created":{"date-parts":[[2022,9,9]],"date-time":"2022-09-09T13:26:05Z","timestamp":1662729965000},"page":"421-431","source":"Crossref","is-referenced-by-count":1,"title":["Verifiable autonomy: From theory to applications"],"prefix":"10.1177","volume":"35","author":[{"given":"Louise","family":"Dennis","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clare","family":"Dixon","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Fisher","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Manchester, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"179","reference":[{"issue":"6","key":"10.3233\/AIC-220115_ref1","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1109\/MIS.2018.111144814","article-title":"Autonomous nuclear waste management","volume":"33","author":"Aitken","year":"2018","journal-title":"IEEE Intell. Syst."},{"key":"10.3233\/AIC-220115_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_13"},{"key":"10.3233\/AIC-220115_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-35092-5_4"},{"key":"10.3233\/AIC-220115_ref4","doi-asserted-by":"publisher","DOI":"10.3390\/jsan10030041"},{"key":"10.3233\/AIC-220115_ref5","unstructured":"G. Alves, L.A. Dennis and M. Fisher, An agent-based architecture with support to ethical decisions on a road traffic scenario, in: IROS Workshop on Building and Evaluating Ethical Robotic Systems (ERS 2021), 2021."},{"key":"10.3233\/AIC-220115_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-14628-3_10"},{"key":"10.3233\/AIC-220115_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54994-7_16"},{"key":"10.3233\/AIC-220115_ref8","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3938851"},{"key":"10.3233\/AIC-220115_ref9","unstructured":"F. Amirabdollahian, K. Dautenhahn, C. Dixon, K. Eder, M. Fisher, K.L. Koay, E. Magid, A. Pipe, M. Salem, J. Saunders and M. Webster, Can you trust your robotic assistant? in: International Conference on Social Robotics, LNCS, Vol. 8239, Springer, 2013, pp. 571\u2013573."},{"key":"10.3233\/AIC-220115_ref10","unstructured":"H. Barringer, M. Fisher, D. Gabbay, R. Owens and M. Reynolds (eds), The Imperative Future: Principles of Executable Temporal Logics, Research Studies Press, 1996."},{"key":"10.3233\/AIC-220115_ref11","doi-asserted-by":"crossref","unstructured":"R.H. Bordini, M. Fisher, C. Pardavila and M. Wooldridge, Model checking AgentSpeak, in: Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-2003), 2003.","DOI":"10.1145\/860575.860641"},{"issue":"5","key":"10.3233\/AIC-220115_ref12","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/MIS.2004.47","article-title":"Model checking rational agents","volume":"19","author":"Bordini","year":"2004","journal-title":"IEEE Intelligent Systems"},{"issue":"2","key":"10.3233\/AIC-220115_ref13","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","article-title":"Verifying multi-agent programs by model checking","volume":"12","author":"Bordini","year":"2006","journal-title":"Journal of Autonomous Agents and Multi-Agent Systems"},{"key":"10.3233\/AIC-220115_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_4"},{"key":"10.3233\/AIC-220115_ref15","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2019.2898267"},{"key":"10.3233\/AIC-220115_ref17","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.329.2"},{"key":"10.3233\/AIC-220115_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51417-4_10"},{"key":"10.3233\/AIC-220115_ref19","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.3938851"},{"key":"10.3233\/AIC-220115_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55754-6_20"},{"key":"10.3233\/AIC-220115_ref21","doi-asserted-by":"publisher","DOI":"10.3390\/computers10020016"},{"key":"10.3233\/AIC-220115_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-66412-1_13"},{"key":"10.3233\/AIC-220115_ref23","doi-asserted-by":"crossref","unstructured":"R.C. Cardoso, A. Ferrando, L.A. Dennis and M. Fisher, Implementing ethical governors in BDI, in: 9th International Workshop on Engineering Multi-Agent Systems, 2021.","DOI":"10.1007\/978-3-030-97457-2_2"},{"key":"10.3233\/AIC-220115_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59299-8_2"},{"key":"10.3233\/AIC-220115_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85739-4_5"},{"key":"10.3233\/AIC-220115_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88549-6_4"},{"key":"10.3233\/AIC-220115_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s43154-021-00058-1"},{"key":"10.3233\/AIC-220115_ref28","doi-asserted-by":"publisher","DOI":"10.32473\/flairs.v34i1.128481"},{"key":"10.3233\/AIC-220115_ref29","unstructured":"V. Charisi, L.A. Dennis, M. Fisher, R. Lieck, A. Matthias, M. Slavkovik, J. Sombetzki, A.F.T. Winfield and R. Yampolskiy, Towards Moral Autonomous Systems, CoRR Abs\/1703.04741, 2017, http:\/\/arxiv.org\/abs\/1703.04741."},{"key":"10.3233\/AIC-220115_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-69128-8_2"},{"key":"10.3233\/AIC-220115_ref31","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1006\/ijhc.1998.0229","article-title":"Brahms: Simulating practice for work systems design","volume":"49","author":"Clancey","year":"1998","journal-title":"International Journal on Human-Computer Studies"},{"key":"10.3233\/AIC-220115_ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-66494-7_7"},{"key":"10.3233\/AIC-220115_ref33","doi-asserted-by":"publisher","DOI":"10.21105\/joss.00617"},{"key":"10.3233\/AIC-220115_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s11948-020-00244-y"},{"key":"10.3233\/AIC-220115_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40379-3_8"},{"key":"10.3233\/AIC-220115_ref36","doi-asserted-by":"crossref","unstructured":"L.A. Dennis, M.M. Bentzen, F. Lindner and M. Fisher, Verifiable machine ethics in changing contexts, in: Proceedings of the AAAI Conference on Artificial Intelligence 35(13), 2021, pp. 11470\u201311478, https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/17366.","DOI":"10.1609\/aaai.v35i13.17366"},{"key":"10.3233\/AIC-220115_ref37","unstructured":"L.A. Dennis and C.P. del Olmo, A defeasible logic implementation of ethical reasoning, in: First International Workshop on Computational Machine Ethics (CME-2021), 2021."},{"key":"10.3233\/AIC-220115_ref38","doi-asserted-by":"crossref","unstructured":"L.A. Dennis, B. Farwer, R.H. Bordini, M. Fisher and M. Wooldridge, A common semantic basis for BDI languages, in: Proc. 7th International Workshop on Programming Multiagent Systems (ProMAS), LNAI, Vol. 4908, Springer, 2008, pp. 124\u2013139.","DOI":"10.1007\/978-3-540-79043-3_8"},{"key":"10.3233\/AIC-220115_ref39","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-419-0-995"},{"key":"10.3233\/AIC-220115_ref40","unstructured":"L.A. Dennis and M. Fisher, Practical challenges in explicit ethical machine reasoning, in: International Symposium on Artificial Intelligence and Mathematics, ISAIM 2018, Fort Lauderdale, Florida, USA, January 3\u20135, 2018, 2018, http:\/\/isaim2018.cs.virginia.edu\/papers\/ISAIM2018_Ethics_Dennis_Fischer.pdf."},{"key":"10.3233\/AIC-220115_ref41","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2020.2991262"},{"key":"10.3233\/AIC-220115_ref42","doi-asserted-by":"crossref","unstructured":"L.A. Dennis and M. Fisher, Verifiable Autonomous Systems \u2013 Using Rational Agents to Provide Assurance About Decisions Made by Machines, Cambridge University Press, 2022, (To appear).","DOI":"10.1017\/9781108755023"},{"issue":"3","key":"10.3233\/AIC-220115_ref43","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s13218-014-0308-1","article-title":"Reconfigurable autonomy","volume":"28","author":"Dennis","year":"2014","journal-title":"KI \u2013 K\u00fcnstliche Intelligenz"},{"issue":"3","key":"10.3233\/AIC-220115_ref44","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/s10515-014-0168-9","article-title":"Practical verification of decision-making in agent-based autonomous systems","volume":"23","author":"Dennis","year":"2016","journal-title":"Autom. Softw. Eng."},{"issue":"3","key":"10.3233\/AIC-220115_ref45","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1109\/MIS.2010.88","article-title":"Satellite control using rational agent programming","volume":"25","author":"Dennis","year":"2010","journal-title":"IEEE Intelligent Systems"},{"key":"10.3233\/AIC-220115_ref46","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.robot.2015.11.012","article-title":"Formal verification of ethical choices in autonomous systems","volume":"77","author":"Dennis","year":"2016","journal-title":"Robotics and Autonomous Systems"},{"issue":"3","key":"10.3233\/AIC-220115_ref47","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1093\/logcom\/exv002","article-title":"Two-stage agent program verification","volume":"28","author":"Dennis","year":"2018","journal-title":"J. Log. Comput."},{"issue":"1","key":"10.3233\/AIC-220115_ref48","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s10515-011-0088-x","article-title":"Model checking agent programming languages","volume":"19","author":"Dennis","year":"2012","journal-title":"Automated Software Engineering"},{"key":"10.3233\/AIC-220115_ref50","unstructured":"L.A. Dennis and N. Oren, Explaining BDI agent behaviour through dialogue, in: 20th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021), 2021, pp. 429\u2013437."},{"key":"10.3233\/AIC-220115_ref51","unstructured":"L.A. Dennis and M. Slavkovik, Machines that know right and cannot do wrong: The theory and practice of machine ethics, IEEE Intelligent Informatics Bulletin 19(1) (2018), http:\/\/www.comp.hkbu.edu.hk\/~cib\/2018\/Aug\/article2\/iib_vol19no1_article2.pdf."},{"key":"10.3233\/AIC-220115_ref52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66595-5_3"},{"key":"10.3233\/AIC-220115_ref53","doi-asserted-by":"crossref","unstructured":"F. Dinmohammadi, M. Fisher, D. Flynn, M. Jump, V. Page, C. Patchett, V. Robu, W. Tang and M. Webster, Certification of safe and trusted robotic inspection of assets, in: Proceedings of the Prognostics and System Health Management Conference, Chongqing, China, 2018.","DOI":"10.1109\/PHM-Chongqing.2018.00054"},{"issue":"1","key":"10.3233\/AIC-220115_ref54","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0004-3702(02)00196-0","article-title":"Resolution in a logic of rational agency","volume":"139","author":"Dixon","year":"2002","journal-title":"Artificial Intelligence"},{"key":"10.3233\/AIC-220115_ref55","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.entcs.2006.11.043","article-title":"Temporal logics of knowledge and their applications in security","volume":"186","author":"Dixon","year":"2007","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"10.3233\/AIC-220115_ref56","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1016\/j.jal.2012.07.001","article-title":"Deductive temporal reasoning with constraints","volume":"11","author":"Dixon","year":"2013","journal-title":"J. Appl. Log."},{"key":"10.3233\/AIC-220115_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10401-0_9"},{"key":"10.3233\/AIC-220115_ref58","doi-asserted-by":"publisher","first-page":"1429","DOI":"10.1016\/j.robot.2012.03.003","article-title":"Towards temporal verification of swarm robotic systems","volume":"60","author":"Dixon","year":"2012","journal-title":"Robotics and Autonomous Systems"},{"key":"10.3233\/AIC-220115_ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30446-1_25"},{"key":"10.3233\/AIC-220115_ref60","unstructured":"M. Farrell, R.C. Cardoso, L. Dennis, C. Dixon, M. Fisher, G. Kourtis, A. Lisitsa, M. Luckcuck and M. Webster, Modular verification of autonomous space robotics, in: Assurance of Autonomy for Robotic Space Missions Workshop, 2019."},{"key":"10.3233\/AIC-220115_ref61","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98938-9_10"},{"key":"10.3233\/AIC-220115_ref62","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW53611.2021.00109"},{"key":"10.3233\/AIC-220115_ref63","doi-asserted-by":"publisher","DOI":"10.3389\/frobt.2021.639282"},{"key":"10.3233\/AIC-220115_ref64","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.257.5"},{"key":"10.3233\/AIC-220115_ref65","doi-asserted-by":"crossref","unstructured":"A. Ferrando and R.C. Cardoso, Towards partial monitoring: It is always too soon to give up, in: Proceedings Third Workshop on Formal Methods for Autonomous Systems, 2021.","DOI":"10.4204\/EPTCS.348.3"},{"key":"10.3233\/AIC-220115_ref66","doi-asserted-by":"crossref","unstructured":"A. Ferrando and R.C. Cardoso, RVPLAN: A general purpose framework for replanning using runtime verification, in: Proceedings of the 5th ACM International Workshop on Verification and MOnitoring at Runtime EXecution (VORTEX\u201921), 2021.","DOI":"10.1145\/3464974.3468447"},{"key":"10.3233\/AIC-220115_ref67","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-63486-5_40"},{"key":"10.3233\/AIC-220115_ref68","unstructured":"A. Ferrando, L.A. Dennis, D. Ancona, M. Fisher and V. Mascardi, Recognising assumption violations in autonomous systems verification, in: Proc. 17th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), IFAAMAS\/ACM, 2018, pp. 1933\u20131935, http:\/\/dl.acm.org\/citation.cfm?id=3238028."},{"key":"10.3233\/AIC-220115_ref69","doi-asserted-by":"crossref","unstructured":"A. Ferrando, L.A. Dennis, D. Ancona, M. Fisher and V. Mascardi, Verifying and validating autonomous systems: An integrated approach, in: Proc. 8th IEEE International Conference on Runtime Verification (RV), 2018.","DOI":"10.1007\/978-3-030-03769-7_15"},{"key":"10.3233\/AIC-220115_ref70","doi-asserted-by":"publisher","DOI":"10.1145\/3447246"},{"key":"10.3233\/AIC-220115_ref71","unstructured":"A. Ferrando, Z. Kootbally, P. Piliptchak, R.C. Cardoso, C. Schlenoff and M. Fisher, Runtime verification of the ARIAC competition: Can a robot be agile and safe at the same time? in: AIRO, 2020."},{"key":"10.3233\/AIC-220115_ref72","unstructured":"M. Fisher, Implementing BDI-like systems by direct execution, in: Proc. 15th International Joint Conference on Artificial Intelligence (IJCAI), Morgan-Kaufmann, 1997, pp. 316\u2013321."},{"key":"10.3233\/AIC-220115_ref73","doi-asserted-by":"publisher","DOI":"10.3390\/robotics10020067"},{"key":"10.3233\/AIC-220115_ref74","doi-asserted-by":"publisher","DOI":"10.1109\/ISSREW.2018.00028"},{"issue":"9","key":"10.3233\/AIC-220115_ref75","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/2494558","article-title":"Verifying autonomous systems","volume":"56","author":"Fisher","year":"2013","journal-title":"ACM Communications"},{"key":"10.3233\/AIC-220115_ref76","doi-asserted-by":"crossref","unstructured":"M. Fisher, A. Ferrando and R.C. Cardoso, Increasing confidence in autonomous systems, in: Proceedings of the 5th ACM International Workshop on Verification and MOnitoring at Runtime EXecution (VORTEX\u201921), 2021.","DOI":"10.1145\/3464974.3468452"},{"key":"10.3233\/AIC-220115_ref77","unstructured":"M. Fisher and C. Ghidini, Programming resource-bounded deliberative agents, in: Proc. 16th International Joint Conference on Artificial Intelligence (IJCAI), Morgan Kaufmann, 1999, pp. 200\u2013205."},{"key":"10.3233\/AIC-220115_ref78","doi-asserted-by":"crossref","unstructured":"M. Fisher and C. Ghidini, The ABC of rational agent programming, in: Proc. 1st International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS), ACM Press, 2002, pp. 849\u2013856.","DOI":"10.1145\/544862.544943"},{"issue":"4","key":"10.3233\/AIC-220115_ref79","doi-asserted-by":"publisher","first-page":"59","DOI":"10.4230\/DagRep.9.4.59","article-title":"Ethics and trust: Principles, verification and validation (Dagstuhl seminar 19171)","volume":"9","author":"Fisher","year":"2019","journal-title":"Reports"},{"issue":"5","key":"10.3233\/AIC-220115_ref80","doi-asserted-by":"publisher","first-page":"114","DOI":"10.4230\/DagRep.6.5.114","article-title":"Engineering moral agents \u2013 from human morality to artificial morality (Dagstuhl seminar 16222)","volume":"6","author":"Fisher","year":"2016","journal-title":"Dagstuhl Reports"},{"key":"10.3233\/AIC-220115_ref81","doi-asserted-by":"publisher","DOI":"10.1007\/s10458-020-09487-2"},{"key":"10.3233\/AIC-220115_ref82","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-67113-0_8"},{"key":"10.3233\/AIC-220115_ref83","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40379-3_13"},{"issue":"3","key":"10.3233\/AIC-220115_ref84","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s10703-020-00347-z","article-title":"Multi-scale verification of distributed synchronisation","volume":"55","author":"Gainer","year":"2020","journal-title":"Formal Methods in Systems Design"},{"issue":"10","key":"10.3233\/AIC-220115_ref85","doi-asserted-by":"publisher","first-page":"95","DOI":"10.4230\/DagRep.9.10.95","article-title":"Analysis of autonomous mobile collectives in complex physical environments (Dagstuhl seminar 19432)","volume":"9","author":"Gleirscher","year":"2019","journal-title":"Reports"},{"key":"10.3233\/AIC-220115_ref86","doi-asserted-by":"crossref","unstructured":"A.J. Hepple, L.A. Dennis and M. Fisher, A common basis for agent organisations in BDI languages, in: Proc. International Workshop on LAnguages, Methodologies and Development Tools for Multi-Agent SystemS (LADS), LNAI, Vol. 5118, Springer, 2008, pp. 171\u2013188.","DOI":"10.1007\/978-3-540-85058-8_5"},{"key":"10.3233\/AIC-220115_ref87","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_12"},{"key":"10.3233\/AIC-220115_ref88","doi-asserted-by":"publisher","first-page":"1553","DOI":"10.1007\/s10817-020-09541-4","article-title":"Theorem proving for pointwise metric temporal logic over the naturals via translations","volume":"64","author":"Hustadt","year":"2020","journal-title":"Journal of Automated Reasoning"},{"key":"10.3233\/AIC-220115_ref89","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1016\/j.scico.2017.05.006","article-title":"Formal verification of autonomous vehicle platooning","volume":"148","author":"Kamali","year":"2017","journal-title":"Sci. Comput. Program."},{"key":"10.3233\/AIC-220115_ref90","doi-asserted-by":"crossref","unstructured":"M. Kamali, S. Linker and M. Fisher, Modular verification of vehicle platooning with respect to decisions, space and time, in: Workshop on Formal Techniques for Safety-Critical Systems (FTSCS), 2018, http:\/\/arxiv.org\/abs\/1804.06647.","DOI":"10.1007\/978-3-030-12988-0_2"},{"issue":"1","key":"10.3233\/AIC-220115_ref91","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1515\/pjbr-2021-0028","article-title":"Use and usability of software verification methods to detect behaviour interference when teaching an assistive home companion robot: A proof-of-concept study","volume":"12","author":"Koay","year":"2021","journal-title":"Paladyn, Journal of Behavioral Robotics"},{"key":"10.3233\/AIC-220115_ref92","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51417-4_8"},{"issue":"2","key":"10.3233\/AIC-220115_ref93","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1016\/j.robot.2011.10.005","article-title":"Analysing robot swarm behaviour via probabilistic model checking","volume":"60","author":"Konur","year":"2012","journal-title":"Robotics and Autonomous Systems"},{"key":"10.3233\/AIC-220115_ref94","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.tcs.2013.07.012","article-title":"Combined model checking for temporal, probabilistic, and real-time logics","volume":"503","author":"Konur","year":"2013","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"10.3233\/AIC-220115_ref96","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1109\/MCI.2013.2279559","article-title":"Autonomous asteroid exploration by rational agents","volume":"8","author":"Lincoln","year":"2013","journal-title":"IEEE Computational Intelligence Magazine"},{"key":"10.3233\/AIC-220115_ref97","unstructured":"S. Linker, Hybrid Multi-Lane Spatial Logic, Archive of Formal Proofs, 2017, https:\/\/www.isa-afp.org\/entries\/Hybrid_Multi_Lane_Spatial_Logic.html."},{"key":"10.3233\/AIC-220115_ref98","doi-asserted-by":"crossref","unstructured":"M. Luckcuck and R.C. Cardoso, Formal verification of a map merging protocol in the multi-agent programming contest, in: 9th International Workshop on Engineering Multi-Agent Systems, 2021.","DOI":"10.1007\/978-3-030-97457-2_12"},{"issue":"5","key":"10.3233\/AIC-220115_ref99","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3342355","article-title":"Formal specification and verification of autonomous robotic systems: A survey","volume":"52","author":"Luckcuck","year":"2019","journal-title":"ACM Comput. Surv."},{"key":"10.3233\/AIC-220115_ref100","doi-asserted-by":"publisher","DOI":"10.5281\/ZENODO.5012322"},{"key":"10.3233\/AIC-220115_ref101","doi-asserted-by":"publisher","DOI":"10.1109\/AERO47225.2020.9172563"},{"key":"10.3233\/AIC-220115_ref102","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1016\/j.ic.2019.02.003","article-title":"Sublogics of a branching time logic of robustness","volume":"266","author":"McCabe-Dansted","year":"2019","journal-title":"Information and Computation"},{"key":"10.3233\/AIC-220115_ref103","doi-asserted-by":"crossref","unstructured":"J. Michaloski, M. Aksu, C. Schlenoff, R.C. Cardoso and M. Fisher, Agile tasking of robotic kitting, in: Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021), 2021.","DOI":"10.1115\/IMECE2021-73683"},{"issue":"4","key":"10.3233\/AIC-220115_ref104","doi-asserted-by":"publisher","first-page":"23:1","DOI":"10.1145\/3331448","article-title":"Modal resolution: Proofs, layers, and refinements","volume":"20","author":"Nalon","year":"2019","journal-title":"ACM Trans. Comput. Log."},{"key":"10.3233\/AIC-220115_ref105","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/694"},{"key":"10.3233\/AIC-220115_ref106","doi-asserted-by":"crossref","unstructured":"C. Nalon, U. Hustadt and C. Dixon, KSP a Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments, Springer, 2018.","DOI":"10.1007\/s10817-018-09503-x"},{"issue":"4","key":"10.3233\/AIC-220115_ref107","doi-asserted-by":"publisher","first-page":"883","DOI":"10.1093\/logcom\/ext074","article-title":"A resolution-based calculus for coalition logic","volume":"24","author":"Nalon","year":"2014","journal-title":"J. Log. Comput."},{"key":"10.3233\/AIC-220115_ref108","doi-asserted-by":"publisher","DOI":"10.3390\/robotics10030097"},{"key":"10.3233\/AIC-220115_ref109","unstructured":"V. Page, M. Webster, M. Fisher and M. Jump, Towards a methodology to test UAVs in hazardous environments, in: ICAS 2019, the Fifteenth International Conference on Autonomic and Autonomous Systems, 2019, pp. 38\u201345, http:\/\/www.thinkmind.org\/index.php?view=article&articleid=icas_2019_3_20_28007."},{"key":"10.3233\/AIC-220115_ref110","doi-asserted-by":"crossref","unstructured":"F. Papacchini, C. Nalon, U. Hustadt and C. Dixon, Efficient local reductions to basic modal logic, in: Automated Deduction \u2013 CADE 28, LNCS, Vol. 12699, Springer, 2021.","DOI":"10.1007\/978-3-030-79876-5_5"},{"issue":"1","key":"10.3233\/AIC-220115_ref112","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10619-014-7161-y","article-title":"An abstract formal basis for digital crowds","volume":"33","author":"Slavkovik","year":"2015","journal-title":"Distributed and Parallel Databases"},{"key":"10.3233\/AIC-220115_ref113","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33353-8_30"},{"key":"10.3233\/AIC-220115_ref114","unstructured":"P. Stringer, Adaptable and verifiable BDI reasoning, in: Proc. 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), ACM, 2021, pp. 1835\u20131836, https:\/\/dl.acm.org\/doi\/10.5555\/3463952.3464256."},{"key":"10.3233\/AIC-220115_ref115","doi-asserted-by":"crossref","unstructured":"P. Stringer, R.C. Cardoso, C. Dixon and L.A. Dennis, Implementing durative actions with failure detection in gwendolen, in: 9th International Workshop on Engineering Multi-Agent Systems, 2021.","DOI":"10.1007\/978-3-030-97457-2_19"},{"key":"10.3233\/AIC-220115_ref116","doi-asserted-by":"publisher","DOI":"10.1145\/3319502.3374793"},{"key":"10.3233\/AIC-220115_ref117","unstructured":"M.B. van Riemsdijk, L.A. Dennis, M. Fisher and K.V. Hindriks, A semantic framework for socially adaptive agents: Towards strong norm compliance, in: Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4\u20138, 2015, 2015, pp. 423\u2013432, http:\/\/dl.acm.org\/citation.cfm?id=2772935."},{"issue":"2","key":"10.3233\/AIC-220115_ref118","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","article-title":"Model checking programs","volume":"10","author":"Visser","year":"2003","journal-title":"Automated Software Engineering"},{"issue":"5","key":"10.3233\/AIC-220115_ref119","doi-asserted-by":"publisher","first-page":"258","DOI":"10.2514\/1.I010096","article-title":"Generating certification evidence for autonomous unmanned aircraft using model checking and simulation","volume":"11","author":"Webster","year":"2014","journal-title":"Journal of Aerospace Information Systems"},{"key":"10.3233\/AIC-220115_ref120","doi-asserted-by":"publisher","DOI":"10.1109\/AERO47225.2020.9172303"},{"issue":"99","key":"10.3233\/AIC-220115_ref121","first-page":"1","article-title":"Toward reliable autonomous robotic assistants through formal verification: A case study","volume":"PP","author":"Webster","year":"2015","journal-title":"IEEE Transactions on Human-Machine Systems"},{"key":"10.3233\/AIC-220115_ref122","doi-asserted-by":"publisher","DOI":"10.1177\/0278364919883338"},{"key":"10.3233\/AIC-220115_ref123","doi-asserted-by":"publisher","DOI":"10.3389\/frobt.2021.665729"},{"key":"10.3233\/AIC-220115_ref124","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25693-7_8"},{"key":"10.3233\/AIC-220115_ref125","unstructured":"T. Zhang, L.A. Dennis and M. Webster, AsteroidX: An asteroid exploration simulation and visualisation tool, in: Workshop on Advances in Space Robotics and Back to Earth, 2021."},{"key":"10.3233\/AIC-220115_ref126","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54549-9_16"},{"key":"10.3233\/AIC-220115_ref127","doi-asserted-by":"crossref","unstructured":"X. Zhao, V. Robu, D. Flynn, F. Dinmohammadi, M. Fisher and M. Webster, Probabilistic model checking of robots deployed in extreme environments, in: Proc. 23rd AAAI Conference on Artificial Intelligence, AAAI Press, 2019, pp. 8066\u20138074, https:\/\/www.aaai.org\/Library\/AAAI\/aaai19contents.php.","DOI":"10.1609\/aaai.v33i01.33018066"}],"container-title":["AI Communications"],"original-title":[],"link":[{"URL":"https:\/\/content.iospress.com\/download?id=10.3233\/AIC-220115","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T18:28:04Z","timestamp":1777400884000},"score":1,"resource":{"primary":{"URL":"https:\/\/journals.sagepub.com\/doi\/full\/10.3233\/AIC-220115"}},"subtitle":[],"editor":[{"given":"Stefano V.","family":"Albrecht","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]},{"given":"Michael","family":"Woolridge","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2022,9,20]]},"references-count":123,"journal-issue":{"issue":"4"},"URL":"https:\/\/doi.org\/10.3233\/aic-220115","relation":{},"ISSN":["1875-8452","0921-7126"],"issn-type":[{"value":"1875-8452","type":"electronic"},{"value":"0921-7126","type":"print"}],"subject":[],"published":{"date-parts":[[2022,9,20]]}}}