Engineering Responsible And Explainable Models In Human-Agent Collectives

ABSTRACT

In human-agent collectives, humans and agents need to work collaboratively and agree on collective decisions. However, ensuring that agents responsibly make decisions is a complex task, especially when encountering dilemmas where the choices available to agents are not unambiguously preferred over another. Therefore, methodologies that allow the certification of such systems are urgently needed. In this paper, we propose a novel engineering methodology based on formal model checking as a step toward providing evidence for the certification of responsible and explainable decision making within human-agent collectives. Our approach, which is based on the MCMAS model checker, verifies the decision-making behavior against the logical formulae specified to guarantee safety and controllability, and address ethical concerns. We propose the use of counterexample traces and simulation results to provide a judgment and an explanation to the AI engineer as to the reasons actions may be refused or allowed. To demonstrate the practical feasibility of our approach, we evaluate it using the real-world problem of human-UAV (unmanned aerial vehicle) teaming in dynamic and uncertain environments.

Introduction

Autonomous systems are becoming increasingly ubiquitous and are making significant impacts in various safety-critical systems, such as exploration robots (Molnar and Veres 2009), driverless cars (Abeywickrama et al. 2020; Dogan et al. 2016) and unmanned aerial and ground vehicles (Ramchurn et al. 2016; Ramchurn, Stein, and Jennings 2021). Although the evolution of robotics has many compelling benefits, as with other emerging technologies, it comes with new risks and challenges. These challenges can be categorized into three broad and interrelated areas of ethical and social concern: safety and errors; law and ethics; and social impact (Lin, Abney, and Bekey 2014). Therefore, it is essential to ensure that agents make correct and responsible decisions, so that humans or other living beings, infrastructure and society as a whole are not harmed.

Researchers have advocated three main principles that can be used by AI systems to support the social good: accountability, responsibility and transparency (ART) (Dignum 2017). The ART principles form the main pillars of responsible AI. Yazdanpanah et al. (2021) highlight the need for an interdisciplinary effort to address different social, technological, legal and ethical challenges. This requires the development of socio-technically expressive notions of responsibility, blameworthiness and accountability. Dignum et al. (2018) define accountability as the need to explain and justify one’s decisions and actions. Responsibility refers both to the capability of AI systems and to the role of people interacting with them (Dignum et al. 2018). Transparency is defined as “the extent to which the system discloses the processes or parameters that relate to its functioning” (Winfield et al. 2021). Approaches to the design of responsible AI broadly focus on regulation by means of legislation and standards or are design based (e.g. ethics by design). Our research concerns the latter and focusses on the engineering of responsibility in the design of human-agent collectives using formal modeling and verification. More specifically, we engineer decision-making behavior to ensure that a human-agent collective is safe (i.e. nothing bad happens), controllable (meaningful control between humans and agents for collective decisions), trustworthy (what will convince us to trust agents) and ethical (what moral decisions agents may have to take) (see Appendix A for a list of definitions used in this work).

Acting in a responsible manner is important for agents, as described earlier, but so is being able to explain why one’s actions are morally right or wrong (Conitzer et al. 2017). As autonomous systems are becoming part of our daily life, issues related to ways that humans interact with such systems become more significant. Among these issues are making machine decisions transparent, understandable and explainable (Goebel et al. 2018; Koeman et al. 2020). According to Wortham and Theodorou (2017) and Sheh (2017), the ability of a robot or an autonomous system to explain its behavior helps the user to develop an accurate mental model of the robot’s reasoning. This can result in better interaction between them (Koeman et al. 2020). These explanations can be in more understandable natural language, for example, answering why-questions for end users of robotic systems (Koeman et al. 2020). Miller (2019) defines explainability or interpretability as “generating decisions in which one of the criteria taken into account during the computation is how well a human could understand the decisions in the given context.” The relationship between the notions of explainable AI and responsible AI has been described by Barredo Arrieta et al. (2020). Responsible AI is a broader concept that imposes the systematic adoption of several AI principles (e.g. explainability, fairness, accountability and privacy), so AI models can be of practical use.

Now, ensuring that autonomous systems work in a responsible and explainable manner is challenging. This is especially the case when dilemmas are encountered. In this paper, we define dilemmas as decision-making situations in which the choices available to agents are not unambiguously preferred over one another (Bjørgen et al. 2018). When humans are involved, new challenges emerge as humans may not always be able to understand what agents are intending to do and vice versa. Also, humans and agents often need to agree on collective decisions using consensus or compromise (Greene et al. 2016; Loreggia et al. 2018). In order to support collective decision making, agents should be able to account for some form of moral values and ethical principles (Awad et al. 2018), as well as constraints on safety and controllability. According to Rossi (2015), the notions of safety constraints and ethical principles are closely intertwined. An action by an agent can cause harm, thus it can be considered unsafe. However, if the action occurred by accident and there was no intention to cause harm, it may not be considered unethical (Rossi 2015). The use of ethical principles allows agents to reason and determine their actions and explain and justify their behavior in terms that are understandable by humans (Rossi 2015). Furthermore, humans would accept and trust agents more, if they behaved as responsibly as humans in the same environment (Rossi 2015).

An example of a situation in which a dilemma occurs that raises ethical concerns can be described as follows. Assume that a UAV is flying above a football stadium with a match in progress and will run out of battery in a few seconds. The UAV has two options: to crash into the football stadium, thus colliding and harming spectators and players on the ground; or to ascend above 500 feet and collide with a small civilian aircraft carrying passengers. Either of these two actions can harm humans, and the agent will be in a dilemma about the correct, morally significant decision to make.

So, how can we certify that the decision making within human-agent collectives is responsible and explainable? To answer this question, methods and tools that allow the certification (Fisher et al. 2021; Luckcuck et al. 2019) of such systems are urgently needed. In general, certification involves negotiating with a legal authority in order to convince them that the relevant safety requirements have been explored and mitigated appropriately (Fisher, Dennis, and Webster 2013). One key technique that can be explored to provide evidence for certification is formal verification using model checking (Fisher et al. 2021; Fisher, Dennis, and Webster 2013). Formal verification applies formal methods to the problem of system verification. Model checking is a type of formal verification which provides automatic verification for finite state concurrent systems (Clarke, Grumberg, and Peled 1999).

There has been significant interest within the AI community about the verification and validation of autonomous systems (e.g. (Choi, Kim, and Tsourdos 2015; Dennis and Fisher 2020; Dennis et al. 2016, 2016; Molnar and Veres 2009; Qu and Veres 2016; Webster et al. 2011, 2014)) (see Section 2 for more details). However, most of these efforts have focussed on the safety concerns of AI. Webster et al. (2014) and Webster et al. (2011) explore formal verification using model checking to provide formal evidence for the certification of autonomous unmanned aircraft. In these works, the aim was to provide evidence that the autonomous system in control of an unmanned aircraft is safe and reliable. The properties verified are based on the notions of rules of the air (Webster et al. 2014) and airmanship. Later, Dennis et al. (2016), Dennis and Fisher (2020), and Dennis and Fisher (2021) advance the work by Webster et al. (2014), by representing and embedding ethical principles in the decision-making process of an autonomous system. It is clear that, while model checking has been applied to provide the certification of autonomous systems with respect to safety, little work has yet been done on ethical concerns. Furthermore, very little work has used techniques like model checking to support responsible and explainable (Li et al. 2020, 2020) decision making within human-agent collectives. Our approach applies model checking as a step toward supporting the certification of responsible (i.e, ethical, controllable, safe and trustworthy) and explainable decision making within human-agent collectives.

The main contributions of this article are:

• We propose a novel engineering methodology to resolve dilemmas posed by human-agent collectives. We use model checking as a step toward providing evidence for the certification of responsible and explainable decision making within human-agent collectives. Thus, we account for ethical principles, safety and controllability in the decision-making process of human-agent collectives in a way that is amenable to certification. Our approach is based on the Model Checker for Multi-Agent Systems (MCMAS) tool (Lomuscio, Qu, and Raimondi 2017).

• We demonstrate the use of counterexample traces and simulation results to provide a judgment and an explanation to the AI engineer on the reasons actions are refused or allowed. The counterexample traces can be used to identify and track any errors and their sources in the model, which consists of a human-agent collective. The step-by-step interactive simulation of the human-agent collectives provides and confirms the expected behavior of the agents, thus giving confidence to the AI engineer. We explore this feature in particular to show and explain the actions allowed for an agent when having to resolve a dilemma. When faced with a dilemma, the interactive simulation provides an explanation to the AI engineer on the permissibility of actions and describes the reasons why a certain action is preferred over another.

• We evaluate the approach using the real-world problem of human-UAV teaming in dynamic and uncertain environments (Ramchurn, Stein, and Jennings 2021, Ramchurn et al. 2016, Ramchurn et al. 2016). The case study concerns a situational awareness gathering scenario typically found in disaster-response settings where a number of casualties or resources need to be located in a disaster space. This study extends it with dilemma situations relating to safety and controllability, and the ethical behavior of agents.

The preliminary results of our study can be found in (Abeywickrama, Cirstea, and Ramchurn 2019). This article builds on that work in the following manner. First, this article provides a step toward explaining why decisions are made by agents in complex dilemma situations, increasing trust for the AI engineer. Second, this article introduces several new dilemmas about the ethical behavior of agents (e.g. technical problem in a UAV resulting in a crash into humans), and controllability between humans and agents (e.g. crashing into critical personal assets of the collective – avoid conflict with a human’s authority; self-censorship/lying by UAVs). Third, we discuss an extended model of two human-UAV collectives with 11 agents to show how our model can scale up to reasonably complex settings.

The rest of this article is organized as follows. Section 2 describes the main work related to our study and then provides background information on model checking multi-agent systems using MCMAS. In Section 3, our approach for engineering responsible and explainable models in human-agent collectives is presented. A case study scenario in UAV teaming in disaster response is provided in Section 4, and Section 5, applies our approach to the case study. In Section 6, we provide a discussion on our work by identifying several limitations, and Section 7 provides concluding remarks and future directions.

Related Work and Background

This section describes the main work related to our study in the areas of ethical dilemmas and principles (Section 2.1), explainable AI (Section 2.2), and model checking (Section 2.3), and then provides background information on model checking multi-agent systems using the MCMAS tool (Section 2.4).

Ethical Dilemmas and Principles

Yu et al. (2018) propose a taxonomy that divides ethics in AI into four fields: exploring ethical dilemmas; individual ethical decision-making frameworks; collective ethical decision-making frameworks; and ethics in human-AI techniques. Ethics has been defined by Cointe, Bonnet, and Boissier (2016) as a normative practical philosophical discipline of how one needs to act toward others. An example of an ethical dilemma situation is the classical trolley problem (Thomson 1985), which describes several cases where the moral permissibility of actions is evaluated. They are: (i) trolley driver: a runaway railway trolley is about to hit and kill five innocent track workmen. These five men can only be saved if the trolley driver turns the trolley to another track that has only one worker. This worker then will be the only one killed; (ii) bystander at the switch: this is same as (i) but instead of the trolley driver, a bystander observes and diverts the trolley by turning a switch; and (iii) fat man: a fat man is standing on a footbridge over the trolley track, and the only way to stop the trolley is by pushing this bystander onto the tracks. Meanwhile, Lindner et al. (2019) describe three ethical dilemmas involving human-agent collectives: coal dilemma, lying dilemma and child dilemma.

Ethical principles are used to satisfy the morals, desires and capacities of an agent (Cointe, Bonnet, and Boissier 2016), and these can be used to guide human behavior on what is right or wrong (Greene et al. 2016). If intelligent agents are required to collaborate with humans, some ethical guidelines need to be embedded in agents so they can act in their environment following values that are aligned to those of humans. Moral philosophy, which is the field that has studied explicit ethical principles most extensively, advocates three general approaches to engineer ethical behavior in agents: virtue-based, deontological and consequentialist (Cointe, Bonnet, and Boissier 2016; Greene et al. 2016; Yu et al. 2018).

In order to address the requirements for autonomous moral decision making, Lindner, Mattmüller, and Nebel (2020), Lindner, Mattmüller, and Nebel (2019), Lindner and Bentzen (2017), Lindner, Bentzen, and Nebel (2017), and Bentzen (2016) introduce a software library called HERA for modeling hybrid ethical reasoning agents. HERA implements multiple ethical principles like utilitarianism, the principle of double effect, and a Pareto-inspired principle. A prototype robot called IMMANUEL that is based on the HERA approach has been discussed. The utilitarianism and do-no-harm ethical principles described in our approach were originally motivated by these authors’ work. Lindner, Bentzen, and Nebel (2017) have developed a model checker specifically to verify moral situations of agents (causal agency models). Krarup et al. (2020) have implemented a system to provide contrasting explanations to compare the ethical outcomes of different plans. Later, Dennis et al. (2021) have extended this work to verify machine ethics in changing contexts. Halilovic and Lindner (2022) present an approach to local navigation of a robot based on explainable AI. Similarly, our approach is based on formal model checking using the MCMAS tool. However, our approach resolves dilemmas not only about ethical behavior but also dilemmas about controllability and safety between humans and agents. Furthermore, this work is evaluated using a case study in human-UAV teaming in disaster response.

