Verifiable autonomy: From theory to applications

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

1. Programming individual autonomous reasoning agents

Over several years we have developed a range of programming languages with strong semantic foundations for the representation and implementation of individual agents. Beginning with basic autonomous agents, we have moved on to the transparent representation of the reasons for autonomous decisions, which in turn provides the basis for explainability, self-awareness and formal verification later. Once our agents become autonomous, then the decisions they are asked to make might become safety-critical or have other legal and ethical ramifications. In unpredictable environments this can quickly lead to the need for ethical decision-making [34] where the agent must reason about right/wrong, good/bad, etc, in order to come up with the most appropriate decision.

Our development of programming languages has proceeded from executable (temporal) logic specifications [10,72], through resource-boundedness and deliberation [77,78] and on to Beliefs-Desires-Intentions (BDI) languages explicitly developed with verification [32,42] or ethical reasoning in mind [23,37].

2. Specification and verification

A particular focus of the group has been the formal specification and verification of agent-based systems [54] and, increasingly, autonomous systems [75]; much of our work on verifiable autonomous systems is collected together in [42]. This work has encompassed a number of facets, summarised as follows.

New formalisms and logical methods. These range across novel temporal logics [56,102], multi-modal logics [88,104–106,110,111], spatial logics [97], formalisms for complex reasoning [36], and refined proof methods [87] (the proof methods often concern clausal resolution techniques). These developments together provide a formal basis for our specification and reasoning across a range of practical agent-based, distributed, or autonomous systems.

Model-checking and program model-checking. An important direction, especially for verifying agents at the heart of practical autonomous systems, involves algorithmic verification techniques such as model-checking [11,12] and, of particular relevance, program model-checking [118]. Program model-checking has been developed for agents and then agent-based autonomous systems through a series of contributions such as [38,44,48] culminating in the MCAPL Framework incorporating the Agent Java Pathfinder tool [33]. This framework has been used across a wide range of agent applications, from ethical robots [15] to road vehicle platoons [89], as we will describe later. Work on extending and refining the framework continues [124].

Runtime verification. In addition to pre-deployment verification techniques, such as proof or model-checking, an increasingly important thread of our work involves verifying agent behaviour at runtime [76]. Consequently, research directions [65], coherent frameworks [70] and practical tools [66,67] have been developed for runtime verification and applied in practice [71].

Simulation-based analysis. As we will see in later sections, we often use a combination of different verification techniques and so work has also progressed on simulation-based techniques, especially for autonomous vehicles, that can be used together with more formal techniques [108,109]. The combination of a diverse range of verification techniques is, itself, important [61,122].

3. Agent flexibility

In developing and verifying agents for use in practical systems, especially autonomous robotic systems, we have tackled a range of important properties and requirements, as we outline below.

Transparency and explainability. The key to an agent is its ability (and necessity) to make decisions. In understanding and explaining agent decisions, transparency about the reasons for those decisions is crucial. We have been part of standards activities for transparency across autonomous systems [123] and continue to ensure that both the programming and architectural approaches we develop are open to analysis. This transparency not only benefits formal verification but also explainability. Consequently both our agents [50] and our robotic systems [91,92] can be designed to provide explanations of their choices and behaviours.

Self-awareness and reconfigurability. Our agents, particularly once embedded in long-lived autonomous systems, must be able to cope, during their lifetimes, with inconsistencies, with unexpected failures, and with additional constraints. Consequently, we have developed self-awareness as a key facet in our systems, with an agent being able to assess not only its own beliefs or intentions but, especially when embodied, its capabilities and effectiveness [41,74]. Once an agent is able to reason about these capabilities it can refine, or even replace, them for example by recognising issues and re-organising or replanning its activities [18,25,39,66]. Particularly when these agents are at the heart of robotic systems, this becomes an important aspect, leading to reconfigurability and increased reliability [43,114,115]

