Sage Journals: Discover world-class research

Abstract

The Autonomy and Verification group1

Part of a wider, international, Autonomy and Verification Network of activity: https://autonomy-and-verification.github.io

sits within the Department of Computer Science2

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.

Keywords

Formal verification agent programming ethical reasoning

Get full access to this article

View all access options for this article.

References

J.M.

Aitken ,

S.M.

Veres ,

Shaukat ,

Gao ,

Cucco ,

L.A.

Dennis ,

Fisher ,

J.A.

Kuo ,

Robinson and

P.E.

Mort , Autonomous nuclear waste management, IEEE Intell. Syst.33(6) (2018), 47–55. doi:10.1109/MIS.2018.111144814.

Al-Shareefi ,

Lisitsa and

Dixon , Clarification of ambiguity for the simple authentication and security layer, in: Proc. 6th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ), Lecture Notes in Computer Science, Vol. 10817, Springer, 2018, pp. 189–203. doi:10.1007/978-3-319-91271-4_13.

Al-Shareefi ,

Lisitsa and

Dixon , Analysing security protocols using scenario based simulation, in: Proc. 13th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS), Lecture Notes in Computer Science, Vol. 11847, Springer, 2019, pp. 47–62. doi:10.1007/978-3-030-35092-5_4.

Alves ,

Dennis and

Fisher , A double-level model checking approach for an agent-based autonomous vehicle and road junction regulations, Journal of Sensor and Actuator Networks10(3) (2021), 41, https://www.mdpi.com/2224-2708/10/3/41. doi:10.3390/jsan10030041.

Alves ,

L.A.

Dennis and

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.

G.V.

Alves ,

Dennis ,

Fernandes and

Fisher , Reliable decision-making in autonomous vehicles, in: Validation and Verification of Automated Systems: Results of the ENABLE-S3 Project, Springer, 2020, pp. 105–117. doi:10.1007/978-3-030-14628-3_10.

G.V.

Alves ,

Dennis and

Fisher , Formalisation and implementation of road junction rules on an autonomous vehicle modelled as an agent, in: Formal Methods. FM 2019 International Workshops, Springer, 2020, pp. 217–232. doi:10.1007/978-3-030-54994-7_16.

G.V.

Alves ,

Dennis and

Fisher , First steps towards an ethical agent for checking decision and behaviour for an autonomous vehicle on the rules of the road, in: Second Workshop on Implementing Machine Ethics, Zenodo, 2020. doi:10.5281/zenodo.3938851.

Amirabdollahian ,

Dautenhahn ,

Dixon ,

Eder ,

Fisher ,

K.L.

Koay ,

Magid ,

Pipe ,

Salem ,

Saunders and

Webster , Can you trust your robotic assistant? in: International Conference on Social Robotics, LNCS, Vol. 8239, Springer, 2013, pp. 571–573.

10.

Barringer ,

Fisher ,

Gabbay ,

Owens and

Reynolds (eds), The Imperative Future: Principles of Executable Temporal Logics, Research Studies Press, 1996.

11.

R.H.

Bordini ,

Fisher ,

Pardavila and

Wooldridge , Model checking AgentSpeak, in: Proceedings of the Second International Joint Conference on Autonomous Agents and Multi-Agent Systems (AAMAS-2003), 2003.

12.

R.H.

Bordini ,

Fisher ,

Visser and

Wooldridge , Model checking rational agents, IEEE Intelligent Systems19(5) (2004), 46–52. doi:10.1109/MIS.2004.47.

13.

R.H.

Bordini ,

Fisher ,

Visser and

Wooldridge , Verifying multi-agent programs by model checking, Journal of Autonomous Agents and Multi-Agent Systems12(2) (2006), 239–256. doi:10.1007/s10458-006-5955-7.

14.

Bourbouh ,

Farrell ,

Mavridou ,

Sljivo ,

Brat ,

L.A.

Dennis and

Fisher , Integrating formal verification and assurance: An inspection rover case study, in: Proc. 13th International Symposium on NASA Formal Methods (NFM), Lecture Notes in Computer Science, Vol. 12673, Springer, 2021, pp. 53–71. doi:10.1007/978-3-030-76384-8_4.

15.

Bremner ,

L.A.