Loreggia et al. (2020), Rossi and Loreggia (2019), Rossi and Mattei (2019), Loreggia et al. (2018), Greene et al. (2016), and Rossi (2015) present a study on the embedding and learning of safety constraints, moral values and ethical principles in collective decision-making systems for societies of machines and humans. In order to model and reason with both preferences and ethical principles in a decision-making scenario, the authors propose a notion of distance between CP-nets (Loreggia et al. 2018). Rossi and Mattei (2019) describe two existing approaches for building ethical bounded AI systems, which are data-driven or rule-based approaches. However, they do not focus on controllability between humans and agents, nor do they use formal model checking.

Papavassiliou et al. (2021) discuss the human behavioral perspectives in order to perform optimal controllability and resource management. Their work proposes a risk-aware resource sharing and management framework for facilitating user QoS satisfaction in the deployment of 5G wireless networks. The goal is to maximize energy efficiency in wireless communications of multi-user heterogeneous networking environments (Papavassiliou et al. 2021).

Explainable AI

Harbers, van den Bosch, and Meyer (2010) present a model for explainable Belief-Desire-Intention(BDI) agents, which describes behavior of BDI agents using beliefs and goals. Four explanation algorithms have been compared in an empirical study involving 20 users. Their user study is based on a fire-fighting training use case. Based on the results, the authors discuss which explanation types need to be provided under different conditions. Kulesza et al. (2012) explore how mental models impact end users’ attempts to debug intelligent agents. This is by providing structural knowledge of a music recommender system. The results of their empirical study show that intelligent agents can provide better feedback, if end users are helped to understand a system’s reasoning. Later, Kulesza et al. (2013) consider the methods in which the intelligent agents need to explain themselves to humans. This is by conducting a user study of 17 participants, focussing on how the soundness and completeness of the explanations impact the fidelity of the mental models of the end users. The authors conclude that completeness is more important than soundness.

Miller (2019) investigates existing works in explainable AI by surveying more than 250 publications from social science venues. Four major findings from the surveyed literature are: (i) the explanations are contrastive, that is they are required in response to particular counterfactual cases; (ii) people select explanations in a biased manner; (iii) the probabilities in explanations are less significant compared to their causes; and (iv) the explanations are social which can be presented as part of an interaction or a conversation. Later, Mualla et al. (2022) present a mechanism for parsimonious explainable AI called HAExA, which is a human-agent explainability architecture allowing remote robots to be operational. HAExA applies both contrastive explanations and explanation filtering, and the architecture has been evaluated using an empirical user study. The authors use parametric and non-parametric statistical testing to analyze the results.

A few works undertake empirical user studies to assess the process of explanation reception (Miller 2019). For instance, Madumal et al. (2019) discuss different levels of explanations for model-free reinforcement learning agents. Causal models are used to derive causal explanations of behavior based on counterfactual analysis of the models. An empirical evaluation has been conducted using a human-computer interaction study, which shows that the abstract causal explanations provide better performance on explanation quality. However, none of the discussed approaches on explainable AI explore explainability at the formal verification level using model checking as considered in our work.

Model Checking

Several approaches have applied the MCMAS tool to formally verify autonomous systems in AI settings (e.g. (Choi, Kim, and Tsourdos 2015; Elkholy et al. 2020; Molnar and Veres 2009)). Molnar and Veres (2009) apply MCMAS for the formal verification of autonomous underwater vehicles. A methodology has been introduced using formal verification for the integrity and fault assessment system of complex autonomous engineering systems (Molnar and Veres 2009). Choi, Kim, and Tsourdos (2015) present an approach for the verification of heterogeneous multi-agent systems using the MCMAS tool. They demonstrate how model checking can be used to verify the decision-making logics of multi-agent systems at the design level. Like us, they also model a collective of human actors and UAVs, but they do not address the resolution of any ethical or controllability dilemmas. Elkholy et al. (2020) using MCMAS propose a formal and operational approach for modeling, verifying, and testing intelligent critical avionics systems.

Webster et al. (2014) and Webster et al. (2011) explore model checking to provide formal evidence for the certification of autonomous unmanned aircraft. The aim is to provide evidence that the autonomous system in control of an unmanned aircraft is safe and reliable. The properties verified are based on the notions of rules of the air (Webster et al. 2014) and airmanship. Like us, the authors model and resolve dilemmas relating to the ethical behavior of agents (e.g. intruder detection and fuel low). Later, Dennis and Fisher (2020), Dennis et al. (2016), and Dennis et al. (2016) advance the work in (Webster et al. 2014), by representing and embedding ethical principles in the decision-making process of an autonomous system. There the authors propose a theoretical framework for ethical plan selection that can be formally verified. They present a verifiable ethical decision-making framework that implements a specified ethical decision policy. The framework pro-actively selects actions that will keep humans out of harm’s way. The systems developed are verifiable in the Agent JPF model checker and can integrate with external systems. Later, Bremner et al. (2019) have implemented BDI style reasoning in Python where Asimov’s laws of robotics have been used as an example of an ethical theory to decide the courses of action. Compared to our study, a key difference in the work by Dennis and Fisher (2020), Dennis et al. (2016), and Dennis et al. (2016) is that model checking is applied at the implementation level using policies. However, in addition to ethical concerns, our work supports verifying dilemmas about controllability between humans and agents for responsible AI. Furthermore, our work exploits counterexample traces and simulation results as a first step toward supporting explainable AI.

Yazdanpanah et al. (2021) and Yazdanpanah et al. (2021) apply formal methods and modal logics for reasoning about accountability using alternative-time temporal logic-based techniques in multiagent systems. Their work focusses on answering “who is accountable for an unfulfilled task in multiagent teams: when, why, and to what extent?” (Yazdanpanah et al. 2021). The main results of their work are on decidability, fairness properties, and computational complexity of the proposed accountability ascription methods in multiagent teams. The authors discuss their approach using application domains like connected and autonomous vehicles. However, their work focusses primarily on accountability concerns of multi-agent systems, whereas our work has a more broader goal of ensuring a human-agent collective is safe, controllable, trustworthy and ethical.

Li et al. (2020), Li et al. (2020), and Casimiro et al. (2021) present a formal framework that incorporates human personality traits to design human-on-the-loop self-adaptive system. There an explanation is used to help a human operator to improve the utility of the overall system. The authors characterize explanations in terms of explanation content, effect and cost (Li et al. 2020). Probabilistic model checking has been used to synthesize optimal explanations, which is based on a formal human model with psychologically relevant aspects of personality. Their work is evaluated using a virtual human and system interaction game. But, the authors do not resolve dilemmas posed by human-agent collectives as performed in our work.

Therefore, from the analysis of the related work, it is clear that although model checking has been applied to provide certification of autonomous systems with respect to safety (e.g. (Adegoke, Ab Aziz, and Yusof 2016; Choi, Kim, and Tsourdos 2015; Molnar and Veres 2009; Qu and Veres 2016)), little work has yet been done on ethical concerns (e.g. (Dennis and Fisher 2020, 2021; Dennis et al. 2016, 2016; Mermet and Simon 2016)). Furthermore, very little work has used techniques like model checking to support certification with respect to responsible and explainable (Li et al. 2020, 2020) decision making within human-agent collectives.

MCMAS Tool and ISPL

Model checking is an automatic verification technique for finite state concurrent systems (Clarke, Grumberg, and Peled 1999). In model checking, the system is represented by a finite model $M$ and the specification by a formula $\varphi$ using appropriate logic. The model checker computes and establishes automatically whether the model $M$ satisfies the formula $\varphi$ ($M\models \varphi$) or not ($M\varphi$).

This study uses the MCMAS tool to model and verify the decision-making behavior in dilemma situations of human-agent collectives. Compared to other model checking tools, MCMAS (Lomuscio, Qu, and Raimondi 2017) is designed to model and verify multi-agent systems (e.g. see (Choi, Kim, and Tsourdos 2015; Molnar and Veres 2009)). Also, the fact that MCMAS can deal with a large multi-agent system (scalable) which is composed of many autonomous agents is another benefit. Thus, in this study, we use MCMAS for the automatic formal verification of human-agent collectives.

At the center of MCMAS and its modeling language is the notion of interpreted systems. Interpreted systems are a formalism that can be used to model multi-agent systems and reason about knowledge (Porter 2004). They are an extension of Kripke semantics for multi-agent systems where the internal states of all agents are composed to obtain the global states of the whole system. Raimondi (2006) describes why interpreted systems are best suited for modeling multi-agent systems. Unlike Kripke models and concurrent game structures for modeling multi-agent systems, interpreted systems are well suited for epistemic modalities expressing agents’ knowledge because they distinguish between local and global states. In addition, interpreted systems are: computationally grounded (i.e. an interpreted system’s semantics can be directly mapped to runs of a system and vice versa); the notion of local states offers a flexible abstraction for an agent; and they can easily be extended to include different modalities (Raimondi 2006).

The MCMAS tool uses a dedicated programming language derived from the formalism of interpreted systems called ISPL (Interpreted Systems Programming Language) (Lomuscio, Qu, and Raimondi 2017). An ISPL specification has six essential parts to represent an interpreted system: agent (environment or standard), InitStates, evaluation, groups, fairness and formulae (Lomuscio, Qu, and Raimondi 2017) (see Table 1).

Table 1. ISPL syntax used in this work.

ISPL	Description
Agent	A multi-agent system is composed of an environment agent and a set of standard agents. The environment agent describes boundary conditions and infrastructure shared by the standard agents (Lomuscio, Qu, and Raimondi 2017). Each agent is modelled using:
	(i) a set of local states;
	(ii) a set of actions;
	(iii) a protocol–a rule describing what actions can be performed in a given local state by an agent;
	(iv) an evolution function, which describes how the local states of agents change as a result of their current local state and other agents’ actions.
InitStates	By using a Boolean expression over local states, InitStates defines a set of initial states for all the agents (Lomuscio, Qu, and Raimondi 2017).
Evaluation	This contains Boolean variables, which are defined as Boolean expressions over the local states of the agents (Lomuscio, Qu, and Raimondi 2017). These Boolean variables are used in the Fairness conditions and in the formulae to be verified.
Groups	Groups can be used to define a group of agents, which can then be used in the Formulae section to verify group modalities.
Fairness	Fairness contains a list of Boolean expressions, and all the formulae contained there must be true infinitely often along all the executions considered by the model checker (Lomuscio, Qu, and Raimondi 2017). In this study, fairness conditions are used to rule out behaviours allowed by the model but not achievable in practice.
Formulae	Formulae defines the properties to be verified. In this work, the properties for model checking are specified using Computational Tree Logic (CTL) along with epistemic operators. Epistemic operators are used to reason about what agents know (e.g. knowledge of an agent or common knowledge of a group of agents) (Lomuscio, Qu, and Raimondi 2017).

Next we describe our proposed methodology for engineering responsible and explainable models in human-agent collectives.

Approach: Engineering Responsible and Explainable Models in Human-Agent Collectives

This section provides an overview of our engineering methodology to resolve dilemmas around ethical concerns, controllability and safety. Our engineering methodology, which is based on the MCMAS tool (Lomuscio, Qu, and Raimondi 2017), is a step toward providing evidence for the certification of responsible and explainable decision making within human-agent collectives. For modeling we primarily use ISPL.

Following standard practice (Clarke, Grumberg, and Peled 1999), the overall model checking process (see Figure 1) is divided into three main tasks: modelling, specification and verification (see Sections 3.1–3.3). In Figure 1, the models and activities of the model checking process are represented as rectangles and ellipses, respectively.

Figure 1. Steps for engineering responsible and explainable models in human-agent collectives at design-time.

Modelling

In what follows, we describe the modeling of a collective of humans and agents to resolve dilemmas involving ethical behavior, controllability and safety. Both humans and machines in the collective are modeled in ISPL as standard agents, and a human-agent collective is modeled as a group (see Section 2.4). Next we discuss ethical principles, which are used in our study for the resolution of ethical dilemmas within human-agent collectives.

Ethical Principles

Moral philosophy, which is the branch of philosophy concerned with ethics, establishes various ethical principles. According to Lindner, Mattmüller, and Nebel (2020), Lindner, Mattmüller, and Nebel (2019), and Lindner, Bentzen, and Nebel (2017), ethical principles are abstract rules according to which concrete courses of actions can be determined. These can be used to guide human behavior about what is right or wrong (Greene et al. 2016; Loreggia et al. 2018; Rossi 2015). If we need intelligent agents to collaborate with humans, some ethical guidelines need to be embedded in these agents so they can act in their environment following values (standards of behavior) that are aligned to humans. A key benefit in the use of ethical principles is to open up the possibility of communicating decisions to the user.

Three main approaches have been advocated in moral philosophy for encoding ethical behavior in agents: virtue-based, deontological and consequentialist (Cointe, Bonnet, and Boissier 2016; Greene et al. 2016; Yu et al. 2018). In a virtue-based approach, an agent is ethical if it acts and thinks according to certain moral values, for example, wisdom, bravery, justice. In a deontological approach, an agent is ethical if it respects obligations and permissions related to possible situations. In a consequentialist approach, an agent is considered ethical if it weighs the morality of the consequences of each action and selects the action that has the most moral consequences. In this paper, we apply a consequentialist approach as it is the most relevant – it weighs the morality of the consequences of each choice as opposed to values like wisdom (virtue ethics) or obligations and permissions (deontological approach) (Cointe, Bonnet, and Boissier 2016). Moreover, the multi-agent model checker used in our study and the semantics of its language are more supportive of such an approach.

