Paper deep dive
Counterfactual Reasoning for Causal Responsibility Attribution in Probabilistic Multi-Agent Systems
Chunyan Mu, Muhammad Najib
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/8/2026, 2:49:56 PM
Summary
This paper introduces a formal framework for attributing causal responsibility in probabilistic multi-agent systems modeled as concurrent stochastic games. It defines retrospective counterfactual responsibility, quantifies it using the Shapley value to ensure fairness and consistency, extends PATL logic for verification, and computes Nash equilibrium strategy profiles where agents balance expected rewards against responsibility allocation.
Entities (8)
Relation Signals (6)
Counterfactual Responsibility → allocatedusing → Shapley Value
confidence 96% · To allocate responsibility among agents, we utilise the Shapley value
Multi-agent systems → modeledas → Concurrent Stochastic Game
confidence 95% · In this work, we model such systems as concurrent stochastic multi-player games
Shapley Value → satisfies → Fairness
confidence 94% · formally show that this method satisfies key desirable properties, including fairness
Shapley Value → satisfies → Consistency
confidence 94% · formally show that this method satisfies key desirable properties, including fairness and consistency.
Nash Equilibrium → enables → Strategic Reasoning
confidence 92% · by adopting Nash equilibrium as the solution concept, we demonstrate how to compute stable strategy profiles
PATL → extendedwith → Degree of Responsibility Operators
confidence 91% · we extend the logic PATL with cumulative reward (similar to rPATL) and introduce degree of responsibility operators.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Responsibility allocation -- determining the extent to which agents are accountable for outcomes -- is a fundamental challenge in the design and analysis of multi-agent systems. In this work, we model such systems as concurrent stochastic multi-player games and introduce a notion of retrospective (backward) counterfactual responsibility, which quantifies an agent's accountability for outcomes resulting from a given strategy profile. To allocate responsibility among agents, we utilise the Shapley value and formally show that this method satisfies key desirable properties, including fairness and consistency. Building on this foundation, we propose a formal framework that supports both verification and strategic reasoning in responsibility-aware multi-agent systems. Furthermore, by adopting Nash equilibrium as the solution concept, we demonstrate how to compute stable strategy profiles in which agents trade off responsibility against expected reward.
Tags
Links
- Source: https://arxiv.org/abs/2605.13077v1
- Canonical: https://arxiv.org/abs/2605.13077v1
PDF not stored locally. Use the link above to view on the source site.
Full Text
75,502 characters extracted from source content.
Expand or collapse full text
11institutetext: 1University of Aberdeen 2Heriot-Watt University Chunyan.Mu@abdn.ac.uk,M.Najib@hw.ac.uk Counterfactual Reasoning for Causal Responsibility Attribution in Probabilistic Multi-Agent Systems Chunyan Mu1 Muhammad Najib2 Abstract Responsibility allocation—determining the extent to which agents are accountable for outcomes—is a fundamental challenge in the design and analysis of multi-agent systems. In this work, we model such systems as concurrent stochastic multi-player games and introduce a notion of retrospective (backward) counterfactual responsibility, which quantifies an agent’s accountability for outcomes resulting from a given strategy profile. To allocate responsibility among agents, we utilise the Shapley value and formally show that this method satisfies key desirable properties, including fairness and consistency. Building on this foundation, we propose a formal framework that supports both verification and strategic reasoning in responsibility-aware multi-agent systems. Furthermore, by adopting Nash equilibrium as the solution concept, we demonstrate how to compute stable strategy profiles in which agents trade off responsibility against expected reward. 1 Introduction The growing emphasis on trustworthy AI [12, 35] necessitates a paradigm shift, particularly regarding responsibility and accountability [21, 29, 8]. To enable responsible behaviour in agents, they must be endowed with an awareness of responsibility. This motivated the notion of responsibility-aware agents [52, 30], which are assumed to consider not only their own rewards/payoffs but also the broader implications of their actions. In MAS setting, where agents interact and may collaborate, the problem of responsibility attribution becomes increasingly important. When multiple agents jointly bring about an outcome, how can we fairly attribute responsibility to each agent, taking into account their respective capability? To illustrate this challenge, consider the following example. Example 1 Consider two autonomous vehicles, A1A_1 and A2A_2, approaching an uncontrolled junction under snowy conditions. A1A_1 is travelling from east to west, A2A_2 from south to north. Each vehicle can either brake or not brake. If neither brakes, they will crash into each other. If both successfully brake (and stop), they will avoid a collision. However, due to the slippery road conditions, there is a 0.20.2 chance that A1A_1 will not be able to stop, and a 0.60.6 chance that A2A_2 will not be able to stop. Each vehicle aims to minimise its travel time to reach its destination. However, a crash would result in a significant cost. Suppose the outcome is a collision resulting from the agents’ chosen actions (or strategies), which vehicle should bear greater responsibility for the collision? Naturally, this depends on the strategies adopted during the interaction. However, responsibility may also hinge on the agents’ capabilities [24]. To illustrate, suppose that A2A_2 can guarantee stopping with certainty. If both agents adopt the same mixed strategy that includes a non-zero probability of not braking, and a collision occurs, it seems reasonable to assign greater responsibility to A2A_2, as it had the capability to avoid the collision entirely. Moreover, there is an inherent trade-off between minimising travel time and avoiding collisions. This creates a strategic decision-making problem in which agents must weigh their utility (e.g., travel time) against potential responsibility penalties for a collision. Given these considerations, some important questions arise: Given the strategy profiles and capabilities, how should responsibility be allocated?, If the agents are aware of responsibility attribution, how should they choose their strategies? In this paper, we aim to such questions. First, we study responsibility attribution through the lens of counterfactual reasoning, which evaluates an agent’s contribution by asking how the outcome would change if the agent had acted differently. We follow well-established accounts of causation in philosophy and AI, where counterfactuals capture “what would have happened otherwise” [15, 34, 41]. We then examine strategic reasoning for responsibility-aware agents—agents that weigh not only their expected rewards but also the potential responsibility they may incur. This perspective provides a framework for addressing the earlier question of (strategic) forward reasoning: how such agents should choose their strategies. Contribution Our main contribution is an approach for responsibility attribution in probabilistic multi-agent systems. Firstly, we introduce a formal framework based on the Shapley value [43] and show that the resulting allocations satisfy desirable properties such as fairness (responsibility reflects contribution) and consistency (an agent’s share does not decrease when its influence increas). Although we do not claim this to be a definitive account of responsibility, the framework is interpretable, and based on a concept used widely across disciplines. Our focus is not on formalising moral responsibility, an extremely complex area with no clear consensus, nevertheless, we believe that our approach can contribute toward such a formalisation. Secondly, we study strategic reasoning in the setting where agents employ randomised memoryless strategy (aka behavioural [18]), i.e., functions that map from state to a probability distribution over actions. Following the tradition of formal method in MAS, we extend the logic PATL with cumulative reward (similar to rPATL [32]) and introduce degree of responsibility operators. We show that model checking this logic remains in PSPACE, thus no harder than rPATL [33]. Finally, we present a method for computing Nash equilibrium strategy profiles where agents’ utility functions incorporate both reward and responsibility allocation. We show that when agents’ temporal objectives are specified as either reachability or safety conditions, these equilibria can also be computed in PSPACE. Related work Research on responsibility and attribution spans a large body of work; here, we highlight some relevant studies and key distinctions. Responsibility attribution is closely tied to causality and counterfactual reasoning. Foundational work by Halpern and Pearl [26] introduced structural causal models, which underpin formal definitions of causality and counterfactual dependence. Building on this, [15] proposed a quantitative notion of responsibility, which later extended to a notion of blame attribution [25]. While conceptually related to our approach, their framework relies on directed acyclic graphs and is primarily suited for reasoning about beliefs, intentions, and epistemic states, whereas our work focuses on temporally extended properties in strategic settings. The Shapley value has also been applied for responsibility allocation. [23] extends the structural-model approach [25] by incorporating the Shapley value to distribute blame, and demonstrating that the allocation scheme satisfies desirable properties. As previously discussed, their model differs from ours and is suited for different purposes. Similarly, [51] apply Shapley-based responsibility allocation in concurrent epistemic games, enabling epistemic modeling but under deterministic assumptions, in contrast to our probabilistic setting. [4] studies backward and forward responsibility in extensive-form games, while [5] employs parametric Markov chains (pMCs), which are closely related to our model. Memoryless strategy profiles naturally correspond to parameters assignements in a pMC, although the converse does not always hold111Some parameter assignments cannot be expressed as individual strategies; see [46, Remark 8]. We address this by imposing additional constraints in our parametric model (Section 7).. Furthermore, [5] primarily focuses on attributing changes to parameters, with its main concern being how variations in temporal satisfaction degrees should be attributed to changes in parameter assignments. In contrast, our work assigns responsibility to individual players. Closer to our work is [36], which uses concurrent stochastic games to reason about causal active and causal passive responsibilities, building on [40]. Their approach considers how strategies contribute to or prevent outcomes but does not employ counterfactual reasoning nor guarantee fair attribution. From temporal-logic perspective, [19] uses LTLf to represent outcomes—similar to ours—but focuses on a single agent from a first-person perspective, whereas our approach adopts a third-person, multi-agent view. Other related works include Naumov and Tao’s logical frameworks for blameworthiness and “seeing-to-it” responsibility [38, 37], as well as STIT‑based accounts [17, 20, 6, 1]. These differ from ours in both their underlying models and their conceptions of responsibility. In particular, STIT approaches define responsibility via an agent’s modal ability to “see to it that” an outcome occurs, whereas our framework evaluates responsibility through counterfactual dependence—what would happen were an agent to act differently—and seeks a fair quantitative attribution across agents. 2 Preliminaries 2.1 Concurrent stochastic game Definition 1 A concurrent stochastic multi-player game (CSG) is a tuple =(,S,s0,(i)i∈,δ,,L)G=( Ag,S,s^0,( Act_i)_i∈ Ag,δ, Ap,L) where: • =1,…,n Ag=\1,…,n\ is a finite set of agents; • S is a finite non-empty set of states; • s0∈Ss^0∈ S is the initial state; • i Act_i is a finite set of actions for i. With each agent i and state s∈Ss∈ S, we associate a non-empty set i(s) Act_i(s) of available actions that i can perform in s. Write =1×⋯×n Act Ag= Act_1×·s× Act_n. • Δ:S×→(S) :S× Act Ag→ Dist(S) is a probabilistic transition function; • Ap is a finite set of atomic propositions; • L:S→2L:S→ 2 Ap is the labelling function mapping each state to a set of atomic propositions drawn from Ap. Following [33], we augment CSGs with reward structures of the form r=(rs,ra)r=(r_s,r_a), where rs:S→ℝr_s:S is the state reward and ra:→ℝr_a: Act Ag is the action reward, and consider cumulative rewards, that is the sum of payoffs accumulated during the run until a specific point. s0s_0s1s_1s2s_2b¯1,b¯2 b_1, b_2b¯1,b2 b_1,b_2b1,b¯2b_1, b_2b1,b2b_1,b_2110.60.60.40.40.20.20.80.80.120.120.880.88∗,∗ , ∗,∗ , Figure 1: CSG model from the running example. Example 2 From the running example, we construct a model in Figure 1. With =1,2 Ag=\1,2\, representing A1A_1 and A2A_2. i=bi,b¯i Act_i=\b_i, b_i\ representing agent i∈i∈ Ag choosing to brake and not brake. s0s_0 is the initial state, and L(s1)=crash,L(s0)=init,L(s2)=passL(s_1)=\ crash\,L(s_0)=\ init\,L(s_2)=\ pass\. Note that from s1s_1 and s2s_2, there are only self-loops. Definition 2 A path π is a non-empty sequence s0a→0s1a→1…s_0 a^0s_1 a^1… of states and joint actions, where a→i∈ a^i∈ Act Ag is the ithi^th joint action, and Δ(si,a→i,si+1)>0 (s_i, a^i,s_i+1)>0. A history ρ is a finite path, ρs(i) _s(i) denotes the ithi^th state of ρ, and ρa→(i) _ a(i) denotes the ithi^th joint action of ρ. In this case, we may write ρs(i)⟶ρa→(i)ρs(i+1) _s(i) _ a(i) _s(i+1). Let (s) Hist_G(s) denote the set of histories of G starting from state s. We write (s)≤k Hist_G(s)^≤ k to denote the set of histories up to and including ρs(k) _s(k). In this work, we assume that players have memoryless strategies. Informally, a memoryless strategy for player i prescribes, from each state s, the probability of each action a∈i(s)a∈ Act_i(s) being chosen. Definition 3 A (memoryless) strategy for i is a function from the set of states to a probability distribution over agent’s set of actions σi:S→(i) _i:S→ Dist( Act_i). A strategy profile is a tuple of strategies for a set of agents, it is denoted by σ→=(σ1,σ2,…,σn) σ=( _1, _2,…, _n). For a set (or coalition) of agents J⊆J Ag, write σ→J σ_J for (σi)i∈J( _i)_i∈ J. Note that a strategy profile σ→ σ for a game G resolves nondeterminism in the game arena. Denote by σ→G_ σ the resulting game arena (essentially, a Markov chain) after applying σ→ σ. Definition 4 A state s and a strategy profile σ→ σ induce a set of histories s0a→0s1a→1…s_0 a^0s_1 a^1…, with ℙ(a→i)⋅Δ(si,a→i,si+1)>0P( a^i)· (s_i, a^i,s_i+1)>0 and s=s0s=s_0, denoted by σ→(s) Hist_ σ(s). For a history ρ∈σ→(s)≤kρ∈ Hist_ σ(s)^≤ k, the probability of ρ=s0⟶a→0s1…⟶a→k−1skρ=s_0 a^0 s_1… a^k-1 s_k, with s0=s_0=s, is given by: ℙ(ρ)≜∏j=1k−1(∏i=1n(σi(sj)(a→ij)))P(ρ) Π^k-1_j=1 (Π^n_i=1 ( _i(s_j)( a^j_i) ) ) For a subset of agents J⊆J Ag and strategies σ→J σ_J, we say that a history ρ is compatible with σ→J σ_J if for every k∈ℕk , there exists a joint action a→k a^k with σi(ρs(k))(a→ik)>0 _i( _s(k))( a^k_i)>0 for each i∈Ji∈ J, such that Δ(sk,a→k,sk+1)>0 (s_k, a^k,s_k+1)>0. We denote by σ→J(s) Hist_ σ_J(s) the set of histories starting from s and compatible with σ→J σ_J that can be induced by memoryless strategies. Definition 5 The payoff function defined as a map from a set of histories to a real value ℘:(s)→ℝ|| : Hist_G(s) ^| Ag|. ℘i ^i denotes the payoff function of i∈i∈ Ag and is defined as: ℘i(ρ)≜(∑j=0t−1(rai(a→j)+rsi(sj))⋅Δ(sj,a→j,sj+1)) ^i(ρ) (Σ^t-1_j=0(r^i_a( a^j)+r^i_s(s_j))· (s_j, a^j,s_j+1) ) where ρ=s0⟶a→0s1⟶a→1…⟶a→t−1st∈(s0)ρ=s_0 a^0 s_1 a^1 … a^t-1 s_t∈ Hist_G(s_0). 2.2 PATL PATL [14] is a logic for reasoning about the strategic abilities of (coalitions of) agents in probabilistic systems. In this paper, we consider PATL with bounded temporal properties. Definition 6(Syntax of PATL) The state formulae (ϕφ) and path formulae (ψ) are defined as follows: ϕ::=a∣¬ϕ∣∣ϕ∧ϕ∣⟨A⟩⋈p[ψ]ψ::=○ϕ∣(ϕ≤kϕ) array[]lclφ&::=&a\ -3.0pt \ φ\ -3.0pt \ φ φ\ -3.0pt \ A _ p[ψ]\\ ψ&::=& φ\ -3.0pt \ ( _≤ kφ) array where a∈a∈ Ap is an atomic proposition, A⊆A Ag is a set of agents, ⋈∈≤,<,≥,> ∈\≤,<,≥,>\, p∈[0,1]p∈[0,1], k∈ℕk is a time bound, and ⟨A⟩ A is the strategy quantifier. The until operator U allows one to derive the temporal modalities ◇ (“eventually”) and □ (“always”): ◇≤kψ≜≤kψ _≤ kψ true~U_≤ k~ψ and □≤kψ≜¬◇≤k(¬ψ) _≤ kψ _≤ k( ψ). Definition 7(Semantics of PATL) The satisfaction relation for a CSG G, state s∈Ss∈ S, history ρ, atom a∈a∈ Ap, and PATL formula is defined as follows: • s⊧as a iff a∈L(s)a∈ L(s). • s⊧¬ϕs φ iff s⊧̸ϕs φ. • s⊧ϕ∧ϕ′s φ φ iff s⊧ϕs φ and s⊧ϕ′s φ . • s⊧⟨A⟩⋈p[ψ]s A _ p[ψ] iff ∃σ→A.∀σ→−A.(ℙ(ρ∈(σ→A,σ→−A)(s)∣ρ⊧ψ)⋈p)∃ σ_A.∀ σ_-A.(P(\ρ∈ Hist_( σ_A, σ_-A)(s) ρ ψ\) p). • ρ⊧○ϕρ φ iff ρs(1)⊧ϕ _s(1) φ. • ρ⊧ϕ≤kϕ′ρ _≤ kφ iff there exists i≤ki≤ k such that: ρs(i)⊧ϕ′ _s(i) φ , and ρs(j)⊧ϕ _s(j) φ for all j<ij<i. We say that formula φ is true in a CGS G iff s0⊧φs^0 . 3 Formalising Counterfactual Responsibility Attribution We build on the concept of Necessary Element of a Sufficient Set (NESS) test [50], which has been used in many game-theoretic frameworks (e.g., [10, 6, 40]), and adapt it to our setting. Definition 8 Given a CSG G, we say that agent i bears backward Counterfactual Responsibility (bCR) in a strategy profile σ→ σ for outcome φ , specified in a PATL path formula, written as i∼φσ→i bCR σ_ , if the following conditions hold: ∃J⊆∖i∃ J Ag \i\ such that ∃ρ′∈σ→J(s0).ρ′⊧̸φ∃ρ ∈ Hist_ σ_J(s^0).ρ and ∀ρ′∈σ→J∪i(s0).ρ′⊧φ∀ρ ∈ Hist_ σ_J∪\i\(s^0).ρ . In words, agent i is responsible for an outcome φ under strategy profile σ→ σ, if it belongs to some coalition J∪iJ∪\i\ whose joint strategies are sufficient to guarantee φ , while the strategies of J (without i) are not. That is, counterfactually, changing i’s strategy could have prevented φ . In the definition above, bCR is a qualitative notion: i either bears responsibility or does not. Our aim is to extend this to a quantitative setting by determining “how much” responsibility agent i bears. Intuitively, this corresponds to measuring i’s marginal contribution to increasing the likelihood/probability of satisfying φ . To this end, we allocate responsibility using the Shapley value. A challenge arises when measuring the marginal contribution of a coalition that does not contain all agents (i.e., non-grand coalition) since the strategies of agents outside that coalition are undefined. We address this by assuming that φ is an undesirable outcome that agents (retrospectively) would prefer to avoid. Thus, when computing marginal contributions, we assume that agents outside the coalition act so as to minimise the probability of satisfying φ 222Although we use “minimise” when defining the strategies of agents outside the coalition, one could instead use “‘maximise” when φ represents a desirable outcome. We conjecture that the properties established in the next section would similarly hold.. Definition 9 Given a bound333This bound comes from the PATL path formula φ . k∈ℕk , the degree of i bearing bCR in σ→ σ for φ is defined as: i(σ→,φ)=∑J⊆∖i|J|!(||−|J|−1)!||!⋅(vσ→,φ(J∪i)−vσ→,φ(J))D^i( σ, )= _J Ag \i\ |J|!(| Ag|-|J|-1)!| Ag|!·(v_ σ, (J∪\i\)-v_ σ, (J)). For any A⊆A Ag, the function vσ→,φ(A)v_ σ, (A) for the k-bounded histories is defined as: vσ→,φ(A)=minσ→−A(ρ∣ρ∈(σ→A,σ→−A)(s0)≤k∧ρ⊧φ)v_ σ, (A)= _ σ_-A Prob(\ρ ρ∈ Hist_( σ_A, σ_-A)(s^0)^≤ k ρ \) Intuitively, the definition of vσ→,φ(A)v_ σ, (A) assumes that the other players are actively trying to minimise the occurrence of φ . This reflects the principle of alternative possibilities and counterfactual reasoning [22, 9, 48, 44]: an agent is considered responsible for an outcome φ under a strategy profile σ→ σ if φ occurs under this strategy profile, and the agent had some alternative strategy that could have prevented φ . Remark 1 We note that whilst min is used for calculating vσ→,φ(A)v_ σ, (A), one may also define it using max when considering φ as a “desirable” outcome. We conjecture that the properties in Section 4 would also hold. Example 3 Continuing the running example, suppose given an outcome φ:=○crash := crash (i.e., crash in the next time-step), and consider the strategy profile σ→ σ corresponding to each agent choosing not to brake with probability of 11. In this case, we obtain: vσ→,φ(1,2) v_ σ, (\1,2\) =1,vσ→,φ(1)=0.6 =1, v_ σ, (\1\)=0.6 vσ→,φ(2) v_ σ, (\2\) =0.2,vσ→,φ(∅)=0.12 =0.2, v_ σ, ( )=0.12 Therefore: 1(σ→,φ) ^1( σ, ) =12⋅(0.6−0.12)+12⋅(1−0.2)=0.64 = 12·(0.6-0.12)+ 12·(1-0.2)=0.64 2(σ→,φ) ^2( σ, ) =12⋅(0.2−0.12)+12⋅(1−0.6)=0.24 = 12·(0.2-0.12)+ 12·(1-0.6)=0.24 Note that A1A_1 has a higher degree of responsibility than A2A_2, intuitively, because A1A_1 has a greater chance of being able to stop (i.e., 0.80.8, compared to 0.40.4 for A2A_2). 4 Desirable Properties In this section, we demonstrate the desirable properties of our responsibility attribution: efficiency, symmetry, null/dummy player, additivity, and monotonicity. To formalise this, we first introduce the notion of attributable value, which represents the total amount of responsibility available for distribution among agents. The attributable value for a strategy profile is the difference between the probability of φ occurring under the strategy profile and the minimum probability achievable if agents act optimally (together) to prevent φ . To illustrate, consider an autonomous vehicle agent i approaching a T-junction. It can turn left or right. Turning left guarantees arriving late (probability 1), while turning right carries a 0.2 probability of lateness. Here, lateness is inevitable with at least a 0.2 probability. Suppose the vehicle adopts a strategy profile of turning left with certainty (probability 1). The attributable value is 1−0.2=0.81-0.2=0.8, meaning the maximum responsibility assignable to i is 0.80.8. Definition 10 Given a strategy profile σ→ σ, an outcome φ , and a bound k∈ℕk , the attributable value of φ w.r.t. σ→ σ is defined as: Υ(σ→,φ)=vσ→,φ()−minσ→(ρ∣ρ∈σ→(s0)≤k∧ρ⊧φ) ( σ, )=v_ σ, ( Ag)- _ σ Prob(\ρ ρ∈ Hist_ σ(s^0)^≤ k ρ \). By Definition 9, we have that: vσ→,φ(∅)=minσ→−∅(ρ∣ρ∈σ→(s0)≤k∧ρ⊧φv_ σ, ( )= _ σ_- Prob(\ρ ρ∈ Hist_ σ(s^0)^≤ k ρ \ and since ∖∅= Ag = Ag, therefore σ→=σ→ σ_ Ag= σ, and we immediately obtain the following lemma. Lemma 1 For a strategy profile σ→ σ and outcome φ , it holds: Υ(σ→,φ)=vσ→,φ()−vσ→,φ(∅) ( σ, )=v_ σ, ( Ag)-v_ σ, ( ) Proof From the definition of attributable value and bCR degree, we have that: vσ→,φ(∅)=minσ→−∅(ρ∣ρ∈σ→(s0)≤k∧ρ⊧φv_ σ, ( )= _ σ_- Prob(\ρ ρ∈ Hist_ σ(s^0)^≤ k ρ \ and since ∖∅= Ag = Ag, therefore σ→=σ→ σ_ Ag= σ, and we immediately obtain the lemma. Example 4 Consider Example 3, the attributable value is: Υ(σ→,φ)=vσ→,φ()−vσ→,φ(∅)=1−0.12=0.88 ( σ, )=v_ σ, ( Ag)-v_ σ, ( )=1-0.12=0.88 Fairness The first three properties relate to fairness. Efficiency guarantees that the sum of assigned responsibility values equals the attributable value, ensuring no unassigned responsibility remains. Conversely, it also ensures that the distributed responsibility does not exceed the attributable value, preventing any agent from bearing excess responsibility. Symmetry ensures that two agents with identical contributions to an outcome receive equal degrees of responsibility. The dummy/null player property ensures that agents who do not contribute to an outcome receive zero responsibility. Proposition 1(Efficiency) For a strategy profile σ→ σ and outcome φ , it holds that: ∑i∈i(σ→,φ)=Υ(σ→,φ). _i∈ AgD^i( σ, )= ( σ, ). Proof ∑i∈i(σ→,φ) _i∈ AgD^i( σ, ) =∑i∈∑J⊆∖i|J|!(||−|J|−1)!||!⋅(vσ→,φ(J∪i)−vσ→,φ(J)) = _i∈ Ag _J Ag \i\ |J|!(| Ag|-|J|-1)!| Ag|!·(v_ σ, (J∪\i\)-v_ σ, (J)) =∑J⊆∑i∈∖J|J|!(||−|J|−1)!||!⋅(vσ→,φ(J∪i)−vσ→,φ(J)) = _J Ag _i∈ Ag J |J|!(| Ag|-|J|-1)!| Ag|!·(v_ σ, (J∪\i\)-v_ σ, (J)) Since for each subset J the term |J|!(||−|J|−1)!||! |J|!(| Ag|-|J|-1)!| Ag|! is the same for each player i not in J, and there are ||−|J|| Ag|-|J| such players, thus we can simplify the inner sum: ∑i∈i(σ→,φ) _i∈ AgD^i( σ, ) =∑J⊆|J|!(||−|J|−1)!||!∑i∈∖J(vσ→,φ(J∪i)−vσ→,φ(J)) = _J Ag |J|!(| Ag|-|J|-1)!| Ag|! _i∈ Ag J(v_ σ, (J∪\i\)-v_ σ, (J)) Observe that the expression ∑i∈∖J(vσ→,φ(J∪i)−vσ→,φ(J)) _i∈ Ag J(v_ σ, (J∪\i\)-v_ σ, (J)) is a telescoping series/sum with respect to all subsets J, thus we can simplify the inner sum further and obtain: ∑i∈i(σ→,φ)=∑J⊆|J|!(||−|J|−1)!||!⋅(vσ→,φ()−vσ→,φ(∅)) _i∈ AgD^i( σ, )= _J Ag |J|!(| Ag|-|J|-1)!| Ag|!· (v_ σ, ( Ag)-v_ σ, ( ) ). Since ∑J⊆|J|!(||−|J|−1)!||!=1 _J Ag |J|!(| Ag|-|J|-1)!| Ag|!=1, we have: ∑i∈i(σ→,φ) _i∈ AgD^i( σ, ) =vσ→,φ()−vσ→,φ(∅). =v_ σ, ( Ag)-v_ σ, ( ). By Lemma 1, we obtain: ∑i∈i(σ→,φ) _i∈ AgD^i( σ, ) =Υ(σ→,φ). = ( σ, ). Example 5 Consider again Example 3 and 4, note that: ∑i∈i(σ→,φ)=0.64+0.24=Υ(σ→,φ)=0.88 _i∈ AgD^i( σ, )=0.64+0.24= ( σ, )=0.88 Symmetry ensures that two agents with identical contributions towards an outcome will receive equal degrees of individual responsibility. Proposition 2(Symmetry) For two agents i,j∈i,j∈ Ag, if: ∀J⊆∖i,j,vσ→,φ(J∪i)=vσ→,φ(J∪j)∀ J Ag \i,j\,v_ σ, (J∪\i\)=v_ σ, (J∪\j\) then: i(σ→,φ)=j(σ→,φ)D^i( σ, )=D^j( σ, ) Proof To prove this claim, we first introduce some notations. Denote by Π() ( Ag) the set of all permutations of Ag. For every permutation π∈Π()π∈ ( Ag), define Pi(π):=j∈:π(j)<π(i),P_i(π):=\j∈ Ag:π(j)<π(i)\, that is the set of agents ahead of agent i when they are ordered according to permutation π. Using an alternative formulation for the Shapley value, we can express the bCR degree as follows. i(σ→,φ)=1||!∑π∈Π()(vσ→,φ(Pi(π)∪i)−vσ→,φ(Pi(π)))D^i( σ, )= 1| Ag|! _π∈ ( Ag) (v_ σ, (P_i(π)∪\i\)-v_ σ, (P_i(π)) ) (1) Define a function f:Π()→Π()f: ( Ag)→ ( Ag) that maps each permutation over the set of agents to another permutation as follows. For every permutation π, the permutation f(π)f(π) is identical to π except that it swaps agent i with agent j. Next we show that the following holds. vσ→,φ(Pi(π)∪i)−vσ→,φ(Pi(π))=vσ→,φ(Pj(f(π))∪j)−vσ→,φ(Pj(f(π)))v_ σ, (P_i(π)∪\i\)-v_ σ, (P_i(π))=v_ σ, (P_j(f(π))∪\j\)-v_ σ, (P_j(f(π))) (2) There are two possible cases: Case 1: agent i appears before agent j under permutation π, i.e., j∉Pi(π)j ∈ P_i(π). Then Pi(π)=Pj(f(π))P_i(π)=P_j(f(π)), as such, vσ→,φ(Pi(π))=vσ→,φ(Pj(f(π)))v_ σ, (P_i(π))=v_ σ, (P_j(f(π))). Morever, since both Pi(π)P_i(π) and Pj(f(π))P_j(f(π)) do not contain i nor j, it holds that: vσ→,φ(Pi(π)∪i)=vσ→,φ(Pj(f(π))∪j)v_ σ, (P_i(π)∪\i\)=v_ σ, (P_j(f(π))∪\j\) Therefore, these two equalities imply Equation 2. Case 2: agent i appears after agent j under permutation π, i.e., j∈Pi(π)j∈ P_i(π). Then Pi(π)∪i=Pj(f(π))∪jP_i(π)∪\i\=P_j(f(π))∪\j\, as such, vσ→,φ(Pi(π)∪i)=vσ→,φ(Pj(f(π))∪j)v_ σ, (P_i(π)∪\i\)=v_ σ, (P_j(f(π))∪\j\). Moreover, Pi(π)∖j=Pj(f(π))∖iP_i(π) \j\=P_j(f(π)) \i\, and since i and j are symmetric, it holds that: vσ→,φ((Pi(π)∖j)∪j)=vσ→,φ((Pj(f(π))∖i)∪i),v_ σ, ((P_i(π) \j\)∪\j\)=v_ σ, ((P_j(f(π)) \i\)∪\i\), i.e., vσ→,φ(Pi(π))=vσ→,φ(Pj(f(π)))v_ σ, (P_i(π))=v_ σ, (P_j(f(π))). Therefore, these two equalities also imply Equation 2. From Equation 1 and Equation 2, we have i(σ→,φ)=1||!∑π∈Π()(vσ→,φ(Pj(f(π))∪j)−vσ→,φ(Pj(f(π))))D^i( σ, )= 1| Ag|! _π∈ ( Ag) (v_ σ, (P_j(f(π))∪\j\)-v_ σ, (P_j(f(π))) ) (3) Since f is bijective, thus Π()=f(π):π∈Π() ( Ag)=\f(π):π∈ ( Ag)\, and by setting μ=f(π)μ=f(π) we obtain i(σ→,φ)=1||!∑μ∈Π()(vσ→,φ(Pj(μ)∪j)−vσ→,φ(Pj(μ)))D^i( σ, )= 1| Ag|! _μ∈ ( Ag) (v_ σ, (P_j(μ)∪\j\)-v_ σ, (P_j(μ)) ) (4) And, consequently i(σ→,φ)=j(σ→,φ)D^i( σ, )=D^j( σ, ). The dummy/null player property guarantees that agents who do not contribute towards an outcome will not receive any responsibility degree values. Proposition 3(Null Player) If for all J⊆∖i:vσ→,φ(J∪i)=vσ→,φ(J)J Ag \i\:v_ σ, (J∪\i\)=v_ σ, (J), then i(σ→,φ)=0D^i( σ, )=0. Proof If for a given J⊆∖i:vσ→,φ(J∪i)=vσ→,φ(J)J Ag \i\:v_ σ, (J∪\i\)=v_ σ, (J), then we have (vσ→,φ(J∪i)−vσ→,φ(J))=0(v_ σ, (J∪\i\)-v_ σ, (J))=0. Since it holds for every J∈∖iJ∈ Ag \i\, then i(σ→,φ) ^i( σ, ) =∑J⊆∖i|J|!(||−|J|−1)!||!⋅0=0. = _J Ag \i\ |J|!(| Ag|-|J|-1)!| Ag|!· 0=0. Consistency Additivity property states that for two independent games, the Shapley value of the combined game is equal to the sum of individual values. However, this raises the question of how to combine the games and to what extent they are truly independent444There have been many attempts to relax the additivity axiom, e.g. [53, 27, 16, 47]., particularly, in our setting. One could define this by considering two separate CSGs, resulting in a “combined” responsibility degree that is simply the sum of the two games. However, we find this approach uninteresting and not particularly useful. Instead, we consider additivity with respect to disjunctions of outcomes φ1∨φ2 _1 _2. Observe that the function i(⋅,⋅)D^i(·,·) is generally not additive. To see this, consider φ1:=φ _1:= and φ2:=¬φ _2:= . Clearly, for any σ→ σ, i(σ→,φ1∨φ2)=0D^i( σ, _1 _2)=0, while it may be the case that i(σ→,φ1)>0D^i( σ, _1)>0 or i(σ→,φ2)>0D^i( σ, _2)>0. However, we can show that subadditivity holds, and for a special case of outcomes we obtain (exact) additivity. Monotonicity intuitively states that for two outcomes φ1 _1 and φ2 _2, where φ1 _1 is “included” in φ2 _2, the degree of responsibility for φ2 _2 would likely increase. Additivity and monotonicity relate to consistency in the sense that if we expand the outcome (under certain conditions), then responsibility should increase or at least not decrease. Proposition 4(Sub-additivity) Given σ→ σ, for any two outcome φ1 _1 and φ2 _2, and any i∈i∈ Ag: i(σ→,φ1∨φ2)≤i(σ→,φ1)+i(σ→,φ2)D^i( σ, _1 _2) ^i( σ, _1)+D^i( σ, _2) Proof For any fixed coalition A⊆A Ag and any strategy profile (σ→A,σ→−A)( σ_A, σ_-A), we have: (ρ∣ρ∈(σ→A,σ→−A)(s0)≤k∧ρ⊧(φ1∨φ2))≤((ρ∣ρ∈(σ→A,σ→−A)(s0)≤k∧ρ⊧φ1)+(ρ∣ρ∈(σ→A,σ→−A)(s0)≤k∧ρ⊧φ2))\ Prob(\ρ ρ∈ Hist_( σ_A, σ_-A)(s^0)^≤ k ρ ( _1 _2)\)\\ ≤\ ( Prob(\ρ ρ∈ Hist_( σ_A, σ_-A)(s^0)^≤ k ρ _1\)\\ \ + Prob(\ρ ρ∈ Hist_( σ_A, σ_-A)(s^0)^≤ k ρ _2\) ) (5) Since the value of the sum at the joint minimiser is no more than the sum of the individual minima, which may occur at different points: minx[f(x)+g(x)]≤minxf(x)+minxg(x) _x[f(x)+g(x)]≤ _xf(x)+ _xg(x) taking the minimum over σ→−A σ_-A on both sides of Equation 5, we have: vσ→,φ1∨φ2(A)≤vσ→,φ1(A)+vσ→,φ2(A)for all A⊆v_ σ, _1 _2(A)≤ v_ σ, _1(A)+v_ σ, _2(A) all A Ag By monotonicity of the Shapley value under pointwise function, we obtain the result. Intuitively, this holds because the worst-case probabilities for φ1∨φ2 _1 _2 may overlap, so responsibility for the disjunction can be “shared” or even “cheaper” than addressing both outcomes individually. Example 6 Continue the running example, suppose given outcomes φ1=○crash _1= \ crash and φ2=○pass _2= \ pass, consider σ→ σ corresponding to each agent choosing to brake with probability of 1, let ∨ denote φ1∨φ2 _1 _2 for short. In this case, we have: vσ→,φ1(1,2)=vσ→,φ1(1)=vσ→,φ1(2)=vσ→,φ1(∅)=0.12, v_ σ,\! _1\!(\1,2\)\!=\!v_ σ,\! _1\!(\1\)\!=\!v_ σ,\! _1\!(\2\)\!=\!v_ σ,\! _1\!( )=0.12, vσ→,φ2(1,2)=0.88,vσ→,φ2(1)=0.8, v_ σ, _2(\1,2\)=0.88, v_ σ, _2(\1\)=0.8, vσ→,φ2(2)=0.4,vσ→,φ2(∅)=0, v_ σ, _2(\2\)=0.4, v_ σ, _2( )=0, vσ→,∨(1,2)=vσ→,∨(1)=vσ→,∨(2)=vσ→,∨(∅)=0.12 v_ σ, (\1,2\)=v_ σ, (\1\)=v_ σ, (\2\)=v_ σ, ( )=0.12 Thus: 1(σ→,φ1) ^1( σ, _1) =2(σ→,φ1)=0, =D^2( σ, _1)=0, 1(σ→,φ2) ^1( σ, _2) =0.64,2(σ→,φ2)=0.24, =0.64,\ D^2( σ, _2)=0.24, 1(σ→,φ1∨φ2) ^1( σ, _1 _2) =2(σ→,φ1∨φ2)=0 =D^2( σ, _1 _2)=0 Clearly, for i=1,2:i=\1,2\: i(σ→,φ1∨φ2)≤i(σ→,φ1)+i(σ→,φ2)D^i( σ, _1 _2) ^i( σ, _1)+D^i( σ, _2). To obtain exact additivity, we define the following conditions. Definition 11 For two outcomes φ1 _1 and φ2 _2, we say that they are disjoint and avoidable, respectively, if i) for all σ→ σ, we have (ρ∣ρ∈σ→(s0)≤k∧ρ⊧φ1∧φ2)=0 Prob(\ρ ρ∈ Hist_ σ(s^0)^≤ k ρ _1 _2\)=0 i) there exists σ→ σ, such that (ρ∣ρ∈σ→(s0)ρ⊧(φ1∨φ2))<1 Prob(\ρ ρ∈ Hist_ σ(s^0)ρ ( _1 _2)\)<1. Proposition 5(Exact Additivity) Let φ1 _1 and φ2 _2 be two outcome formulas such that they are disjoint and avoidable, then for any i∈i∈ Ag: i(σ→,φ1∨φ2)=i(σ→,φ1)+i(σ→,φ2)D^i( σ, _1 _2)=D^i( σ, _1)+D^i( σ, _2) Proof By the disjointness assumption on φ1 _1 and φ2 _2, and the standard property of probability over disjoint events, we have: (ρ∣ρ∈σ→A,σ→−A(s0)≤k∧ρ⊧(φ1∨φ2))=(ρ∣ρ∈σ→A,σ→−A(s0)≤k∧ρ⊧φ1)+(ρ∣ρ∈σ→A,σ→−A(s0)≤k∧ρ⊧φ2)\ Prob(\ρ ρ∈ Hist_ σ_A, σ_-A(s^0)^≤ k ρ ( _1 _2)\)\\ =\ Prob(\ρ ρ∈ Hist_ σ_A, σ_-A(s^0)^≤ k ρ _1\)\\ \ + Prob(\ρ ρ∈ Hist_ σ_A, σ_-A(s^0)^≤ k ρ _2\) (6) Applying the pessimistic valuation to both sides of Equation 6, we obtain: vσ→,φ1∨φ2(A)≥vσ→,φ1(A)+vσ→,φ2(A)for all A⊆v_ σ, _1 _2(A)≥ v_ σ, _1(A)+v_ σ, _2(A) all A Ag Since φ1∨φ2 _1 _2 is avoidable (thus i(σ→,φ1∨φ2)>0D^i( σ, _1 _2)>0) by the assumption, by monotonicity of the Shapley value under pointwise function, we have: i(σ→,φ1∨φ2)≥i(σ→,φ1)+i(σ→,φ2)D^i( σ, _1 _2) ^i( σ, _1)+D^i( σ, _2) By combining with Proposition 4, we obtain the proposition. Intuitively, when outcomes are disjoint, preventing either one contributes uniquely to the disjunction. This prevents overlap in marginal contributions and can make the total responsibility grow. Example 7 Note that the scenario proposed in Example 6 does not satisfy Proposition 5, as it meets assumption i) but violates assumption i). Proposition 6(Monotonicity) If φ1⇒φ2 _1 _2 and φ2 _2 is avoidable, then for any i∈i∈ Ag and a given σ→ σ: i(σ→,φ1)≤i(σ→,φ2)D^i( σ, _1) ^i( σ, _2) Proof For every coalition A⊆A Ag, and any strategy profile (σ→A,σ→−A)( σ_A, σ_-A), the implication φ1⇒φ2 _1 _2 ensures: (ρ∣ρ∈σ→A,σ→−A(s0)≤k∧ρ⊧φ1) Prob(\ρ ρ∈ Hist_ σ_A, σ_-A(s^0)^≤ k ρ _1\) ≤ ≤ (ρ∣ρ∈σ→A,σ→−A(s0)≤k∧ρ⊧φ2) Prob(\ρ ρ∈ Hist_ σ_A, σ_-A(s^0)^≤ k ρ _2\) Therefore, taking the minimum over σ→−A σ_-A, we get: vσ→,φ1(A)≤vσ→,φ2(A)for all A⊆v_ σ, _1(A)≤ v_ σ, _2(A) all A Ag Since φ2 _2 is avoidable (thus i(σ→,φ2)>0D^i( σ, _2)>0) by the assumption, and the Shapley value is monotonic under pointwise comparison of value functions, it follows that: i(σ→,φ1)≤i(σ→,φ2).D^i( σ, _1) ^i( σ, _2). Intuitively, responsibility should not decrease when the outcome becomes more inclusive - any trace satisfying φ1 _1 also satisfies φ2 _2, so agents influencing φ1 _1 also influencing φ2 _2, potentially to a greater extent. Example 8 Continue the running example, consider φ1=○crash _1= crash and φ2=◇≤2crash _2= _≤ 2\ crash and σ→ σ corresponding to each agent choosing not to brake with probability of 1. Clearly, in this case, φ1⇒φ2 _1 _2 and φ2 _2 is avoidable. We have: 1(σ→,φ1)=1(σ→,φ2)=0.64D^1( σ, _1)=D^1( σ, _2)=0.64, 2(σ→,φ1)=2(σ→,φ2)=0.24D^2( σ, _1)=D^2( σ, _2)=0.24. We have “==” specifically here as there is only a self-loop from s1s_1. 5 Logic with CR attributions: PATL-SR We introduce PATL-SR, a variant of PATL that incorporates quantified reward and responsibility attribution formulae as defined in Definition 9. Definition 12 The syntax of PATL-SR is made up of state formulae and history formulae represented by ϕφ and ψ, respectively. ϕ::=a∣¬ϕ∣∣ϕ∧ϕ∣∣⟨A⟩⋈p[ψ]∣∣⟨A⟩⋈q[ψ]∣⟨A⟩⋈d[i(σ→,ψ)]ψ::=○ϕ∣ϕ≤kϕ array[]lclφ&::=&a\ -3.0pt \ φ\ -3.0pt \ φ φ\ -3.0pt \ A _ p[ψ]\ -3.0pt \ A _ q[ψ]\ -3.0pt \\ && A _ d[ bCR_i( σ,ψ)]\\ ψ&::=& φ\ -3.0pt \ _≤ kφ array q,d∈ℝq,d are reward and responsibility degree bounds, respectively. The formula ⟨A⟩⋈q[◇≤kψ] A _ q\ [ _≤ kψ] expresses that the coalition A has a strategy such that the expected rewards of satisfying path formula ψ is ⋈q q when the strategy is followed. The formula ⟨A⟩⋈d[i(σ→,ψ)] A _ d\ [ bCR_i( σ,ψ)] expresses that, under strategy profile σ→ σ, the backward counterfactual responsibility of i in ensuring ψ within coalition A is quantified by ⋈d d. Definition 13 Given a model G, semantics for PATL-SR are interpreted as follows. For a state s∈Ss∈ S of ℳM, the satisfaction relation s⊧ϕs φ for state formula denotes “s satisfies ϕφ”: • s⊧as a iff a∈L(s)a∈ L(s). • s⊧¬ϕs φ iff s⊧̸ϕs φ. • s⊧ϕ∧ϕ′s φ φ iff s⊧ϕs φ and s⊧ϕ′s φ . • s⊧⟨A⟩⋈p[ψ]s A _ p[ψ] iff ∃σ→A.∀σ→−A.(ℙ(ρ∈(σ→A,σ→−A)(s)∣ρ⊧ψ)⋈p)∃ σ_A.∀ σ_-A.(P(\ρ∈ Hist_( σ_A, σ_-A)(s) ρ ψ\) p). • s⊧⟨A⟩⋈q[ψ]s A _ q[ψ] iff there exists a strategy profile of coalition A such that the expected accumulated reward of paths from state s which are consistent with the strategy and satisfy ψ is ⋈q q, i.e., ∃σ→A.σ→A(s,(r,ψ))⋈q∃ σ_A.E σ_A_G (s, rew(r,ψ) ) q, where: (r,ψ)(ρ)=∑i=0k(ra(ρa(i))+rs(ρs(i)))if ρ⊧ψ;0otherwise rew(r,ψ)(ρ)= \ array[]lΣ^k_i=0(r_a( _a(i))+r_s( _s(i)))&if ρ ψ;\\ 0&otherwise array . where k denotes the time bound of ψ. • s⊧⟨A⟩⋈d[i(σ→,ψ)]s A _ d[ bCR_i( σ,ψ)] iff i(σ→A,ψ)⋈dD^i( σ_A,ψ) d, where: i(σ→A,ψ)=∑J⊆A∖i|J|!(|A|−|J|−1)|A|!⋅(vσ→A,ψ(J∪i)−vσ→A,ψ(i)).D^i( σ_A,ψ)= _J A \i\ |J|!(|A|-|J|-1)|A|!·(v_ σ_A,ψ(J∪\i\)-v_ σ_A,ψ(\i\)). For a history ρ∈ℳ(s0)ρ∈ Hist_M(s_0), the satisfaction relation ρ⊧ψρ ψ for a path formula ψ denotes that “ρ satisfies ψ”: • ρ⊧○ϕρ φ iff ρs(1)⊧ϕ _s(1) φ. • ρ⊧ϕ≤kϕ′ρ _≤ kφ iff there exists i≤ki≤ k such that: ρs(i)⊧ϕ′ _s(i) φ , and ρs(j)⊧ϕ _s(j) φ for all j<ij<i. Example 9 Consider our running example with the outcome that “a crash takes place within 2 time steps”, which can be expressed by: ψ=⟨1,2⟩◇≤2crashψ= \1,2\ _≤ 2\ crash. Suppose 11 and 22 both choose to brake under σ→ σ, thus: vσ→,ψ(1,2)=vσ→,ψ(1)=vσ→,ψ(2)=vσ→,ψ(∅)=0.12v_ σ,ψ(\1,2\)=v_ σ,ψ(\1\)=v_ σ,ψ(\2\)=v_ σ,ψ( )=0.12, and thus 1(σ→,ψ)=2(σ→,ψ)=0D^1( σ,ψ)=D^2( σ,ψ)=0. So: ≤0[i(σ→,ψ)]D_≤ 0[ bCR_i( σ,ψ)] is true. 6 Model Checking PATL-SR The model checking of PATL-SR works in a similar way to rPATL proposed in [32]. The main difference is that we have the new ⋈d[i(σ→,ψ)]D_ d[ bCR_i( σ,ψ)] operator, which corresponds to computing the function i(σ→A,ψ)D^i( σ_A,ψ) in Definition 13, which is presented in Algorithm 1. Computing such function can be done in polynomial space. Algorithm 1 degree-BCR: Calculate i(σ→A,ψ)D^i( σ_A,ψ) 1:Input: ℳ,i,σ→,A,ψ,kM,i, σ,A,ψ,k 2:Output: i(σ→A,ψ)D^i( σ_A,ψ) 3:d←0d← 0 4:for each J⊆A∖iJ A \i\ do 5: v1←minσ→−(J∪i)(ρ∣ρ∈(σ→(J∪i),σ→−(J∪i))(s0)≤k∧ρ⊧ψ)v_1← _ σ_-(J∪\i\) Prob(\ρ ρ∈ Hist_( σ_(J∪\i\), σ_-(J∪\i\))(s^0)^≤ k ρ ψ\) 6: v2←minσ→−J(ρ∣ρ∈(σ→J,σ→−J)(s0)≤k∧ρ⊧ψ)v_2← _ σ_-J Prob(\ρ ρ∈ Hist_( σ_J, σ_-J)(s^0)^≤ k ρ ψ\) 7: d←d+|J|!(||−|J|−1)||!⋅(v1−v2)d← d+ |J|!(| Ag|-|J|-1)| Ag|!·(v_1-v_2) 8:end for 9:Return d Lemma 2 Given a CSG G, a coalition A, strategy profile σ→ σ, and a path formula ψ, computing i(σ→A,ψ)D^i( σ_A,ψ) can be done in polynomial space. Proof To show that it can be computed in polynomial space, we propose Algorithm 1. We show that the algorithm runs in PSPACE. We first examine lines 5 and 6. Observe that computing: minσ→−J(ρ∣ρ∈(σ→J,σ→−J)(s0)≤k∧ρ⊧ℳψ) _ σ_-J Prob(\ρ ρ∈ Hist_( σ_J, σ_-J)(s^0)^≤ k ρ _Mψ\) corresponds to model checking a probabilistic CTL (PCTL) formula over a Markov Decision Process (MDP) [3]. When we apply the (partial) strategy profile σ→J σ_J, we obtain an MDP σ→JG_ σ_J. We then compute the quantitative value of the PCTL formula min=?ψP_ =?ψ, which represents the minimum probability value of ψ in the MDP σ→JG_ σ_J. This can be solved in polynomial time using linear programming and value iteration method [3]. Therefore, lines 5 and 6 are solvable in polynomial time. Furthermore, the values |J|!|J|! and ||!| Ag|! require O(nlogn)O(n n) bits. Since for each subset J, we only need to keep the current intermediate result in memory, and each intermediate result is of polynomial size, the PSPACE membership follows immediately. Theorem 6.1 Model checking PATL-SR is in PSPACE. Proof The proof consists of two parts. First, we show that model checking PATL-SR formula without D operators is in PSPACE. This follows from the fact that the fragment of PATL-SR without D operators corresponds to the logic rPATL proposed in [32], whose model checking over CSGs is shown to be in PSPACE. Second, by Lemma 2, model checking PATL-SR formulae of the form ⟨A⟩⋈d[i(σ→,ψ)] A _ d[ bCR_i( σ,ψ)] can also be done in PSPACE. Therefore, the PATL-SR model checking problem can be solved in PSPACE. 7 CR-aware Strategic Decision-Making This section addresses how agents should (or, would) choose strategies when they are aware of counterfactual responsibility attributions. We introduce a utility function (defined shortly) that incorporates both the agent’s payoff and its degree of responsibility. To identify stable outcomes, we use Nash equilibrium (NE) assuming agents act rationally to maximise their utility. First, we introduce a parametric model. Observe that the set of all memoryless strategies for player i from state s can be encoded by a set of variables Vsi=xa:a∈i(s)V^i_s=\x_a:a∈ Act_i(s)\. Intuitively, the value of xa∈Vsix_a∈ V^i_s corresponds to the probability of action a being chosen by player i in state s. Let Vi=⋃s∈SVsiV^i= _s∈ SV^i_s. A memoryless (mixed) strategy for i in G thus corresponds to an evaluation of such a set of variables represented by a function Ci:Vi→ℝC^i:V^i . Definition 14 Given =(,S,s0,(i)i∈,δ,,L)G=( Ag,S,s^0,( Act_i)_i∈ Ag,δ, Ap,L), we construct the corresponding parametric stochastic multi-agent system (PSMAS) as a tuple ℳ=(,S,s0,,V,Δ,,L)M=( Ag,S,s^0, Act,V, , Ap,L), where: Vi=xi,1,…,xi,k⊆V^i=\x_i,1,…,x_i,k\ V is a finite set of variables (parameters) over ℝkR^k for each agent i; Δ:S×S→ℱx :S× Act Ag× S _x is the probabilistic transition function, where ℱxF_x is the set of polynomials over V with rational coefficients which can be viewed as a parametric transition probability matrix that respects the distribution in δ. Observe that the resulting PSMAS ℳM is polynomial in size wrt the game G. Next, we introduce the notion of admissible evaluations in a given PSMAS. An evaluation CiC^i is admissible if: (1) ΔCi(s,a→,s)∈[0,1] _C^i(s, a,s)∈[0,1] for all s,s′∈Ss,s ∈ S and a→∈ a∈ Act Ag, i.e., each joint action has a probability between 0 and 1; (2) Ci(x)∈[0,1]C^i(x)∈[0,1] for all i∈i∈ Ag and x∈Vix∈ V^i, i.e., for each player, each action probability is between 0 and 1; (3) ∑x∈VsiCi(x)=1 _x∈ V^i_sC^i(x)=1 for all i∈i∈ Ag and s∈Ss∈ S, i.e., For each player and each state, the total of action probability values should equal to 1. Henceforth, we assume that the model takes the form of a PSMAS. When evaluating solutions, we further assume that such solutions are admissible. 7.1 Responsibility-aware Utility Function Definition 15(Responsibility-aware Utility Function) Given ℳM and an outcome φ and strategy profile σ→ σ, for an agent i, the utility function is defined as: uiφ(σ→)≜∑ρ∈σ→(s0)℘i(ρ)−λ⋅i(σ→,φ)u _i( σ) _ρ∈ Hist_ σ(s^0) ^i(ρ)-λ·D^i( σ, ) (7) where ℘i(ρ) ^i(ρ) and i(σ→,φ)D^i( σ, ) are the payoff function and bCR degree function defined in Definition 5 and 9 respectively, λ∈ℝλ is a coefficient. Definition 16(NE-Computation) Given a PSMAS ℳM, a PATL-SR path formula φ , and utility functions (uiφ(σ→))i∈(u _i( σ))_i∈ Ag, the NE-Computation problem is to compute a NE strategy profile σ→ σ that satisfies φ . The high level process to address NE-Computation consists of two main steps: (i) Satisfaction filtering: identify the set of strategy profiles that satisfy φ . This is achieved through parametric model checking on ℳM, which yields rational valuation functions ViV^i for each agent i∈i∈ Ag. These functions capture the probabilities of selecting actions a∈a∈ Act in each state s under mixed strategies. (i) Equilibrium filtering: refine this set by isolating the strategies that constitute an NE. This involves formulating a system of equations characterising NE conditions and solving them within the strategy set obtained in (i). Proposition 7(Quasi-Concavity of Utility) The utility function uiφu _i is quasi-concave if the following conditions hold: 1) linearity of reward: the expected reward is linear in σ→i σ_i; 2) linearity of responsibility contribution: the responsibility-valuation function vσ→,φ(A)v_ σ, (A) is linear in σ→i σ_i for all coalition A⊆A Ag; 3) fixed strategies of others: the strategy profile σ→−i σ_-i of other agents is fixed. Proof Under condition 1) and 2), both the expected reward and the BCR degree term are linear functions of σ→i σ_i. A linear function is trivially quasi-concave (and also quasi-convex). Since σ→−i σ_-i is fixed, we are examining a function ui(σ→i)u_i( σ_i) over a convex domain (probability simplex), which is a linear combination of linear terms. Hence uiu_i is quasi-concave in σ→i σ_i under these conditions. In our setting, quasi-concavity is evaluated with respect to an individual agent’s mixed strategy. To ensure this is well-defined, we fix the strategies of all other agents. This is a standard approach in both game-theoretic best-response analysis and parametric model checking [45, 7]. When both reward and responsibility allocation are linear in the agent’s strategy, the resulting utility function is quasi-concave, enabling NE computation via convex optimisation. In our PSMAS, strategies are symbolically encoded using parameters that represent the probabilities of actions. When the system and property satisfaction probability can be expressed as a linear function of these parameters, both the reward and responsibility expressions remain linear. Consequently, the symbolic utility is linear. We demonstrate that for outcomes expressible as either reachability or safety objectives, the quasi-concavity property is obtained. Proposition 8 In a game where the formula φ is a reachability or safety formula, the quasi-concavity property (Proposition 7) holds. Proof For the responsibility component, note that when φ is either reachability or safety, pure memoryless strategies are sufficient to satisfy it [13]. Thus, the probability of satisfying φ can be expressed as a linear polynomial over strategy parameters xix_i. Consequently, vσ→,φ(A)v_ σ, (A) is linear in σ→i σ_i, and thus vσ→,φ(A∪i)−vσ→,φ(A)v_ σ, (A∪\i\)-v_ σ, (A) is also linear in σ→i σ_i. Therefore, i(σ→,φ)D^i( σ, ) is linear. For the reward component, since pure memoryless strategies are sufficient, the reward can be represented by a linear function. This linearity condition also trivially extends to strategy profiles. In general, uiφu _i is quasi-concave in σ→i σ_i when the agent’s preference for mixing strategies leads to at least as good an outcome as playing pure strategies, or formally, when the level sets σ→i∣uiφ(σ→i,σ→−i)≥c σ_i u _i( σ_i, σ_-i)≥ c are convex for every c∈ℝc [39]. This result enables the use of convex optimisation (best response over pure strategies) to compute Nash equilibria when the assumptions hold. Computing bCR-aware utility. The computation of the responsibility-aware utility valuation function, as given in Equation 7, for outcome ψ involves: i) calculating the expected rewards: (℘i(ρ∈σ→A(s)∣ρ⊧ℳψ))E( ^i(\ρ∈ Hist_ σ_A(s) ρ _Mψ\)), and i) calculating the bCR degree: i(σ→A,ψ)D^i( σ_A,ψ). Finally, computing the best response set i(σ→∖i)BR_i( σ_ Ag i) corresponds to finding the set of strategies σi _i that maximise the utility as the NE. 7.2 NE for Responsibility-aware Strategy Definition 17(NE for bCR-aware Strategy) Given ℳM, for each agent i, and σ→∖i σ_ Ag i, a strategy σi _i is a best response w.r.t. the utility function defined in (7), if it is the set: i(σ→∖i)≜ _i( σ_ Ag i) σi∣maxσi(uiφ(σi,σ→∖i)) \ _i _ _i(u _i( _i, σ_ Ag i))\ A strategy profile σ→ σ is a mixed NE if it is a best response for every agent, meaning that σ→∈i(σ→∖i) σ _i( σ_ Ag i) holds for all i∈i∈ Ag in ℳM. Example 10 Revisiting our running example, consider ψ=○crashψ= \ crash, A1A_1 and A2A_2 choose “braking” with probability x1x_1 and ‘x2x_2 respectively under σ→ σ. Suppose that the payoffs for A1A_1 and A2A_2 “braking” yields 3 and 1 respectively, while “not-braking” results in a payoff of 2 and 3 respectively, the payoffs of reaching s1s_1 (crash) for A1A_1 and A2A_2 is −3-3 and −1-1 respectively. The expected payoff can be computed as: ∑ρ∈σ→(s0)℘1(ρ)=x1+0.4x2−1.6x1x2−1 _ρ∈ Hist_ σ(s^0) ^1(ρ)=x_1+0.4x_2-1.6x_1x_2-1 ∑ρ∈σ→(s0)℘2(ρ)=−1.6x1−2x2+1.6x1x2+2 _ρ∈ Hist_ σ(s^0) ^2(ρ)=-1.6x_1-2x_2+1.6x_1x_2+2 vσ→,ψ(1,2)=vσ→,ψ(2)=0.2x1(1−x2)v_ σ,ψ(\1,2\)=v_ σ,ψ(\2\)=0.2x_1(1-x_2) vσ→,ψ(1)=vσ→,ψ(∅)=0.12x1x2v_ σ,ψ(\1\)=v_ σ,ψ( )=0.12x_1x_2 1(σ→,ψ)=0,2(σ→,ψ)=0.2x1−0.32x1x2D^1( σ,ψ)=0,\ D^2( σ,ψ)=0.2x_1-0.32x_1x_2 Consider an example form of the polynomial function: ∑ρ∈σ→(s0)℘i(ρ)−10⋅i(σ→,ψ) _ρ∈ Hist_ σ(s^0) ^i(ρ)-10·D^i( σ,ψ) we obtain the utility function as: u1ψ(σ→) u^ψ_1( σ) =x1+0.4x2−1.6x1x2−1 =x_1+0.4x_2-1.6x_1x_2-1 u2ψ(σ→) u^ψ_2( σ) =−3.6x1−2x2+4.8x1x2+2. =-3.6x_1-2x_2+4.8x_1x_2+2. Parametric best response expressions. When performing parametric model checking against PATL-SR formulas to evaluate best responses, we obtain parametric expressions that encode optimal strategies. These expressions include parameters representing the probabilities of different actions for each agent. By varying these parameters, we can identify best-response strategies within the strategy profile space, i.e., action probabilities that maximise each agent’s utility. This approach enables a systematic exploration of how changes in action probabilities affect both the overall performance and allocation of responsibility within the strategy profile. Finding the stable responsibility-aware strategy If the utility function uiφu _i is quasi-concave (more specifically linear and convex) with respect to agent i’s mixed strategies in a given model ℳM, then a mixed strategy profile σ→ σ is a NE if and only if every pure strategy played with positive probability in σi _i is a best response to the mixed strategies of the other agents [39]. This implies that, in a mixed NE, an agent randomises only among actions that yield the same expected utility, i.e., every action in the support of an agent’s equilibrium mixed strategy must lead to an identical valuation: uiφ(σ→−i,σi)=uiφ(σ→−i,σi′)u _i( σ_-i, _i)=u _i( σ_-i, _i ). For any two actions a,a′∈a,a ∈ Act corresponding to σi _i and σi′ _i , provided they have nonzero probabilities. This property forms the basis for expressing the NE condition: uiφ(σ→−i,σi)=uiφ(σ→−i,σi′)∀σi,σi′∑j=1mσij=1∀i0≤σij≤1∀i,j \ array[]lu _i( σ_-i, _i)=u _i( σ_-i, _i ) ∀ _i, _i \\ Σ^m_j=1 _ij=1 ∀ i\\ 0≤ _ij≤ 1 ∀ i,j array . (8) Solving these equations allows us to identify the NE and determine the optimal strategy profile for the given objective. This leads to the following theorem, whose proof follows from a reduction to the existential theory of real numbers [11]. Theorem 7.1 Computing NE strategy satisfying PATL-SR formula φ can be done in PSPACE. Example 11 Revisiting Example 10, by solving the NE condition equations, we have: x1=0.42x_1=0.42, x2=0.625x_2=0.625. 8 Conclusion and Future Work We introduce a formal definition of backward (counterfactual) responsibility allocation and provide a framework to model and reason about it. Our definition of responsibility allocation satisfies desirable properties such as fairness and consistency. Utilising this definition, we propose PATL-SR as a language to strategically reason about responsibility allocation, reward, and temporal objectives in probabilistic multi-agent systems. We demonstrate that the model checking problem is in PSPACE, thus no more complex than rPATL as proposed in [32]. Furthermore, we present an approach to calculate NE strategy profiles, where players’ utility functions consider both reward and responsibility allocation. These strategy profiles correspond to stable behaviour in the game and offer a method to determine how agents should or would choose their strategies. This corresponds to game theory’s normative (how agents should/ought to act) and descriptive (how agents would act) interpretations [49]. Both interpretations are valuable for the analysis, verification, and design of responsibility-aware MASs. As discussed in [31], bounded temporal properties may require memory. Therefore, a potential future direction is to generalise our approach to finite-memory agents. However, this would necessitate a different approach, as using a parametric model would no longer suffice. Another intriguing future direction is to incorporate responsibility allocation into normative systems [2], where norms can be introduced to achieve desirable outcomes from the designer’s perspective [42]. Additionally, when integrating learning components into the systems, such as in a multi-agent reinforcement learning setting, it is worth exploring how to incorporate responsibility allocation with rewards. This could involve designing reward structures or reward machines [28] to achieve desirable outcomes. References [1] A. I. R. Abarca and J. M. Broersen (2022) A stit logic of responsibility.. In AAMAS, p. 1717–1719. Cited by: §1. [2] T. Ågotnes, W. van der Hoek, and M. Wooldridge (2007) Normative system games. In Proceedings of the 6th international joint conference on Autonomous agents and multiagent systems, p. 1–8. Cited by: §8. [3] C. Baier and J. Katoen (2008) Principles of model checking. MIT Press. External Links: ISBN 978-0-262-02649-9 Cited by: §6, §6. [4] C. Baier, F. Funke, and R. Majumdar (2021) A game-theoretic account of responsibility allocation. In IJCAI, p. 1773–1779. Cited by: §1. [5] C. Baier, F. Funke, and R. Majumdar (2021) Responsibility attribution in parameterized markovian models. In AAAI, p. 11734–11743. Cited by: §1. [6] A. Baltag, I. Canavotto, and S. Smets (2021) Causal agency and responsibility: a refinement of stit logic. Logic in high definition: Trends in logical semantics, p. 149–176. Cited by: §1, §3. [7] N. Basset, M. Z. Kwiatkowska, U. Topcu, and C. Wiltsche (2015) Strategy synthesis for stochastic games with multiple long-run objectives. In TACAS, C. Baier and C. Tinelli (Eds.), Lecture Notes in Computer Science, Vol. 9035, p. 256–271. Cited by: §7.1. [8] V. Belle, H. Chockler, S. Vallor, K. R. Varshney, J. Vennekens, and S. Beckers (2024) Trustworthiness and responsibility in ai-causality, learning, and verification (dagstuhl seminar 24121). Dagstuhl Reports 14, p. 75–91. Cited by: §1. [9] N. Belnap and M. Perloff (1992) The way of the agent. Studia Logica 51, p. 463–484. Cited by: §3. [10] M. Braham and M. van Hees (2012) An anatomy of moral responsibility. Mind 121, p. 601–634. Cited by: §3. [11] J. Canny (1988) Some algebraic and geometric computations in pspace. In Proceedings of the twentieth annual ACM symposium on Theory of computing, p. 460–467. Cited by: §7.2. [12] R. Chatila, V. Dignum, M. Fisher, F. Giannotti, K. Morik, S. Russell, and K. Yeung (2021) Trustworthy ai. Reflections on artificial intelligence for humanity, p. 13–39. Cited by: §1. [13] K. Chatterjee and T. A. Henzinger (2012) A survey of stochastic ω-regular games. Journal of Computer and System Sciences 78 (2), p. 394–413. Cited by: §7.1. [14] T. Chen and J. Lu (2007) Probabilistic alternating-time temporal logic and model checking algorithm. In FSKD, p. 35–39. Cited by: §2.2. [15] H. Chockler and J. Y. Halpern (2004) Responsibility and blame: A structural-model approach. J. Artif. Intell. Res. 22, p. 93–115. Cited by: §1, §1. [16] Y. Chun (1989) A new axiomatization of the shapley value. Games and Economic Behavior 1 (2), p. 119–130. Cited by: footnote 4. [17] R. Ciuni and R. Mastop (2009) Attributing distributed responsibility in stit logic. In Logic, Rationality, and Interaction: Second International Workshop, LORI 2009, Chongqing, China, October 8-11, 2009. Proceedings 2, p. 66–75. Cited by: §1. [18] J. Cristau, C. David, and F. Horn (2010) How do we remember the past in randomised strategies?. Proceedings of GandALF 2010 25. Cited by: §1. [19] G. De Giacomo, E. Lorini, T. Parker, and G. Parretti (2025) Responsibility anticipation and attribution in ltlf. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, IJCAI, Cited by: §1. [20] T. De Lima, L. Royakkers, and F. Dignum (2010) A logic for reasoning about responsibility. Logic Journal of the IGPL 18 (1), p. 99–117. Cited by: §1. [21] V. Dignum (2020) Responsibility and artificial intelligence. The oxford handbook of ethics of AI 4698, p. 215. Cited by: §1. [22] H. Frankfurt (2018) Alternate possibilities and moral responsibility. In Moral responsibility and alternative possibilities, p. 17–25. Cited by: §3. [23] M. Friedenberg and J. Y. Halpern (2019) Blameworthiness in multi-agent settings. In AAAI, p. 525–532. Cited by: §1. [24] T. Gerstenberg, A. Ejova, and D. Lagnado (2011) Blame the skilled. In Proceedings of the annual meeting of the cognitive science society, Vol. 33. Cited by: §1. [25] J. Y. Halpern and M. Kleiman-Weiner (2018) Towards formal definitions of blameworthiness, intention, and moral responsibility. In AAAI, p. 1853–1860. Cited by: §1, §1. [26] J. Y. Halpern and J. Pearl (2005) Causes and explanations: a structural-model approach. part i: causes. The British journal for the philosophy of science. Cited by: §1. [27] S. Hart and A. Mas-Colell (1989) Potential, value, and consistency. Econometrica: Journal of the Econometric Society, p. 589–614. Cited by: footnote 4. [28] R. T. Icarte, T. Q. Klassen, R. Valenzano, and S. A. McIlraith (2022) Reward machines: exploiting reward function structure in reinforcement learning. Journal of Artificial Intelligence Research 73, p. 173–208. Cited by: §8. [29] D. Kaur, S. Uslu, K. J. Rittichier, and A. Durresi (2022) Trustworthy artificial intelligence: a review. ACM computing surveys (CSUR) 55 (2), p. 1–38. Cited by: §1. [30] T. Kobayashi, M. Bondu, and F. Ishikawa (2023) Formal modelling of safety architecture for responsibility-aware autonomous vehicle via event-b refinement. In International Symposium on Formal Methods, p. 533–549. Cited by: §1. [31] M. Kwiatkowska, G. Norman, D. Parker, and G. Santos (2018) Automated verification of concurrent stochastic games. In Quantitative Evaluation of Systems: 15th International Conference, QEST 2018, Beijing, China, September 4-7, 2018, Proceedings 15, p. 223–239. Cited by: §8. [32] M. Kwiatkowska, G. Norman, D. Parker, and G. Santos (2019) Equilibria-based probabilistic model checking for concurrent stochastic games. In International Symposium on Formal Methods, p. 298–315. Cited by: §1, §6, §8, §6. [33] M. Kwiatkowska, G. Norman, D. Parker, and G. Santos (2021) Automatic verification of concurrent stochastic systems. Formal Methods in System Design 58 (1), p. 188–250. Cited by: §1, §2.1. [34] D. Lewis (2013) Counterfactuals. John Wiley & Sons. Cited by: §1. [35] B. Li, P. Qi, B. Liu, S. Di, J. Liu, J. Pei, J. Yi, and B. Zhou (2023) Trustworthy ai: from principles to practices. ACM Computing Surveys 55 (9), p. 1–46. Cited by: §1. [36] C. Mu, M. Najib, and N. Oren (2025) Responsibility-aware strategic reasoning in probabilistic multi-agent systems. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 39, p. 23258–23266. Cited by: §1. [37] P. Naumov and J. Tao (2021) Two forms of responsibility in strategic games. In IJCAI, p. 1989–1995. Cited by: §1. [38] P. Naumov and J. Tao (2019) Blameworthiness in strategic games. In Proceedings of the AAAI Conference on Artificial Intelligence, Vol. 33, p. 3011–3018. Cited by: §1. [39] M. J. Osborne and A. Rubinstein (1994) A course in game theory. The MIT Press. External Links: ISBN 0-262-65040-1 Cited by: §7.1, §7.2. [40] T. Parker, U. Grandi, and E. Lorini (2023) Anticipating responsibility in multiagent planning. In ECAI, Vol. 372, p. 1859–1866. Cited by: §1, §3. [41] J. Pearl (2009) Causality. Cambridge university press. Cited by: §1. [42] G. Perelli (2019) Enforcing equilibria in multi-agent systems. In AAMAS, Vol. 1, p. 188–196. Cited by: §8. [43] L. S. Shapley (1953) A value for n-person games. In Contributions to the Theory of Games I, H. W. Kuhn and A. W. Tucker (Eds.), p. 307–317. Cited by: §1. [44] Q. Shi and P. Naumov (2025) Responsibility in multi-step decision schemes. Journal of Philosophical Logic, p. 1–39. Cited by: §3. [45] Y. Shoham and K. Leyton-Brown (2009) Multiagent systems - algorithmic, game-theoretic, and logical foundations. Cambridge University Press. External Links: ISBN 978-0-521-89943-7 Cited by: §7.1. [46] D. Stan, M. Najib, A. W. Lin, and P. A. Abdulla (2024) Concurrent stochastic lossy channel games. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), p. 46–1. Cited by: footnote 1. [47] R. van den Brink (2002) An axiomatization of the shapley value using a fairness property. International Journal of Game Theory 30, p. 309–319. Cited by: footnote 4. [48] D. Widerker (2017) Moral responsibility and alternative possibilities: essays on the importance of alternative possibilities. Routledge. Cited by: §3. [49] M. Wooldridge (2012) Does game theory work?. IEEE Intelligent Systems 27 (6), p. 76–80. Cited by: §8. [50] R. W. Wright (1985) Causation in tort law. Calif. L. Rev. 73, p. 1735. Cited by: §3. [51] V. Yazdanpanah, M. Dastani, W. Jamroga, N. Alechina, and B. Logan (2019) Strategic responsibility under imperfect information. In AAMAS, p. 592–600. Cited by: §1. [52] V. Yazdanpanah, E. H. Gerding, S. Stein, M. Dastani, C. M. Jonker, T. J. Norman, and S. D. Ramchurn (2023) Reasoning about responsibility in autonomous systems: challenges and opportunities. Ai & Society 38 (4), p. 1453–1464. Cited by: §1. [53] H. P. Young (1985) Monotonic solutions of cooperative games. International Journal of Game Theory 14 (2), p. 65–72. Cited by: footnote 4.