Dennis ,

Fisher and

A.F.

Winfield , On proactive, transparent, and verifiable ethical reasoning for robots, in: Proceedings of the IEEE, 2019, pp. 1–21. doi:10.1109/JPROC.2019.2898267.

16.

British Standards Institution (BSI), BS 8611 Robots and Robotic Devices – Guide to the ethical design and application, 2016.

17.

R.C.

Cardoso ,

L.A.

Dennis ,

Farrell ,

Fisher and

Luckcuck , Towards compositional verification for modular robotic systems, in: Proceedings Second Workshop on Formal Methods for Autonomous Systems, Virtual, 7th of December 2020, Electronic Proceedings in Theoretical Computer Science, Vol. 329, Open Publishing Association, 2020, pp. 15–22. doi:10.4204/EPTCS.329.2.

18.

R.C.

Cardoso ,

L.A.

Dennis and

Fisher , Plan library reconfigurability in BDI agents, in: Proc. 7th International Workshop on Engineering Multi-Agent Systems (EMAS), Lecture Notes in Computer Science, Vol. 12058, Springer, 2019, pp. 195–212. doi:10.1007/978-3-030-51417-4_10.

19.

R.C.

Cardoso ,

Ene ,

Evans and

L.A.

Dennis , Ethical governor systems viewed as a multi-agent problem, in: Second Workshop on Implementing Machine Ethics, Zenodo, 2020. doi:10.5281/zenodo.3938851.

20.

R.C.

Cardoso ,

Farrell ,

Luckcuck ,

Ferrando and

Fisher , Heterogeneous verification of an autonomous curiosity rover, in: NASA Formal Methods, Springer, 2020, pp. 353–360. doi:10.1007/978-3-030-55754-6_20.

21.

R.C.

Cardoso and

Ferrando , A review of agent-based programming for multi-agent systems, Computers10(2) (2021), 16. doi:10.3390/computers10020016.

22.

R.C.

Cardoso ,

Ferrando ,

L.A.

Dennis and

Fisher , An interface for programming verifiable autonomous agents in ROS, in: Proc. 17th European Conference on Multi-Agent Systems and Agreement Technologies (EUMAS-AT), Lecture Notes in Computer Science, Vol. 12520, Springer, 2020, pp. 191–205. doi:10.1007/978-3-030-66412-1_13.

23.

R.C.

Cardoso ,

Ferrando ,

L.A.

Dennis and

Fisher , Implementing ethical governors in BDI, in: 9th International Workshop on Engineering Multi-Agent Systems, 2021.

24.

R.C.

Cardoso ,

Ferrando and

Papacchini , LFC: Combining autonomous agents and automated planning in the multi-agent programming contest, in: The Multi-Agent Programming Contest 2019, Springer, 2020, pp. 31–58. doi:10.1007/978-3-030-59299-8_2.

25.

R.C.

Cardoso ,

Ferrando and

Papacchini , Automated planning and BDI agents: A case study, in: Advances in Practical Applications of Agents, Multi-Agent Systems, and Social Good. the PAAMS Collection, Springer, 2021, pp. 52–63. doi:10.1007/978-3-030-85739-4_5.

26.

R.C.

Cardoso ,

Ferrando ,

Papacchini ,

Luckcuck ,

Linker and

T.R.

Payne , MLFC: From 10 to 50 planners in the multi-agent programming contest, in: The Multi-Agent Programming Contest 2021, Springer, 2021, pp. 82–107. doi:10.1007/978-3-030-88549-6_4.

27.

R.C.

Cardoso ,

Kourtis ,

L.A.

Dennis ,

Dixon ,

Farrell ,

Fisher and

Webster , A Review of Verification and Validation for Space Autonomous Systems, Current Robotics Reports, 2021. doi:10.1007/s43154-021-00058-1.

28.

R.C.

Cardoso ,

J.L.

Michaloski ,

Schlenoff ,

Ferrando ,

L.A.

Dennis and

Fisher , Agile tasking of robotic systems with explicit autonomy, in: The International FLAIRS Conference Proceedings, Vol. 34, 2021. doi:10.32473/flairs.v34i1.128481.

29.

Charisi ,

L.A.

Dennis ,

Fisher ,

Lieck ,