Based on the consequentialist approach, we therefore describe and model two ethical principles: utilitarian and do-no-harm (Lindner, Bentzen, and Nebel 2017; Lindner, Mattmüller, and Nebel 2019, 2020). Both principles presuppose a theory of what is good and bad, and assign utilities to consequences accordingly. With respect to determining the utility values for reflecting what is morally good or bad, the AI engineer can review the code of conduct or safety regulations formalized in the domain of application (e.g (UAViators 2021). in UAVs).

• Utilitarian principle: an agent is permitted to perform an action if its consequence has the highest utility value compared to the consequences of other actions. Thus, it is allowed to perform an action that has the least harm.

• Do-no-harm principle: an agent refrains from performing actions that can cause harm, that is, actions that have any negative consequences.

In this research, these ethical principles are modeled using ISPL and enforced as a set of logical formulae to be checked against the model (i.e. the description of an actual case of an ethical dilemma situation). Next we describe and define an ethical dilemma that uses these ethical principles.

Ethical Dilemmas

Our approach for modeling dilemma situations on ethical concerns was originally motivated by the formal semantics proposed by Bentzen (2016) where moral cases capturing actions, causes, intentions and utilities have been represented. We extend and build on their work to facilitate rigorous model checking using the MCMAS tool, and evaluate our approach using a case study in human-UAV teaming (see Section 4.2). A formal case description of an ethical dilemma consists of several elements that have been adapted from (Lindner and Bentzen 2017; Lindner, Bentzen, and Nebel 2017; Lindner, Mattmüller, and Nebel 2020). In our study, an ethical dilemma is formally defined as:

Definition

Ethical Dilemma for an Agent. An ethical dilemma can be represented as a tuple $M=(A,C,u,W)$ in which:

• $A=\{A_1,A_2,\dots \}$ is the set of actions. For example, actions during a communication dropout of a UAV: collideAndDamageSelf, collideWithHumans;

• $C=\{C_1,C_2,\dots \}$ is the set of consequences that indicate the effects of actions. For example, consequences during a communication dropout: humanSurvives, uavCollidesAndHarmsHumans. To simplify modelling, here we assume that each action has one consequence, that is, $c:A\to C$. However, our approach can be extended to allow several consequences for each action;

• Mapping of consequences to utilities, that is, $u:C\to \mathbb{Z}$. Utilities $u$ are used to rank the consequences where each literal is assigned with an integer value indicating the moral significance of the consequence: $u(c)>=0$ implies a good outcome with no harm, and $u(c)<0$ implies some harm;

• $W$ is a set of Boolean interpretations of $A$ (Lindner, Bentzen, and Nebel 2017), and its elements correspond to actions available to the agent called options (a.k.a. permissible actions). It is assumed that each $w\in W$ assigns $1(true)$ to exactly one element of $A$, that is, each option involves exactly one action to be performed. The options $w$ are determined using the ethical principle applied (i.e. utilitarian or do-no-harm), as formally defined next.

Utilitarian Principle: According to the utilitarian principle, an action $A_j$ is permissible (referred to as an option $w$ here) if and only if its consequence yields the highest utility, that is: $\mathrm{\forall }i.(u(c(A_j))\ge u(c(A_i)))$.

Do-no-harm Principle: In the do-no-harm principle, an action $A_j$ is permissible (referred to as an option $w$) if and only if its consequence is morally good (positive) or indifferent (zero utility), that is: $u(c(A_j))\ge 0$.

Next we describe how controllability dilemmas and safety concerns are modeled and resolved in our work.

Controllability Dilemmas and Safety Concerns Between Humans and Agents

In addition to the dilemmas around ethical behavior described earlier, we model dilemmas about controllability and safety between humans and agents (e.g. see dilemmas D4.1–D4.5 in Section 4.2). By controllability we mean meaningful control between humans and agents so authority can be shared and assigned to facilitate collective and responsible decisions (Ramchurn et al. 2016; Ramchurn, Stein, and Jennings 2021). The resolution of these dilemmas is modeled by exploiting: (i) the evolution function of the ISPL specification in MCMAS; and (ii) the environment agent in ISPL which describes boundary conditions and infrastructure shared by the standard agents.

In ISPL, all actions of an agent are publicly observable. This feature essentially supports the interaction between agents and the environment. Then, this public observability of actions feature is used in the evolution function of an agent, which describes how the local states of agents evolve (i.e. change value over time). This function returns the next local state based on the agent’s current local state, and the joint actions performed by all other agents at a given instant. In interpreted systems, the agents synchronize with each other and the environment via joint actions. The conjunction of all the agents’ evolution function is used to compute a global evolution function of the system. Also, in MCMAS, the agent actions defined in the agent states can then be used by the environment agent to update its variables. These variables include any observable variables used by other agents. In this manner, we control and coordinate the execution of agent states of human and machine agents in the collectives.

See Section 5.2.3 for several controllability dilemmas modeled and resolved using ISPL in the case study – controllability between a UAV and a bronze commander when requesting manual control (dilemma D4.1); controllability between a planning agent and a bronze commander when requesting replanning routes (dilemma D4.3); and controllability between a UAV and a silver commander when crashing into critical personal assets of the collective (dilemma D4.4).

Specification

Having described the model of the human-agent collectives in the preceding subsection, we now focus on the specification of properties, which is the second step of our methodology. In model checking, specification is the statement of the system properties that the design needs to satisfy. In this study, based on the system requirements, properties are formalized focussing on the required behavior of the humans and agents in the collectives to ensure they are ethical, controllable, and safe (Figure 1). Safety ensures that nothing bad happens (e.g. “the do not stay above 500 feet rule for a UAV;” “the do not enter a no-fly zone during flight rule for a UAV”). We also specify properties to ensure the correct control between humans and agents to resolve controllability dilemmas. For example, see Section 5.3.1 for properties defined to ensure controllability behavior between humans and agents during the communication dropout of a UAV. These properties are included in the Formulae section of the ISPL specification (Section 2.4). In our study, we use CTL along with epistemic operators to specify the properties used for model checking. In addition, we use fairness conditions (Lomuscio, Qu, and Raimondi 2017) to rule out unrealistic behavior in the model or to avoid a particular state forever. For example, the UAVs cannot avoid their move toward task states forever (see Section 5.3.2). We also check for any deadlock state in the model where no agents can make progress.

Verification and Simulation

Verification and simulation are the final step in our proposed methodology, which performs the actual validation of the model against the specification. During verification, the MCMAS model checker takes the model of dilemma situations of the human-agent collective and required properties as inputs (Figure 1). It checks the permissibility of actions by verifying the decision-making behavior in dilemma situations against the logical formulae capturing safety, controllability and ethical behavior. Any violations result in counterexample traces that hold information about the properties violated. We exploit the counterexample traces and the step-by-step interactive simulation to provide a judgment and an explanation to the AI engineer. The counterexample traces can be used to identify and track any errors and their sources in the model, which consists of a collective of human and machine agents in collaboration.

The step-by-step interactive simulation of the human-agent collectives shows and confirms the expected behavior of the agents as opposed to counterexamples which highlight any errors. This essentially gives confidence to the AI engineer in the correctness of the behavior of the human-agent collectives modeled. The simulation is performed by first selecting an initial state and then by choosing a successor state among those reachable via the enabled transitions. In our study, we explore the simulation feature in particular to show and explain the actions allowed for an agent when resolving a dilemma (see Section 5.4.1). During a dilemma, the simulation provides an explanation to the AI engineer on the permissibility of actions, and describes the reasons why a certain action is preferred against another.

The verification and simulations results can be used by the AI engineer to improve and refine the design of the model iteratively and build a specification that is correct (Figure 1).

Case Study: UAV Teaming Dilemmas in Disaster Response

In this section, we describe the case study scenario of human-UAV teaming in disaster response. Based on this scenario, in Section 5, we then proceed to demonstrate how our model checking approach can be used to engineer responsible and explainable models in human-agent collectives.

Scenario

The scenario is based on a case study in human-UAV teaming in dynamic and uncertain environments (Ramchurn et al. 2016, 2016; Ramchurn, Stein, and Jennings 2021) focussing on a situational awareness-gathering task typically found in disaster-response settings where a number of casualties or resources need to be located or verified in a disaster space. This study extends it with dilemma situations relating to safety and controllability, as well as the ethical behavior of agents.

As illustrated in Figure 2, let us consider two human-agent collectives in which the first collective contains two UAVs deployed to monitor and analyze two target locations. The second collective contains a single UAV deployed to analyze a single target location in the same disaster space. In the first team, the two UAVs are commanded by two bronze commanders¹ and a silver commander; and in the latter, a single UAV is handled by a bronze and a silver commander. As the UAVs of both these collectives share the same space, in order to find a consensus the agents are expected to inform and negotiate their availability and routes with the other UAVs and their commanders.

Figure 2. Two human-UAV collectives with UAVs deployed to monitor separate target locations. Silver and bronze commanders provide tactical and operational support.

In a human-UAV collective:

• Bronze commanders monitor video feeds from their UAVs and provide mission-planning support. They can change the routes of their UAVs and take manual control to perform specific operations (e.g. examine a target location more closely, drop off medical supplies).

• Silver commanders are tactical commanders at a base station. They can only create tasks and either manually specify paths or use the planning agent to generate paths for individual UAVs. The silver commanders can also use an interface to modify paths provided by the planning agent. The video feeds and images can be flagged by a silver commander to be examined by a bronze commander at a target location.

• The planning agent in the base station server uses a multi-agent planning algorithm (e.g. (Ramchurn et al. 2016)). It estimates the time to move to a target and allocates a UAV to it based on the amount of fuel available. In the case where tasks may need more than one UAV, the algorithm will ensure that the correct set of UAVs is allocated to complete the mission.

• The environment agent represents the environment in which UAVs and commanders operate. It is used to describe boundary conditions and infrastructure shared by the humans and agents, for example, rain status, ground visibility, wind strength and risk level. For this the environment agent gets queried by the UAVs and human actors of the model.

Having provided a summary of the scenario, next we describe the human-UAV dilemmas in the case study.

Human-UAV Teaming Dilemmas

As mentioned in Section 1, dilemmas are decision-making situations in which choices available to an agent are not unambiguously preferred over another (Bjørgen et al. 2018). This is because either of the available choices to the agent will cause some harm, which can be to the humans, animals, infrastructure, other UAVs or the UAV itself.

The case study describes four main dilemma situations out of which the first three dilemmas concern the ethical choices a UAV can take, while the fourth relates to controllability and safety between the humans and agents. Figure 3 illustrates a classification for different dilemmas with examples from the case study. UK’s Watchkeeper program provides a real world example of a human-UAV teaming dilemma (Wikipedia 2020). The Thales Watchkeeper WK450 is a UAV for all weather, intelligence, surveillance, target acquisition and reconnaissance that is used by the British army. Lately, it has been used by the UK border force to monitor migrant crossings in the channel. But, unfortunately, several units have crashed during training exercises in the past few years.

Figure 3. Classification of dilemmas in our case study.

Figure 4 illustrates a Kripke model (Kripke 1963) of two human-UAV collectives in which the first collective contains two UAVs, a silver commander, a bronze commander and a planning agent; the second collective contains a single UAV, a silver and bronze commander, and a planning agent. A Kripke model provides a formal yet an intuitive and expressive model; thus it is explored in this article to illustrate the different dilemma situations. It shows the possible worlds (states) and accessibility relations (solid arrows) of the humans and agents, and the different dilemma situations (see D1–D4). In Figure 4, the controllability situations between agent states that are in a dilemma (see controllability dilemmas D4.1–D4.5) are illustrated using dash arrows. A global Kripke model is obtained by composing the Kripke models of the individual agents. Note that the states and transitions of each agent are used to obtain the states and transitions of the entire system.

Figure 4. Kripke model with two human-agent collectives for case study scenario showing dilemmas D1–D4. Controllability between agent states is shown using dash arrows.

D1 – Communication dropout: This occurs when a UAV loses contact with its server for a prolonged time. Without communication, the UAV’s position is unknown to the humans involved and other UAVs; it therefore poses a risk to others and cannot simply wait. After a communication dropout the UAV can make a choice to:

• wait until communication is restored;

• crash into an empty field if available;

• collide and damage infrastructure or vehicles on the ground;

• collide with vehicles in the air (e.g. other UAVs or flying objects);

• collide and harm animals on a field; or,

• collide and harm humans on the ground.

Indeed, this is a dilemma as all of these actions can cause harm to humans or animals or physical damage to the infrastructure or the UAV itself. The agent needs to calculate and decide what is the best action it could perform using the applied ethical principle.

D2 – Technical problem/Battery low dilemmas: In what follows, we describe two dilemmas that occur when a UAV encounters a technical problem, and when its battery is depleted, requiring it to perform an emergency landing.

• D2.1: Technical problem in a UAV resulting in a crash into humans: This dilemma is a variant of the classical trolley problem (Section 2.1), which considers what a UAV should do in the case it is about to crash into humans; this provides several critical moral arguments. Here, we assume the technical problem faced is that of a depleted battery.

