Counterfactual Reasoning for Responsibility Attribution in Probabilistic Multi-Agent Systems

1 Introduction

The growing emphasis on trustworthy AI [Chatila et al., 2021; Li et al., 2023] necessitates a paradigm shift, particularly regarding responsibility and accountability [Dignum, 2020; Kaur et al., 2022; Belle et al., 2024]. To enable responsible behaviour in agents, they must be endowed with an awareness of responsibility. This motivated the notion of responsibility-aware agents [Yazdanpanah et al., 2023; Kobayashi et al., 2023], 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, A1 and A2, approaching an uncontrolled junction under snowy conditions. A1 is travelling from east to west, A2 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.2 chance that A1 will not be able to stop, and a 0.6 chance that A2 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 [Gerstenberg et al., 2011]. To illustrate, suppose that A2 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 A2, 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 answer 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" [Chockler and Halpern, 2004; Lewis, 2013; Pearl, 2009]. 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 [Shapley, 1953] 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 increase). 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 strategies (aka behavioural [Cristau et al., 2010]), i.e., functions that map from state to a probability distribution over actions. Following the tradition of formal methods in MAS, we extend the logic PATL with cumulative reward (similar to rPATL [Kwiatkowska et al., 2019]) and introduce degree of responsibility operators. We show that model checking this logic remains in PSPACE, thus no harder than rPATL [Kwiatkowska et al., 2021]. 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. Due to space constraints, extended version of the paper containing full proofs is provided in [Mu and Najib, 2026].

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 [Halpern and Pearl, 2005] introduced structural causal models, which underpin formal definitions of causality and counterfactual dependence. Building on this, [Chockler and Halpern, 2004] proposed a quantitative notion of responsibility, which later extended to a notion of blame attribution [Halpern and Kleiman-Weiner, 2018]. 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. [Friedenberg and Halpern, 2019] extends the structural-model approach [Halpern and Kleiman-Weiner, 2018] 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, [Yazdanpanah et al., 2019] apply Shapley-based responsibility allocation in concurrent epistemic games, enabling epistemic modeling but under deterministic assumptions, in contrast to our probabilistic setting. [Baier et al., 2021a] studies backward and forward responsibility in extensiveform games, while [Baier et al., 2021b] 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 hold 1 . Furthermore, [Baier et al., 2021b] 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 [Mu et al., 2025], which uses concurrent stochastic games to reason about causal active and causal passive responsibilities, building on [Parker et al., 2023]. Their approach considers how strategies contribute to or prevent outcomes but does not employ counterfactual reasoning nor guarantee fair attribution. From temporal-logic perspective, [De Giacomo et al., 2025] 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 [Naumov and Tao, 2019; Naumov and Tao, 2021], as well as STIT-based accounts [Ciuni and Mastop, 2009; De Lima et al., 2010; Baltag et al., 2021; Abarca and Broersen, 2022]. 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 G = (Ag, S, s0 , (Acti)i∈Ag, δ, Ap, L) where:

• Ag = {1, . . . , n} is a finite set of agents;
• S is a finite non-empty set of states;
• s0 ∈ S is the initial state;
• Acti is a finite set of actions for i. With each agent i and state s ∈ S, we associate a non-empty set Acti(s) of available actions that i can perform in s. Write Act Ag = Act1 × · · · × Actn.
• ∆ : S × Act Ag → Dist(S) is a probabilistic transition function;
• Ap is a finite set of atomic propositions;
• L : S → 2Ap is the labelling function mapping each state to a set of atomic propositions drawn from Ap.

Following [Kwiatkowska et al., 2021], we augment CSGs with reward structures of the form r = (rs, ra), where rs : S → R is the state reward and ra : Act Ag → R is the action reward, and consider cumulative rewards, that is the sum of payoffs accumulated during the run until a specific point.

1 Some parameter assignments cannot be expressed as individual strategies; see [Stan et al., 2024, Remark 8]. We address this by imposing additional constraints in our parametric model (Section 6).

Example 2. From the running example, we construct a model in Figure 1. With Ag = {1, 2}, representing A1 and A2. Acti = {bi,¯bi} representing agent i ∈ Ag choosing to brake and not brake. s0 is the initial state, and L(s1) = {crash},L(s0) = {init},L(s2) = {pass}. Note that from s1 and s2, there are only self-loops.