Matthias ,

Slavkovik ,

Sombetzki ,

A.F.T.

Winfield and

Yampolskiy , Towards Moral Autonomous Systems, CoRR Abs/1703.04741, 2017, http://arxiv.org/abs/1703.04741.

30.

Chatila ,

Dignum ,

Fisher ,

Giannotti ,

Morik ,

Russell and

Yeung , Trustworthy AI, in: Reflections on Artificial Intelligence for Humanity, Springer, 2021, pp. 13–39. doi:10.1007/978-3-030-69128-8_2.

31.

W.J.

Clancey ,

Sachs ,

Sierhuis and

van Hoof , Brahms: Simulating practice for work systems design, International Journal on Human-Computer Studies49 (1998), 831–865. doi:10.1006/ijhc.1998.0229.

32.

Dennis and

Fisher , Verifiable autonomy and responsible robotics, in: Software Engineering for Robotics, Springer, 2021, pp. 189–217. doi:10.1007/978-3-030-66494-7_7.

33.

L.A.

Dennis , The MCAPL framework including the agent infrastructure layer an agent Java pathfinder, J. Open Source Software3(24) (2018), 617. doi:10.21105/joss.00617.

34.

L.A.

Dennis , Computational Goals, Values and Decision-Making, Science & Engineering Ethics, 2020. doi:10.1007/s11948-020-00244-y.

35.

L.A.

Dennis ,

J.M.

Aitken ,

Collenette ,

Cucco ,

Kamali ,

McAree ,

Shaukat ,

Atkinson ,

Gao ,

S.M.

Veres and

Fisher , Agent-based autonomous systems and abstraction engines: Theory meets practice, in: Proc, in: 17th Annual Conference on Towards Autonomous Robotic Systems (TAROS), 2016, pp. 75–86. doi:10.1007/978-3-319-40379-3_8.

36.

L.A.

Dennis ,

M.M.

Bentzen ,

Lindner and

Fisher , Verifiable machine ethics in changing contexts, in: Proceedings of the AAAI Conference on Artificial Intelligence 35(13), 2021, pp. 11470–11478, https://ojs.aaai.org/index.php/AAAI/article/view/17366.

37.

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.

38.

L.A.

Dennis ,

Farwer ,

R.H.

Bordini ,

Fisher and

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–139.

39.

L.A.

Dennis and

Fisher , Actions with durations and failures in BDI languages, in: ECAI 2014–21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic – Including Prestigious Applications of Intelligent Systems (PAIS 2014), 2014, pp. 995–996. doi:10.3233/978-1-61499-419-0-995.

40.

L.A.

Dennis and

Fisher , Practical challenges in explicit ethical machine reasoning, in: International Symposium on Artificial Intelligence and Mathematics, ISAIM 2018, Fort Lauderdale, Florida, USA, January 3–5, 2018, 2018, http://isaim2018.cs.virginia.edu/papers/ISAIM2018_Ethics_Dennis_Fischer.pdf.

41.

L.A.

Dennis and

Fisher , Verifiable self-aware agent-based autonomous systems, in: Proceedings of the IEEE, 2020, pp. 1011–1026, (Special issue on Self-Aware Autonomous Systems). doi:10.1109/JPROC.2020.2991262.

42.

L.A.

Dennis and

Fisher , Verifiable Autonomous Systems – Using Rational Agents to Provide Assurance About Decisions Made by Machines, Cambridge University Press, 2022, (To appear).

43.

L.A.

Dennis ,

Fisher ,

J.M.

Aitken ,

S.M.

Veres ,

Gao ,

Shaukat and

Burroughes , Reconfigurable autonomy, KI – Künstliche Intelligenz28(3) (2014), 199–207. doi:10.1007/s13218-014-0308-1.

44.

L.A.

Dennis ,

Fisher ,

Lincoln ,

Lisitsa and

S.M.

Veres , Practical verification of decision-making in agent-based autonomous systems, Autom. Softw. Eng.23(3) (2016), 305–359. doi:10.1007/s10515-014-0168-9.

45.

L.A.

Dennis ,

Fisher ,

Lisitsa ,

Lincoln and

S.M.