Now let us relate the trolley driver scenario described in Section 2.1 to our case study. Assume that a UAV is flying above a football stadium with a match in progress and is about to run out of battery in a few seconds. It has two options – first, to crash into the football stadium, thus colliding and harming spectators and players on the ground; or second, to ascend above 500 feet and collide with a small civilian aircraft carrying passengers. Either of these two actions can harm humans, and the agent will be in a dilemma about the correct, morally significant decision to make. However, the collision with the small civilian aircraft is not guaranteed to harm humans, as the aircraft may survive the impact of the collision. The question the designer is faced with is: is it morally ethical for the agent to ascend and collide with the aircraft or crash into the football stadium?

• D2.2: Battery low resulting in an emergency landing: A UAV has detected that its battery level is too low and it is unable to reach its destination or base station. Thus, it needs to perform an immediate emergency landing. This dilemma differs from D2.1, as the agent has determined that it could perform an emergency landing as opposed to crashing. Let us assume that there is no empty field in sight for the UAV to land. Here, the UAV will be in a dilemma about deciding where to land responsibly. The choices a UAV has to make are similar to those in D1 except that the UAV has to land within a deadline. If the UAV decides to land in a field where there are humans, it may collide with and harm humans on the ground. If it chooses to land in a field with animals, it may cause harm to them. Instead, if the UAV decides to land on infrastructure (e.g. public road with power lines), it may damage the infrastructure and the UAV itself. As seen here, any of the UAV’s choices may cause harm to or damage humans, animals, infrastructure or the UAV itself.

D3 – Intruder detection and collision: An intruder can be of two types: malicious which can be another UAV intentionally trying to harm or collide; or non-malicious which can be birds or another UAV unintentionally crossing paths. With respect to this dilemma, assume that a UAV has detected that an aerial vehicle is in close range and is on a collision course even after taking evasive actions. The UAV will be in a dilemma whether to:

• collide with the intruder head on;

• collide with some infrastructure on its path; or,

• break a safety constraint (e.g. staying above 500 feet and thereby putting itself in danger of collision with other flying objects).

D4 – Controllability between humans and agents: This dilemma considers issues of controllability and the safety of humans and UAVs. This can be caused by several factors such as: humans not being able to react swiftly; human fatigue and loss of focus level (e.g. due to the high number of UAVs to be monitored); limited sensing range of UAVs. Therefore, to manage such situations, the mission management system used by the commanders would need to assess their fitness and focus levels and determine whether they can be given control of the UAVs (see (Cummings et al. 2013)). For example, the bronze commanders can be equipped with head-mounted displays that monitor their attention and levels of cognitive overload.

The controllability dilemmas (illustrated using dash arrows in Figure 4) can be of three main types, i.e. controllability between: (i) humans and agents; (ii) two or more agents; or (iii) two humans. We only consider the first two types in this article. Human-human dilemmas are beyond the scope of this paper and we will consider them in future work. We identify several examples from the case study on this dilemma in the following where D4.1–D4.4 are based on human-agent controllability, while D4.5 is between two agents.

• D4.1: Request for manual control: A bronze commander can ask to control and guide their UAV manually. However, the UAV can make a decision to allow or reject the request depending on its current state. For example, if the UAV is in an emergency avoid state (i.e. an intruder detected or an above safe-altitude state) or a battery too low state, the request for manual control will not be allowed.

• D4.2: Request for replanning routes by a commander: A similar dilemma situation may occur when the silver commander needs to replan the routes of UAVs. The UAV can make a decision to permit or disallow requests depending on its current state (e.g. if the UAV is in an emergency avoid state), as applied during the manual control request (D4.1).

• D4.3: Request for replanning routes by planning agent: As mentioned previously, the planning agent is used by a silver commander to automatically compute a plan for a UAV. Let us assume that UAV2_HAC1 had a communication dropout, and the planning agent has been called to compute a plan after reallocating tasks. In this context, the planning agent will be in a dilemma and it will only compute a plan depending on the state of the BronzeCommander1_HAC1 that handles UAV1_HAC1. If the BronzeCommander1_HAC1 is engaged in some task (e.g. taking manual control of their UAV), the planning agent can reject the planning request by the silver commander.

• D4.4: Crashing into critical personal assets of the collective – avoid conflict with a human’s authority: This dilemma involves collaboration between a human and an agent on authority where the human can impose authority over an agent that can lead to an ethical conflict. Also, this dilemma highlights the importance of humans being in the decision-making loop (Cummings 2014). Let us assume that the sudden failure of a UAV forces it to crash and there are only two sites available: a UAV hangar that accommodates UAV aircraft, critical equipment and storage facilities; and a public car park with many parked vehicles. The agent needs to evaluate the consequences of each crash and select the morally significant option based on the ethical principle applied. However, the authority of the human operator is an additional significant consideration during the decision making. In this situation, the human can choose the site and let the UAV execute the decision or instead the human can override the UAV’s decision. This situation can lead to an ethical conflict as the human and agent can disagree, especially if the human has personal factors to consider (e.g. a crash resulting in damage to critical personal assets in the hangar), which may not be known to the agent. This requires effective sharing and controlling of authority between the human and the agent in order to manage the potential conflict. Should the agent give away control to the human if there are personal factors involved in the decision?

• D4.5: Self-censorship/lying dilemma: This dilemma deals with self-censorship or lying by UAVs of different human-UAV collectives. Therefore, it can be categorized as a controllability dilemma between agents (Figure 3). In the case study, we consider two teams of human-agent collectives functioning in a particular locality (see Figure 2). As the UAVs of both these collectives share the same space, in order to find a consensus the agents are expected to inform and negotiate their availability and routes with the other UAVs and their commanders. Although the humans (e.g. silver commanders) are not directly involved in this dilemma, the agents communicate and negotiate on behalf of their commanders. Here, an agent may consider exposing additional information to another UAV in a different collective as a violation of its privacy. Is it morally ethical for a UAV to conceal its status (e.g. availability, route information) to another UAV when requested in order to benefit its human user? This dilemma may also be modeled as an ethical dilemma; however, in that case both ethical principles – utilitarian and do-no-harm – would evaluate lying as a forbidden action.

Model Checking Human-UAV Collectives

In this section, we apply our approach to the case study described in Section 4. Our contribution here is a novel engineering methodology to resolve dilemmas using model checking, as a step toward providing evidence for the certification of responsible and explainable decision making within human-agent collectives. See Section 2.4 for a summary of the ISPL language semantics used in this paper.

Before describing the model checking of different dilemmas of the case study, we explain the coordination between humans and agents using a simplified model of two agents (UAV1_HAC1 and BronzeCommander1_HAC1) (see Section 5.1). This is mainly to explain how ISPL executes agent states of the different agents – humans or machine agents – in the collective step by step. Then, we describe the modeling (Section 5.2), specification (Section 5.3) and verification (Section 5.4), performed using MCMAS of the different dilemmas in the case study.

The relationship between the global Kripke model explained in the previous section and the ISPL model of the human-agent collectives described here can be explained as follows. MCMAS uses an interpreted system (Lomuscio, Qu, and Raimondi 2017) to describe Kripke models in a succinct way. The possible worlds ($W_i$) of the Kripke model (Figure 4) correspond to the states of an agent in ISPL (e.g. MoveTowardsTask), while the accessibility relations ($r_j$) of the Kripke model relate to an action within the evolution function in ISPL.

Listing 1: human-UAV collective modeled in ISPL.

1 Groups 2 multiUAVHumanAgentCollective = {UAV1_HAC1, UAV2_HAC1, BronzeCommander1_HAC1, BronzeCommander2_HAC1, SilverCommander_HAC1, PlanningAgent_HAC1, UAV3_HAC2, BronzeCommander_HAC2, SilverCommander_HAC2, PlanningAgent_HAC2, Environment}; 3 end Groups

In the case study scenario, 11 agents have been modeled in ISPL (see multiUAVHumanAgentCollective group in Listing 1) to represent the decision-making behavior of the human-UAV collectives. The first human-UAV collective has two UAVs, two bronze commanders, a silver commander and a planning agent. At the same time, the second collective has a UAV, a bronze commander, a silver commander, and a planning agent. The environment agent is shared between the two collectives. For a description of the different agents modeled in the case study and their local states see Appendix B.

Consequentialist approach: In this paper, our work follows a consequentialist approach (Section 3.1.1), and toward achieving this, we model the evaluation of the consequences and actions of an ethical dilemma as two separate agent states. There the model first reasons the consequences with utility values, and then decides on the permissible actions (e.g. see corresponding $W_{12}$ of UAV1_HAC1 in Figure 4). Also, as a step towards supporting explainable AI, a second agent state describes the rationale for the judgment on the permissibility or non-permissibility of actions to the AI engineer (e.g. see corresponding $W_{20}$ of UAV1_HAC1 in Figure 4). Note that these two states on evaluating consequences and actions do not alter the behavior of any human or machine agent. The agent states for evaluating consequences and actions evolve using the evolution function of the UAV, which updates the local states of an agent. That is, when the agent is in the state where it evaluates consequences, the agent will evolve to its corresponding permissible actions state.

Modelling of an Agent and Communication Between Agents

In this subsection, we explain the coordination between humans and agents using a simplified model of two agents (see Listing 2 and Listing 3 for UAV1_HAC1 and BronzeCommander1_HAC1). When describing this model, we also explain the underlying ISPL semantics used. As stated in Section 2.4, an agent is modeled in ISPL using: (i) a set of local states; (ii) a set of actions; (iii) a protocol; and (iv) an evolution function. An ISPL program of a multi-agent system is composed of a number of standard agents and the environment agent.

• Local states: The local states are the internal states of an agent (Lomuscio, Qu, and Raimondi 2017). These are modeled using private local variables, which means that an agent can only observe its own local states, and the protocol or the evolution function of an agent cannot refer to other agents’ local variables. For example, see states—MoveTowardsTask and AboveSafeAltitude for UAV1_HAC1 in Listing 2. The only exception is that standard agents can see some variables of the environment agent, which are called local observable variables. However, the values of these variables can only be changed by the environment.

• Actions: The interaction between agents and the environment is performed by means of publicly observable local actions. Note that although all actions are publicly observable, we only exploit this feature when we need to control and coordinate the execution of agent states of different agents. In the example, UAV1_HAC1 has actions to launch the mission, move to the target location, and alert its commander about the unsafe altitude (see Listing 2). BronzeCommander1_HAC1 has actions to analyze video feed from the UAV and request manual control (see Listing 3).

• Protocol: Protocols are rules describing what actions can be performed by an agent in a given local state. When the UAV is on the ground (OnGround state), the possible actions for the UAV are: receiveLaunchCommand and launchMission. As local states are defined as variables, protocols are expressed as functions from variable assignments to actions. Protocols are non-deterministic, which means it is possible to associate a set of actions to a given variable assignment. The action to be performed is selected non-deterministically from the set of actions.

• Evolution function: The evolution function allows the local states of agents (human or machine) to evolve based on their current local state and on other agents’ actions. The conjunction of all the agents’ evolution function is used to compute a global evolution function of the human-agent collectives. In Listing 2, the evolution function for UAV1_HAC1 would move the agent to the AboveSafeAltitude state, if the current state is MoveTowardsTask and if the UAV’s altitude reaches more than 500 feet. Likewise, the evolution function for BronzeCommander1_HAC1 would move that agent to the ManualControlRequest state, if the current state is MonitorVideoFeed and when it executes the requestManualControl action. We also exploit the evolution function to support controllability between human and machine agents, and resolve any controllability dilemmas (Section 3.1.3). For example, BronzeCommander1_HAC1 will be able to enter a ManualControl state only if UAV1_HAC1 is not in an emergency avoid or battery low state. For this purpose, BronzeCommander1_HAC1 checks whether the UAV1_HAC1 is executing any of the actions with respect to the emergency avoid or battery low states.

Listing 2: simplified model of UAV1_HAC1.

1 Agent UAV1_HAC1 2 3 Vars: 4 state : {OnGround,MoveTowardsTask, AboveSafeAltitude,EmergencyAvoid,…}; – Declaration of states 5 altitude : 0.505; – Declaration of altitude 500 to 505 feet 6 end Vars 7 8 – Declares the possible actions for UAV1_HAC1 9 Actions = {receiveLaunchCommand, launchMission,move,alertCommanderOnSafeAltitude, alertCommanderOnIntruderDetected,…}; 10 11 – A rule that describes what actions are possible in each local state by UAV1_HAC1 12 Protocol: 13 (state=OnGround): {receiveLaunchCommand, launchMission}; 14 (state=MoveTowardsTask): {move}; 15 (state=EmergencyAvoid): {alertCommanderOnSafeAltitude}; 16 … 17 end Protocol 18 19 – Evolution function which describes how the local states of UAV1_HAC1 changes as a result of its current local state and actions of other agents (i.e. BronzeCommander1_HAC1) 20 Evolution: 21 state = MoveTowardsTask if (state = OnGround and Action=launchMission); 22 state = AboveSafeAltitude if (state = MoveTowardsTask and altitude > 500); 23 state = EmergencyAvoid if((state = AboveSafeAltitude) and (Action = alertCommanderOnSafeAltitude)); 24 … 25 end Evolution 26 end Agent

Listing 3: simplified model of BronzeCommander1_HAC1.