Definition 2. A path π is a non-empty sequence s0⃗a0 s1⃗a1 . . . of states and joint actions, where ⃗ai ∈ Act Ag is the ith joint action, and ∆(si,⃗ai , si+1) > 0. A history ρ is a finite path, ρs(i) denotes the ith state of ρ, and ρ⃗a(i) denotes the ith joint action of ρ. In this case, we may write ρs(i) ρ⃗a(i) -→ ρs(i + 1). Let HistG(s) denote the set of histories of G starting from state s. We write HistG(s)≤k to denote the set of histories up to and including ρ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 ∈ Acti(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 → Dist(Acti). A strategy profile is a tuple of strategies for a set of agents, it is denoted by ⃗σ = (σ1, σ2, . . . , σn). For a set (or coalition) of agents J ⊆ Ag, write ⃗σJ for (σ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 s0⃗a0 s1⃗a1 . . . , with P(⃗ai ) · ∆(si,⃗ai , si+1) > 0 and s = s0, denoted by Hist⃗σ(s). For a history ρ ∈ Hist⃗σ(s)≤k , the probability of ρ = s0 ⃗a0 -→ s1 . . . ⃗ak-1 -→ sk, with s0 = s, is given by:

For a subset of agents J ⊆ Ag and strategies ⃗σJ, we say that a history ρ is compatible with ⃗σJ if for every k ∈ N, there exists a joint action ⃗ak with σi(ρs(k))(⃗aki ) > 0 for each i ∈ J, such that ∆(sk,⃗ak , sk+1) > 0. We denote by Hist⃗σJ (s) the set of histories starting from s and compatible with ⃗σ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 ℘ : HistG(s) → R|Ag| . ℘i denotes the payoff function of i ∈ Ag and is defined as:

2.2 PATL

PATL [Chen and Lu, 2007] 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:

where a ∈ Ap is an atomic proposition, A ⊆ Ag is a set of agents, ▷◁ ∈ {≤, <, ≥, >}, p ∈ [0, 1], k ∈ N is a time bound, and ⟨A⟩ is the strategy quantifier.

The until operator U allows one to derive the temporal modalities ♢ ("eventually") and □ ("always"): ♢≤kψ ≜ true U≤k ψ and □≤kψ ≜ ¬♢≤k(¬ψ).

Definition 7 (Semantics of PATL). The satisfaction relation for a CSG G, state s ∈ S, history ρ, atom a ∈ Ap, and PATL formula is defined as follows:

• s |= a iff a ∈ L(s).
• s |= ¬ϕ iff s ̸|= ϕ.
• s |= ϕ ∧ ϕ′ iff s |= ϕ and s |= ϕ′ .
• s |= ⟨A⟩P▷◁p[ψ] iff ∃⃗σA.∀⃗σ-A.(P({ρ ∈ Hist(⃗σA,⃗σ-A)(s) | ρ |= ψ}) ▷◁ p).
• ρ |=⃝ϕ iff ρs(1) |= ϕ.
• ρ |= ϕU≤kϕ′ iff there exists i ≤ k such that: ρs(i) |= ϕ′ , and ρs(j) |= ϕ for all j < i.

We say that formula φ is true in a CGS G iff s0 |= φ.

3 Formalising Counterfactual Responsibility Attribution

We build on the concept of Necessary Element of a Sufficient Set (NESS) test [Wright, 1985], which has been used in many game-theoretic frameworks (e.g., [Braham and van Hees, 2012; Baltag et al., 2021; Parker et al., 2023]), 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 ∼ bCR⃗σφ, if the following conditions hold: ∃J ⊆ Ag \ {i} such that ∃ρ′ ∈ Hist⃗σJ (s0 ).ρ′ ̸|= φ and ∀ρ′′ ∈ Hist⃗σJ∪{i} (s0 ).ρ′′ |= φ.

In words, agent i is responsible for an outcome φ under strategy profile ⃗σ, if it belongs to some coalition J ∪ {i} whose joint strategies are sufficient to guarantee φ, while the strategies of J (without i) are not.

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. When computing computing marginal contributions, we assume that agents outside the coalition minimise the probability of satisfying φ. This imposes no moral duty on them; it simply provides a counterfactual baseline for non-grand coalitions, whose outside behaviour would otherwise be undefined.

Definition 9. Given a bound 2 k ∈ N, the degree of i bearing bCR in ⃗σ for φ is defined as:

For any A ⊆ Ag, the function v⃗σ,φ(A) for the k-bounded histories is defined as:

Example 3. Continuing the running example, suppose given an outcome φ := ⃝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 1. In this case, we obtain:

Therefore:

Note that A1 has a higher degree of responsibility than A2, intuitively, because A1 has a greater chance of being able to stop (i.e., 0.8, compared to 0.4 for A2). For comparison, under the other pure profiles (b1, b2), (b1,¯b2), and (¯b1, b2), the corresponding responsibility pairs (D1 ,D2 ) are (0, 0), (0, 0.08), and (0.48, 0), respectively.

2 This bound comes from the PATL path formula φ.

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.8, meaning the maximum responsibility assignable to i is 0.8.

Definition 10. Given a strategy profile ⃗σ, an outcome φ, and a bound k ∈ N, the attributable value of φ w.r.t. ⃗σ is defined as: Υ(⃗σ, φ) = v⃗σ,φ(Ag) - min⃗σ Prob({ρ | ρ ∈ Hist⃗σ(s0 )≤k ∧ ρ |= φ}).

By Definition 9, we have that:

and since Ag \ ∅ = Ag, therefore ⃗σAg = ⃗σ, and we immediately obtain the following lemma.

Lemma 1. For a strategy profile ⃗σ and outcome φ, it holds:

Example 4. Consider Example 3, the attributable value is:

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∈Ag Di (⃗σ, φ) = Υ(⃗σ, φ).

Example 5. Consider again Example 3 and 4, note that:

Proposition 2 (Symmetry). For two agents i, j ∈ Ag, if:

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 independent 3 , 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. Observe that the function Di (·, ·) is generally not additive. To see this, consider φ1 := φ and φ2 := ¬φ. Clearly, for any ⃗σ, Di (⃗σ, φ1 ∨ φ2) = 0, while it may be the case that Di (⃗σ, φ1) > 0 or Di (⃗σ, φ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 and φ2, where φ1 is "included" in φ2, the degree of responsibility for φ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 and φ2, and any i ∈ Ag:

Example 6. Continue the running example, suppose given outcomes φ1 = ⃝ crash and φ2 = ⃝ pass, consider ⃗σ corresponding to each agent choosing to brake with probability of 1, let ∨ denote φ1 ∨ φ2 for short. In this case, we have:

Thus:

Clearly, for i = {1, 2} : Di (⃗σ, φ1 ∨ φ2) ≤ Di (⃗σ, φ1) + Di (⃗σ, φ2).

To obtain exact additivity, we define the following conditions.

Definition 11. For two outcomes φ1 and φ2, we say that they are disjoint and avoidable, respectively, if

1. for all ⃗σ, we have Prob({ρ | ρ ∈ Hist⃗σ(s0 )≤k ∧ ρ |= φ1 ∧ φ2}) = 0
2. ii) there exists ⃗σ, such that Prob({ρ | ρ ∈ Hist⃗σ(s0 )ρ |= (φ1 ∨ φ2)}) < 1.

Proposition 5 (Exact Additivity). Let φ1 and φ2 be two outcome formulas such that they are disjoint and avoidable, then for any i ∈ Ag:

3 There have been many attempts to relax the additivity axiom, e.g. [Young, 1985; Hart and Mas-Colell, 1989; Chun, 1989; van den Brink, 2002].

Example 7. Note that the scenario proposed in Example 6 does not satisfy Proposition 5, as it meets assumption i) but violates assumption ii).