Trustworthiness and verifiable ethical reasoning. While trustworthiness in standard systems is often equivalent to reliability, the additional aspect of decision-making that agents must achieve extends trustworthiness. Typically, in order to trust an agent we not only require it to be reliable but also, since we cannot control all its decisions, require that it makes decisions for our benefit [30]. Understanding, programming and verifying that an agent, possibly embedded into an autonomous system, will make the best decisions, or at least make the decisions we would have made, is a key part of our work. This quickly moves us into the field of ethical decision-making, where agents must make their decisions based on high-level principles such as good/bad, right/wrong, etc. Considering loss of trust and how to repair this is also important [116].

As part of this work we have developed a range of ethical reasoning capabilities for agents [23,40,51], even capturing different ethical values/concerns as a multi-agent problem and developing mechanisms to resolve dilemmas [19]. We have devised this ethical reasoning, for both agents and autonomous systems, to be amenable to formal verification and have provided verification techniques for a range of ethical styles [15,36,46,117]. There are many applications of this, with one practical one being the development of ethical reasoning in the context of autonomous road vehicle decisions [5,7,8].

Security and privacy. Our previous work on security, using temporal and modal logics [55], has led on to work on security verification and evaluation [2,3]. Recent work has also involved combining informal threat analysis techniques with our formal verification approaches [59,101], allowing formal techniques to be focussed on the areas of highest risk.

As agents communicate important information, privacy is also crucial. Our work in this area has concentrated on verifying (lack of) any information leakage or diffusion in agent-based social networks [49,52] and on formalising digital crowds [112].

4. Multi-agent systems

Programming multi-agent systems. Many of the programming frameworks that we have developed for individual agents naturally extend to multi-agent systems [21]. Indeed, executable specifications were designed with all systems being inherently multi-agent. Our work here has developed and applied multi-agent concepts across a range of structures, such as organisations [86], multiple advisors [19], swarms, digital crowds [112] and even social networks [49].

Collaboration, coordination and particularly teamworking between agents and humans is vital for many current and future applications. Our work in this area has particularly focussed on the Brahms framework, developed by Sierhuis and utilised by NASA [31], for which we have developed a formal verification framework [113]. In addition to examples of teamwork in social robotics, we also explore human-robot teamwork in more extreme environments [120].

Formally verifying multi-agent systems. Although many of the programming and verification techniques for agents described above are directly relevant to multi-agent systems, some of the work of the group has specificallly targetted these multi-agent aspects. These contributions include synchronisation across multiple agents [84], verification of coalitions [87,107], model-checking [13], verification of swarms [58,83,93,95], and verification of human-agent teamwork [113,120].

5. Heterogeneous formal verification

It is central to much of our work, especially within practical agent-based systems, that we utilise multiple different verification techniques. No single technique is sufficient for all aspects of these complex systems [61]. Consequently, we have devised a range of different ways to combine and concentrate verification, covering modularity, combinations, heterogeneity, and corroborative approaches.

Modular verification [17], particularly of complex systems, is essential [60,90] in order to deal with the size of, and diverse issues across, these systems. To tackle this diversity, combining formal verification approaches for several different formal logics [94] can be important [4,47,90]. Going further, heterogeneous verification, where very different types of verification are used for different parts of a complex system, is also essential for large, practical autonomous systems [20,119]. Finally, corroborative verification [122], where several different, but complementary, verification techniques are together used to confirm a single component’s/agent’s behaviour, is also important [68,69].

6. Applications

Our techniques and approaches are applicable across a wide range of application areas, often embodied systems such as robots or vehicles.

6.1. General robotics issues (inc. ROS verification, robot kitting, hazardous environments, etc)

Often, we provide general techniques and tools that can be used across a range of robotic systems. For example, runtime verification for use across ROS (“Robot Operating System”) architectures [67], transparent ethical reasoning approaches [15], verification across robotic systems [99], and agent architectures [22,35]. In addition, we have particularly examined robotics for general manufacturing tasks [28,71,103] and robots used in hazardous environments [1,73,127], such as in nuclear, offshore, or space scenarios.3