1 Agent BronzeCommander1_HAC1 2 3 Vars: 4 state : {MonitorVideoFeed, ManualControlRequest, ManualControl,…}; – declaration of states 5 end Vars 6 7 – Declares the possible actions for BronzeCommander1_HAC1 8 Actions = {analyzeVideoFeed, requestManualControl, takeManualControl,…}; 9 10 – A rule that descrubes what actions are possible in each local state by BronzeCommander1_HAC1 11 Protocol: 12 (state=MonitorVideoFeed) : {analyzeVideoFeed}; 13 (state=ManualControlRequest): {requestManualControl}; 14 (state=ManualControl): {takeManualControl}; 15 … 16 end Protocol 17 18 – Evolution function which describes how the local states of BronzeCommander1_HAC1 changes as a result of its current local state and actions of other agents (i.e. UAV1_HAC1) 19 Evolution: 20 state = MonitorVideoFeed if(Action = analyzeVideoFeed); 21 22 state = ManualControlRequest if(state = MonitorVideoFeed and Action = requestManualControl); 23 24 state = ManualControl if(state = ManualControlRequest and Action = takeManualControl) and !(UAV1_HAC1.Action=alertCommanderOnSafeAltitude or UAV1_HAC1.Action = alertCommanderOnIntruderDetected or UAV1_HAC1.Action = returnToBase or UAV1_HAC1.Action = landOnEmptyPublicRoad or UAV1_HAC1.Action = landOnFieldWithOverheadPowerlines or UAV1_HAC1.Action = landOnFieldWithPeople); 25 … 26 end Evolution 27 end Agent

Modelling of Ethical and Controllability Dilemmas

Having described a simplified model of the agents, in this subsection, we discuss the actual modeling performed to resolve the different dilemmas of the case study. This is using two ethical dilemmas (communication dropout – Section 5.2.1 and the technical problem resulting in a crash on humans – Section 5.2.2) and several controllability dilemmas (see Section 5.2.3).

Modelling of Communication Dropout Dilemma

• Define actions: Following the formal steps provided in Section 3.1.2 in defining an ethical dilemma situation, Listing 4 provides the different actions a UAV can take during a communication dropout state.

  Listing 4: actions for UAV1_HAC1 during a communication dropout.

  1 Actions = {waitForCommunication, collideAndDamageSelf, collideWithInfrastructure, collideWithAnimals, collideWithHumans};

• Define consequences: Listing 5 provides the consequences for a UAV during a communication dropout.

  Listing 5: consequences for UAV1_HAC1 in a communication dropout.

  1 {uavWaitsForCommunication, uavCollidesAndHarmsSelf, uavCollidesAndDamagesInfrastructure, uavCollidesAndHarmsAnimals, uavCollidesAndHarmsHumans, uavMissesHuman, humanSurvives};

• Define utilities and assign them to consequences: Listing 6 describes the utilities assigned to rank the consequences during the communication dropout of UAV1_HAC1 when the agent follows the utilitarian ethical principle. Listing 7 provides the same, if the agent follows the do-no-harm principle. In the first case, the MCMAS model checker will permit actions that correspond to the consequences that have the highest utility, while in the second case, only actions with positive or neutral consequences will be allowed. The engineer draws out utility comparisons in the model based on safety regulations/code of conduct (e.g. (UAViators. Humanitarian UAV code of conduct 2021)). When defining the values for utilities, the goal of the engineer is to judge what would pose the greatest risk depending on what the UAVs can sense and what the humans can control.

Listing 6: utilities to rank the consequences following the utilitarian principle.

1 UAV1_HAC1.uavCollidesAndHarmsHumans = −3 and UAV1_HAC1.uavCollidesAndHarmsAnimals = −2 and UAV1_HAC1.uavCollidesAndDamagesInfrastructure = −1 and UAV1_HAC1.uavWaitsForCommunication = 0 and UAV1_HAC1.uavCollidesAndHarmsSelf = 1 and UAV1_HAC1.uavMissesHuman = 2 and UAV1_HAC1.humanSurvives = 3;

Listing 7: utilities to rank the consequences following the do-no-harm principle.

1 UAV1_HAC1.uavCollidesAndHarmsHumans = −4 and UAV1_HAC1.uavCollidesAndHarmsAnimals = −3 and UAV1_HAC1.uavCollidesAndDamagesInfrastructure = −2 and UAV1_HAC1.uavCollidesAndHarmsSelf = −1 and UAV1_HAC1.uavWaitsForCommunication = 0 and UAV1_HAC1.uavMissesHuman = 1 and UAV1_HAC1.humanSurvives = 2;

• Evaluate consequences allowed: Listing 8 provides an example of an ISPL code part that evaluates utilities to determine which consequences are allowed during the communication dropout of UAV1_HAC1 (similar code exists for each choice of consequences). Note that wait for communication in our model is a wait that is beyond a reasonable time, which is risky. Therefore, according to the utilitarian principle, a UAV crashing and harming itself has been evaluated as a more moral option (i.e. less harmful to humans/society).

Listing 8: ISPL code part on evaluating utilities to determine the consequences allowed.

1 state = EvaluateDropoutConsequencesSet1 if state = CommunicationDropout and (humanSurvives ≥ uavCollidesAndHarmsHumans and humanSurvives ≥ uavCollidesAndHarmsAnimals and humanSurvives ≥ uavCollidesAndDamagesInfrastructure and humanSurvives ≥ uavWaitsForCommunication and humanSurvives ≥ uavCollidesAndHarmsSelf and humanSurvives ≥ uavMissesHuman); 2 …

• Evaluate and explain actions allowed: Listing 9 provides an example of an ISPL code part on how actions are mapped depending on the consequences allowed during the communication dropout of UAV1_HAC1. Note that similar code exists for each choice of consequences. As stated in Section 3.1.2, these actions available to an agent are known as options ($w$) or permissible actions.

Listing 9: ISPL code part on mapping of consequences to actions.

1 state = ExplainDropoutActionsSet1 if (state = EvaluateDropoutConsequencesSet1); 2 state = ExplainDropoutActionsSet2 if (state = EvaluateDropoutConsequencesSet2); 3 …

Having described the modeling of the communication dropout dilemma (D1), we now focus on a technical problem in a UAV resulting in a crash on humans ethical dilemma (D2.1).

Modelling of a Technical Problem in a UAV Resulting in a Crash on Humans Dilemma

This dilemma (D2.1) specifies a decision-making situation where a UAV is about to run out of battery, and the only actions possible are to either crash into humans in a football ground or ascend 500 feet and crash into a civilian aircraft. As in the communication dropout example, we follow the formal steps provided in Section 3.1.2 in defining an ethical dilemma.

• Define actions and consequences: Listing 10 describes the different actions a UAV can take during this dilemma, and Listing 11 provides the consequences for UAV1_HAC1 during this dilemma.

Listing 10: actions for UAV1_HAC1 during a technical problem in a UAV resulting in a crash on humans dilemma.

1 Actions = {landOnPeopleInFootballStadium, ascendAbove500Feet, collideWithSmallAircraft};

Listing 11: consequences for UAV1_HAC1 during a technical problem in a UAV resulting in a crash on humans dilemma.

1 {uavCollidesWithFootballPlayersuavCollidesAndHarmsPeopleIn- -FootballStadium, uavCollidesWithSmallAircraft};

• Define utilities and assign them to consequences: Listings 12 and 13 present the utilities defined to rank those consequences when the agent follows the utilitarian and the do-no-harm ethical principles respectively. In the utilitarian case, the MCMAS model checker will permit actions that correspond to the consequences that have the highest utility. On the contrary, in the do-no-harm case, only actions with positive or neutral consequences will be allowed.

Listing 12: utilities to rank the consequences following the utilitarian principle.

1 UAV1_HAC1.uavCollidesWithPeopleInFootballStadiumDuringBatteryLow = 1; 2 UAV1_HAC1.uavCollidesWithSmallAircraftDuringBatteryLow = 2;

Listing 13: utilities to rank the consequences following the do-no-harm principle.

1 UAV1_HAC1.uavCollidesWithPeopleInFootballStadiumDuringBatteryLow = −2; 2 UAV1_HAC1.uavCollidesWithSmallAircraftDuringBatteryLow = −1;

• Evaluate consequences allowed: Listing 14 provides an example of an ISPL code part that evaluates utilities to determine which consequences are allowed for UAV1_HAC1 during this dilemma. There is similar code for each choice of consequences.

Listing 14: ISPL code part on evaluating utilities to determine the consequences allowed.

1state = BatteryLowCrashInFootballStadium if((state = BatteryLow) and (sensorAlertCollisionWithHumans=true)); 2state = EvaluateBatteryLowCrashInFootballStadiumConsequencesSet2 if state = BatteryLowCrashInFootballStadium and (uavCollidesWithSmallAircraftDuringBatteryLow ≥ uavCollidesWithPeopleInFootballStadiumDuringBatteryLow); 3state = EvaluateBatteryLowCrashInFootballStadiumConsequencesSet1 if state = BatteryLowCrashInFootballStadium and (uavCollidesWithPeopleInFootballStadiumDuringBatteryLow ≥ uavCollidesWithSmallAircraftDuringBatteryLow);

• Evaluate and explain actions allowed: Listing 15 provides an example of an ISPL code part with respect to how actions have been mapped depending on the consequences allowed for UAV1_HAC1.

Listing 15: ISPL code part on the mapping of consequences to actions.

1 state = ExplainBatteryLowCrashInFootballStadiumActionsSet2 if (state = EvaluateBatteryLowCrashInFootballStadiumConsequencesSet2); 2 state = ExplainBatteryLowCrashInFootballStadiumActionsSet1 if (state = EvaluateBatteryLowCrashInFootballStadiumConsequencesSet1);

Modelling of Controllability Dilemmas

Here we discuss the modeling performed to resolve several key controllability dilemmas in the case study. For a description of these dilemmas, see D4 in Section 4.2.

Listing 16 presents an example of a controllability dilemma modeled (dilemma D4.1) between BronzeCommander1_HAC1 and UAV1_HAC1. It allows for the manual control of UAV1_HAC1 only if it is not in an emergency avoid or battery low state.

Similarly, in another example, Listing 17 provides controllability (dilemma D4.3) between the planning agent and BronzeCommander1_HAC1 to check the availability of the commander before planning a task for their UAV. The resolution of both these controllability dilemmas has been modeled by exploiting the evolution function of the ISPL specification in MCMAS, which we exploit to control and coordinate the execution of both human and machine agents.

Listing 16: controllability between UAV1_HAC1 and BronzeCommander1_HAC1.

1 state = ManualControlRequest if(state = MonitorVideoFeed and Action = requestManualControl); 2 state = ManualControl if(state = ManualControlRequest and Action = takeManualControl) and !(UAV1_HAC1.Action=alertCommanderOnSafeAltitude or UAV1_HAC1.Action = alertCommanderOnIntruderDetected or UAV1_HAC1.Action = returnToBase or UAV1_HAC1.Action = landOnEmptyPublicRoad or UAV1_HAC1.Action = landOnFieldWithOverheadPowerlines or UAV1_HAC1.Action = landOnFieldWithPeople);

Listing 17: controllability between PlanningAgent_HAC1 and BronzeCommander1_HAC1.

1 state=PlanRoute if (state = CheckCommanderStatus and (Action=receivePlanCommand or Action=planRoute or Action=sendPlannedRoute) and !(BronzeCommander1_HAC1.Action = takeManualControl));

Listing 18 models the controllability between an agent and the silver commander during dilemma D4.4 (crashing on humans – avoid conflict with a human’s authority). In this example, the agent requests silver commander’s authorization to crash into the site of the critical personal assets of the collective and not into the public car park.

Listing 18: controllability between UAV1_HAC1 and SilverCommander_HAC1 on crash site.

1 state = EvaluateCrashIntoCriticalPersonalAssets if ((state = MoveTowardsTask and Action=move) and (crashIntoCriticalPersonalAssets=true)); 2 state = RequestSilverCommanderAuthorizationToCrash if(state = EvaluateCrashIntoCriticalPersonalAssets and Action = requestSilverCommanderAuthorizationToCrash); 3 state = CrashIntoCriticalPersonalAssets if((state = RequestSilverCommanderAuthorizationToCrash and Action = crashIntoCriticalPersonalAssets) and SilverCommander_HAC1.Action = authorizeDecisionToCrashIntoCriticalPersonalAssets); 4 state = CrashIntoCarPark if((state = RequestSilverCommanderAuthorizationToCrash and Action = crashIntoCarPark) and SilverCommander_HAC1.Action =rejectDecisionToCrashIntoCriticalPersonalAssets);

Next, we describe an example of the modeling performed to resolve lying by a UAV (dilemma D4.5). Assume that UAV1_HAC1 requests UAV3_HAC1 to reveal its status (e.g. availability, route information) (see Listing 19). In the case study, a UAV will only reveal its status information if the requesting UAV is in flight. If the requesting UAV is on the ground, the other UAV is allowed to conceal its status as it is not in a critical state of flight. As mentioned in Section 4.2, dilemma D4.5 can also be modeled as an ethical dilemma as opposed to a controllability dilemma as described here. In such a case, however, both ethical principles – utilitarian and do-no-harm – would evaluate lying as a non-permissible action.