Proposition 6 (Monotonicity). If φ1 ⇒ φ2 and φ2 is avoidable, then for any i ∈ Ag and a given ⃗σ:

Intuitively, responsibility should not decrease when the outcome becomes more inclusive - any trace satisfying φ1 also satisfies φ2, so agents influencing φ1 also influencing φ2, potentially to a greater extent.

Example 8. Continue the running example, consider φ1=⃝ crash and φ2=♢≤2 crash and ⃗σ corresponding to each agent choosing not to brake with probability of 1. Clearly, in this case, φ1 ⇒ φ2 and φ2 is avoidable. We have: D1 (⃗σ, φ1) = D1 (⃗σ, φ2) = 0.64, D2 (⃗σ, φ1) = D2 (⃗σ, φ2) = 0.24. We have "=" specifically here as there is only a self-loop from s1.

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 new formulae of PATL-SR is given as:

q, d ∈ R are reward and responsibility degree bounds, respectively.

The formula ⟨A⟩R▷◁q [♢≤kψ] expresses that the coalition A has a strategy such that the expected rewards of satisfying path formula ψ is ▷◁ q when the strategy is followed. The formula ⟨A⟩D▷◁d [bCRi(⃗σ, ψ)] expresses that, under strategy profile ⃗σ, the backward counterfactual responsibility of i in ensuring ψ within coalition A is quantified by ▷◁ d.