³
Particularly through involvement in the UK’s “Robots for a Safer World” programme and, within that, RAIN (https://rainhub.org.uk), ORCA (https://orcahub.org), and FAIR-SPACE (https://www.fairspacehub.org).

6.2. Autonomous road vehicles (inc. “Rules of the road”, platoons/convoys, ethical decisions, etc)

We have used agents, particularly our BDI-style agents, in the high-level, transparent and verifiable control of autonomous road vehicles. This particularly concerns two aspects: ensuring that individual vehicles (verifiably) make the safe/legal/ethical decisions [4–8,64] and that we can verify behaviour of platoons or convoys of (road) vehicles [89,90,97]. The former is important when we are working towards regulatory approval for “driverless” cars; the latter represents a key step towards fully autonomous vehicles.

6.3. Unmanned air vehicles (inc. “Rules of the AIr”, safe operating envelopes, etc)

Our work with unmanned air systems, specifically UAVs, is again focussed on using agent architectures for these systems, and also on applying heterogeneous verification techniques to tackle their complex issues. In particular, we have combined diverse techniques such as simulation and formal verification [108,119] in order to provide a general approach to the analysis, and potentially certification, of UAVs operating in critical environments [53,109]

6.4. Space robotics (inc. orbital, formation-flying, astronaut-robot teams, etc)

Primarily through UKRI funded projects on Engineering Autonomous Space Software and Future AI and Robotics for Space (FAIR-SPACE) we have applied our techniques to the Space domain. This work includes utilising BDI agent programming and simulation in space systems [45,96,125], the development and verification of astronaut-rover teamwork [120], verification and validation across space robotics [20,27,60,63], and work (with NASA) towards verification tool-chains supporting assurance [14].

6.5. Domestic robotics (inc. safety, social/trust issues, teaching of robots, etc)

Particularly through work on the “Trustworthy Robotic Assistants” (robosafe.org) project, and subsequently with the universities of Hertfordshire (UK) and Waterloo (Canada), we have looked at agent architectures (and, again, formal verification) for domestic robotic assistants. The specific issues we have explored include safety [57,82], trust [9], reliability [121], and teaching the robots new behaviours [91].

7. Broader impact

The activities of the Autonomy and Verification Group have led to impact beyond just standard research outputs.

7.1. Standards and usage

Our work, particularly on transparent behaviours and formal verification, has led to significant involvement in developing national and international standards. Our standards work has primarily been with the British Standards Institution, for example on BS8611: “Guide to the Ethical Design and Application of Robots and Robotic Devices” [16], and the IEEE, for example on P7001: “Transparency of Autonomous Systems” [123] and P7009: “Failsafe Design of Autonomous Systems” [62]. Not directly relating to standards, our work has contributed to general issues, for example concerning “Moral Autonomous Systems” [29].

7.2. Regulations, assurance and certification

As an example of work with regulatory bodies, we produced a white paper with the UK’s Office for Nuclear Regulation entitled “Principles for the Development and Assurance of Autonomous Systems for Safe Use in Hazardous Environments” [100]. In addition we have produced publications giving routes to, and guidelines for, certification [53,81,119], self-certification [74], and assurance [14,126] of autonomous systems.

7.3. International activities

We have organised a range of conferences/workshops, most recently SCAV, EMAS, FroCoS, JELIA, CLIMA, AREA, FMAS, and a number of Dagstuhl Seminars [79,80,85]. Similarly, we have organised a range of journal special issues, most recently the AI Journal Special Issue on Ethics for Autonomous Systems.

We also play a leading part in international organisations, such as the IEEE Technical Committee on the Verificaiton of Autonomous Systems, the ACM SIGAI, and the European Association for Multi-Agent Systems.

The group has been involved in international competitions, both concerning agents and robotics. In particular, the Multi-Agent Programming Contest where we have won [24,26,98]. We have also worked with NIST in the USA in extending their ARIAC robotic competition [71]

7.4. Outreach and engagement

Particularly via robotics, we continue to be involved in outreach and public engagement activities.

Louise Dennis leads the LegoRovers4

⁴
http://www.cs.man.ac.uk/~dennisl/legorovers/

activity that is regularly used in schools and has been showcased at a range of science festivals, such as Cheltenham Science Festival. Aspects of this system are described in [35]. We have also been involved in the development of resources for the teaching of the Python programming language, based around the control of Raspberry Pi based robots, both in simulation and using real robots.5

⁵

https://www.csc.liv.ac.uk/~lad/pyrobots/index.html

Source code and support materials for all our outreach systems can be found on GitHub.6

⁶

https://github.com/legorovers

While at Liverpool the group worked with artists Cecile B. Evans to produce the “Sprung a Leak” exhibit at Tate Liverpool during 2016 and 2017.7

⁷

https://www.youtube.com/watch?v=-UBWJ4FYphU

This is an 18 minute play, involving three robots, as well as synchronised video images; members of the public could walk within the play as it unfolded. At Liverpool this attracted over 100,000 visitors before moving on to Belgium, Germany and Japan.

8. Challenges and open problems

In this area many challenges and open problems remain.

Programming individual autonomous reasoning agents. Challenges here include enabling more flexible reasoning – such as contextual, priority-based and probabilistic reasoning around plan and intention selection, integration with AI planning tools, and techniques for reasoning about failure and adaptation. Similarly there are challenges in transparency and explainability – while it has long been recognised that cognitive agents can, in principle, explain themselves there has been relatively little work exploring how to do this in practice. Advances have been made in all these areas, but there is comparatively little work that does so while trying to maintain properties such as verifiability.

Specification and verification. The challenges here include enabling better use of different types of verification together to improve verification of systems overall; creating toolkits that enable a unified specification, design, verification and implementation workflow; better analysis and verification of machine learning sub components; improved formal verification techniques to cope with complex autonomous systems; and better consideration of factors such as trustworthiness, security, privacy when designing systems.

Agent flexibility. Capturing, and formalising, both ethical principles and concepts of responsibility across agent-based systems, and then moving from these to both execution and formal verification. Incorporating, and verifying, not only reliability but safety and security issues.

Multi-agent systems. Being able to handle complex human-agent-robot teams, and in particular the dynamic nature of responsibility and autonomy within realistic and practical teams.

Applications. Real applications, from straightforward individual robots, to more complex teams and truly autonomous vehicles acting well beyond human control. Also the practical ethical issues of domestic robotic assistants with safety, social and privacy responsibilities.

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-s.web.bisu.edu.cn/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-s.web.bisu.edu.cn/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-s.web.bisu.edu.cn/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

1. Programming individual autonomous reasoning agents

2. Specification and verification

3. Agent flexibility

4. Multi-agent systems

5. Heterogeneous formal verification

6. Applications

6.1. General robotics issues (inc. ROS verification, robot kitting, hazardous environments, etc)

3 Particularly through involvement in the UK’s “Robots for a Safer World” programme and, within that, RAIN (https://rainhub.org.uk), ORCA (https://orcahub.org), and FAIR-SPACE (https://www.fairspacehub.org).

6.3. Unmanned air vehicles (inc. “Rules of the AIr”, safe operating envelopes, etc)

6.4. Space robotics (inc. orbital, formation-flying, astronaut-robot teams, etc)

6.5. Domestic robotics (inc. safety, social/trust issues, teaching of robots, etc)

7. Broader impact

7.1. Standards and usage

7.2. Regulations, assurance and certification

7.3. International activities

7.4. Outreach and engagement

4 http://www.cs.man.ac.uk/~dennisl/legorovers/

References

³
Particularly through involvement in the UK’s “Robots for a Safer World” programme and, within that, RAIN (https://rainhub.org.uk), ORCA (https://orcahub.org), and FAIR-SPACE (https://www.fairspacehub.org).

⁴
http://www.cs.man.ac.uk/~dennisl/legorovers/