Listing 19: controllability between UAV1_HAC1 and UAV3_HAC1 on lying.

1 state = ProvideUAVStatus if (Action = availabilityStatus and !(UAV1_HAC1.Action = receiveLaunchCommand or UAV1_HAC1.Action = launchMission));

Property Specification on Dilemmas and Safety Concerns

Having described the modeling of two ethical dilemmas and several controllability dilemmas in the previous subsection, we now explain the formulae specified to ensure the resolution of those dilemmas in the case study. In order to better understand the different formulae, we provide the Boolean variables used in those formulae in Appendix C (see Listing 20).

Note that in the formulae specified the temporal operators $AG$, $AF$ and $AX$ for formula $\phi$ are read as: “for all paths, $\phi$ holds globally;” “for all paths, $\phi$ holds at some point in the future” and “for all paths, in the next state $\phi$ holds” respectively. Meanwhile, $K$ is an epistemic operator which can be used to express the knowledge of an agent, and $GCK$ is used to express common knowledge in a group of agents.

Property Specification on Ethical and Controllability Dilemmas

During a communication dropout of a UAV, we assume the following controllability behavior between humans and agents: (i) the silver commander stops other UAVs in flight; (ii) the other UAVs will move into standby mode waiting for instruction; (iii) the silver commander issues a replanning request for other UAVs. The other UAVs will allow the replanning request only if they are not in an emergency avoid or battery low state; (iv) the planning agent, which is called by a silver commander, will only plan a task for the other UAVs if those UAVs are not in a manual control state (i.e. its bronze commander is not in a busy state). As mentioned in Section 3.1.3, by controllability we mean meaningful control between humans and agents so authority can be shared and assigned to facilitate collective and responsible decisions.

We have specified several properties to ensure the resolution of the communication dropout ethical dilemma (D1), and controllability behavior between humans and agents. First, formula 1 has been specified to ensure that if UAV1_HAC1 has a communication dropout then the silver commander should stop UAV2_HAC1. Then, formula 2 ensures that when the command to stop UAV2_HAC1 is issued, UAV2_HAC1 needs to move to a standby mode in the immediate next state, and a replanning request needs to be performed. The silver commander will be allowed to replan and edit the task manually or automatically by invoking the planning agent only if UAV2_HAC1 is not under an emergency avoid or battery low state (see formulae 3 and 4 for dilemma D4.2). Formulae 5–8 have been provided to ensure controllability (dilemma D4.3) between the planning agent and BronzeCommander2_HAC1, that is, to check whether UAV2_HAC1 is under manual control by BronzeCommander2_HAC1. If not, replanning is performed by the planning agent and the UAV2_HAC1 can move toward the new task.

(1) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}CommunicationDropout\to \text{break}AX(SC\mathrm{\_}HAC1\mathrm{\_}CommandToStopUAVs));$(1)

(2) $AG(SC\mathrm{\_}HAC1\mathrm{\_}CommandToStopUAVs\to \text{break}AX(UAV2\mathrm{\_}HAC1\mathrm{\_}StandbyandSC\mathrm{\_}HAC1\mathrm{\_}ReplanRoutesRequest));$(2)

(3) $AG(SC\mathrm{\_}HAC1\mathrm{\_}ReplanRoutesRequest\to \text{break}AX(SC\mathrm{\_}HAC1\mathrm{\_}ReplanRoutesRequestAllowed));$(3)

(4) $AG(SC\mathrm{\_}HAC1\mathrm{\_}ReplanRoutesRequestAllowed\to \text{break}AX(SC\mathrm{\_}HAC1\mathrm{\_}ReplanRoutes));$(4)

(5) $AG(SC\mathrm{\_}HAC1\mathrm{\_}ReplanRoutes\to \text{break}AX(PA\mathrm{\_}HAC1\mathrm{\_}CheckCommanderStatus));$(5)

(6) $AG(PA\mathrm{\_}HAC1\mathrm{\_}CheckCommanderStatus\to \text{break}AX(PA\mathrm{\_}HAC1\mathrm{\_}PlanRouteAllowed));$(6)

(7) $AG(PA\mathrm{\_}HAC1\mathrm{\_}PlanRouteAllowed\to \text{break}AX(PA\mathrm{\_}HAC1\mathrm{\_}PlanRoute));$(7)

(8) $AG(PA\mathrm{\_}HAC1\mathrm{\_}PlanRoute\to \text{break}AX(UAV2\mathrm{\_}HAC1\mathrm{\_}MoveTowardsTask));$(8)

Formula 9 is an example of a property that has been specified for the communication dropout dilemma. This is to ensure the correct mapping of consequences to permissible actions (see corresponding Listing 9). Note that similar formulae have been specified to ensure the correct mapping of other choices of consequences to their corresponding permissible actions.

(9) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}EvaluateDropoutConsequencesSet1\to \text{break}AX(UAV1\mathrm{\_}HAC1\mathrm{\_}ExplainDropoutActionsSet1));$(9)

Similarly, formula 10 is an example property specified to ensure the correct mapping of consequences to permissible actions (see corresponding Listing 15) for the technical problem in a UAV resulting in a crash on humans ethical dilemma. We have specified similar formulae to ensure the correct mapping of other choices of consequences to their corresponding permissible actions.

(10) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}EvaluateBatteryLowCrashInFootballStadiumConsequencesSet1\to AX(UAV1\mathrm{\_}HAC1\mathrm{\_}ExplainBatteryLowCrashInFootballStadiumActionsSet1));$(10)

Formulae 11–12 are specified to handle the manual control dilemma D4.1 modeled in Listing 16, which are controllability constraints between humans and agents. These ensure that the manual control of UAV1_HAC1 by BronzeCommander1_HAC1 is only allowed if the UAV is not in an emergency avoid or battery low state.

(11) $AG(BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlRequest\to \text{break}AX(BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlAllowed));$(11)

(12) $AG(BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlAllowed\to \text{break}AX(BC1\mathrm{\_}HAC1\mathrm{\_}ManualControl));$(12)

Formulae 13–16 are specified to verify dilemma D4.4 (crashing into critical personal assets of the collective) modeled in Listing 18, which are controllability constraints between the silver commander and the UAV. This verifies whether human’s authority is provided first for the agent to allow it to crash into the critical personal assets of the collective. If the silver commander’s authorization is not received, then the UAV needs to crash into the public car park.

(13) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}EvaluateCrashIntoCriticalPersonalAssets\to \text{break}AX(UAV1\mathrm{\_}HAC1\mathrm{\_}RequestSilverCommanderAuthorizationToCrash));$(13)

(14) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}RequestSilverCommanderAuthorizationToCrash\to \text{break}AX(SC\mathrm{\_}HAC1\mathrm{\_}AuthorizeDecisionToCrashIntoCriticalPersonalAssetsor\text{break}SC\mathrm{\_}HAC1\mathrm{\_}RejectDecisionToCrashIntoCriticalPersonalAssets));$(14)

(15) $AG(SC\mathrm{\_}HAC1\mathrm{\_}AuthorizeDecisionToCrashIntoCriticalPersonalAssets\to \text{break}AX(UAV1\mathrm{\_}HAC1\mathrm{\_}CrashCrashIntoCriticalPersonalAssets));$(15)

(16) $AG(SC\mathrm{\_}HAC1\mathrm{\_}RejectDecisionToCrashIntoCriticalPersonalAssets\to \text{break}AX(UAV1\mathrm{\_}HAC1\mathrm{\_}CrashIntoCarPark));$(16)

Formula 17 has been specified to handle the self-certification dilemma (D4.5) modeled in Listing 19, which has been specified as a controllability constraint on two UAVs. In this example, this verifies whether UAV3_HAC2 provides its status to UAV1_HAC1 (without self-concealment), if UAV1_HAC1 is in flight.

(17) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}RequestUAVStatus\to \text{break}AX(UAV3\mathrm{\_}HAC2\mathrm{\_}ProvideUAVStatus));$(17)

Property Specification on Safety Concerns

In addition to the ethical and controllability properties discussed previously, we specify formulae to ensure the general safety of the model so nothing bad happens, as well as epistemic properties and fairness constraints, as described below.

To this end, formulae 18 and 19 specify that after the corresponding launch or land command is issued by the silver commander, the UAVs need to launch or land respectively, sometime in the future.

(18) $AG(SC\mathrm{\_}HAC1\mathrm{\_}CommandToLaunch\to \text{break}AF(UAV1\mathrm{\_}HAC1\mathrm{\_}Launch)and(UAV2\mathrm{\_}HAC1\mathrm{\_}Launch));$(18)

(19) $AG(SC\mathrm{\_}HAC1\mathrm{\_}CommandToLand\to \text{break}AF(UAV1\mathrm{\_}HAC1\mathrm{\_}Land)and(UAV2\mathrm{\_}HAC1\mathrm{\_}Land));$(19)

Formula 20 specifies a safety requirement that needs to be enforced when the environment is risky, that is, if (i) the wind strength is adverse; (ii) there is presence of heavy rain; or (iii) the ground visibility is low. In such a situation, UAVs should not be allowed for launch by the silver commander and they need to remain on ground until the risk level subsides.

(20) $AG(Env\mathrm{\_}PreFlightRisky\to \text{break}AX(UAVs\mathrm{\_}HAC1\mathrm{\_}OnGround));$(20)

Formula 21 performs a safety check during the pre-flight stage. It verifies whether there is any route conflict between the UAVs, that is, whether their positions – longitude, latitude, altitude – overlap or not. If there is such an overlap, this property ensures that the environment agent notifies the silver commander about the conflict immediately in the next state.

(21) $AG(UAV1\mathrm{\_}UAV2\mathrm{\_}HAC1\mathrm{\_}RoutesConflict\to \text{break}AX(Env\mathrm{\_}RouteConflict));$(21)

Formula 22 specifies a safety property to ensure during the pre-flight stage: if the route of a UAV is in a no-fly zone then the silver commander needs to be notified immediately. Formula 23 ensures the same outcome when a UAV enters a no-fly zone during flight.

(22) $AG((UAV1\mathrm{\_}HAC1\mathrm{\_}NoFlyZoneAtRouteor\text{break}UAV2\mathrm{\_}HAC1\mathrm{\_}NoFlyZoneAtRoute)\to \text{break}AX(Env\mathrm{\_}NoFlyZoneAtRoute))$(22)

(23) $AG((UAV1\mathrm{\_}HAC1\mathrm{\_}NoFlyZoneEntryor\text{break}UAV2\mathrm{\_}HAC1\mathrm{\_}NoFlyZoneEntry)\to \text{break}AX(Env\mathrm{\_}NoFlyZoneEntry));$(23)

Formula 24 specifies a safety property that if the UAV1_HAC1 detects an intruder or if it is above the safe flying altitude, it should invoke its emergency avoid behavior immediately in the next state, which contains behavior to mitigate the emergency situation.

(24) $AG(UAV1\mathrm{\_}HAC1\mathrm{\_}IntruderAboveSafeAlt\to \text{break}AX(UAV1\mathrm{\_}HAC1\mathrm{\_}EmergencyAvoid));$(24)

Formulae 25 and 26 provide examples of epistemic properties defined in the specification at the agent and human-agent collective levels respectively. As stated in Section 2.4, epistemic operators are used to reason about what agents know (e.g. knowledge of an agent or common knowledge of a group of agents). Formula 25 states that it is always true that when a UAV is in an emergency avoid state, then the bronze commander knows that the manual control of that UAV cannot be requested. Meanwhile, formula 26 is much stronger and it specifies that when a UAV is in an emergency avoid state, it is common knowledge in the group $multiUAVHumanAgentCollective$ that the bronze commander cannot request manual control of their UAV.

(25) $AG(BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlRequest\to \text{break}K(BronzeCommander1\mathrm{\_}HAC1,BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlAllowed));$(25)

(26) $AG(BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlRequest\to \text{break}GCK(multiUAVHumanAgentCollective,BC1\mathrm{\_}HAC1\mathrm{\_}ManualControlAllowed));$(26)

Two fairness conditions have been specified (see formulae in 27), so UAV 1 and UAV 2 cannot avoid their move toward task states forever. In this example, it is required that the propositions UAV1_HAC1_MoveTowardsTask and UAV2_HAC1_MoveTowardsTask (see Appendix A) are true infinitely often. As mentioned in Section 2.4, fairness conditions are specified to rule out unwanted behavior or to avoid a particular state forever.

(27) $UAV1\mathrm{\_}HAC1\mathrm{\_}MoveTowardsTask;\text{break}UAV2\mathrm{\_}HAC1\mathrm{\_}MoveTowardsTask;$(27)

Having described the modeling and specification of different dilemmas in the case study, we now provide their actual verification and simulation results using the MCMAS tool.

Verification and Simulation Results of Ethical and Controllability Dilemmas