Definition 13. Given a model G, the semantics of the new PATL-SR operators are defined as follows; the full formal definitions are provided in the supplementary material.

• s |= ⟨A⟩R▷◁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, i.e., ∃⃗σA.E⃗σA G (s, rew(r, ψ)) ▷◁ q, where: rew(r, ψ)(ρ) =

where k denotes the time bound of ψ.

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}⟩♢≤2 crash. Suppose 1 and 2 both choose to brake under ⃗σ, thus: v⃗σ,ψ({1, 2}) = v⃗σ,ψ({1}) = v⃗σ,ψ({2}) = v⃗σ,ψ(∅) = 0.12, and thus D1 (⃗σ, ψ) = D2 (⃗σ, ψ) = 0. So: D≤0[bCRi(⃗σ, ψ)] is true.

The model checking of PATL-SR works in a similar way to rPATL proposed in [Kwiatkowska et al., 2019]. The main difference is that we have the new D▷◁d[bCRi(⃗σ, ψ)] operator, which corresponds to computing the function Di (⃗σA, ψ) in Definition 13. Computing such function can be done in polynomial space.

Lemma 2. Given a CSG G, a coalition A, strategy profile ⃗σ, and a path formula ψ, computing Di (⃗σA, ψ) can be done in polynomial space.

Theorem 1. Model checking PATL-SR is in PSPACE.

6 CR-aware Strategic Decision-Making

This section studies how agents choose strategies when they are aware of counterfactual responsibility attributions. We define a utility function that combines an agent's payoff with its degree of responsibility, and use Nash equilibrium (NE) to characterise stable strategy profiles under this utility. To retain decidability, we restrict attention to memoryless strategies and reachability/safety objectives [Ummels and Wojtczak, 2011].

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 V i s = {xa : a ∈ Acti(s)}. Intuitively, the value of xa ∈ V i s corresponds to the probability of action a being chosen by player i in state s. Let V i = ⋃s∈S V 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 C i : V i → R.

Definition 14. Given G = (Ag, S, s0 , (Acti)i∈Ag, δ, Ap, L), we construct the corresponding parametric stochastic multi-agent system (PSMAS) as a tuple M=(Ag, S, s0 , Act, V,∆, Ap,L), where: V i = {xi,1, . . . , xi,k} ⊆ V is a finite set of variables (parameters) over Rk for each agent i; ∆ : S × Act Ag × S → Fx is the probabilistic transition function, where Fx 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 PSMASMis polynomial in size wrt the game G. Next, we introduce the notion of admissible evaluations in a given PSMAS. An evaluation C i is admissible if: (1) ∆Ci(s,⃗a, s) ∈ [0, 1] for all s, s′ ∈ S and ⃗a ∈ Act Ag , i.e., each joint action has a probability between 0 and 1; (2) C i (x) ∈ [0, 1] for all i ∈ Ag and x ∈ V i , i.e., for each player, each action probability is between 0 and 1; (3) ∑x∈V i s C i (x) = 1 for all i ∈ Ag and s ∈ 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.

Definition 15 (Responsibility-aware Utility Function). Given M and an outcome φ and strategy profile ⃗σ, for an agent i, the utility function is defined as:

where ℘i (ρ) and Di (⃗σ, φ) are the payoff function and bCR degree function defined in Definition 5 and 9 respectively, λ ∈ R is a coefficient.

Definition 16 (NE-COMPUTATION). Given a PSMASM, a PATL-SR path formula φ, and utility functions (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 V i for each agent i ∈ Ag. These functions capture the probabilities of selecting actions a ∈ Act in each state s under mixed strategies. (ii) 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 uφi is quasi-concave if the following conditions hold:

1. linearity of reward: the expected reward is linear in ⃗σi;
2. linearity of responsibility contribution: the responsibility-valuation function v⃗σ,φ(A) is linear in ⃗σi for all coalition A ⊆ Ag;
3. fixed strategies of others: the strategy profile ⃗σ-i of other agents is fixed.

In our setting, quasi-concavity is evaluated with respect to an individual agent's mixed strategy. To ensure this is welldefined, we fix the strategies of all other agents. This is a standard approach in both game-theoretic best-response analysis and parametric model checking [Shoham and Leyton-Brown, 2009; Basset et al., 2015]. 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 a PSMAS, memoryless strategies are encoded symbolically by parameters denoting action probabilities. With the other agents' strategies fixed, quasi-concavity follows whenever the reward and responsibility terms are linear in the strategy parameters of the agent under consideration. We show that, for reachability and safety objectives in our setting, these terms satisfy the required conditions, yielding the following result.

Proposition 8. In a game where the formula φ is a reachability or safety formula, the quasi-concavity property (Proposition 7) holds.

In general, uφi is quasi-concave in ⃗σ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 | uφi (⃗σi, ⃗σ-i) ≥ c are convex for every c ∈ R [Osborne and Rubinstein, 1994]. 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. For a fixed outcome φ, computing uφi (⃗σ) requires: i) calculating the expected rewards: E(℘i ({ρ ∈ Hist⃗σA (s) | ρ |=M ψ})), and ii) calculating the bCR degree: Di (⃗σA, ψ). Finally, computing the best response set BRi(⃗σAg\i) corresponds to finding the set of strategies σi that maximise the utility as the NE.

Definition 17 (NE for bCR-aware Strategy). Given M, for each agent i, and ⃗σAg\i, a strategy σi is a best response w.r.t. the utility function defined in (1), if it is the set:

A strategy profile ⃗σ is a mixed NE if it is a best response for every agent, meaning that ⃗σ ∈ BRi(⃗σAg\i) holds for all i ∈ Ag inM.

Example 10. Revisiting our running example, consider ψ = ⃝ crash, A1 and A2 choose "braking" with probability x1 and 'x2 respectively under ⃗σ. Suppose that the payoffs for A1 and A2 "braking" yields 3 and 1 respectively, while "notbraking" results in a payoff of 2 and 3 respectively, the payoffs of reaching s1 (crash) for A1 and A2 is -3 and -1 respectively. The expected payoff can be computed as:

Consider an example form of the polynomial function:

we obtain the utility function as:

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 uφi is quasi-concave 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 is a best response to the mixed strategies of the other agents [Osborne and Rubinstein, 1994]. 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: uφi (⃗σ-i, σi) = uφi (⃗σ-i, σi′). For any two actions a, a′ ∈ Act corresponding to σi and σi′, provided they have nonzero probabilities. This property forms the basis for expressing the NE condition:

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 [Canny, 1988].

Theorem 2. Computing an 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.42, x2 = 0.625.

7 Conclusion and FutureWork

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 PATLSR 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 [Kwiatkowska et al., 2019]. 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 [Wooldridge, 2012]. Both interpretations are valuable for the analysis, verification, and design of responsibility-aware MASs.

As discussed in [Kwiatkowska et al., 2018], 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 [ ˚Agotnes et al., 2007], where norms can be introduced to achieve desirable outcomes from the designer's perspective [Perelli, 2019]. 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 [Icarte et al., 2022] to achieve desirable outcomes.

Acknowledgments

Chunyan Mu acknowledges the support provided by the University of Aberdeen through the research leave project on

• "Responsibility-aware Trustworthy AI", and the National Decommissioning Centre (NDC) project on "Decision-Making for Oil & Gas Decommissioning: A Formal AI-Driven Approach".