Veres , Satellite control using rational agent programming, IEEE Intelligent Systems25(3) (2010), 92–97. doi:10.1109/MIS.2010.88.

46.

L.A.

Dennis ,

Fisher ,

Slavkovik and

Webster , Formal verification of ethical choices in autonomous systems, Robotics and Autonomous Systems77 (2016), 1–14. doi:10.1016/j.robot.2015.11.012.

47.

L.A.

Dennis ,

Fisher and

Webster , Two-stage agent program verification, J. Log. Comput.28(3) (2018), 499–523. doi:10.1093/logcom/exv002.

48.

L.A.

Dennis ,

Fisher ,

Webster and

R.H.

Bordini , Model checking agent programming languages, Automated Software Engineering19(1) (2012), 5–63. doi:10.1007/s10515-011-0088-x.

49.

L.A.

Dennis ,

Fu and

Slavkovik , Markov Chain Model Representation of Information Diffusion in Social Networks, Journal of Logic and Computation (2021), to appear.

50.

L.A.

Dennis and

Oren , Explaining BDI agent behaviour through dialogue, in: 20th International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2021), 2021, pp. 429–437.

51.

L.A.

Dennis and

Slavkovik , Machines that know right and cannot do wrong: The theory and practice of machine ethics, IEEE Intelligent Informatics Bulletin19(1) (2018), http://www.comp.hkbu.edu.hk/~cib/2018/Aug/article2/iib_vol19no1_article2.pdf.

52.

L.A.

Dennis ,

Slavkovik and

Fisher , “How did they know?” – model-checking for analysis of information leakage in social networks, in: Coordination, Organizations, Institutions, and Norms in Agent Systems XII – COIN 2016 International Workshops, COIN@AAMAS, Singapore, Singapore, May 9, 2016, COIN@ECAI, The Hague, The Netherlands, August 30, 2016, Revised Selected Papers, 2016, pp. 42–59. doi:10.1007/978-3-319-66595-5_3.

53.

Dinmohammadi ,

Fisher ,

Flynn ,

Jump ,

Page ,

Patchett ,

Robu ,

Tang and

Webster , Certification of safe and trusted robotic inspection of assets, in: Proceedings of the Prognostics and System Health Management Conference, Chongqing, China, 2018.

54.

Dixon ,

Fisher and

Bolotov , Resolution in a logic of rational agency, Artificial Intelligence139(1) (2002), 47–89. doi:10.1016/S0004-3702(02)00196-0.

55.

Dixon ,

M.C.F.

Gago ,

Fisher and

van der Hoek , Temporal logics of knowledge and their applications in security, Electron. Notes Theor. Comput. Sci.186 (2007), 27–42. doi:10.1016/j.entcs.2006.11.043.

56.

Dixon ,

Konev ,

Fisher and

Nietiadi , Deductive temporal reasoning with constraints, J. Appl. Log.11(1) (2013), 30–51. doi:10.1016/j.jal.2012.07.001.

57.

Dixon ,

Webster ,

Saunders ,

Fisher and

Dautenhahn , ‘the fridge door is open’ – temporal verification of a robotic assistant’s behaviours, in: Advances in Autonomous Robotics Systems (TAROS), Lecture Notes in Computer Science, Vol. 8717, Springer, 2014, pp. 97–108. doi:10.1007/978-3-319-10401-0_9.

58.

Dixon ,

Winfield ,

Fisher and

Zeng , Towards temporal verification of swarm robotic systems, Robotics and Autonomous Systems60 (2012), 1429–1441. doi:10.1016/j.robot.2012.03.003.

59.

Farrell ,

Bradbury ,

Fisher ,

L.A.

Dennis ,

Dixon ,

Yuan and

Maple , Using threat analysis techniques to guide formal verification: A case study of cooperative awareness messages, in: Software Engineering and Formal Methods, Springer, Cham, 2019, pp. 471–490. doi:10.1007/978-3-030-30446-1_25.

60.

Farrell ,

R.C.

Cardoso ,

Dennis ,

Dixon ,

Fisher ,

Kourtis ,

Lisitsa ,

Luckcuck and

Webster , Modular verification of autonomous space robotics, in: Assurance of Autonomy for Robotic Space Missions Workshop, 2019.

61.

Farrell ,

Luckcuck and

