For developing human-centred trustworthy autonomous systems and ensuring their safe and effective integration with the society, it is crucial to enrich autonomous agents with the capacity to represent and reason about their accountability. This is, on one hand, about their accountability as collaborative teams and, on the other hand, their individual degree of accountability in a team. In this context, accountability is understood as being responsible for failing to deliver a task that a team was allocated and able to fulfil. To that end, the semantic (strategic reasoning) machinery of the Alternating-time Temporal Logic (ATL) is a natural modelling approach as it captures the temporal, strategic, and coalitional dynamics of the notion of accountability. This allows focusing on the main problem on: “Who is accountable for an unfulfilled task in multiagent teams: when, why, and to what extent?” We apply ATL-based semantics to define accountability in multiagent teams and develop a fair and computationally feasible procedure for ascribing a degree of accountability to involved agents in accountable teams. Our main results are on decidability, fairness properties, and computational complexity of the presented accountability ascription methods in multiagent teams.
For developing human-centred Trustworthy Autonomous Systems (TAS), accountability reasoning plays a key role as it contributes to: assessing the reliability of task allocations, ensuring verifiably safe and responsible human-agent collectives, and measuring the extent of each individual agent’s contribution to potential failures [Yazdanpanah et al., 2021b].
Accountability, as the task-oriented form of responsibility, is understood as being responsible for failing to deliver an allocated task [Yazdanpanah et al., 2021a]. This notion relates to but is distinguishable from the epistemic notion of blameworthiness (as being responsible for knowingly causing an outcome) and the normative notion of liability/culpability (as being responsible for causing a normatively undesirable outcome) [van de Poel, 2011; Alechina et al., 2017; Chockler and Halpern, 2004]. We abstract from such neighbouring notions, as well as the exact procedure of task allocation, and merely focus on the notion of accountability.
Supporting the reliability and verifiability of AI systems are key to ensure a trustworthy performance of autonomous systems in human-agent collectives, i.e., ensuring a desirable behaviour of TAS [Jennings et al., 2014; Abeywickrama et al., 2019]. Then, measuring the extent of agents’ contribution to potential failures—e.g., undelivered tasks— constitutes their degree of accountability for such undesirable state of affairs [van de Poel, 2011].
In addition to technological importance, addressing the accountability ascription problem—by determining accountable teams and ascribing a degree of accountability to involved agents in a fair and computationally feasible fashion— also contributes to comply with ethical AI guidelines [EC: The High-Level Expert Group on AI, 2019]. It enables determining who is to account for a (potentially undesirable) system behaviour and fosters the societal alignment of autonomous systems [Russell, 2019; Office for Artificial Intelligence - GOV.UK, 2020; Kalenka and Jennings, 1999].
In relation to the concept of explainability in autonomous systems [Miller, 2019; Belle, 2017], as the capacity to describe why a particular behaviour is materialised, accountability is focused on determining who and to what extent should account for it [van de Poel, 2011]. In the responsibility reasoning literature, accountability is understood as (i.e., is a form of) task-oriented responsibility. In the prospective form, one allocates a task to (an agent or) agent group and sees them accountable to bring it about. Then in the retrospective form of accountability (which is the main focus of this work), if remains unfulfilled, is to account for ¬ . This is in particular a challenging problem in situations where tasks are allocated to agent groups or coordinated teams. Then, observing that a task is not delivered makes it clear that a team is to account for it; but the the extent/degree of accountability of each individual is not well-defined. This problem corresponds to what is known as a responsibility voids in the literature on moral responsibility [Braham and van Hees, 2011] and the retrospective dimension of task coordination in multiagent systems [Yazdanpanah et al., 2020].
Although responsibility voids are well-studied in the philosophical literature [Braham and van Hees, 2011; van de Poel et al., 2012] and multiagent systems research [Yazdanpanah et al., 2019; Friedenberg and Halpern, 2019], various aspects of their task-oriented dual, i.e., accountability voids in multiagent teams, are less-explored. A notion of accountability is used in [Baldoni et al., 2019] for engineering business processes and in [Baldoni et al., 2020] to reason about organisational robustness; but they do not capture accountability voids in multiagent teams.
For the first time, this paper presents a verifiable notion of accountability in ATL semantics, approaches the problem of accountability voids in multiagent teams, and develops algorithmic logic-based methods to resolve them. We show the applicability of our methods and present formal results on decidability and computational complexity of the presented solution concepts. Our accountability ascription techniques contribute to developing verifiably safe and responsible autonomous system and support their integrability to form trustworthy human-agent collectives.1 2
In this section, we present the intuition behind our work using a running example, analyse various conceptual aspects, and recall key formal notions. 2.1
Imagine a vaccination project that demands 6 units of vaccine (each unit sufficient for vaccinating 1000 patients) to be delivered and injected while we have vaccine delivery agents a1, a2, and a3 with the capacity to deliver 5, 3, and 2 units of vaccine, respectively; and injection specialist agents a4, a5, and a6, respectively capable of injecting 1, 5, and 5 units of vaccine. To fulfil this project, one needs to allocate the tasks to capable teams of agents. The task allocation process itself is well-studied in the multiagent systems context [Macarthur et al., 2011] and is beyond the focus of this work. Task allocation can be done in an efficient manner (e.g., by allocating tasks to a minimal team of agents) or in a more resilient fashion (e.g., by considering backup teams and allocating each task to more than one capable team). For instance, a1, a3, a4, and a5 can collectively handle the project as they are able to efficiently fulfil both the delivery task as well as the injection task in this project. In a more resilient allocation (which also requires some form of coordination), delivery and injection tasks in this project can be allocated also to the backup team a1, a2, a4, and a6. This team overlaps with the main team 1Note that accountability is related to but different from the normative and legal notion of liability [Hart, 2008; Yazdanpanah et al., 2021a] — which is not the focus of this work. We argue that distinguishing various forms of responsibility and developing operational tools to reason about them in AI systems are key to ensuring the trustworthy behaviour and safety of such systems. In this work, we focus on reasoning about accountability in multiagent teams which itself can be a base, but not the only requirement, for ascribing liability in a given context and with regard to a set of legal rules and regulative norms. • • • while a2 and a6 can substitute for tasks originally allocated to a3 and a5.
Our focus in this work is not on the allocation itself but on the accountability ascription problem: verifying who are the accountable teams if a task-oriented (vaccination) project fails and on determining each agent’s degree of accountability for such an outcome. Although we abstract from the allocation process, it is crucial to note that the accountability ascription problem follows the ascription process (in a temporal order) and relates to the properties that the allocation satisfies. In particular, if the allocation process merely gives each task to a single agent, there is no need to determine a degree of accountability as tasks are directly linked to an accountable agent, i.e., each agent is fully accountable for failed tasks that were allocated to her. However, in real-life applications (e.g., in our vaccination project) single agents may be incapable of delivering the tasks, thus it is necessary to allow allocating tasks to agent teams. While allocating tasks to teams provides more flexibility, any task failure leads to so called “accountability voids” and what is known as the “problem of many hands” [Braham and van Hees, 2011; van de Poel et al., 2012]—where a team is clearly accountable but the degree of accountability of each member is not welldefined. We deem that having a clear understanding of, and computationally tractable methods for ascribing, individual’s degree of accountability is key for defining justifiable sanctioning measures and, in turn, coordinating the behaviour of multiagent teams towards desirable ones. 2.2
To model Multiagent Systems (MAS) and reason about their behaviour, we use standard Concurrent Game Structures (CGS) and employ the syntax of the Alternating-time Temporal Logic (ATL), adopted from [Alur et al., 2002]. The ATL language and CGS, as its semantic machinery, allow representing and reasoning about the temporal modalities of tasks and accountability. In addition, ATL is implementable using well-established model checking tools [Lomuscio et al., 2017] and is expressive for specifying team-level capacities (e.g., in contrast to similar logics like the Computation Tree Logic). Having modalities to reason about the strategic capacity of groups of agents, and not only individuals, make ATL and the machinery of CGS natural choices as they allow modelling team-level accountability and support the transition towards individual-level abilities—crucial for resolving accountability voids.
Formally, we model a MAS as a CGS M = ⟨ ; Q; Act; ; ; d; o⟩ where:
= {a1; : : : ; an} is a finite, non-empty set of n agents; • Q is a finite, non-empty set of states; • Act is a finite set of atomic actions;
is a set of atomic propositions (with p ∈ proposition); as a generic ∶ ↦ 2Q is a propositional evaluation function (determining propositions that hold in a state); • d ∶ × Q ↦ P(Act) a function that specifies the sets of actions available to agents at each state; • o is a transition function that assigns the outcome state q′ = o(q; 1; : : : ; n) to state q and a tuple of actions i ∈ d(ai; q) that can be executed by in q.
In a CGS M, state formulae ' ∶∶= p S ¬' S ' ∧ ' (p ∈ ) specify properties of states and path formulae ∶∶= 4 ' S 'U ' S ◻' specify temporal properties over sequences of states. p ∈ is a proposition (an atomic property that may be valid in a state in Q), ¬ and ∧ are standard logical operators, 4 ' means that ' is true in the next state of M, U ' means that has to hold at least until ' becomes true; and ◻' means that ' is always true. We denote ¬ ◻ ¬' by ◇'. This modality refers to the truth of ' in some point in time in future and is known as the “existence” or “sometimes-in-future” modality. In our work, we specify tasks as path formulae and (task) projects as a set of tasks (examples will be provided later). ATL is generic for specifying temporal properties over infinite sequences. However, due to the temporally finite nature of tasks in real-life applications (e.g., most tasks have a deadline), we follow [De Giacomo and Vardi, 2015] and introduce a finite notion of history, and base our accountability reasoning on such finite traces. In the following, to improve readability, we directly refer to elements of a specific (also known as pointed) CGS M, e.g., as M is fixed, we write Q instead of Q in M.
Successors, Computations, and Histories: For two states q and q′, we say q′ is a successor of q if there exist actions i ∈ d(ai; q) for ai ∈ in q such that q′ = o(q; 1; : : : ; n), i.e., agents in can collectively guarantee in q that q′ will be the next system state. A computation of a CGS M is an infinite sequence of states = q0; q1; : : : such that, for all k > 0, we have that qk is a successor of qk−1. We refer to a computation that starts in q as a q-computation. We denote the k’th state in by [k], and [0; k] and [k; ∞] respectively denote the finite prefix q0; : : : ; qk and infinite suffix qk; qk+1; : : : of . Finally, we say a finite sequence of states q0; : : : ; qn is a q-history if qn = q, n ≥ 1, and for all 0 ≤ k < n we have that qk+1 is a successor of qk. We refer to any qk on a history h as a member of h.
Strategies and Outcomes: A strategy for an agent a ∈ is 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 strategy Z = { ai S ai ∈ } is an indexed set of strategies, one for every ai ∈ . Then, out(q; Z ) is defined as the set of q-computations that agents in can enforce by following their corresponding strategies in Z .
Formulas of the language LAT L are defined by the following syntax, '; ∶∶= p S ¬' S ' ∧ S ⟪ ⟫ 4 ' S ⟪ ⟫'U S ⟪ ⟫ ◻ ' where p ∈ is an atomic proposition, and ⊆ is a typical group of agents. Informally, ⟪ ⟫ 4 ' means that has a strategy to ensure that the next state satisfies '; ⟪ ⟫'U means that has a strategy to ensure while maintaining the truth of '; and ⟪ ⟫ ◻ ' means that has a strategy to ensure that ' is always true. The semantics of AT L is defined relative to a CGS M and state q and is given below: • M; q ⊧ p iff q ∈ ( )
p ; • M; q ⊧ ¬' iff M; q ⊧~ '; • M; q ⊧ ' ∧ iff M; q ⊧ ' and M; q ⊧ ; • M; q ⊧ ⟪ ⟫ 4 ' iff exists a strategy Z such that for all computations ∈ out(q; Z ), M; [1] ⊧ '; • M; q ⊧ ⟪ ⟫'U iff exists a strategy Z such that for all computations ∈ out(q; Z ), for some i, M; [i] ⊧ , and for all j < i, M; [j] ⊧ '; • M; q ⊧ ⟪ ⟫ ◻ ' iff exists a strategy Z such that for all computations ∈ out(q; Z ), for all i, M; [i] ⊧ '.
J KM the set of states in which ' holds. 3
We assume a function T d the matrix of already alloMca(ted;'ta;sqk)sthanatdhraestudrnirsec1t iafcacegsisvetno state formula ' is expected to be delivered by a team ⊆ by a particular state q ∈ Q, and returns 0 otherwise. Then T Md;';q denotes the set of such teams. (In this formulation, we represent single agents as singleton groups.) Accordingly, to have a track of the point of allocation we use T Ma( ; '; q) in which returning 1 means that in q, team received the task to fulfil '. Then T Ma; ';q denotes the set of such teams. If a project P is allocated to , then T a superscripts “a” and “d” arMe (a p;a'rti;oqf)th=e1f u∶n∀c'tiion∈ Pna.mHeserteo, distinguish whether q is the state in which a task is allocated (a) or expected to be delivered (d). For instance, if the task of delivering a vaccines box (denoted by v) is allocated to agent group {Alice; Bob} in state q1 and expected to be fulfilled by state q4 then T Ma({Alice; Bob}; v; q1) = 1 (determining the point of task allocation) and T d Alice; Bob}; v; q4) = 1 (determining the expected pointMof({task delivery). These auxiliary notions allow defining the task-oriented notion of accountability as follows.
Definition 1. In a multiagent system modelled by CGS M, let ' be a state formula, q be a state, h = q0; : : : ; qn(qn = q) be the materialised q-history, and be a team of agents. We say is weakly q-accountable for ' based on h iff: 1. q ∈~ J'KM, 2. T Md( ; '; q) = 1, and 3. there exist qi; qj (i ≤ j) ∈ h such that T a
and has a strategy in qj to ensure thatMM( ; q;'⊧; q'i.) = 1 Moreover, a team is q-accountable for ' based on h iff it is weakly q-accountable and there exist no weakly qaccountable ′ ⊂ for '. Analogously, is (weakly) qaccountable for a project P based on h iff it is (weakly) qaccountable for all ' ∈ P .
Informally, a team is (weakly) q-accountable for ' only if it is not the case while the team was tasked and able to see to it that ' holds in q. Distinguishing the weak form of accountability is to realise who are the core members of a team, minimally accountable for a failed task. To have a reasonably fair degree of accountability, we later focus on this minimal group. Moreover, note that tasks in a project may be fulfilled through a path and not necessarily jointly in a particular state. This can be reduced to the availability of a path (and accordingly a strategy) such that tasks are satisfied through the path. If joint delivery is required in a domain, tasks can be bounded together in a conjunctive form and defined as a single task—and not as different members of a project. In general, tasks in a project can be delivered sequentially. The temporal modality inside each task specification determines the temporal requirements on when it should be delivered.
Our vaccination scenario can be modelled as the 3-state partial CGS presented in Figure 1. (We say partial as it depicts only some of the states, necessary for our accountability reasoning, and not all of the possible states.) As discussed, various task allocation processes can be used. Imagine the case that in q0, the delivery task with a temporal expectation that vaccines should be delivered immediately, i.e., 4 'D, is allocated to {a1; a3} and then in qD, the task to inject vaccines immediately, i.e., 4 'I , is allocated to {a4; a5}.
Given these allocations, if we reach to q1, we have the history h = q0; q1 and the delivery team {a1; a3} is q1accountable for 'D as they were tasked to and able to deliver all the 6 units of vaccine. However, in this situation, no team is q-accountable for 'I as the task to inject was specifically allocated in qD which is not a state in the materialised history. However, the allocation process could be less granular and (instead of micro-managing each task in particular states and efficiently allocating them to only one group) have allocated the project P = {4 'D; 4 4 'I } to in q0. This means that all the agents in are expected to ensure that vaccines are delivered in an immediate next state after q0 and then are all injected in one immediate state further. Then in q1, team would be weakly q-accountable for both non-delivery and non-injection. Next, we present the generalised form of such properties on the relation between (weak) accountable teams on the task level and project level. 3.2
As discussed, verifying if a team is accountable for a particular path formula ' is conditioned to whether they were tasked to fulfil '. Thus, to verify accountability for a task, it is crucial to consider that the allocation process may give a task to more than one team (with the aim to have a level of resiliency). We refer to the number of distinguishable teams that are tasked to fulfil ' by its degree of resilience (as a result of introducing redundancy) and denote it by DR('). For instance, if the task to deliver the required units of vaccine ('D) is allocated to two teams, then DR('D) = 2.
Proposition 1. If 1 and 2 are q-accountable for ' and DR('D) = 1, then 1 = 2.
Proof. The minimality condition for accountability implies that 1 and 2 have no excess members such that one team can be a subset of another one. They can either fully overlap or be distinct teams. Considering that the degree of resilience is 1, the former is the case. ◻
The proposition shows that accountability is a strong concept as it requires the team to be a minimal weakly accountable team of agents. As a corollary we have: Corollary 1. If is q-accountable for ' then ′ ⊃ weakly q-accountable for '. is
Next, we show that a degree of resilience DR(') = k implies having k teams weakly q-accountable for ' based on h if the allocation process is suitable in the sense of [Yazdanpanah et al., 2020]. Formally, suitability indicates that if T Ma( ; '; q) = 1 then M; q ⊧ ⟪ ⟫'.
Proposition 2. Let be a q-accountable team for ' based on h. Given a valid task allocation, if DR(') = k then there exist k − 1 teams ′ ≠ weakly q-accountable for ' based on h.
Proof. The suitability of the allocation process implies that other k − 1 teams have a strategy to see to it that ' is the case. The minimality condition cannot be satisfied necessarily as a suitable allocation process may give a task to a team and its super team(s). They posses a strategy to fulfil the task but do not necessarily satisfy the minimality condition. Thus, in accordance to Corollary 1, we have the result on these teams being weakly accountable but not necessarily accountable for '. ◻
Note that this result holds even if the teams received the task in question in different states through the history (and not necessarily in the same state). We leave further dynamics of task allocation with the notion of accountability and studying how the coherency aspects of task allocation affects the accountability ascription problem to further research.
Moving to the project level accountability, we have: Proposition 3. If is weakly q-accountable for P , then there exist a q-accountable team for all ' ∈ P .
Proof. In case is q-accountable for the project, then it is the unique minimal team and accordingly q-accountable for all the involved tasks. But in case it is a weakly q-accountable team, it has a strategy to fulfil every ' from a point of allocation through the history. However, it is not minimal. For each ', eliminating excess members guarantees the existence of minimal team. ◻ 3.3
In this section, we show that determining if a team is accountable for a task is a decidable problem by proving the following theorem in a constructive way.
Theorem 1. The accountability verification problem in ATLmodelled multiagent systems is decidable.
To prove decidability, we give Algorithm 1 that, given a multiagent system model M, a task allocation (accessible via T d and T a qlM), (an;d'a; qta)sk ' (pMat(h f;o'rm;qu)l)a,)a, rqe-thuirsntosrtyhehs=etqo0;f:w: :e;aqkll(yqq=accountable teams for ' based on h.
In this procedure, to verify if a team (among the teams
that were expected to bring about ') is accountable, we go
through the states of history h and use ATL model-checking
from [Alur et al., 2002] to determine whether was capable
of fulfilling the task. Note that we are taking a generic
approach as the procedure does not rely on a specific degree of
resilience and relaxes the assumption that the allocation
process was a suitable one
Next, we present computational complexity results for accountability verification. id ⟨
;id le; ⋆
; ⋆⟩ ; ⋆ le; ⋆ ⟨D; ⋆; D; ⋆; ⋆; ⋆⟩
⟨⋆; ⋆; ⋆; I; I; ⋆⟩ start
q0 ¬'D; ¬'I qI ¬'D; 'I Input: Model M; q ∈ Q; task ', set T Md;';q, and history h = q0; : : : ; ql(q = ql).
Result: AcchM;';q, the set of weakly q-accountable
teams for ' based on h.
1 AcchM;';q ← ∅;
2 if q ∈~ J'KM then
3 forall ∈ T Md;';q do
for i = 1 to l do
if M; ql−i ⊧ ⟪ ⟫'
AcchM;';q ← AcchM;';q ∪ { }; In this section, we establish the complexity of the presented accountability verification (Algorithm 1). One of the main advantages of accountability reasoning using ATL semantics is that its (task) formulae, in turn the process for verifying accountability, can be model-checked in deterministic linear time [Alur et al., 2002; Bulling et al., 2010].
Theorem 2. Accountability verification in ATL-modelled multiagent systems is P-complete, and can be done in time O(l:DR('):SMS:S'S), where SMS is given by the number of transitions in M, l is the length of the history, and DR(') is the degree of resilience for '.
Proof. The complexity of the model checking part (line 5 in Algorithm 1) is provided by the complexity of model checking ATL [Alur et al., 2002] which is polynomial an can be done in O(SMS:S'S). In Algorithm 1, we call this modelchecking for every member of T Md;';q (with the cardinality equal to DR(')) through all the states of history h with length l. ◻
And for project-level accountability verification, we have the following result.
Proposition 4. Verifying if a team is accountable for a project P is SP S times the task complexity (Theorem 2) for verifying the longest ' ∈ P .
This shows a desirable tractability for verifying projectlevel accountability as it requires SP S calls to Algorithm 1. 4
Accountability voids are situations in which a task is unfulfilled and a (non-singleton) team of agents or, more problematically, various teams of agents are found to be accountable for it. For instance, imagine that we allocate the task to deliver vaccines (Figure 1) to {a1; a2} and also to {a1; a3} (to have a degree of resilience equal to 2 on this task). Then, 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 are accountable?” As agent a1 is a member of both of the accountable teams, it seems unreasonable to see all of the three agents equally accountable and ascribe accountability— eventually, potential sanctioning measures or penalties—in a uniform way.
In this section, we present a novel rule-based method, with a tractable complexity, for ascribing accountability.2 This method corresponds to Marginal Contribution Networks (MC Nets) [Ieong and Shoham, 2005], and in turn provides a computationally tractable way to compute a degree of accountability that satisfies the Shapley-based notion of fairness [Shapley, 1953].
2There are recent attempts to address this problem using Shapley-based cost allocation [Yazdanpanah et al., 2019; Friedenberg and Halpern, 2019]. However, such approaches seem operationally infeasible due to non-tractable complexity of the standard method for computing the Shapley value. See more on related work and positioning of our contribution in Section 5.
For accountability ascription in multiagent teams, we present a two-phase procedure. For readability, we present these two phases separately (in Algorithm 2 and Definition 2). This separation also allows computing the degree of accountability of each agent in a modular way. This results in a tractable complexity as we do not need to go through all the agents and compute all the degrees. The first phase, takes the randomly indexed set AcchM;';q of accountable teams and generates a set of accountability rules.
Input: Randomly indexed Acch;' .
M;q
Result: RhM;';q, the set of accountability rules for '. 1 k ← SAcchM;';qS; 2 RhM;';q ← ∅; 3 for i = 1 to k do 4 rule ← i ∶ ( i; ∅) ↦ 1~k ; 5 RhM;';q ← RhM;';q ∪ {rule}; 6 end
M;q
As a result, this process generates k rules, where k is the size of Acch;' . In Section 4.3, we will show that the pre
M;q sented process generates a rule-based representation of a cooperative game, use this auxiliary game to compute the contribution of individuals to accountable groups, and formulate their individual degree of accountability. In each rule of type 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 the rule, and vi as the value of the rule. Intuitively, by assigning 1~k to k accountable groups (in each rule i generated by Algorithm 2), we see all groups in AcchM;';q equally accountable while the contribution of agents to such groups is the base for computing their individual degree of accountability (in Definition 2).
M;q be the set of q-accountability rules generated by Algorithm 2 for ' based on h. For agent a ∈ , 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 a’s degree of q-accountability for ' based on h, denoted by acch;' vr other
M;q(a), is equal to 0 if !(a) = ∅ and ∑r∈!(a) SPrS wise.
Analogously, agents degree of accountability for a project is commutable based on the set of accountability rules that is generated for the project in question. In the following, we apply this notion to our vaccination example and present the fairness properties as well as the computational complexity for computing this degree.
In the vaccination scenario, in order to ascribe degrees of accountability to agents, we first generate rules that correspond to the set of accountable teams (in AcchM;';q). In this 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 ∶ ({a1; a3}; ∅) ↦ 1~2}. Then, for all the agents the second case of Definition 2 applies as they are all a member of a positive set in a rule. Computing the share that each agent gets in its corresponding applicable rules, we have that acch;' M;q(a2) = acch;'
M;q(a1) = 1~2 and acch;' M;q(a3) = 1~4.
As observed, this degree is responsive to the larger contribution of a1 (as it could contribute to two accountable teams) and the symmetric presence of a2 and a3 (both contributory to only one accountable teams). Note that although a2 and a3 had different delivery capacities, they received similar tasks in this scenario, i.e., to cooperate with a1 and provide the vaccine unit that a1 could not deliver.
These desirable properties, generally known as fairness properties in the game-theoretic literature, are not specific to this scenario but generally valid for this degree of accountability. 4.3
The following Theorem shows that the presented degree of accountability satisfies all the Shapley-based fairness axioms [Shapley, 1953].
Theorem 3. The presented degree of accountability acch;'
M;q(a) in Definition 2 guarantees the following fairness axioms: (1) ∑ai∈ acch;'
, acch;' M;q(ai) = 1 (Efficiency); (2) for any ai; aj ∈ M;q(ai) = acchM;';q(aj ) if for all ∈ AcchM;';q we have that ai ∈ Ô⇒ aj ∈ (Symmetry); (3) acchM;';q(ai) = 0 if for all ∈ AcchM;';q, we have that ai ∈~ (Dummy Player); (4) the summation of ai’s degree of accountability for k different tasks '1; : : : ; 'k is k times its degree for {'1; : : : ; 'k} (Additivity).
To prove, we use the following lemmas and show that the presented set of rules constitute a basic Marginal Contribution Net (MC Net) [Ieong and Shoham, 2005] and that the degree corresponds to the Shapley value of agents in this MC Net. Accordingly, we have that our accountability degree satisfies the four axiomatic fairness properties that uniquely characterise the Shapley value.
Lemma 1. RhM;';q is a basic Marginal Contribution Net (MC Net) [Ieong and Shoham, 2005].
Proof. The set of rules in Rh;' M;q correspond to the settheoretic representation of MC Nets in [Ohta et al., 2009]. ◻
Note that in each rule, the intersection of the positive set and the negative set is empty by definition (Pi ∩ Ni = ∅). This allows relying on a linear computation of the Shapley value of the MC Net.
Lemma 2. For each ai ∈ ley value of ai in Rh;' .
M;q , acch;'
M;q(a) computes the ShapProof. In RhM;';q, rules only consist of positive literals [Ieong and Shoham, 2005]. In such an MC Net, Shapley value of each agent is equal to the summation of its Shapley value in all the applicable rules. Next, we show the desirable complexity of computing the degree of accountability. time for computing Theorem 4. The total running acch;'
M;q(a) is linear in the size of the input.
Proof. We show this by first focusing on the computation of the degree itself and then the complexity for generating Rh;' M;q as its input. To compute the degree of any agent, we are computing its Shapley value in each rule and then apply a summation for all the applicable rules. In MC Nets with positive literals, each agent’s Shapely is equal to the value of the rule over the number of members in P [Ieong and Shoham, 2005]. We have that the upper bound for the number of rules is the degree of resilience of the task. Thus, as the Shapley in a given rule can be computed in time linear in the pattern of the rule, the total running time for computing the degree is linear in the size of the input. And we have that the preceding rule generation process goes through the set of accountable teams which is at most equal to the degree of resilience, thus does not affect the computing time. ◻ 5
In relation to past work, in particular to recent work on logic-based responsibility reasoning in multiagent settings [Friedenberg and Halpern, 2019; Yazdanpanah et al., 2019], we focused on verifying the task-based notion of accountability (as a specific form of responsibility reasoning) while [Friedenberg and Halpern, 2019] study the epistemic notion of blameworthiness and [Yazdanpanah et al., 2019] focus on the responsibility of agents with imperfect information. In comparison to these, we assumed perfect information and focused on task dynamics and the task-oriented notion of accountability. As discussed in [Yazdanpanah et al., 2021a], task-based accountability focuses on reasoning about agents 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 of affair and blameworthiness is concerned with agents who not only caused a situation but did it knowingly.
In this work, we used finite histories as a natural choice
for modelling the temporally-bounded concept of task. This
corresponds with the so called provenance traces [Tsakalakis
et al., 2020], commonly used for reasoning about the
reasons behind a materialised situation and providing
behaviouraware explanations. Finally, we share the perspective with
[Friedenberg and Halpern, 2019; Yazdanpanah et al., 2019]
for applicability of cost sharing methods, such as the Shapley
value, for ascribing responsibility (in our case
accountability). However, in comparison to the standard Shapley
calculation with computationally intractable complexity, our
rulebased representation resulted in a computationally tractable
method for ascribing accountability degrees. Interestingly,
this low-complexity accountability ascription process is also
applicable to handle the complexity in imperfect
information settings
We proposed a formal account of the notion of accountability and presented ATL-based techniques to verify accountability in multiagent settings and ascribe a fair degree of accountability to individual agents. Based on a novel rule-based representation, we developed a fair and computationally tractable degree for resolving accountability voids in multiagent teams.
The results of this study and developed accountability ascription method also contribute to integrating ethics into AI systems and ensuring their safety and trustworthiness. In particular, as discussed in [Yazdanpanah et al., 2021a], developing computational tools to verify and reason about different forms of responsibility and task-oriented accountability is necessary for design and development of safe and trustworthy AI. Such AI systems are expected to make autonomous decisions and, at the same time, need to make sure that their decisions are in compliance with safety concerns and ethical values. To that end, we need to enrich such systems (and their behaviour monitoring units) with the capacity to contemplate how accountabilities, for potential consequences of such decisions, are to be ascribed. Furthermore, embedding accountability reasoning into AI systems contributes to providing transparency on who is, and to what extent they are, accountable for potentially undesirable behaviour of a given AI-based product [Winfield and Jirotka, 2018].
In this work, we focused on teams of agents assuming their intra-team capacity to coordinate towards the fulfilment of tasks. An interesting extension would be to consider the feasibility of team formations based on the value of inter-agent interactions [Beal et al., 2020]. This way, we can reason about feasible team structures in presence of inter-agent incompatibilities and study their dynamics with the accountability ascription problem in multiagent teams.
This work was supported by the UK Engineering and Physical Sciences Research Council (EPSRC) through the Trustworthy Autonomous Systems Hub (EP/V00784X/1), the platform grant entitled “AutoTrust: Designing a Human-Centred Trusted, Secure, Intelligent and Usable Internet of Vehicles” (EP/R029563/1), and the Turing AI Fellowship on CitizenCentric AI Systems (EP/V022067/1).