The verification of the human-agent collective with ethical dilemma situations against the constraints specified on safety, controllability and ethical behavior can result in counterexample traces on any property violations. Figure 5 shows the results of verification using MCMAS in the command line. In general, in model checking, a counterexample trace is used to identify and track any errors in the model. As an additional step, our study uses a counterexample trace as a judgment that can be explored by the engineer to identify the reasons why any actions for an agent are non-permissible in the human-agent collective. MCMAS allows the analysis of counterexamples as a directed graph showing the execution of states and their descriptions (e.g. see Figure 6). There temporal transitions are represented by a black arrow labeled with the joint action performed (Figure 6). These can be explored by the engineer to identify errors and their sources (e.g. properties) in the specification. In Figure 6, the engineer can identify that the formula SC_HAC1_AuthorizeDecisionToCrashIntoCriticalPersonalAssets has been violated, and then by observing the states, the reason for the violation can be determined. As stated in Section 5.3.1, this formula specifies that the silver commander’s authorization is provided first in order to allow the agent to crash into the critical personal assets of the collective. Here, in the model, the silver commander has rejected the authorization to crash, which resulted in the violation of the formula during verification.

Figure 5. Example of verification results of formulae for case study in the command line.

Figure 6. Counterexample for violation of formula on silver commander authorisation for crash into critical personal assets.

Explainable AI: Simulating Explainable Models of Dilemmas

We simulate the ethical and controllability dilemma situations in MCMAS in order to show and explain the actions permissible for an agent in a step-by-step manner. This study provides a step toward supporting explainable AI by communicating decisions and the choices the agents have to make based on (i) the ethical principles; and (ii) controllability between humans and agents. Ethical principles are usually formulated in an action-based manner in order to judge the execution of an action (Lindner, Mattmüller, and Nebel 2019, 2020). The use of ethical principles opens the possibility to communicate decisions to the user, who in our work is the AI engineer. The explanation describes to the AI engineer the actions that are allowed and refused. The explanation can explicitly refer to any ethical principles or controllability constraints that have been applied. It can also provide the reasons why a certain action is preferred over another.

The structure of the explanation provided by an agent depends on the type of dilemma (Figure 3). During an ethical dilemma, the explanation by the agent has following elements:

1. actions permissible;

2. actions non-permissible;

3. reasons for non-permissibility of actions;

4. any ethical principle applied.

For example, an explanation when resolving the dilemma D2.1 (technical problem in a UAV resulting in a crash on humans) will contain:

Table

Permissible actions—collideWithSmallAircraft; Non-permissible actions—landOnPeopleInFootballStadium; Justification—morally significant action selected based on ethical principle; Ethical principle applied—Utilitarian (see simulation result in Figure 7)

Figure 7. Explainable simulated models when resolving dilemma 2.1 for UAV1_HAC1—technical problem in a UAV resulting in a crash on humans.

In a controllability dilemma, the explanation describes the reason why an action is non-permissible. For example, in the dilemma D4.1 (request for manual control), the explanation will state:

Table

Request for manual control of UAV has been rejected—UAV is under emergency avoid state.

Table 2 summarizes the judgments provided with permissible and non-permissible actions during the communication dropout dilemma (D1), and technical problem in a UAV resulting in a crash on humans dilemma (D2.1). In this manner, by using the results from counterexamples and interactive simulation, the engineer can get an understanding of how the actions have been judged. The results can be used to improve and refine the design of the model iteratively and build a specification that is correct.

Table 2. Judgments summarized during communication dropout and battery row resulting in crash on humans dilemmas.

Dilemma	Ethical Principle	Permissible Actions	Non-permissible Actions
D1: Communication Dropout	Utilitarian	collideAndDamageSelf	collideWithHumans,
			collideWithAnimals,
			collideWithInfrastructure,
			collideWithOtherUAV,
			waitForCommunication
D1: Communication Dropout	Do-no-harm	waitForCommunication	collideWithHumans,
			collideWithAnimals,
			collideWithInfrastructure,
			collideWithOtherUAV,
			collideAndDamageSelf
D2.1: Battery Low - Crash on Humans	Utilitarian	collideWithSmallAircraft,	landOnPeopleInFootballStadiumn
		ascendAbove500Feet
D2.1: Battery Low – Crash on Humans	Do-no-harm	ascendAbove500Feet	landOnPeopleInFootballStadiumn,
			collideWithSmallAircraft

Discussion

In this section, we provide a brief a discussion of the results with some limitations of this work.

Generality of the Proposed Methodology to Handle Uncertainty: This work follows an ethics-by-design approach proposed by Cointe, Bonnet, and Boissier (2016) where an ethical agent is designed by a priori analysis of all possible situations it may encounter, and implementing, for each situation, a way to avoid potential unethical behaviors. The consequences and actions of agents are known a priori, and the utilities are prescribed and determined at design time. We defined two ethical principles that follow a consequentialist approach: utilitarian and do-no-harm. An alternative solution to ours would be when the consequences of agents are not known a priori.

In such cases, model-based reinforcement learning algorithms could be applied but further research is needed to investigate how model checking can be used to verify various dilemmas at runtime. At present MCMAS does not support any verification of machine learning models, although there are initial tools built to support verification of neural networks (Akintunde et al. 2019), parameterized (Kouvaros and Lomuscio 2016) and open multi-agent systems (Kouvaros et al. 2019).

Other paradigms that can be used to complement our approach include: (i) extending game-theoretic concepts to incorporate ethical aspects; and (ii) applying machine learning techniques to moral dilemmas. The first approach is an extension to the extensive form, which is one of the standard representation schemes in game theory (Conitzer et al. 2017). The second approach proposes to apply machine learning techniques which can learn to classify actions as morally correct or wrong (Conitzer et al. 2017). These are proposed to be applied on a labeled dataset of moral dilemmas represented as feature values. Although a machine learning-based approach is more flexible than a game-theoretic approach, both approaches complement each other. One can use game-theoretic analysis of ethics as a feature to train machine learning approaches. On the other hand, the outcome of a machine learning approach can help to identify which moral aspects are missing from moral game theoretic concepts (Conitzer et al. 2017).

State Explosion Problem: Model checking is automated, simpler to apply and describe finite state models. However, one of the main limitations of model checking is the state explosion problem, which means the number of states of the model growing exponentially with the number of variables (Clarke et al. 2012). The model created for the case study scenario has 11 agents (see Listing 1) and 31 formulae. During verification using MCMAS, the number of reachable states reached 7.0072e + 38 which demonstrates the scalability of our model. Also, the execution time of the model was only 9.521 seconds. This is in contrast to other model checkers like SMV and Spin which can take relatively longer time to execute (Choi, Kim, and Tsourdos 2015).

Human Bias when Specifying Values for Utilities: In this paper, utilities have been used to encode agents with the moral values aligned to humans. As a human decides on the values of these utilities, this process can be biased. However, in our work, an engineer would only draw out utility comparisons in the model based on code of conduct or safety regulations formalized in the domain of application (e.g (UAViators 2021). in UAVs). Hence, we try to remove the risk of introducing human bias on the part of the AI engineer. Our approach of using utility comparisons to handle ethical dilemmas has also been explored by other authors (e.g. (Lindner, Mattmüller, and Nebel 2019, 2020)).

Instantaneous Observability of Agent Actions: As stated in Section 5.1, in ISPL all actions of an agent are publicly observable. This is to support interaction between agents and the environment. This feature of public observability of actions is used in the evolution function, which allows the local states of agents to evolve based on their current local state and on other agents’ actions. This poses an important question – how realistic is it to assume that the other agents’ actions are instantaneously observable in a multi-agent system? However, in this paper, we only exploit this publicly observable feature of actions selectively when we need to control and coordinate the execution of agent states of different agents.

Lack of a Strong Metric to Evaluate Dilemma Resolution: In this work, the AI engineer is the user of the system and he/she is also the person who judges whether the resolution of dilemmas has been correctly performed by the model. This is done by visually analyzing the simulation results and verification results such as counterexamples, using the MCMAS tool. However, this may not be the best solution, and instead there is a need to identify a strong metric.

Explanations in Natural Language: In our work, we exploited the step-by-step interactive simulation of the human-agent collectives to show and explain the actions allowed by an agent when having to resolve a dilemma. However, these explanations will be more useful to end users, if they answer the why-questions in natural language instead of embedding the explanations in the simulation steps.

Conclusion and Future Work

In this work, we proposed a novel engineering methodology based on model checking as a step toward the certification of responsible and explainable decision making within human-agent collectives. The key challenge that we have tried to resolve in human-agent collectives is dilemmas. We have shown how our approach, which is based on the MCMAS model checker, can be used to verify the decision-making behavior against the logical formulae specified to guarantee safety, controllability and address ethical concerns. The counterexample traces and the simulation results were used to provide a judgment, and an explanation to the AI engineer. We evaluated the approach using the real-world problem of human-UAV teaming in dynamic and uncertain environments. This work extended it with dilemma situations that both humans and agents may encounter.

In order to exploit the full potential of this work, there remain several open issues that need to be resolved, and some of them are highlighted below.

Encoding Ethical Behaviour in Agents: In this work, out of the three possible approaches (i.e. consequentialist, virtue-based and deontological) we have explored a consequentialist approach to encode ethical behavior in agents of a collective (Section 3.1.1). A consequentialist approach weighs the morality of the consequences of each choice as opposed to values like wisdom (virtue ethics) or obligations and permissions (deontological approach) (Cointe, Bonnet, and Boissier 2016). So an interesting future direction is to investigate how we could support a virtue-based or a deontological approach. As such, our work can benefit from exploring all three ethical behavior encoding techniques. A virtue-based approach is possible, for example: a list of state-action pairs could be created in which a human determines whether that action is virtuous (e.g. brave) in that state. A deontological approach could be adopted by maintaining a list of actions that are permissible or required in a given state. Furthermore, to simplify modeling, we have assumed that each action has one consequence. Although individual actions of an agent usually have multiple consequences, the dilemmas posed by our scenarios can be modeled with one-action-one-consequence. Also, MCMAS, while having useful features, currently allows only one consequence per action (Boolean, enumeration, integer variables only). We will look to expand the approach to consider more complex consequences in future work.

Grounding in Real-World Human-UAV Interactions: This work proposed a step-by-step methodology to engineer responsible and explainable models in human-agent collectives at design time. Here, the decision-making situations an agent may encounter are known a priori, and the dilemmas have been resolved in a way as to ensure responsible and explainable behavior by both humans and agents. Future studies should investigate how our method can be grounded in a real-world UAV-human interaction, and how the resolving of dilemmas can be tested with users.

Providing strong Metrics and Explanations in Natural Language: Further research is needed to identify strong metrics which can be used to check whether a dilemma has been correctly resolved. Also, future work needs to investigate how the different agent actions in the simulation can be translated into natural language (e.g. see (Koeman et al. 2020)).

Acknowledgements

The authors would like to thank Prof. Alessio Lomuscio, Imperial College London, for informal discussions on the MCMAS tool. The work presented in this paper was supported by the AXA Research Fund, and the UK Engineering and Physical Sciences Research Council (EPSRC)-funded Smart Cities Platform under the grant [EP/P010164/1]. D.A. is also supported by the UKRI Trustworthy Autonomous Systems Node in Functionality under Grant EP/V026518/1. For the purpose of open access, the author(s) has applied a Creative Commons Attribution (CC BY) licence to any Author Accepted Manuscript version arising from this submission.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Supplementary material

Supplemental data for this article can be accessed online at https://doi.org/10.1080/08839514.2023.2282834

Additional information

Funding

This work was supported by the AXA Research Fund; Smart Cities Platform [EP/P010164/1]; UKRI Trustworthy Autonomous Systems Node in Functionality [EP/V026518/1].

Notes

1. Emergency response teams organize themselves into bronze, silver and gold levels. Bronze and silver represent the operational and tactical decision-making levels respectively and these are the only levels we need to consider for the purpose of this paper.

Appendix A.

Here we provide definitions of the different terms used in this work (see Table A1).

Table A1. Definitions used in this work.

Term	Definition used
Explainability/Interpretability	“Generating decisions in which one of the criteria taken into account during the computation is how well a human could understand the decisions in the given context” (Miller 2019).
Accountability	“Degree to which the actions of an entity can be traced uniquely to the entity” (Standardization, International Organization for 2017).
Responsible AI	There are three main principles that can be used by AI systems to support social good: accountability, responsibility and transparency (ART) (Dignum 2017). The ART principles form the main pillars of responsible AI. Meanwhile, responsibility refers both to the capability of AI systems and to the role of people interacting with them (Dignum et al. 2018).
Transparency	“Transparency can be defined as the extent to which the system discloses the processes or parameters that relate to its functioning” (Winfield et al. 2021).
Fairness	Fairness conditions are used to rule out behaviors allowed by the model but not achievable in practice. According to (Leslie 2019), “designers and implementers are held accountable for being equitable and for not harming anyone through bias or discrimination.”
Safety	“Expectation that a system does not, under defined conditions, lead to a state in which human life, health, property, or the environment is endangered” (Standardization, International Organization for 2017).
Controllable	Controllability means meaningful control between humans and agents for collective decisions for responsible AI (Ramchurn et al. 2016; Ramchurn, Stein, and Jennings 2021)
Ethics	AI ethics is “a set of values, principles, and techniques that employ widely accepted standards of right and wrong to guide moral conduct in the development and use of AI technologies” (Leslie 2019).
Trustworthy	AS are considered trustworthy when the design, engineering, and operation of these systems generate positive outcomes and mitigate outcomes which can be harmful (Naiseh, Bentley, and Ramchurn 2022). The trustworthiness of AS can be dependent on many factors, such as: (i) explainability, accountability and understandability to different users; (ii) robustness of AS in dynamic and uncertain environments; (iii) assurance of their design and operation; (iv) confidence in their ability to adapt their functionality; (v) security against attacks on the systems, users and deployed environment; (vi) governance and regulation of their design and operation; and (vii) consideration of ethics and human values during deployment and use (Naiseh, Bentley, and Ramchurn 2022).