Fisher , Robotics and integrated formal methods: Necessity meets opportunity, in: Proc. 14th International Conference on Integrated Formal Methods (IFM), Lecture Notes in Computer Science, Vol. 11023, Springer, 2018, pp. 161–171. doi:10.1007/978-3-319-98938-9_10.

62.

Farrell ,

Luckcuck ,

Pullum ,

Fisher ,

Hessami ,

Gal ,

Murahwi and

Wallace , Evolution of the IEEE P7009 standard: Towards fail-safe design of autonomous systems, in: Proc. IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW), 2021, pp. 401–406. doi:10.1109/ISSREW53611.2021.00109.

63.

Farrell ,

Mavrakis ,

Ferrando ,

Dixon and

Gao , Formal modelling and runtime verification of autonomous grasping for active debris removal, Frontiers in Robotics and AI8 (2022), 639282. doi:10.3389/frobt.2021.639282.

64.

L.E.R.

Fernandes ,

Custodio ,

G.V.

Alves and

Fisher , A rational agent controlling an autonomous vehicle: Implementation and formal verification, in: Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@IFM 2017, Turin, Italy, 19th September 2017, 2017, pp. 35–42. doi:10.4204/EPTCS.257.5.

65.

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.

66.

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’21), 2021.

67.

Ferrando ,

R.C.

Cardoso ,

Fisher ,

Ancona ,

Franceschini and

Mascardi , ROSMonitoring: A runtime verification framework for ROS, in: Towards Autonomous Robotic Systems, Springer, 2020, pp. 387–399. doi:10.1007/978-3-030-63486-5_40.

68.

Ferrando ,

L.A.

Dennis ,

Ancona ,

Fisher and

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–1935, http://dl.acm.org/citation.cfm?id=3238028.

69.

Ferrando ,

L.A.

Dennis ,

Ancona ,

Fisher and

Mascardi , Verifying and validating autonomous systems: An integrated approach, in: Proc. 8th IEEE International Conference on Runtime Verification (RV), 2018.

70.

Ferrando ,

L.A.

Dennis ,

R.C.

Cardoso ,

Fisher ,

Ancona and

Mascardi , Toward a holistic approach to verification and validation of autonomous cognitive systems, ACM Trans. Softw. Eng. Methodol.30(4) (2021), 43. doi:10.1145/3447246.

71.

Ferrando ,

Kootbally ,

Piliptchak ,

R.C.

Cardoso ,

Schlenoff and

Fisher , Runtime verification of the ARIAC competition: Can a robot be agile and safe at the same time? in: AIRO, 2020.

72.

Fisher , Implementing BDI-like systems by direct execution, in: Proc. 15th International Joint Conference on Artificial Intelligence (IJCAI), Morgan-Kaufmann, 1997, pp. 316–321.

73.

Fisher ,

R.C.

Cardoso ,

E.C.

Collins ,

Dadswell ,

L.A.

Dennis ,

Dixon ,

Farrell ,

Ferrando ,

Huang ,

Jump ,

Kourtis ,

Lisitsa ,

Luckcuck ,

Luo ,

Page ,

Papacchini and

Webster , An overview of verification and validation challenges for inspection robots, Robotics10(2) (2021), 67, https://www.mdpi.com/2218-6581/10/2/67. doi:10.3390/robotics10020067.

74.

Fisher ,

Collins ,

L.A.

Dennis ,

Luckcuck ,

Webster ,

Jump ,

Pagé ,

Patchett ,

Dinmohammadi ,

Flynn ,

Robu and

Zhao , Verifiable self-certifying autonomous systems, in: Proc. 2018 IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops, IEEE, 2018, pp. 341–348. doi:10.1109/ISSREW.2018.00028.

75.

Fisher ,

L.A.

Dennis and

Webster , Verifying autonomous systems, ACM Communications56(9) (2013), 84–93. doi:10.1145/2494558.

76.

Fisher ,

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’21), 2021.

77.

Fisher and

Ghidini , Programming resource-bounded deliberative agents, in: Proc. 16th International Joint Conference on Artificial Intelligence (IJCAI), Morgan Kaufmann, 1999, pp. 200–205.

78.

Fisher and

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–856.

79.

Fisher ,

List ,

