Applying Strategic Reasoning for Accountability Ascription in Multiagent Teams Vahid Yazdanpanah1,∗ , Sebastian Stein1 , Enrico H. Gerding1 , Nicholas R. Jennings2 1 University of Southampton 2 Imperial College London v.yazdanpanah@soton.ac.uk, {ss2, eg}@ecs.soton.ac.uk, n.jennings@imperial.ac.uk Abstract blameworthiness (as being responsible for knowingly causing an outcome) and the normative notion of liability/culpability For developing human-centred trustworthy au- (as being responsible for causing a normatively undesir- tonomous systems and ensuring their safe and ef- able outcome) [van de Poel, 2011; Alechina et al., 2017; fective integration with the society, it is crucial to Chockler and Halpern, 2004]. We abstract from such neigh- enrich autonomous agents with the capacity to rep- bouring notions, as well as the exact procedure of task allo- resent and reason about their accountability. This cation, and merely focus on the notion of accountability. is, on one hand, about their accountability as col- laborative teams and, on the other hand, their in- Supporting the reliability and verifiability of AI systems dividual degree of accountability in a team. In are key to ensure a trustworthy performance of autonomous this context, accountability is understood as be- systems in human-agent collectives, i.e., ensuring a desir- ing responsible for failing to deliver a task that a able behaviour of TAS [Jennings et al., 2014; Abeywick- team was allocated and able to fulfil. To that end, rama et al., 2019]. Then, measuring the extent of agents’ the semantic (strategic reasoning) machinery of the contribution to potential failures—e.g., undelivered tasks— Alternating-time Temporal Logic (ATL) is a nat- constitutes their degree of accountability for such undesirable ural modelling approach as it captures the tempo- state of affairs [van de Poel, 2011]. ral, strategic, and coalitional dynamics of the no- In addition to technological importance, addressing the tion of accountability. This allows focusing on the accountability ascription problem—by determining account- main problem on: “Who is accountable for an un- able teams and ascribing a degree of accountability to in- fulfilled task in multiagent teams: when, why, and volved agents in a fair and computationally feasible fashion— to what extent?” We apply ATL-based semantics to also contributes to comply with ethical AI guidelines [EC: define accountability in multiagent teams and de- The High-Level Expert Group on AI, 2019]. It enables de- velop a fair and computationally feasible procedure termining who is to account for a (potentially undesirable) for ascribing a degree of accountability to involved system behaviour and fosters the societal alignment of au- agents in accountable teams. Our main results are tonomous systems [Russell, 2019; Office for Artificial Intel- on decidability, fairness properties, and computa- ligence - GOV.UK, 2020; Kalenka and Jennings, 1999]. tional complexity of the presented accountability In relation to the concept of explainability in autonomous ascription methods in multiagent teams. systems [Miller, 2019; Belle, 2017], as the capacity to de- scribe why a particular behaviour is materialised, account- 1 Introduction ability is focused on determining who and to what extent should account for it [van de Poel, 2011]. In the responsibility For developing human-centred Trustworthy Autonomous reasoning literature, accountability is understood as (i.e., is a Systems (TAS), accountability reasoning plays a key role as form of) task-oriented responsibility. In the prospective form, it contributes to: assessing the reliability of task allocations, one allocates a task τ to (an agent or) agent group α and sees ensuring verifiably safe and responsible human-agent collec- them accountable to bring it about. Then in the retrospective tives, and measuring the extent of each individual agent’s con- form of accountability (which is the main focus of this work), tribution to potential failures [Yazdanpanah et al., 2021b]. if τ remains unfulfilled, α is to account for ¬τ . This is in Accountability, as the task-oriented form of responsibility, particular a challenging problem in situations where tasks are is understood as being responsible for failing to deliver an allocated to agent groups or coordinated teams. Then, ob- allocated task [Yazdanpanah et al., 2021a]. This notion re- serving that a task is not delivered makes it clear that a team lates to but is distinguishable from the epistemic notion of is to account for it; but the the extent/degree of accountability ∗ Contact Author: v.yazdanpanah@soton.ac.uk of each individual is not well-defined. This problem corre- Copyright © 2021 for this paper by its authors. Use permitted sponds to what is known as a responsibility voids in the lit- under Creative Commons License Attribution 4.0 International (CC erature on moral responsibility [Braham and van Hees, 2011] BY 4.0). and the retrospective dimension of task coordination in mul- tiagent systems [Yazdanpanah et al., 2020]. while a2 and a6 can substitute for tasks originally allocated Although responsibility voids are well-studied in the philo- to a3 and a5 . sophical literature [Braham and van Hees, 2011; van de Poel Our focus in this work is not on the allocation itself but et al., 2012] and multiagent systems research [Yazdanpanah on the accountability ascription problem: verifying who are et al., 2019; Friedenberg and Halpern, 2019], various aspects the accountable teams if a task-oriented (vaccination) project of their task-oriented dual, i.e., accountability voids in multi- fails and on determining each agent’s degree of accountabil- agent teams, are less-explored. A notion of accountability is ity for such an outcome. Although we abstract from the al- used in [Baldoni et al., 2019] for engineering business pro- location process, it is crucial to note that the accountability cesses and in [Baldoni et al., 2020] to reason about organisa- ascription problem follows the ascription process (in a tem- tional robustness; but they do not capture accountability voids poral order) and relates to the properties that the allocation in multiagent teams. satisfies. In particular, if the allocation process merely gives For the first time, this paper presents a verifiable notion of each task to a single agent, there is no need to determine accountability in ATL semantics, approaches the problem of a degree of accountability as tasks are directly linked to an accountability voids in multiagent teams, and develops algo- accountable agent, i.e., each agent is fully accountable for rithmic logic-based methods to resolve them. We show the failed tasks that were allocated to her. However, in real-life applicability of our methods and present formal results on applications (e.g., in our vaccination project) single agents decidability and computational complexity of the presented may be incapable of delivering the tasks, thus it is neces- solution concepts. Our accountability ascription techniques sary to allow allocating tasks to agent teams. While allocat- contribute to developing verifiably safe and responsible au- ing tasks to teams provides more flexibility, any task failure tonomous system and support their integrability to form trust- leads to so called “accountability voids” and what is known as worthy human-agent collectives.1 the “problem of many hands” [Braham and van Hees, 2011; van de Poel et al., 2012]—where a team is clearly accountable 2 Accountability Analysis in ATL Semantics but the degree of accountability of each member is not well- defined. We deem that having a clear understanding of, and In this section, we present the intuition behind our work using computationally tractable methods for ascribing, individual’s a running example, analyse various conceptual aspects, and degree of accountability is key for defining justifiable sanc- recall key formal notions. tioning measures and, in turn, coordinating the behaviour of multiagent teams towards desirable ones. 2.1 Conceptual Analysis Imagine a vaccination project that demands 6 units of vac- 2.2 ATL Notions and Formal Preliminaries cine (each unit sufficient for vaccinating 1000 patients) to be To model Multiagent Systems (MAS) and reason about their delivered and injected while we have vaccine delivery agents behaviour, we use standard Concurrent Game Structures a1 , a2 , and a3 with the capacity to deliver 5, 3, and 2 units of (CGS) and employ the syntax of the Alternating-time Tempo- vaccine, respectively; and injection specialist agents a4 , a5 , ral Logic (ATL), adopted from [Alur et al., 2002]. The ATL and a6 , respectively capable of injecting 1, 5, and 5 units of language and CGS, as its semantic machinery, allow repre- vaccine. To fulfil this project, one needs to allocate the tasks senting and reasoning about the temporal modalities of tasks to capable teams of agents. The task allocation process itself and accountability. In addition, ATL is implementable us- is well-studied in the multiagent systems context [Macarthur ing well-established model checking tools [Lomuscio et al., et al., 2011] and is beyond the focus of this work. Task allo- 2017] and is expressive for specifying team-level capacities cation can be done in an efficient manner (e.g., by allocating (e.g., in contrast to similar logics like the Computation Tree tasks to a minimal team of agents) or in a more resilient fash- Logic). Having modalities to reason about the strategic ca- ion (e.g., by considering backup teams and allocating each pacity of groups of agents, and not only individuals, make task to more than one capable team). For instance, a1 , a3 , a4 , ATL and the machinery of CGS natural choices as they allow and a5 can collectively handle the project as they are able to modelling team-level accountability and support the transi- efficiently fulfil both the delivery task as well as the injection tion towards individual-level abilities—crucial for resolving task in this project. In a more resilient allocation (which also accountability voids. requires some form of coordination), delivery and injection Formally, we model a MAS as a CGS M = tasks in this project can be allocated also to the backup team ⟨Σ, Q, Act, Π, π, d, o⟩ where: a1 , a2 , a4 , and a6 . This team overlaps with the main team • Σ = {a1 , . . . , an } is a finite, non-empty set of n agents; 1 Note that accountability is related to but different from the nor- • Q is a finite, non-empty set of states; mative and legal notion of liability [Hart, 2008; Yazdanpanah et al., • Act is a finite set of atomic actions; 2021a] — which is not the focus of this work. We argue that distin- guishing various forms of responsibility and developing operational • Π is a set of atomic propositions (with p ∈ Π as a generic tools to reason about them in AI systems are key to ensuring the proposition); trustworthy behaviour and safety of such systems. In this work, we • π ∶ Π ↦ 2Q is a propositional evaluation function (deter- focus on reasoning about accountability in multiagent teams which mining propositions that hold in a state); itself can be a base, but not the only requirement, for ascribing lia- bility in a given context and with regard to a set of legal rules and • d ∶ Σ × Q ↦ P(Act) a function that specifies the sets of regulative norms. actions available to agents at each state; • o is a transition function that assigns the outcome state • M, q ⊧ ⟪Γ⟫ ◯ ϕ iff exists a strategy ZΓ such that for all q ′ = o(q, α1 , . . . , αn ) to state q and a tuple of actions computations λ ∈ out(q, ZΓ ), M, λ[1] ⊧ ϕ; αi ∈ d(ai , q) that can be executed by Σ in q. • M, q ⊧ ⟪Γ⟫ϕUψ iff exists a strategy ZΓ such that for all In a CGS M, state formulae ϕ ∶∶= p ∣ ¬ϕ ∣ ϕ ∧ ϕ (p ∈ Π) computations λ ∈ out(q, ZΓ ), for some i, M, λ[i] ⊧ ψ, specify properties of states and path formulae ψ ∶∶= ◯ ϕ ∣ and for all j < i, M, λ[j] ⊧ ϕ; ϕUϕ ∣ ◻ϕ specify temporal properties over sequences of • M, q ⊧ ⟪Γ⟫ ◻ ϕ iff exists a strategy ZΓ such that for all states. p ∈ Π is a proposition (an atomic property that may computations λ ∈ out(q, ZΓ ), for all i, M, λ[i] ⊧ ϕ. be valid in a state in Q), ¬ and ∧ are standard logical opera- tors, ◯ ϕ means that ϕ is true in the next state of M, ψUϕ Moreover, given a formula ϕ, we denote by JϕKM the set means that ψ has to hold at least until ϕ becomes true; and ◻ϕ of states in which ϕ holds. means that ϕ is always true. We denote ¬ ◻ ¬ϕ by ◇ϕ. This modality refers to the truth of ϕ in some point in time in fu- 3 Verifiably Accountable Teams ture and is known as the “existence” or “sometimes-in-future” modality. In our work, we specify tasks as path formulae and We assume a function TM d (Γ, ϕ, q) that has direct access to (task) projects as a set of tasks (examples will be provided the matrix of already allocated tasks and returns 1 if a given later). ATL is generic for specifying temporal properties over state formula ϕ is expected to be delivered by a team Γ ⊆ Σ infinite sequences. However, due to the temporally finite na- by a particular state q ∈ Q, and returns 0 otherwise. Then d,ϕ ture of tasks in real-life applications (e.g., most tasks have a TM,q denotes the set of such teams. (In this formulation, we deadline), we follow [De Giacomo and Vardi, 2015] and in- represent single agents as singleton groups.) Accordingly, to troduce a finite notion of history, and base our accountability have a track of the point of allocation we use TM a (Γ, ϕ, q) in reasoning on such finite traces. In the following, to improve which returning 1 means that in q, team Γ received the task to a,ϕ readability, we directly refer to elements of a specific (also fulfil ϕ. Then TM,q denotes the set of such teams. If a project known as pointed) CGS M, e.g., as M is fixed, we write Q P is allocated to Γ, then TM a (Γ, ϕi , q) = 1 ∶ ∀ϕi ∈ P . Here, instead of Q in M. superscripts “a” and “d” are a part of the function names to Successors, Computations, and Histories: For two states q distinguish whether q is the state in which a task is allocated and q ′ , we say q ′ is a successor of q if there exist actions αi ∈ (a) or expected to be delivered (d). For instance, if the task of d(ai , q) for ai ∈ Σ in q such that q ′ = o(q, α1 , . . . , αn ), i.e., delivering a vaccines box (denoted by v) is allocated to agent agents in Σ can collectively guarantee in q that q ′ will be the group {Alice, Bob} in state q1 and expected to be fulfilled next system state. A computation of a CGS M is an infinite by state q4 then TM a ({Alice, Bob}, v, q1 ) = 1 (determining sequence of states λ = q0 , q1 , . . . such that, for all k > 0, we the point of task allocation) and TM d ({Alice, Bob}, v, q4 ) = have that qk is a successor of qk−1 . We refer to a computation 1 (determining the expected point of task delivery). These that starts in q as a q-computation. We denote the k’th state auxiliary notions allow defining the task-oriented notion of in λ by λ[k], and λ[0, k] and λ[k, ∞] respectively denote accountability as follows. the finite prefix q0 , . . . , qk and infinite suffix qk , qk+1 , . . . of λ. Finally, we say a finite sequence of states q0 , . . . , qn is a Definition 1. In a multiagent system modelled by CGS M, q-history if qn = q, n ≥ 1, and for all 0 ≤ k < n we have that let ϕ be a state formula, q be a state, h = q0 , . . . , qn (qn = q) qk+1 is a successor of qk . We refer to any qk on a history h as be the materialised q-history, and Γ be a team of agents. We a member of h. say Γ is weakly q-accountable for ϕ based on h iff: Strategies and Outcomes: A strategy for an agent a ∈ Σ is 1. q ∈/ JϕKM , a function ζa ∶ Q ↦ Act such that for all q ∈ Q, we have that ζa (q) ∈ d(a, q). For a group of agents Γ ⊆ Σ, a collective d 2. TM (Γ, ϕ, q) = 1, and strategy ZΓ = {ζai ∣ ai ∈ Γ} is an indexed set of strategies, 3. there exist qi , qj (i ≤ j) ∈ h such that TM a (Γ, ϕ, qi ) = 1 one for every ai ∈ Γ. Then, out(q, ZΓ ) is defined as the set and Γ has a strategy in qj to ensure that M, q ⊧ ϕ. of q-computations that agents in Γ can enforce by following Moreover, a team Γ is q-accountable for ϕ based on h their corresponding strategies in ZΓ . iff it is weakly q-accountable and there exist no weakly q- Formulas of the language LAT L are defined by the follow- accountable Γ′ ⊂ Γ for ϕ. Analogously, Γ is (weakly) q- ing syntax, ϕ, ψ ∶∶= p ∣ ¬ϕ ∣ ϕ ∧ ψ ∣ ⟪Γ⟫ ◯ ϕ ∣ ⟪Γ⟫ϕUψ ∣ accountable for a project P based on h iff it is (weakly) q- ⟪Γ⟫ ◻ ϕ where p ∈ Π is an atomic proposition, and Γ ⊆ Σ accountable for all ϕ ∈ P . is a typical group of agents. Informally, ⟪Γ⟫ ◯ ϕ means that Γ has a strategy to ensure that the next state satisfies Informally, a team is (weakly) q-accountable for ϕ only if ϕ; ⟪Γ⟫ϕUψ means that Γ has a strategy to ensure ψ while it is not the case while the team was tasked and able to see maintaining the truth of ϕ; and ⟪Γ⟫ ◻ ϕ means that Γ has to it that ϕ holds in q. Distinguishing the weak form of ac- a strategy to ensure that ϕ is always true. The semantics of countability is to realise who are the core members of a team, AT L is defined relative to a CGS M and state q and is given minimally accountable for a failed task. To have a reasonably below: fair degree of accountability, we later focus on this minimal • M, q ⊧ p iff q ∈ π(p); group. Moreover, note that tasks in a project may be ful- filled through a path and not necessarily jointly in a particular • M, q ⊧ ¬ϕ iff M, q ⊧ / ϕ; state. This can be reduced to the availability of a path (and • M, q ⊧ ϕ ∧ ψ iff M, q ⊧ ϕ and M, q ⊧ ψ; accordingly a strategy) such that tasks are satisfied through the path. If joint delivery is required in a domain, tasks can Next, we show that a degree of resilience DR(ϕ) = k im- be bounded together in a conjunctive form and defined as a plies having k teams weakly q-accountable for ϕ based on single task—and not as different members of a project. In h if the allocation process is suitable in the sense of [Yaz- general, tasks in a project can be delivered sequentially. The danpanah et al., 2020]. Formally, suitability indicates that if temporal modality inside each task specification determines TMa (Γ, ϕ, q) = 1 then M, q ⊧ ⟪Γ⟫ϕ. the temporal requirements on when it should be delivered. Proposition 2. Let Γ be a q-accountable team for ϕ based on h. Given a valid task allocation, if DR(ϕ) = k then there 3.1 Accountability Reasoning in Practice exist k − 1 teams Γ′ ≠ Γ weakly q-accountable for ϕ based on Our vaccination scenario can be modelled as the 3-state par- h. tial CGS presented in Figure 1. (We say partial as it depicts only some of the states, necessary for our accountability rea- Proof. The suitability of the allocation process implies that soning, and not all of the possible states.) As discussed, var- other k − 1 teams have a strategy to see to it that ϕ is the case. ious task allocation processes can be used. Imagine the case The minimality condition cannot be satisfied necessarily as a that in q0 , the delivery task with a temporal expectation that suitable allocation process may give a task to a team and its vaccines should be delivered immediately, i.e., ◯ ϕD , is allo- super team(s). They posses a strategy to fulfil the task but cated to {a1 , a3 } and then in qD , the task to inject vaccines do not necessarily satisfy the minimality condition. Thus, in immediately, i.e., ◯ ϕI , is allocated to {a4 , a5 }. accordance to Corollary 1, we have the result on these teams Given these allocations, if we reach to q1 , we have the being weakly accountable but not necessarily accountable for history h = q0 , q1 and the delivery team {a1 , a3 } is q1 - ϕ. ◻ accountable for ϕD as they were tasked to and able to deliver Note that this result holds even if the teams received the all the 6 units of vaccine. However, in this situation, no team task in question in different states through the history (and is q-accountable for ϕI as the task to inject was specifically not necessarily in the same state). We leave further dynamics allocated in qD which is not a state in the materialised history. of task allocation with the notion of accountability and study- However, the allocation process could be less granular and ing how the coherency aspects of task allocation affects the (instead of micro-managing each task in particular states and accountability ascription problem to further research. efficiently allocating them to only one group) have allocated Moving to the project level accountability, we have: the project P = {◯ ϕD , ◯ ◯ ϕI } to Σ in q0 . This means Proposition 3. If Γ is weakly q-accountable for P , then there that all the agents in Σ are expected to ensure that vaccines exist a q-accountable team for all ϕ ∈ P . are delivered in an immediate next state after q0 and then are all injected in one immediate state further. Then in q1 , team Proof. In case Γ is q-accountable for the project, then it is Σ would be weakly q-accountable for both non-delivery and the unique minimal team and accordingly q-accountable for non-injection. Next, we present the generalised form of such all the involved tasks. But in case it is a weakly q-accountable properties on the relation between (weak) accountable teams team, it has a strategy to fulfil every ϕ from a point of allo- on the task level and project level. cation through the history. However, it is not minimal. For each ϕ, eliminating excess members guarantees the existence 3.2 Properties of minimal team. ◻ As discussed, verifying if a team is accountable for a par- 3.3 Decidability ticular path formula ϕ is conditioned to whether they were tasked to fulfil ϕ. Thus, to verify accountability for a task, it In this section, we show that determining if a team is account- is crucial to consider that the allocation process may give a able for a task is a decidable problem by proving the follow- task to more than one team (with the aim to have a level of ing theorem in a constructive way. resiliency). We refer to the number of distinguishable teams Theorem 1. The accountability verification problem in ATL- that are tasked to fulfil ϕ by its degree of resilience (as a result modelled multiagent systems is decidable. of introducing redundancy) and denote it by DR(ϕ). For in- To prove decidability, we give Algorithm 1 that, given a stance, if the task to deliver the required units of vaccine (ϕD ) multiagent system model M, a task allocation (accessible via is allocated to two teams, then DR(ϕD ) = 2. TMd (Γ, ϕ, q) and TMa (Γ, ϕ, q)), a q-history h = q0 , . . . , ql (q = Proposition 1. If Γ1 and Γ2 are q-accountable for ϕ and ql ), and a task ϕ (path formula), returns the set of weakly q- DR(ϕD ) = 1, then Γ1 = Γ2 . accountable teams for ϕ based on h. Proof. The minimality condition for accountability implies In this procedure, to verify if a team Γ (among the teams that Γ1 and Γ2 have no excess members such that one team that were expected to bring about ϕ) is accountable, we go can be a subset of another one. They can either fully overlap through the states of history h and use ATL model-checking or be distinct teams. Considering that the degree of resilience from [Alur et al., 2002] to determine whether Γ was capable is 1, the former is the case. ◻ of fulfilling the task. Note that we are taking a generic ap- proach as the procedure does not rely on a specific degree of The proposition shows that accountability is a strong con- resilience and relaxes the assumption that the allocation pro- cept as it requires the team to be a minimal weakly account- cess was a suitable one (in the sense of [Yazdanpanah et al., able team of agents. As a corollary we have: 2020]). Corollary 1. If Γ is q-accountable for ϕ then Γ′ ⊃ Γ is Next, we present computational complexity results for ac- weakly q-accountable for ϕ. countability verification. ⋆⟩ q1 ⋆, e, ⋆ , idl , ⋆, ¬ϕD , ¬ϕI l e ⟨id ⟨D, ⋆, D, ⋆, ⋆, ⋆⟩ ⟨⋆, ⋆, ⋆, I, I, ⋆⟩ start q0 qD qI ¬ϕD , ¬ϕI ϕD , ¬ϕI ¬ϕD , ϕI Figure 1: We model the scenario as M = ⟨Σ, Q, Π, π, Act, d, o⟩ where: Σ = {a1 , . . . , a6 }; Q = {q0 , q1 , . . . , qD , qI }; Π = {ϕD , ϕI } (ϕD represents the completed delivery of vaccines (yellow states) and ϕI that they are injected (green states)); Act = {D, I, idle} to represent two possible actions of delivery (D) and injection (I) as well as inaction (idle); d(ai , q) = {D, idle} (1 ≤ i ≤ 3) and d(aj , q) = {I, idle} (4 ≤ i ≤ 6) for all q ∈ Q; and both π and o are as represented in the automaton. For readability, we coloured the states, used ⋆ to refer to any action available to an agent, and used dashed lines to represent other paths that may result form unrepresented actions. Algorithm 1: Accountability Verification equal to DR(ϕ)) through all the states of history h with length l. ◻ Input: Model M; q ∈ Q; task ϕ, set TM,q d,ϕ , and history h = q0 , . . . , ql (q = ql ). And for project-level accountability verification, we have the following result. Result: Acch,ϕ M,q , the set of weakly q-accountable teams for ϕ based on h. Proposition 4. Verifying if a team Γ is accountable for a project P is ∣P ∣ times the task complexity (Theorem 2) for M,q ← ∅; h,ϕ 1 Acc verifying the longest ϕ ∈ P . 2 if q ∈ / JϕKM then 3 forall Γ ∈ TM,qd,ϕ do This shows a desirable tractability for verifying project- 4 for i = 1 to l do level accountability as it requires ∣P ∣ calls to Algorithm 1. 5 if M, ql−i ⊧ ⟪Γ⟫ϕ (standard, see [Alur et al., 2002]) then 4 A Fair Degree of Accountability Acch,ϕ M,q ← AccM,q ∪ {Γ}; h,ϕ 6 Accountability voids are situations in which a task is unful- 7 end filled and a (non-singleton) team of agents or, more problem- 8 end atically, various teams of agents are found to be accountable 9 end for it. For instance, imagine that we allocate the task to de- 10 end liver vaccines (Figure 1) to {a1 , a2 } and also to {a1 , a3 } (to h,ϕ have a degree of resilience equal to 2 on this task). Then, 11 return Acc M,q ; as the system evolves, if we realise that the vaccines are not delivered, we will have two accountable teams. Then the question is: “to what extent each of the team members 3.4 Complexity are accountable?” As agent a1 is a member of both of the In this section, we establish the complexity of the presented accountable teams, it seems unreasonable to see all of the accountability verification (Algorithm 1). One of the main three agents equally accountable and ascribe accountability— advantages of accountability reasoning using ATL semantics eventually, potential sanctioning measures or penalties—in a is that its (task) formulae, in turn the process for verifying uniform way. accountability, can be model-checked in deterministic linear In this section, we present a novel rule-based method, with time [Alur et al., 2002; Bulling et al., 2010]. a tractable complexity, for ascribing accountability.2 This method corresponds to Marginal Contribution Networks (MC Theorem 2. Accountability verification in ATL-modelled Nets) [Ieong and Shoham, 2005], and in turn provides a multiagent systems is P-complete, and can be done in time computationally tractable way to compute a degree of ac- O(l.DR(ϕ).∣M∣.∣ϕ∣), where ∣M∣ is given by the number of countability that satisfies the Shapley-based notion of fair- transitions in M, l is the length of the history, and DR(ϕ) is ness [Shapley, 1953]. the degree of resilience for ϕ. 2 Proof. The complexity of the model checking part (line 5 in There are recent attempts to address this problem using Shapley-based cost allocation [Yazdanpanah et al., 2019; Frieden- Algorithm 1) is provided by the complexity of model check- berg and Halpern, 2019]. However, such approaches seem opera- ing ATL [Alur et al., 2002] which is polynomial an can be tionally infeasible due to non-tractable complexity of the standard done in O(∣M∣.∣ϕ∣). In Algorithm 1, we call this model- method for computing the Shapley value. See more on related work d,ϕ checking for every member of TM,q (with the cardinality and positioning of our contribution in Section 5. 4.1 A Rule-Based Accountability Ascription spond to the set of accountable teams (in Acch,ϕ M,q ). In this For accountability ascription in multiagent teams, we present case, as both {a1 , a2 } and {a1 , a3 } are accountable, we will have two rules in Rh,ϕ M,q = {ρ1 ∶ ({a1 , a2 }, ∅) ↦ 1/2, ρ2 ∶ a two-phase procedure. For readability, we present these two phases separately (in Algorithm 2 and Definition 2). This ({a1 , a3 }, ∅) ↦ 1/2}. Then, for all the agents the sec- separation also allows computing the degree of accountability ond case of Definition 2 applies as they are all a member of each agent in a modular way. This results in a tractable of a positive set in a rule. Computing the share that each complexity as we do not need to go through all the agents and agent gets in its corresponding applicable rules, we have that compute all the degrees. The first phase, takes the randomly M,q (a1 ) = 1/2 and accM,q (a2 ) = accM,q (a3 ) = 1/4. acch,ϕ h,ϕ h,ϕ indexed set Acch,ϕ M,q of accountable teams and generates a set As observed, this degree is responsive to the larger contri- of accountability rules. bution of a1 (as it could contribute to two accountable teams) and the symmetric presence of a2 and a3 (both contributory Algorithm 2: Generating Accountability Rules to only one accountable teams). Note that although a2 and a3 had different delivery capacities, they received similar tasks Input: Randomly indexed Acch,ϕ M,q . in this scenario, i.e., to cooperate with a1 and provide the Result: Rh,ϕ M,q , the set of accountability rules for ϕ. vaccine unit that a1 could not deliver. k ← ∣Acch,ϕ These desirable properties, generally known as fairness 1 M,q ∣; properties in the game-theoretic literature, are not specific to 2 M,q ← ∅; Rh,ϕ this scenario but generally valid for this degree of account- 3 for i = 1 to k do ability. 4 rule ← ρi ∶ (Γi , ∅) ↦ 1/k ; 4.3 Fairness Properties M,q ← RM,q ∪ {rule}; Rh,ϕ h,ϕ 5 6 end The following Theorem shows that the presented degree of h,ϕ accountability satisfies all the Shapley-based fairness ax- 7 return R M,q ; ioms [Shapley, 1953]. Theorem 3. The presented degree of accountability M,q (a) in Definition 2 guarantees the following fair- acch,ϕ As a result, this process generates k rules, where k is the size of Acch,ϕM,q . In Section 4.3, we will show that the pre- M,q (ai ) = 1 (Efficiency); (2) ness axioms: (1) ∑ai ∈Σ acch,ϕ sented process generates a rule-based representation of a co- operative game, use this auxiliary game to compute the con- for any ai , aj ∈ Σ, acch,ϕ M,q (ai ) = accM,q (aj ) if for all h,ϕ tribution of individuals to accountable groups, and formulate Γ ∈ Acch,ϕ M,q we have that ai ∈ Γ Ô⇒ aj ∈ Γ (Symmetry); their individual degree of accountability. In each rule of type M,q (ai ) = 0 if for all Γ ∈ AccM,q , we have that (3) acch,ϕ h,ϕ ρi ∶ (Pi , Ni ) ↦ vi , we refer to ρi as the title/index of the ith rule, Pi as the positive set in the rule, Ni as the negative set in ai ∈/ Γ (Dummy Player); (4) the summation of ai ’s degree of the rule, and vi as the value of the rule. Intuitively, by assign- accountability for k different tasks ϕ1 , . . . , ϕk is k times its ing 1/k to k accountable groups (in each rule ρi generated by degree for {ϕ1 , . . . , ϕk } (Additivity). Algorithm 2), we see all groups in Acch,ϕ M,q equally account- To prove, we use the following lemmas and show that the able while the contribution of agents to such groups is the presented set of rules constitute a basic Marginal Contribution base for computing their individual degree of accountability Net (MC Net) [Ieong and Shoham, 2005] and that the degree (in Definition 2). corresponds to the Shapley value of agents in this MC Net. Accordingly, we have that our accountability degree satisfies Definition 2. Let Rh,ϕM,q be the set of q-accountability rules the four axiomatic fairness properties that uniquely charac- generated by Algorithm 2 for ϕ based on h. For agent a ∈ Σ, terise the Shapley value. we say a rule ρr is applicable if a ∈ Pr and by ω(a) denote the set of rule indices that are applicable to a. Then we say agent Lemma 1. Rh,ϕM,q is a basic Marginal Contribution Net (MC a’s degree of q-accountability for ϕ based on h, denoted by Net) [Ieong and Shoham, 2005]. M,q (a), is equal to 0 if ω(a) = ∅ and ∑r∈ω(a) ∣Pr ∣ other- acch,ϕ vr Proof. The set of rules in Rh,ϕM,q correspond to the set- wise. theoretic representation of MC Nets in [Ohta et al., 2009]. ◻ Analogously, agents degree of accountability for a project Note that in each rule, the intersection of the positive set is commutable based on the set of accountability rules that and the negative set is empty by definition (Pi ∩ Ni = ∅). is generated for the project in question. In the following, we This allows relying on a linear computation of the Shapley apply this notion to our vaccination example and present the value of the MC Net. fairness properties as well as the computational complexity for computing this degree. Lemma 2. For each ai ∈ Σ, acch,ϕ M,q (a) computes the Shap- ley value of ai in Rh,ϕ M,q . 4.2 Accountability Ascription in Practice In the vaccination scenario, in order to ascribe degrees of Proof. In Rh,ϕ [ M,q , rules only consist of positive literals Ieong accountability to agents, we first generate rules that corre- and Shoham, 2005]. In such an MC Net, Shapley value of each agent is equal to the summation of its Shapley value in 2019]) as it is a module that comes after the verification of ac- all the applicable rules. ◻ countable teams, hence does not require any changes to their model-checking under imperfect information. 4.4 Complexity Next, we show the desirable complexity of computing the de- 6 Conclusions gree of accountability. We proposed a formal account of the notion of accountability Theorem 4. The total running time for computing and presented ATL-based techniques to verify accountability M,q (a) is linear in the size of the input. acch,ϕ in multiagent settings and ascribe a fair degree of accountabil- ity to individual agents. Based on a novel rule-based repre- Proof. We show this by first focusing on the computation of sentation, we developed a fair and computationally tractable the degree itself and then the complexity for generating Rh,ϕ M,q degree for resolving accountability voids in multiagent teams. as its input. To compute the degree of any agent, we are com- The results of this study and developed accountability as- puting its Shapley value in each rule and then apply a sum- cription method also contribute to integrating ethics into AI mation for all the applicable rules. In MC Nets with positive systems and ensuring their safety and trustworthiness. In par- literals, each agent’s Shapely is equal to the value of the rule ticular, as discussed in [Yazdanpanah et al., 2021a], devel- over the number of members in P [Ieong and Shoham, 2005]. oping computational tools to verify and reason about differ- We have that the upper bound for the number of rules is the ent forms of responsibility and task-oriented accountability is degree of resilience of the task. Thus, as the Shapley in a necessary for design and development of safe and trustwor- given rule can be computed in time linear in the pattern of the thy AI. Such AI systems are expected to make autonomous rule, the total running time for computing the degree is linear decisions and, at the same time, need to make sure that their in the size of the input. And we have that the preceding rule decisions are in compliance with safety concerns and ethical generation process goes through the set of accountable teams values. To that end, we need to enrich such systems (and which is at most equal to the degree of resilience, thus does their behaviour monitoring units) with the capacity to con- not affect the computing time. ◻ template how accountabilities, for potential consequences of such decisions, are to be ascribed. Furthermore, embedding 5 Related Work accountability reasoning into AI systems contributes to pro- In relation to past work, in particular to recent work viding transparency on who is, and to what extent they are, on logic-based responsibility reasoning in multiagent set- accountable for potentially undesirable behaviour of a given tings [Friedenberg and Halpern, 2019; Yazdanpanah et al., AI-based product [Winfield and Jirotka, 2018]. 2019], we focused on verifying the task-based notion of ac- In this work, we focused on teams of agents assuming their countability (as a specific form of responsibility reasoning) intra-team capacity to coordinate towards the fulfilment of while [Friedenberg and Halpern, 2019] study the epistemic tasks. An interesting extension would be to consider the feasi- notion of blameworthiness and [Yazdanpanah et al., 2019] bility of team formations based on the value of inter-agent in- focus on the responsibility of agents with imperfect informa- teractions [Beal et al., 2020]. This way, we can reason about tion. In comparison to these, we assumed perfect information feasible team structures in presence of inter-agent incompat- and focused on task dynamics and the task-oriented notion of ibilities and study their dynamics with the accountability as- accountability. As discussed in [Yazdanpanah et al., 2021a], cription problem in multiagent teams. task-based accountability focuses on reasoning about agents Acknowledgements that received a task but failed to deliver it while responsibility in its generic from is about the ability to cause or avoid a state This work was supported by the UK Engineering and Phys- of affair and blameworthiness is concerned with agents who ical Sciences Research Council (EPSRC) through the Trust- not only caused a situation but did it knowingly. worthy Autonomous Systems Hub (EP/V00784X/1), the plat- In this work, we used finite histories as a natural choice form grant entitled “AutoTrust: Designing a Human-Centred for modelling the temporally-bounded concept of task. This Trusted, Secure, Intelligent and Usable Internet of Vehicles” corresponds with the so called provenance traces [Tsakalakis (EP/R029563/1), and the Turing AI Fellowship on Citizen- et al., 2020], commonly used for reasoning about the rea- Centric AI Systems (EP/V022067/1). sons behind a materialised situation and providing behaviour- aware explanations. Finally, we share the perspective with References [Friedenberg and Halpern, 2019; Yazdanpanah et al., 2019] [Abeywickrama et al., 2019] Dhaminda B Abeywickrama, for applicability of cost sharing methods, such as the Shapley value, for ascribing responsibility (in our case accountabil- Corina Cirstea, and Sarvapali D Ramchurn. Model check- ity). However, in comparison to the standard Shapley calcu- ing human-agent collectives for responsible AI. In Pro- lation with computationally intractable complexity, our rule- ceedings of Robot and Human Interactive Communication, based representation resulted in a computationally tractable pages 1–8, 2019. method for ascribing accountability degrees. Interestingly, [Alechina et al., 2017] Natasha Alechina, Joseph Y. this low-complexity accountability ascription process is also Halpern, and Brian Logan. Causality, responsibility and applicable to handle the complexity in imperfect informa- blame in team plans. In Proceedings of AAMAS-2017, tion settings (e.g., in combination with [Yazdanpanah et al., pages 1091–1099, 2017. [Alur et al., 2002] Rajeev Alur, Thomas A. Henzinger, and making by autonomous agents. In Cognition, Agency and Orna Kupferman. Alternating-time temporal logic. J. Rationality, pages 135–149. Springer, 1999. ACM, 49(5):672–713, 2002. [Lomuscio et al., 2017] Alessio Lomuscio, Hongyang Qu, [Baldoni et al., 2019] Matteo Baldoni, Cristina Baroglio, and Franco Raimondi. MCMAS: an open-source model Olivier Boissier, Roberto Micalizio, and Stefano Tedeschi. checker for the verification of multi-agent systems. Int. J. Accountability and responsibility in multiagent organiza- Softw. Tools Technol. Transf., 19(1):9–30, 2017. tions for engineering business processes. In Proceedings [Macarthur et al., 2011] Kathryn Sarah Macarthur, Ruben of EMAS, pages 3–24, 2019. Stranders, Sarvapali Ramchurn, and Nicholas R. Jennings. [Baldoni et al., 2020] Matteo Baldoni, Cristina Baroglio, A distributed anytime algorithm for dynamic task alloca- and Roberto Micalizio. Fragility and robustness in mul- tion in multi-agent systems. In Proceedings of AAAI-2011, tiagent systems. In Proceedings of EMAS, pages 61–77, pages 701–706, 2011. 2020. [Miller, 2019] Tim Miller. Explanation in artificial intelli- [Beal et al., 2020] Ryan Beal, Narayan Changder, Timothy gence: Insights from the social sciences. Artificial Intelli- Norman, and Sarvapali Ramchurn. Learning the value of gence, 267:1–38, 2019. teamwork to form efficient teams. In Proceedings of AAAI- [Office for Artificial Intelligence - GOV.UK, 2020] 2020, volume 34, pages 7063–7070, 2020. Office for Artificial Intelligence - GOV.UK. A [Belle, 2017] Vaishak Belle. Logic meets probability: To- guide to using artificial intelligence in the public wards explainable ai systems for uncertain worlds. In IJ- sector. https://www.gov.uk/government/publications/ CAI, pages 5116–5120, 2017. a-guide-to-using-artificial-intelligence-in-the-public-sector, [Braham and van Hees, 2011] Matthew Braham and Martin 2020. Accessed: 2021-05-01. van Hees. Responsibility voids. The Philosophical Quar- [Ohta et al., 2009] Naoki Ohta, Vincent Conitzer, Ryo terly, 61(242):6–15, 2011. Ichimura, Yuko Sakurai, Atsushi Iwasaki, and Makoto [Bulling et al., 2010] Nils Bulling, Jurgen Dix, and Woj- Yokoo. Coalition structure generation utilizing compact ciech Jamroga. Model checking logics of strategic abil- characteristic function representations. In International ity: Complexity. In Specification and Verification of Multi- Conference on Principles and Practice of Constraint Pro- agent Systems, pages 125–159. Springer, 2010. gramming, pages 623–638, 2009. [Chockler and Halpern, 2004] Hana Chockler and Joseph Y [Russell, 2019] Stuart Russell. Human compatible: Artificial Halpern. Responsibility and blame: A structural-model intelligence and the problem of control. Penguin, 2019. approach. JAIR, 22:93–115, 2004. [Shapley, 1953] Lloyd S Shapley. A value for n-person [De Giacomo and Vardi, 2015] Giuseppe De Giacomo and games. Contributions to the Theory of Games, 2(28):307– Moshe Vardi. Synthesis for LTL and LDL on finite traces. 317, 1953. In Proceedings of IJCAI-2015. Citeseer, 2015. [Tsakalakis et al., 2020] Niko Tsakalakis, Laura [EC: The High-Level Expert Group on AI, 2019] EC: The Carmichael, Sophie Stalla-Bourdillon, Luc Moreau, High-Level Expert Group on AI. Ethics guidelines for Dong Huynh, and Ayah Helal. Explanations for AI: trustworthy AI. https://ec.europa.eu/digital-single-market/ Computable or not? In Web Science Companion, pages en/news/ethics-guidelines-trustworthy-ai, 2019. Ac- 77–77, 2020. cessed: 2021-05-01. [van de Poel et al., 2012] Ibo van de Poel, Jessica Nihlén [Friedenberg and Halpern, 2019] Meir Friedenberg and Fahlquist, Neelke Doorn, Sjoerd Zwart, and Lamber Roy- Joseph Y Halpern. Blameworthiness in multi-agent akkers. The problem of many hands: Climate change as settings. In Proceedings of AAAI-2019, pages 525–532, an example. Science and engineering ethics, 18(1):49–67, 2019. 2012. [Hart, 2008] Herbert Lionel Adolphus Hart. Punishment and [van de Poel, 2011] Ibo van de Poel. The relation between responsibility: Essays in the philosophy of law. Oxford forward-looking and backward-looking responsibility. In University Press, 2008. Moral responsibility, pages 37–52. Springer, 2011. [Ieong and Shoham, 2005] Samuel Ieong and Yoav Shoham. [Winfield and Jirotka, 2018] Alan FT Winfield and Marina Marginal contribution nets: a compact representation Jirotka. Ethical governance is essential to building trust scheme for coalitional games. In Proceedings of E- in robotics and artificial intelligence systems. Philosoph- Commerce-2005, pages 193–202, 2005. ical Transactions of the Royal Society A: Mathematical, [Jennings et al., 2014] Nicholas R Jennings, Luc Moreau, Physical and Engineering Sciences, 2018. David Nicholson, Sarvapali Ramchurn, Stephen Roberts, [Yazdanpanah et al., 2019] Vahid Yazdanpanah, Mehdi Das- Tom Rodden, and Alex Rogers. Human-agent collectives. tani, Wojciech Jamroga, Natasha Alechina, and Brian Lo- Communications of the ACM, 57(12):80–88, 2014. gan. Strategic responsibility under imperfect information. [Kalenka and Jennings, 1999] Susanne Kalenka and In Proceedings of AAMAS-2019, pages 592–600, 2019. Nicholas R Jennings. Socially responsible decision [Yazdanpanah et al., 2020] Vahid Yazdanpanah, Mehdi Das- responsibility in multiagent settings. In ACM Collective tani, Shaheen Fatima, Nicholas R. Jennings, Devrim Mu- Intelligence Conference 2021 (CI-2021), April 2021. rat Yazan, and W. Henk Zijm. Task coordination in mul- [Yazdanpanah et al., 2021b] Vahid Yazdanpanah, Enrico H. tiagent systems. In Proceedings of AAMAS-2020, pages Gerding, Sebastian Stein, Mehdi Dastani, Catholijn M. 2056–2058, 2020. Jonker, and Timothy J. Norman. Responsibility research [Yazdanpanah et al., 2021a] Vahid Yazdanpanah, Enrico H. for trustworthy autonomous systems. In Proceedings of Gerding, Sebastian Stein, Corina Cirstea, m.c. schraefel, AAMAS-2021, page 57–62, 2021. Timothy J. Norman, and Nicholas R. Jennings. Collective