Appendix B.

In the following, we describe the human and machine agents modeled in the case study using ISPL (see Table A2), and their local states (see Table A3).

Table A2. Descriptions of the human and machine agents modeled using ISPL in the case study.

Agent Name	Agent Description
UAV1_HAC1	UAV 1 in human-agent collective 1
UAV2_HAC1	UAV 2 in human-agent collective 1
BronzeCommander1_HAC1	Bronze commander 1 in human-agent collective 1
BronzeCommander2_HAC1	Bronze commander 2 in human-agent collective 1
SilverCommander_HAC1	Silver commander in human-agent collective 1
PlanningAgent_HAC1	Planning agent in human-agent collective 1
UAV3_HAC2	UAV 3 in human-agent collective 2
BronzeCommander_HAC2	Bronze commander in human-agent collective 2
SilverCommander_HAC2	Silver commander in human-agent collective 2
PlanningAgent_HAC2	Planning agent in human-agent collective 2
Environment	Environment agent shared by all human and machine agents in the collectives

Table A3. Descriptions of local states of the agents in the case study.

Agent Name	State Name	State Description
UAV	OnGround	UAV is on the ground
	MoveTowardsTask	UAV moves toward its task
	Land	UAV lands
	Standby	UAV waits for instruction from the server
	IntruderDetected	UAV detects an intruder (malicious or non-malicious) through its sensors
	AboveSafeAltitude	UAV is above a safe altitude of 500 feet
	EmergencyAvoid	UAV is in an emergency state – it detects an intruder or it is at an above safe altitude
	CommunicationDropout	UAV loses contact with the server for a prolonged time (relates to dilemma D1)
	EvaluateDropoutConsequencesSet1	An example state that evaluates utilities to determine which consequences are allowed during a communication dropout of a UAV (relates to dilemma D1)
	ExplainDropoutActionsSet1	An example state that explains the allowed actions during a communication dropout of a UAV (relates to dilemma D1)
	BatteryLow	UAV’s battery level is below the safe threshold level
	BatteryLowCrashInFootballStadium	UAV evaluates whether to crash into a football stadium below or into a civilian aircraft flying above (relates to dilemma D2.1)
	EvaluateBatteryLowCrashInFootballStadiumConsequencesSet1	An example state that evaluates utilities to determine which consequences are allowed when resolving the “technical problem in a UAV resulting in a crash on humans” dilemma (relates to dilemma D2.1)
	ExplainBatteryLowCrashInFootballStadiumActionsSet1	An example state that explains the permissible actions when resolving the “technical problem in a UAV resulting in a crash on humans dilemma” (relates to dilemma D2.1)
	EvaluateCrashIntoCriticalPersonalAssets	UAV evaluates whether to crash into the critical personal assets of the collective or a public car park (relates to dilemma D4.4)
	RequestSilverCommanderAuthorizationToCrash	UAV requests authorization from the silver commander to crash into the critical personal assets of the human-UAV collectives (relates to dilemma D4.4)
	CrashIntoCriticalPersonalAssets	UAV crashes into the critical personal assets of the collectives (relates to dilemma D4.4)
	CrashIntoCarPark	UAV crashes into the public car park, as silver commander does not authorize to crash into the critical personal assets of the collectives (relates to dilemma D4.4)
	RequestUAVStatus	UAV requests another UAV to inform its status (availability or route information). This relates to dilemma D4.5
	ProvideUAVStatus	UAV provides the requesting UAV its status information (availability or route information). This relates to dilemma D4.5
Silver Commander	CommandToLaunch	Silver commander issues a command to launch the UAVs
	CommandToLand	Silver commander issues a command to land the UAVs
	CommandToStopUAVs	Silver commander issues a command to stop the UAVs in flight and wait for instruction (UAVs move into standby state)
	ReplanRoutesRequest	Silver commander before replanning a route for a UAV, checks whether the UAV is in a battery low or emergency avoid state (relates to dilemma D4.2)
	PlanRoutes	Silver commander plans routes either manually or using a planning agent
	ReplanRoutes	Silver commander re-plans route for a UAV by invoking the planning agent
	AuthorizeDecisionToCrashIntoCriticalPersonalAssets	Silver commander authorizes the UAV to crash into the critical personal assets of the collectives (relates to dilemma D4.4)
	RejectDecisionToCrashIntoCriticalPersonalAssets	Silver commander rejects the UAV’s request to crash into the critical personal assets of the collectives (relates to dilemma D4.4)
Bronze Commander	MonitorVideoFeed	Bronze commander monitors video feed of his/her UAV
	ManualControl	Bronze commander takes manual control of his/her UAV
	ManualControlRequest	Bronze commander requests manual control for his/her UAV
Planning Agent	CheckCommanderStatus	Planning agent checks whether the commander is engaged in some important task (e.g. bronze commander taking manual control of his/her UAV), before calling its plan routes function (related to dilemma D4.3)
	PlanRoute	Planning agent plans a route for a UAV (related to dilemma D4.3)
Environment	PreFlightRisky	Environment agent detects that the risk level of the flight is high for a UAV, which can be due to high wind strength/heavy rain/low visibility. Then it notifies the silver commander
	RouteConflict	Environment agent detects a route conflict between the UAVs, and then notifies the silver commander
	NoFlyZoneAtRoute	Environment agent detects that the route of a UAV crosses into a no-fly zone, and then notifies the silver commander
	NoFlyZoneEntryDuringFlight	Environment agent detects that a UAV is crossing into a no-fly zone during flight, and then informs the silver commander

Appendix C.

Listing 20 provides Boolean variables declared in the different formulae described in this article. These variables have been declared in the evaluation part of ISPL.

Listing 20: Boolean variables used in formulae provided section 5.3.

1 ———-Used in Dilemma D1 - Communication Dropout———-

2 UAV1_HAC1_CommunicationDropout if(UAV1_HAC1.state = CommunicationDropout);

3 SC_HAC1_CommandToStopUAVs if(SilverCommander_HAC1.state = CommandToStopUAVs);

4 UAV2_HAC1_Standby if(UAV2_HAC1.state = Standby);

5 SC_HAC1_ReplanRoutesRequest if(SilverCommander_HAC1.state = ReplanRoutesRequest);

6 SC_HAC1_ReplanRoutesRequestAllowed if(SilverCommander_HAC1.state = ReplanRoutesRequest) and !(UAV2_HAC1.state=EmergencyAvoid or UAV2_HAC1.state=BatteryLow);

7 SC_HAC1_ReplanRoutes if(SilverCommander_HAC1.state = ReplanRoutes);

8 PA_HAC1_CheckCommanderStatus if(PlanningAgent_HAC1.state = CheckCommanderStatus);

9 PA_HAC1_PlanRouteAllowed if(PlanningAgent_HAC1.state = CheckCommanderStatus and !(BronzeCommander2_HAC1.state = ManualControl));

10 PA_HAC1_PlanRoute if(PlanningAgent_HAC1.state = PlanRoute);

11 UAV1_HAC1_MoveTowardsTask if(UAV1_HAC1.state = MoveTowardsTask);

12 UAV2_HAC1_MoveTowardsTask if(UAV2_HAC1.state = MoveTowardsTask);

13

14 UAV1_HAC1_EvaluateDropoutConsequencesSet1 if (UAV1_HAC1.state = EvaluateDropoutConsequencesSet1);

15 UAV1_HAC1_ExplainDropoutActionsSet1 if(UAV1_HAC1.state = ExplainDropoutActionsSet1);

16

17 –Used in Dilemma D2.1 - Battery Low Resulting in Crash on Humans—

18 UAV1_HAC1_EvaluateBatteryLowCrashInFootballStadiumConsequencesSet1 if(UAV1_HAC1.state = EvaluateBatteryLowCrashInFootballStadiumConsequencesSet1);

19 UAV1_HAC1_ExplainBatteryLowCrashInFootballStadiumActionsSet1 if(UAV1_HAC1.state = ExplainBatteryLowCrashInFootballStadiumActionsSet1);

20 UAV1_HAC1_EvaluateBatteryLowCrashInFootballStadiumConsequencesSet2 if(UAV1_HAC1.state = EvaluateBatteryLowCrashInFootballStadiumConsequencesSet2);

21 UAV1_HAC1_ExplainBatteryLowCrashInFootballStadiumActionsSet2 if(UAV1_HAC1.state = ExplainBatteryLowCrashInFootballStadiumActionsSet2);

22

23 ———-Used in Controllability Dilemmas———-

24 BC1_HAC1_ManualControlRequest if(BronzeCommander1_HAC1.state = ManualControlRequest);

25 BC1_HAC1_ManualControlAllowed if(BronzeCommander1_HAC1.state = ManualControlRequest and !(UAV1_HAC1.state = EmergencyAvoid or UAV1_HAC1.state=BatteryLow));

26 BC1_HAC1_ManualControl if(BronzeCommander1_HAC1.state = ManualControlAllowed);

27

28 UAV1_HAC1_EvaluateCrashIntoCriticalPersonalAssets if (UAV1_HAC1.state = EvaluateCrashIntoCriticalPersonalAssets);

29 UAV1_HAC1_RequestSilverCommanderAuthorizationToCrash if (UAV1_HAC1.state = RequestSilverCommanderAuthorizationToCrash);

30 SC_HAC1_AuthorizeDecisionToCrashIntoCriticalPersonalAssets if (SilverCommander_HAC1.state = AuthorizeDecisionToCrashIntoCriticalPersonalAssets);

31 SC_HAC1_RejectDecisionToCrashIntoCriticalPersonalAssets if (SilverCommander_HAC1.state = RejectDecisionToCrashIntoCriticalPersonalAssets);

32 UAV1_HAC1_CrashIntoCriticalPersonalAssets if (UAV1_HAC1.state = CrashIntoCriticalPersonalAssets);

33 UAV1_HAC1_CrashIntoCarPark if (UAV1_HAC1.state = CrashIntoCarPark);

34

35 UAV1_HAC1_RequestUAVStatus if (UAV1_HAC1.state = RequestUAVStatus);

36 UAV3_HAC2_ProvideUAVStatus if (UAV3_HAC2.state = ProvideUAVStatus);

37

38 ———-Used in Safety Properties———-

39 —(Environment Agent)—

40 Env_PreFlightRisky if(Environment.state = PreFlightRisky);

41 Env_RouteConflict if(Environment.state = RouteConflict);

42 Env_NoFlyZoneAtRoute if(Environment.state = NoFlyZoneAtRoute);

43 Env_NoFlyZoneEntry if(Environment.state = NoFlyZoneEntryDuringFlight);

44 —(Silver Commander in HAC1)—

45 SC_HAC1_CommandToLaunch if(SilverCommander_HAC1.state = CommandToLaunch);

46 SC_HAC1_CommandToLand if(SilverCommander_HAC1.state = CommandToLand);

47 SC_HAC1_PlanRoutes if(SilverCommander_HAC1.state = PlanRoutes);

48 —(UAV1 and UAV2 in HAC1)—

49 UAV1_HAC1_Launch if(UAV1_HAC1.state = OnGround);

50 UAV2_HAC1_Launch if(UAV2_HAC1.state = OnGround);

51 UAV1_UAV2_HAC1_RoutesConflict if(UAV1_HAC1.routeLatitude = UAV2_HAC1.routeLatitude and UAV1_HAC1.routeLongitude = UAV2_HAC1.routeLongitude and UAV1_HAC1.altitude = UAV2_HAC1.altitude and UAV1_HAC1.routeTime = UAV2_HAC1.routeTime);

52 UAV1_HAC1_NoFlyZoneAtRoute if(UAV1_HAC1.routeLongitude = Environment.noFlyZoneLongitude and UAV1_HAC1.routeLatitude = Environment.noFlyZoneLatitude);

53 UAV2_HAC1_NoFlyZoneAtRoute if(UAV2_HAC1.routeLongitude = Environment.noFlyZoneLongitude and UAV2_HAC1.routeLatitude = Environment.noFlyZoneLatitude);

54 UAV1_HAC1_NoFlyZoneEntry if(UAV1_HAC1.currentLongitude = Environment.noFlyZoneLongitude and UAV1_HAC1.currentLatitude = Environment.noFlyZoneLatitude);

55 UAV2_HAC1_NoFlyZoneEntry if(UAV2_HAC1.currentLongitude = Environment.noFlyZoneLongitude and UAV2_HAC1.currentLatitude = Environment.noFlyZoneLatitude);

56 UAV1_HAC1_IntruderAboveSafeAlt if(UAV1_HAC1.state = IntruderDetected or UAV1_HAC1.state = AboveSafeAltitude);

57 UAV1_HAC1_EmergencyAvoid if(UAV1_HAC1.state = EmergencyAvoid);

58 UAV1_HAC1_Land if(UAV1_HAC1.state = Land);

59 UAV2_HAC1_Land if(UAV2_HAC1.state = Land);

60 UAVs_HAC1_OnGround if ((UAV1_HAC1.state=OnGround) and (UAV2_HAC1.state=OnGround));