Slavkovik and

Weiss , Ethics and trust: Principles, verification and validation (Dagstuhl seminar 19171), Reports9(4) (2019), 59–86. doi:10.4230/DagRep.9.4.59.

80.

Fisher ,

List ,

Slavkovik and

A.F.T.

Winfield , Engineering moral agents – from human morality to artificial morality (Dagstuhl seminar 16222), Dagstuhl Reports6(5) (2016), 114–137. doi:10.4230/DagRep.6.5.114.

81.

Fisher ,

Mascardi ,

K.Y.

Rozier ,

Schlingloff ,

Winikoff and

Yorke-Smith , Towards a framework for certification of reliable autonomous systems, Autonomous Agents and Multi Agent Systems35(1) (2021), 8. doi:10.1007/s10458-020-09487-2.

82.

Gainer ,

Dixon ,

Dautenhahn ,

Fisher ,

Hustadt ,

Saunders and

Webster , CRutoN: Automatic verification of a robotic assistant’s behaviours, in: Critical Systems: Formal Methods and Automated Verification (FMICS-AVoCS), 2017, pp. 119–133. doi:10.1007/978-3-319-67113-0_8.

83.

Gainer ,

Dixon and

Hustadt , Probabilistic model checking of ant-based positionless swarming, in: Proc. 17th Annual Conference on Towards Autonomous Robotic Systems (TAROS), 2016, pp. 127–138. doi:10.1007/978-3-319-40379-3_13.

84.

Gainer ,

Linker ,

Dixon ,

Hustadt and

Fisher , Multi-scale verification of distributed synchronisation, Formal Methods in Systems Design55(3) (2020), 171–221. doi:10.1007/s10703-020-00347-z.

85.

Gleirscher ,

A.E.

Haxthausen ,

Leucker and

Linker , Analysis of autonomous mobile collectives in complex physical environments (Dagstuhl seminar 19432), Reports9(10) (2019), 95–116. doi:10.4230/DagRep.9.10.95.

86.

A.J.

Hepple ,

L.A.

Dennis and

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–188.

87.

Hustadt ,

Gainer ,

Dixon ,

Nalon and

Zhang , Ordered resolution for coalition logic, in: Proc. 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), 2015, pp. 169–184. doi:10.1007/978-3-319-24312-2_12.

88.

Hustadt ,

Ozaki and

Dixon , Theorem proving for pointwise metric temporal logic over the naturals via translations, Journal of Automated Reasoning64 (2020), 1553–1610. doi:10.1007/s10817-020-09541-4.

89.

Kamali ,

L.A.

Dennis ,

McAree ,

Fisher and

S.M.

Veres , Formal verification of autonomous vehicle platooning, Sci. Comput. Program.148 (2017), 88–106. doi:10.1016/j.scico.2017.05.006.

90.

Kamali ,

Linker and

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.

91.

K.L.

Koay ,

Webster ,

Dixon ,

Gainer ,

Syrdal ,

Fisher and

Dautenhahn , Use and usability of software verification methods to detect behaviour interference when teaching an assistive home companion robot: A proof-of-concept study, Paladyn, Journal of Behavioral Robotics12(1) (2021), 402–422, https://www.degruyter.com/document/doi/10.1515/pjbr-2021-0028/html. doi:10.1515/pjbr-2021-0028.

92.

V.J.

Koeman ,

L.A.

Dennis ,

Webster ,

Fisher and

Hindriks , The “why did you do that?” button: Answering why-questions for end users of robotic systems, in: Engineering Multi-Agent Systems, Springer, 2020, pp. 152–172. doi:10.1007/978-3-030-51417-4_8.

93.

Konur ,

Dixon and

Fisher , Analysing robot swarm behaviour via probabilistic model checking, Robotics and Autonomous Systems60(2) (2012), 199–213. doi:10.1016/j.robot.2011.10.005.

94.

Konur ,

Fisher and

Schewe , Combined model checking for temporal, probabilistic, and real-time logics, Theoretical Computer Science503 (2013), 61–88. doi:10.1016/j.tcs.2013.07.012.

95.

Kourtis ,

Dixon ,

Fisher and

Lisitsa , Parameterized verification of leader/follower systems via first-order temporal logic, Formal Methods in System Design (2022).

96.

Lincoln ,

Veres ,

Dennis ,

Fisher and

Lisitsa , Autonomous asteroid exploration by rational agents, IEEE Computational Intelligence Magazine8(4) (2013), 25–38. doi:10.1109/MCI.2013.2279559.

97.

Linker , Hybrid Multi-Lane Spatial Logic, Archive of Formal Proofs, 2017, https://www.isa-afp.org/entries/Hybrid_Multi_Lane_Spatial_Logic.html.

98.

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.

99.

Luckcuck ,

Farrell ,

L.A.

Dennis ,

Dixon and

Fisher , Formal specification and verification of autonomous robotic systems: A survey, ACM Comput. Surv.52(5) (2019), 1–41. doi:10.1145/3342355.

100.

Luckcuck ,

Fisher ,

Dennis ,

Frost ,

White and

Styles , Principles for the Development and Assurance of Autonomous Systems for Safe Use in Hazardous Environments, Technical Report, Zenodo, 2021. doi:10.5281/ZENODO.5012322.

101.

Maple ,

Bradbury ,

Yuan ,

Farrell ,

Dixon ,

Fisher and

U.I.

Atmaca , Security-minded verification of space systems, in: 2020 IEEE Aerospace Conference, 2020, pp. 1–13. doi:10.1109/AERO47225.2020.9172563.

102.

J.C.

McCabe-Dansted ,

Dixon ,

French and

Reynolds , Sublogics of a branching time logic of robustness, Information and Computation266 (2019), 126–160. doi:10.1016/j.ic.2019.02.003.

103.

Michaloski ,

Aksu ,

Schlenoff ,

R.C.

Cardoso and

Fisher , Agile tasking of robotic kitting, in: Proceedings of the ASME 2021 International Mechanical Engineering Congress and Exposition (IMECE2021), 2021.

104.

Nalon ,

Dixon and

Hustadt , Modal resolution: Proofs, layers, and refinements, ACM Trans. Comput. Log.20(4) (2019), 23:1–23:38. doi:10.1145/3331448.

105.

Nalon ,

Hustadt and

Dixon , KSP: A resolution-based prover for multimodal k, abridged report, in: Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence (IJCAI), 2017, pp. 4919–4923. doi:10.24963/ijcai.2017/694.

106.

Nalon ,

Hustadt and

Dixon , KSP a Resolution-Based Theorem Prover for Kn: Architecture, Refinements, Strategies and Experiments, Springer, 2018.

107.

Nalon ,

Zhang ,

Dixon and

Hustadt , A resolution-based calculus for coalition logic, J. Log. Comput.24(4) (2014), 883–917. doi:10.1093/logcom/ext074.

108.

Page ,

Dadswell ,

Webster ,

Jump and

Fisher , Towards the determination of safe operating envelopes for autonomous UAS in offshore inspection missions, Robotics10(3) (2021), https://www.mdpi.com/2218-6581/10/3/97. doi:10.3390/robotics10030097.

109.

Page ,

Webster ,

Fisher and

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–45, http://www.thinkmind.org/index.php?view=article&articleid=icas_2019_3_20_28007.

110.

Papacchini ,

Nalon ,

Hustadt and

Dixon , Efficient local reductions to basic modal logic, in: Automated Deduction – CADE 28, LNCS, Vol. 12699, Springer, 2021.

111.

Papacchini ,

Nalon ,

Hustadt and

Dixon , Local is Best: Efficient Reductions to Modal Logic K, Journal of Automated Reasoning (2022), accepted.

112.

Slavkovik ,

L.A.

Dennis and

Fisher , An abstract formal basis for digital crowds, Distributed and Parallel Databases33(1) (2015), 3–31. doi:10.1007/s10619-014-7161-y.

113.

Stocker ,

L.A.

Dennis ,

Dixon and

Fisher , Verification of brahms human-robot teamwork models, in: Proc. 13th European Conference on Logics in Artificial Intelligence (JELIA), LNCS, Vol. 7519, Springer, 2012, pp. 385–397. doi:10.1007/978-3-642-33353-8_30.

114.

Stringer , Adaptable and verifiable BDI reasoning, in: Proc. 20th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), ACM, 2021, pp. 1835–1836, https://dl.acm.org/doi/10.5555/3463952.3464256.

115.

Stringer ,

R.C.

Cardoso ,

Dixon and

L.A.

Dennis , Implementing durative actions with failure detection in gwendolen, in: 9th International Workshop on Engineering Multi-Agent Systems, 2021.

116.

Tolmeijer ,

Weiss ,

Hanheide ,

Lindner ,

T.M.

Powers ,

Dixon and

M.L.

Tielman , Taxonomy of trust-relevant failures and mitigation strategies, in: Proceedings of the 2020 ACM/IEEE International Conference on Human-Robot Interaction, Association for Computing Machinery, New York, NY, USA, 2020, pp. 3–12. ISBN 9781450367462. doi:10.1145/3319502.3374793.

117.

M.B.

van Riemsdijk ,

L.A.

Dennis ,

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–8, 2015, 2015, pp. 423–432, http://dl.acm.org/citation.cfm?id=2772935.

118.

Visser ,

Havelund ,

G.P.

Brat ,

Park and

Lerda , Model checking programs, Automated Software Engineering10(2) (2003), 203–232. doi:10.1023/A:1022920129859.

119.

Webster ,

Cameron ,

Fisher and

Jump , Generating certification evidence for autonomous unmanned aircraft using model checking and simulation, Journal of Aerospace Information Systems11(5) (2014), 258–279. doi:10.2514/1.I010096.

120.

Webster ,

L.A.

Dennis ,

Dixon ,

Fisher ,

Stocker and

Sierhuis , Formal verification of astronaut-rover teams for planetary surface operations, in: 2020 IEEE Aerospace Conference, 2020, pp. 1–8. doi:10.1109/AERO47225.2020.9172303.

121.

Webster ,

Dixon ,

Fisher ,

Salem ,

Saunders ,

K.L.

Koay ,

Dautenhahn and

Saez-Pons , Toward reliable autonomous robotic assistants through formal verification: A case study, IEEE Transactions on Human-Machine SystemsPP(99) (2015), 1–11.

122.

Webster ,

Western ,

Araiza-Illan ,

Dixon ,

Eder ,

Fisher and

A.G.

Pipe , A corroborative approach to verification and validation of human–robot teams, International Journal of Robotics Research39(1) (2020). doi:10.1177/0278364919883338.

123.

A.F.T.

Winfield ,

Booth ,

L.A.

Dennis ,

Egawa ,

Hastie ,

Jacobs ,

R.I.

Muttram ,

J.I.

Olszewska ,

Rajabiyazdi ,

Theodorou ,

M.A.

Underwood ,

R.H.

Wortham and

Watson , IEEE P7001: A proposed standard on transparency, Frontiers in Robotics and AI8 (2021), 225. doi:10.3389/frobt.2021.665729.

124.

Winikoff ,

L.A.

Dennis and

Fisher , Slicing agent programs for more efficient verification, in: Proc. 6th International Workshop in Engineering Multi-Agent Systems, Lecture Notes in Computer Science, Vol. 11375, Stockholm, Sweden, 2019, pp. 139–157. doi:10.1007/978-3-030-25693-7_8.

125.

Zhang ,

L.A.

Dennis and

Webster , AsteroidX: An asteroid exploration simulation and visualisation tool, in: Workshop on Advances in Space Robotics and Back to Earth, 2021.

126.

Zhao ,

Banks ,

Sharp ,

Robu ,

Flynn ,

Fisher and

Huang , A safety framework for critical systems utilising deep neural networks, in: Proc. 39th International Conference on Computer Safety, Reliability, and Security (SAFECOMP), Lecture Notes in Computer Science, Vol. 12234, Springer, 2020, pp. 244–259. doi:10.1007/978-3-030-54549-9_16.

127.

Zhao ,

Robu ,

Flynn ,

Dinmohammadi ,

Fisher and

Webster , Probabilistic model checking of robots deployed in extreme environments, in: Proc. 23rd AAAI Conference on Artificial Intelligence, AAAI Press, 2019, pp. 8066–8074, https://www.aaai.org/Library/AAAI/aaai19contents.php.

Verifiable autonomy: From theory to applications

Abstract

Keywords

Get full access to this article

References