Responsibility Anticipation and Attribution in LTLf

1 Introduction

Responsibility is a key notion in the areas of machine ethics and multi-agent systems. In recent times, there have been several and diverse attempts to formalize it, using various approaches such as game-theoretic tools [Baier et al., 2021; Braham and van Hees, 2012; Lorini and M¨uhlenbernd, 2018] and logical tools including STIT logic [Lorini et al., 2014; Abarca and Broersen, 2022; Baltag et al., 2021; Lorini and Schwarzentruber, 2011], LTLf [Parker et al., 2023], ATL [Yazdanpanah et al., 2019; Bulling and Dastani, 2013], logics of strategic and extensive games [Shi, 2024; Naumov and Tao, 2021; Naumov and Tao, 2023], structural equation models [Chockler and Halpern, 2004]. However, the overall picture on the conceptual and computational aspects of responsibility remains rather fragmented. This is due to its polysemic nature and to its many dimensions (e.g., forward-looking vs backward-looking, active vs passive, direct vs indirect, causal vs moral, attributed vs anticipated).

In this paper we provide (i) a comprehensive analysis of the complexity of reasoning about strategic responsibility, namely, the responsibility of an agent due to its choice of a given strategy, and (ii) a number of algorithms that can be used to automate reasoning about strategic responsibility.

We limit ourselves to analyzing causal responsibility [Vincent, 2011], which considers whether or not an agent caused a certain state of affairs to occur by making a certain choice.

It is a general notion of responsibility that is a necessary condition for both legal [Jansen, 2014] and moral [Talbert, 2023] responsibility. We consider the two main forms of responsibility that exist in the literature, active responsibility and passive responsibility. Active responsibility captures the notion of an agent making φ happen, while passive responsibility consists in the agent merely letting φ happen. The distinction between the two notions was proposed in [Lorini et al., 2014] in an action-based setting. Active responsibility corresponds to the notion of deliberative stit studied in STIT logic [Belnap et al., 2001] while passive responsibility corresponds to the counterfactual notion of (something) could have been prevented (CHP), a fundamental component of the notion of regret as highlighted in [Lorini and Schwarzentruber, 2011]. More recently, a plan-based analysis of active and passive responsibility was proposed in [Parker et al., 2023]. In line with their work we distinguish the concepts of responsibility anticipation and responsibility attribution. Responsibility anticipation is an ex ante notion: it is the responsibility that an agent could incur by making a certain choice. Responsibility attribution is an ex post notion: it is ascribed to a given agent after the agent and the environment have made their choices and the result of their choices has been revealed.

Passive responsibility for φ, as defined in [Lorini et al., 2014], is a notion of responsibility in a weak sense. As pointed out in [Braham and van Hees, 2012], to strengthen it one could add the requirement that the alternative option the agent could have chosen was preferred by some rationality requirement, implying that the agent has no excuse for letting φ happen. A simple and universal rationality requirement is dominance: there was an alternative recommended option that dominates its actual choice, which is equivalent to saying that the agent's actual choice was not best-effort.

Since the notions of dominance and best-effort are been well-studied in the field of strategy synthesis, it is natural to combine the theory of responsibility with existing work on best-effort synthesis, which is the focus of the present paper. By doing this we gain a better understanding of the computational complexity of reasoning about strategic responsibility and novel algorithms for it. It also leads to the novel notion of strong passive responsibility, which is particularly useful for agents who use responsibility to evaluate their options.

Our formal analysis of responsibility relies on LTL on finite traces (LTLf ), a popular temporal logic which we have chosen due to its popularity in strategy synthesis, as well as normative specifications in multi-agent systems and AI more broadly. We formally specify various notions of responsibility and relate them to combinations of forms of LTLf synthesis studied in the literature [De Giacomo and Vardi, 2015; Aminof et al., 2019; Aminof et al., 2021; Aminof et al., 2023]. This allows us to give a computational grounding to such notions of responsibility and devise algorithms and computational complexity characterization to assess them. We also contribute to the LTLf strategy reasoning by devising algorithms for and proving the computational complexity of checking strategic properties, like winning, dominant, and best-effort (vs. synthesizing strategies with these properties [De Giacomo and Vardi, 2015; Aminof et al., 2019; Aminof et al., 2021; Aminof et al., 2023]).

2 Preliminaries

A trace over an alphabet of symbols Σ is a finite or infinite sequence of elements from Σ. The empty trace is λ. The length of a trace is |π|. Traces are indexed starting at zero, and we write π = π0π1 · · · . For a finite trace π, we denote by lst(π) the index of its last element, i.e., |π|-1. We denote by πk = π0 · · · πk the prefix of π up to the k-th index.

Linear Temporal Logic on finite traces (LTLf ) is a specification language for expressing temporal properties over finite traces [De Giacomo and Vardi, 2013]. LTLf has the same syntax as LTL [Pnueli, 1977], which is instead interpreted over infinite traces. Given a set AP of atomic propositions (aka atoms), the LTLf formulas over AP are: φ ::= a | ¬φ | φ ∧ φ | ◦φ | φU φ, where a ∈ AP, and ◦ (Next) and U (Until) are temporal operators. Additional operators are defined as abbreviations and include: standard Boolean operators of propositional logic; ·φ ≡ ¬◦¬φ (Weak Next); ✸φ ≡ true U φ (Eventually); and ✷φ ≡ ¬✸¬φ (Always). The size of φ, written |φ|, is the number of its subformulas.

LTLf formulas are interpreted over finite traces π over the alphabet Σ = 2AP , i.e., consisting of propositional interpretations of atoms. For i ≤ lst(π), we have that πi ∈ 2AP is the i-th interpretation of π. That an LTLf formula φ holds at instant i of trace π, written π, i |= φ, is defined inductively:

• π, i |= a iff a ∈ πi (for a ∈ AP);
• π, i |= ¬φ iff π, i ̸|= φ;
• π, i |= φ1 ∧φ2 iff π, i |= φ1 and π, i |= φ2;
• π, i |= ◦φ iff i < lst(π) and π, i + 1 |= φ;
• π, i |= φ1 U φ2 iff ∃j such that i ≤ j ≤ lst(π) and π, j |= φ2, and ∀k, i ≤ k < j we have that π, k |= φ1. We say that π satisfies φ, written π |= φ, if π, 0 |= φ.

We consider LTLf formulas over AP = Y ∪ X, where Y and X are disjoint sets of atoms under control of agent and environment, respectively, as in LTLf reactive synthesis [De Giacomo and Vardi, 2015]. Traces over Σ = 2Y∪X will be denoted π = (Y0 ∪ X0)(Y1 ∪ X1) · · · where Yi ⊆ Y and Xi ⊆ X for every i ≥ 0. Such finite traces are sometimes also called histories.

An agent strategy is a function σag : (2X )∗ → 2Y mapping sequences of environment choices to an agent choice. We require σag to be stopping [De Giacomo et al., 2021], i.e., the agent stops the execution of any action at some point of the trace, written stop. Formally, an agent strategy σag is stopping if for every trace π ∈ (2Y∪X )ω there exists k ∈ N such that, for every j ≥ k, we have that σag(πj ) = stop and, for every i < k, we have that σag(πi ) ̸= stop. An environment strategy is a function σenv : (2Y )+ → 2X mapping nonempty sequences of agent choices to an environment choice. The domain of σag includes the empty sequence λ as we assume that the agent moves first.

A trace π = (Y0 ∪X0) · · · (Yn∪Xn) is consistent with σag if: (i) Y0 = σ(λ); (ii) Yi = σag(X0 · · · Xi-1) for every i > 0; and (iii) σag(X0 · · ·Xn) = stop. Similarly, π is consistent with σenv if Xj = σenv(Y0 · · · Yj) for every j ≥ 0. We denote by Play(σag, σenv) the shortest trace that is consistent with both σag and σenv.

Let ψ be an LTLf formula over Y ∪ X. An agent strategy σag is winning for (aka enforces) ψ if Play(σag, σenv) |= ψ for every environment strategy σenv. Conversely, an environment strategy σenv is winning (aka enforces) for ψ if every finite prefix of Play(σag, σenv) satisfies ψ for every agent strategy σag. An environment specification E is an LTLf formula that is environment enforceable [Aminof et al., 2019] and ΣE is the set of environment strategies that enforce E. An agent strategy σag is winning for (aka enforces) φ under E if Play(σag, σenv) |= φ for every environment strategy σenv ∈ ΣE. We may omit φ and/or E when they are clear from the context and say, e.g., σag is winning for φ.

In this paper, we are interested in the result that every LTLf formula φ can be transformed into a finite automaton that accepts exactly the traces that satisfy φ [De Giacomo and Vardi, 2015]. A nondeterministic finite automaton (NFA) is a tuple N = (Σ, S, s0, δ, F ), where: Σ is a finite input alphabet; S is a finite set of states; s0 ∈ S is the initial state; δ : S×Σ → 2S is the transition function; and F ⊆ S is the set of final states. The size of N is |S|. Given a word π = π0 · · · πn ∈ Σ∗ , a run of N in π is a sequence of states s0 · · · sn+1 starting in the initial state of N and such that si+1 ∈ δ(si, πi) for every i ≥ 0. A word π is accepted by N if it has a run whose last reached state is final. The language of N, written L(N), is the set of words accepted by N. An automaton N is a deterministic finite automaton (DFA) if |δ(s, a)| ≤ 1 for every (s, a) ∈ S × Σ. Checking non-emptiness of L(N), written NONEMPTY(N), can be done by checking the existence of a path from the initial state of N to some final state. Given the NFAs N1 and N2 with languages L(N1) and L(N2), respectively, we can build in polynomial time the product NFA N = N1×N2 such that L(N) = L(N1)∩L(N2). We denote nondeterministic and deterministic automata by N and A, respectively. Every LTLf formula φ can be transformed into an NFA Nφ = TONFA(φ) (resp. DFA Aφ = TODFA(φ)) with size at most exponential (resp. doubly-exponential) in |φ| and whose language is exactly the set of traces satisfying φ [De Giacomo and Vardi, 2015].

A DFA game is a DFA G with input alphabet 2Y∪X , where Y and X are two disjoint sets under control of agent and environment, respectively. The notions of strategy and play also apply DFA games. An agent strategy is winning if Play(σag, σenv) is accepted by G for every environment strategy σenv. Conversely, an environment strategy is winning if Play(σag, σenv) is not accepted by G for every agent strategy σag. The agent winning region is the set of states s ∈ S for which the agent has a winning strategy in the game G ′ = (2Y∪X , S, s, δ, F), i.e., the same game as G, but with initial state s. The environment winning region is defined analogously. Solving a DFA game is the problem of computing the agent winning region, written W = WINREGION(G). Games played over DFAs are determined, meaning that the agent winning region and the environment winning region partition the state space [Gale and Stewart, 1953]. The environment winning region is denoted ENVWIN(G). DFA games can be solved in polynomial time in the size of the game via a least-fixpoint computation [Apt and Gr¨adel, 2011].

We will need to restrict transitions in a DFA to those that do not allow leaving a given set of states. Given a DFA A and a set of states Q ⊆ S, the restriction of A to Q can be built in polynomial time and is denoted A′ = RESTR(A, Q).

We represent agent strategies as terminating transducers [Bansal et al., 2023] σag = (2X , 2Y , S, s0, η, κ, F), where: 2X is the input alphabet; 2Y is the output alphabet; S is a finite set of states; s0 ∈ S is the initial state; η : S×2X → S is the transition function; κ : S → 2Y is the output function; and F ⊆ S is the set of terminating states. The size of σag, denoted |σag|, is |S|. Given an input sequence X0 · · ·Xn ∈ (2X )∗ , the output sequence is κ(s0) · · · κ(sn), where s0 is the initial state of σag and si+1 = η(si,Xi) for every i ≥ 0. A transducer σag can be transformed in polynomial time into a DFA Aσag = TODFA(σag) whose language is the set of traces consistent with σag.

3 Active Responsibility

The first notion of responsibility that we consider is active responsibility, which captures: (i) that the agent selected a strategy that forced a certain outcome, while (ii) having the possibility of selecting an alternative strategy that would have not forced that outcome for at least some environment response. In the context of LTLf , we formalize this notion as follows:

Definition 1. [Active Responsibility] The agent has active responsibility for φ under σag and E if: (i) Play(σag, σenv) |= φ for every environment strategy σenv ∈ ΣE; and (ii) there exists a pair of strategies (σ′ag , σ′env ) such that σ′env ∈ ΣE and Play(σ′ag , σ′env ) ̸|= φ.

By condition (i), active responsibility is related to winning strategies used in reactive synthesis [De Giacomo and Vardi, 2015; Aminof et al., 2019] (see Preliminaries); by condition (ii), active responsibility is related to a form of strategies called weak [Cimatti et al., 2003], which only ensure the existence of an environment strategy for which a certain outcome occurs. Formally, an agent strategy σ′ag is weak for ¬φ under E if there exists an environment strategy σ′env ∈ ΣE such that Play(σ′ag , σ′env ) |= ¬φ. The following shows the relation between active responsibility, winning, and weak strategies.

Theorem 1. The agent has active responsibility for φ under σag and E iff σag is winning for φ under E and there exists some agent strategy σ′ag that is weak for ¬φ under E.

We now illustrate how these notions can be applied to assess active responsibility using a relatively simple example.

Example 1. An agent is assigned the task to take care of a plant. In doing so, the agent must consider the possibility that the environment could also water the plan by raining.

Consider the following outcomes:

• φ = "The plant is watered at least once";
• ¬φ = "The plan is never watered".

Furthermore, consider the following agent strategies:

• σ1 = "Water the plant in the morning";
• σ2 = "Never water the plant".

Finally, consider the following environment specifications:

• E1 = "The weather can rain";
• E2 = "The weather surely rains".

We have the following:

1. The agent has active responsibility for φ under σ1 and E1. In fact, σ1 is winning for φ under E1 and a weak strategy for ¬φ under E1 exists. One such a weak strategy is σ2, since it satisfies ¬φ together with the environment strategy that the weather never rains.
2. The agent does not have active responsibility for φunder σ2 and E1, since σ2 is not winning for φ under E1.
3. The agent does not have active responsibility for φunder σ1 and E2. In fact, no weak strategy for ¬φ under E2 exists, i.e., regardless of which strategy the agent selects, the plant will be watered.

In what follows, we study the decision problem of checking if the agent has active responsibility. That is: given an LTLf formula φ, an LTLf environment specification E, and an agent strategy σag, we want to decide whether the agent has active responsibility for φ under σag and E. The following establishes the computational complexity of the problem.

Theorem 2. Checking if the agent has active responsibility for φ under σag and E is: PSPACE-complete wrt φ; 2EXPTIME-complete wrt E; and polynomial wrt σag.

We prove membership of checking active responsibility by exhibiting a sound and complete algorithm to solve it. Based on Theorem 1, this algorithm checks that σag is winning for φ under E and that there exists a weak strategy for ¬φ under E. First, we give an algorithm for each such check.

We begin by giving an algorithm to check if a strategy σag is winning for φ under E, denoted CHECKWIN(φ, E, σag): 1. Construct the NFA N¬φ of ¬φ, the DFA AE of E, and the DFA Aσag of σag; 2. Restrict AE to the environment winning region and obtain DFA A′E ; and 3. Check language nonemptiness of the product N = N¬φ × A′E × Aσag . Intuitively, CHECKWIN(φ, E, σag) checks whether there exists a trace consistent with σag that satisfies ¬φ, i.e., that witnesses that σag is not winning for φ. By the notion of product of automata, we have that the language of N is exactly the set of traces that satisfy ¬φ and are consistent with σag and some environment strategy enforcing E. As a result, we have that σag is winning for φ under E iff L(N) is empty.

The complexity of CHECKWIN(φ, E, σag) wrt φ is dominated by checking language non-emptiness of the product N = N¬φ × A′E × Aσag . That can be done on-the-fly while building the product [Vardi and Wolper, 1986]. Being N¬φ exponential in |φ|, we get PSPACE membership wrt φ. The complexity wrt E is dominated by computing and restricting the automaton AE, which is doubly-exponential in |E|, and gives 2EXPTIME membership wrt E. Finally, the product automaton N is polynomial in |σag|, which gives polynomial complexity wrt σag. The complexity of CHECKWIN(φ, E, σag) establishes membership of checking if a strategy is winning for φ under E.

Note that CHECKWIN(φ, E, σag) constructs the DFA of E, which involves a doubly-exponential blowup, while it constructs the NFA of ¬φ, which involves a singly-exponential blowup instead. This is because in order to reason about traces consistent with environment strategies enforcing an environment specification E, we must restrict its DFA AE to the environment winning region WE = ENVWIN(AE). That is, we have that A′E = RESTR(AE,WE) accepts exactly the traces π that satisfy E and are consistent with some environment strategy enforcing E. Such construction, which leads to a doubly-exponential blowup wrt E, is unavoidable, as also confirmed by the computational complexity of checking if a strategy is winning, established in the following.

Lemma 1. Checking if σag is winning for φ under E is: PSPACE-complete wrt φ; 2EXPTIME-complete wrt E; and polynomial wrt σag.

We now give an algorithm to check if a weak strategy for ¬φ under E exists, denoted EXISTSWEAK(¬φ, E): 1. Construct the NFA N¬φ of ¬φ and DFA AE of E; 2. Restrict AE to the environment winning region and obtain DFA A′E ; and 3. Check language non-emptiness of the product N =N¬φ ×A′E . EXISTSWEAK(¬φ, E) is similar to CHECKWIN(φ, E). It checks whether there exists a trace satisfying ¬φ and consistent with some environment strategy enforcing E, i.e., that witnesses that a weak strategy for ¬φ under E exists. Its complexity analysis establishes PSPACE and 2EXPTIME membership wrt φ and E, respectively, of checking the existence of a weak strategy. The following establishes the computational complexity of checking the existence of a weak strategy for an arbitrary LTLf formula.

Lemma 2. Checking the existence of a weak strategy for φ under E is: PSPACE-complete wrt φ; and 2EXPTIME-complete wrt E.

The algorithm for checking if the agent has active responsibility for φ under σag and E checks both CHECKWIN(φ, E, σag) and EXISTSWEAK(¬φ, E). Such algorithm is sound and complete by Theorem 1. Its complexity establishes membership of checking active responsibility. Hardness of checking active responsibility follows by a polynomial-time reduction from checking if a strategy σag is winning for φ under E, whose hardness is shown in Lemma 1. The reduction shows that σag is winning for φ under E iff the agent has active responsibility for φ ∧ ¬y under E and σag, where y is a new atom under agent's control. Putting together membership and hardness of checking active responsibility, we obtain the complexity characterization in Theorem 2.

4 Passive Responsibility Anticipation

While active responsibility captures the notion of an agent forcing φ to occur, passive responsibility consists in the agent merely letting φ occur. In this context, we distinguish between responsibility anticipation and attribution. The first is an "ex ante" notion, we want to check whether the currently selected agent strategy allows for φ to occur; the latter is an "ex post" notion, in the actual history, generated by the currently selected agent strategy, φ occurred, and we want to check if the agent let it happen. Note that this distinction is not meaningful for active responsibility: to decide whether the agent has active responsibility for φ we need to check all histories consistent with its strategy, so looking at a specific history is not relevant. In other words, the definitions of anticipation and attribution for active responsibility are equivalent.

In the context of passive responsibility, we also distinguish between weak and strong responsibility. The former captures that, given the environment response, there exists another agent strategy which would have falsified φ; this is the "classical" notion of passive responsibility and is widely studied in the literature [Lorini et al., 2014; Parker et al., 2023]. The latter captures that there exists another agent strategy that would have been better at falsifying φ, considering all possible environment responses. As emphasized in Section 1, if an agent has strong passive responsibility for φ, then it cannot give an "excuse" for letting φ occur. To the best of our knowledge, this notion is novel to our work.

Definition 2 (Weak Passive Responsibility Anticipation). The agent anticipates weak passive responsibility for φ under σag and E if: (i) there exists an environment strategy σenv ∈ ΣE such that Play(σag, σenv) |= φ; and (ii) there exists an agent strategy σ′ag such that Play(σ′ag , σenv) ̸|= φ.

The definition of strong passive responsibility is based on the game-theoretic notion of dominance [Apt and Gr¨adel, 2011; Aminof et al., 2021]. Let σ1 and σ2 be agent strategies. We say that σ1 dominates σ2 for φ under E, written σ1 ≥φ|E σ2, if Play(σ2, σenv) |= φ then Play(σ1, σenv) |= φ for every environment strategy σenv ∈ ΣE. Furthermore, we say that σ1 strictly dominates σ2, written σ1 >φ|E σ2, if σ1 ≥φ|E σ2 and σ2 ̸≥φ|E σ1. Intuitively: σ1 ≥φ|E σ2 means that σ1 is at least as good as σ2 (wrt φ and E); σ1 >φ|E σ2 means that σ1 is strictly better than σ2 (wrt φ and E).

Definition 3 (Strong Passive Responsibility Anticipation). The agent anticipates strong passive responsibility for φ under σag and E if: (i) there exists an environment strategy σenv ∈ ΣE such that Play(σag, σenv) |= φ; and (ii) there exists an agent strategy σ′ag such that σ′ag ≥¬φ|E σag and Play(σ′ag , σenv) ̸|= φ.

Weak and strong passive responsibility anticipation are related to a form of strategies called dominant and besteffort, respectively, which have been recently investigated in the literature on reactive synthesis [Aminof et al., 2021; Aminof et al., 2023]. In what follows, we briefly review dominant and best-effort strategies in the context of LTLf .

Formally, an agent strategy σag is dominant for φ under E if σag ≥φ|E σ′ag for every agent strategy σ′ag . An agent strategy is best-effort for φ under E if there does not exist another agent strategy σ′ag such that σ′ag >φ|E σag. Best-effort strategies always exist and capture the game-theoretic rationality principle that the agent should not use a strategy that is strictly dominated [Aminof et al., 2021]. If the agent uses a strictly dominated strategy σ1, say σ2 >φ|E σ1, then it is not doing its best wrt φ: if it used σ2 instead, it would have satisfied φ against a strictly larger set of environment strategies. Dominant strategies [Aminof et al., 2023] are slightly stronger than best-effort strategies, but do not always exist. Intuitively, a dominant strategy satisfies φ against every environment strategy for which it is possible to do so. Winning, dominant, and best-effort strategies are related [Aminof et al., 2023]. Specifically: if a winning strategy exists, the winning strategies are exactly the dominant strategies; and if a dominant strategy exists, the dominant strategies are exactly the best-effort strategies. The following establishes the relation between weak (resp. strong) passive responsibility anticipation and dominant (resp. best-effort) strategies.

Theorem 3. The agent anticipates weak (resp. strong) passive responsibility for φ under σag and E iff σag is not dominant (resp. is not best-effort) for ¬φ under E.

Theorem 3 leads to the following observations.

1. If no dominant strategy for ¬φ exists, the agent anticipates weak passive responsibility for φ regardless of the strategy it selects. In the context of LTLf , dominant strategies rarely exists [Aminof et al., 2023], i.e., that the agent anticipates weak passive responsibility is often unavoidable;
2. A best-effort strategy for ¬φ always exists, meaning that the agent can always avoid to anticipate strong passive responsibility for φ by selecting one such a strategy.

Putting such observations together with the relation between dominant and best-effort strategies, we can observe the following. The agent should always select a strategy σag that is best-effort for ¬φ. On one hand, we have that σag avoids strong passive responsibility anticipation for φ. On the other hand, if a dominant strategy for ¬φ exists, we have that σag is also dominant for ¬φ, and the agent does not anticipate neither weak nor strong passive responsibility for φ.

In other words, best-effort strategies unify under one strategy concept weak and strong passive responsibility anticipation. Given the relation between best-effort strategies and strong passive responsibility anticipation established in Theorem 3, we argue that strong passive responsibility is strictly more useful than classical weak passive responsibility to develop and evaluate responsibility-aware autonomous agents. This makes our notion of strong passive responsibility a significant contribution to the field of responsibility analysis.

We now illustrate such notions using the example of the autonomous agent that has to water a plant.

Example 2. Consider the same outcomes, agent strategies, and environment specification in Example 1.

1. The agent does not anticipate neither weak nor strong passive responsibility for φ under σ2 and E1. In fact, σ2 is dominant (and hence, best-effort) for ¬φ under E1. To see this, observe that σ2 is the unique agent strategy for which ¬φ is satisfied together with the environment strategy that the weather never rains.
2. The agent anticipates weak and strong passive responsibility for φ under σ1 and E1. In fact, σ1 is not dominant (and hence, not best-effort) for ¬φ under E1.

Consider the following outcomes and agent strategy

• φ′ = "The plant is either never watered or watered more than once"
• ¬φ′ = "The water is watered exactly once"
• σ3 = "Water the plant day and night". We have the following.
• The agent does not anticipate strong passive responsibility for φ′ under σ2 and E1. In fact, σ2 is best-effort for ¬φ′ under E1. However, the agent anticipates weak passive responsibility for φ′ under σ2 and E1. This is because σ2 not dominate σ1 wrt ¬φ′ : σ2 does not satisfy ¬φ′ together with the environment strategy that the weather never rains, whereas σ1 does.
• The agent anticipates both weak and strong passive responsibility for φ′ under σ3 and E1. In fact, σ3 is not best-effort for ¬φ′ under E1. To see this, observe that σ3 never satisfies ¬φ′ for every environment strategy. On the other hand, σ2 satisfies ¬φ′ together with the environment strategy that the weather rains only in the morning, i.e., σ2 strictly dominates σ3 wrt ¬φ′ and E1.

We now study the decision problem of checking if the agent anticipates weak (resp. strong) passive responsibility. That is: given an LTLf formula φ, an LTLf environment specification E, and an agent strategy σag, we want to decide whether the agent anticipates weak (resp. strong) passive responsibility for φ under σag and E. The following establish the computational complexity of the problems.

Theorem 4. Checking if the agent anticipates weak passive responsibility for φ under σag and E is: PSPACE-complete wrt φ; 2EXPTIME-complete wrt E; and polynomial wrt σag.

Theorem 5. Checking if the agent anticipates strong passive responsibility for φ under σag and E is: 2EXPTIME-complete wrt φ and E; and polynomial wrt σag.

We prove membership in Theorems 4 and 5 constructively by exhibiting a sound and complete algorithm for checking their corresponding responsibility notion.

We consider weak passive responsibility first. Based on Theorem 3, checking weak passive responsibility anticipation can be reduced to checking if a strategy is (not) dominant. In what follows, we give an algorithm to check if a strategy σag is dominant for φ under E, denoted CHECKDOM(φ, E, σag):

1. Let Y ′ = {y′ s.t. y ∈ Y} and X ′ = {x′ s.t. x ∈ X};
2. Define φ′ and E ′ as copies of φ and E over Y ′ ∪X ′ ;
3. N¬φ = TONFA(¬φ) and Nφ′ = TONFA(φ′ )
4. AE = TODFA(E) and AE ′ = TODFA(E ′ )
5. WE = ENVWIN(AE) andWE ′ = ENVWIN(AE ′)
6. A′E = RESTR(AE,WE) and A′E ′ = RESTR(AE ′ ,W ′E )
7. Aσag = TODFA(σag)
8. N = AY̸=Y ′ × (N¬φ × A′E × Aσag ) × (Nφ′ × A′E ′ )
9. if NONEMPTY(N) return false; else return true

Intuitively, CHECKDOM(φ, E, σag) checks the existence of a pair of traces (π, π′ ) such that, for some environment strategy σenv enforcing E, we have that π = Play(σag, σenv) |= ¬φ, and, for some agent strategy σ′ag distinct from the currently selected agent strategy σag, we have that π′ = Play(σ′ag , σenv) |= φ, i.e., π and π′ witness that σag is not dominant for φ, as it does not dominate σ′ag . To do so, CHECKDOM(φ, E, σag) checks language nonemptiness of an automaton N obtained by product of several automata, including:

• AY̸=Y ′ , whose language is the set of pairs of traces (π, π′ ) such that, if the agent makes the same choices

in both π and π′ , then the environment does the same (see Figure 1);

• (N¬φ×A′E ×Aσag ), whose language is the set of traces π = Play(σag, σenv) |= ¬φ, where σag is the input strategy and σenv is some environment strategy enforcing E;
• (Nφ′ ×A′E ′), whose language is the set of traces π′ = Play(σ′ag , σenv) |= φ for some agent strategy σ′ag and some environment strategy σenv enforcing E.

By the notion of product of automata, the language of N is the set of pairs of traces (π, π′ ) mentioned above. It follows that σag is dominant for φ under E iff L(N) is empty.

The complexity of CHECKDOM(φ, E, σag) gives PSPACE and 2EXPTIME membership wrt φ and E, respectively, and polynomial complexity wrt σag. Its analysis is similar to that of CHECKWIN(φ, E, σag). The computational complexity of checking if a strategy is dominant is the following:

Lemma 3. Checking if σag is dominant for φ under E is: PSPACE-complete wrt φ; 2EXPTIME-complete wrt E; and polynomial wrt σag.

The algorithm for checking if the agent anticipates weak passive responsibility for φ under σag and E checks whether σag is not dominant for ¬φ under E, written ¬CHECKDOM(¬φ, E, σag). Such algorithm is sound and complete by Theorem 3 and its complexity establishes membership of checking weak passive responsibility anticipation. Hardness of weak passive responsibility anticipation follows by its relation with dominant strategies, established in Theorem 3, and hardness of checking if a strategy is dominant, established in Lemma 3. Putting together membership and hardness of weak passive responsibility anticipation, we obtain the complexity characterization in Theorem 4.

We now turn to the decision problem of checking strong passive responsibility anticipation. Based on Theorem 3, this problem is reducible to checking if a strategy is (not) besteffort. In what follows, we give an algorithm to check if a strategy σag is best-effort for φ under E. This algorithm bases on solving a DFA game, using the notions of winning and weak strategy. We reviewed winning strategies in DFA games in Section 2. In the context of a DFA game G, an agent strategy σag is weak if there exists an environment strategy σenv such that Play(σag, σenv) is accepted by G. The weakly winning region W ′ is defined analogously to the winning region, i.e., W ′ is the set of states of G where the agent has a weak strategy. The weakly winning region W ′ can be computed in polynomial time with a least fixpoint computation over the state space of G, written W ′ = WEAKREGION(G).

The following is the algorithm for checking if a strategy σag is best-effort for φ under E, denoted CHECKBE(φ, E , σag).

1. Aφ = TODFA(φ) and AE = TODFA(E);
2. WE = ENVWIN(AE); and A′E = RESTR(AE,WE);
3. G = Aφ ×A′E ;
4. W = WINREGION(G) andW ′ = WEAKREGION(G);
5. Aσag = TODFA(σag)
6. Gσag = G × Aσag .Say: SG × Sσag is the state set of Gσag ; s0 is the initial state of Gσag ; and F is the set of final states of Gσag ;
7. Wσag = {(sG, sσag ) ∈ SG ×Sσag ) | sG ∈ W};
8. W ′σag = {(sG, sσag ) ∈ SG ×Sσag ) | sG ∈W ′ };
9. for every state s ∈ SG ×Sσag reachable from s0:
10. (A) if s ∈ Wσag and there exists a path ρ = s · · · s′ such that s′ ̸∈ F and ρ can't be extended to reach F return false;
11. (B) else if s ∈ W ′σag \ Wσag and no path from s to F exists return false;

10. return true

CHECKBE(φ, E, σag) uses a characterization of best-effort strategies based on the notion of value of a history, which we sketch [Aminof et al., 2021]. Intuitively, the value of a history h is: +1 ("winning") if the agent has a winning strategy for φ under E starting from h; 0 ("pending") if the agent has a weak strategy for φ under E starting from h; and -1 ("losing") otherwise. A best-effort strategy is one that witness the maximum value of each history consistent with it. The DFA game G solved by CHECKBE(φ, E, σag) (Lines 1-4) satisfies the following: histories whose runs lead to a state in the winning region W are winning; among the remaining histories, those whose runs lead to a state in the weakly winning region W ′ are pending; and the remaining are losing [Aminof et al., 2021]. By the notion of product of automata, the DFA Gσag (Lines 6-8) satisfies the following: histories whose runs lead to Wσag are winning and consistent with σag; and, among the remaining histories, those whose runs lead to W ′σag are pending and consistent with σag. CHECKBE(φ, E, σag) checks that the agent is able to: (A) reach a final state from every state inWσag regardless of the environment response, so that σag is winning in every winning history consistent with it; (B) reach a final state from every state in W ′σag \Wσag for some environment response, so that σag is weak in every pending history consistent with it. By the history-based characterization of best-effort strategies, σag is best-effort for φ under E iff neither (A) nor (B) is violated.

The complexity of CHECKBE(φ, E, σag) is dominated by constructing and solving games of doubly-exponential size in |φ| and |E|, so that CHECKBE(φ, E, σag) establishes 2EXPTIME membership wrt φ and E. The size of Gσag is polynomial in |σag|, which establishes polynomial complexity wrt σag. Hardness and computational complexity of checking if a strategy is best-effort are established in the following:

Lemma 4. Checking if σag is best-effort for φ under E is: 2EXPTIME-complete wrt φ and E; and polynomial wrt σag.

The algorithm for checking if the agent anticipates strong passive responsibility for φ under σag and E checks whether σag is not best-effort for ¬φ under E, written ¬CHECKBE(¬φ, E, σag). Such algorithm is sound and complete by Theorem 3 and its complexity establishes membership of checking strong passive responsibility anticipation. Hardness of strong passive responsibility anticipation follows by its relation with best-effort strategies, established in Theorem 3, and the complexity of checking if a strategy is besteffort, established in Lemma 4. Putting together membership and hardness of strong passive responsibility anticipation, we get the complexity characterization in Theorem 5.

5 Passive Responsibility Attribution

We now consider passive responsibility attribution after a history where φ occurs. Passive responsibility on histories is attributed "ex post" by counterfactually reasoning about what could have happened in the past, "fixing" the environment response to also comply with the history under consideration.

Definition 4 (Weak (resp. Strong) Passive Responsibility Attribution). The agent has weak (resp. strong) passive responsibility for φ under σag, E, and h such that h |= φ if: (i) there exists an environment strategy σenv ∈ ΣE such that h is consistent with σenv and h = Play(σag, σenv); and (ii) there exists another agent strategy σ′ag (resp. σ′ag ≥¬φ|E σag) such that Play(σ′ag , σenv) ̸|= φ.

As with passive responsibility anticipation, attribution of strong passive responsibility implies attribution of weak passive responsibility, and weak and strong passive responsibility attribution are related to dominant and best-effort strategies, respectively. The relation follows by observing that we can construct an LTLf environment specification Eh that captures exactly the environment strategies consistent with h. Formally, let h = (Y0 ∪ X0) · · · (Yn ∪ Xn) be a history. That h is consistent with an environment strategy σenv means that Xi = σenv(Y0 · · · Yi) for every i ≥ 0. Such behavior can be captured by the following LTLf environment specification.

It easy to see that h is consistent with σenv iff σenv enforces Eh. It follows that E ∧ Eh captures exactly the set of environment strategies enforcing E and consistent with h. We then derive the relation between passive responsibility attribution and dominant and best-effort strategies.

Theorem 6. The agent is attributed weak (resp. strong) passive responsibility for φ under σag, E, and h iff σag is not dominant (resp. best-effort) for ¬φ under E ∧ Eh.

Next. we turn to the decision problem of checking weak (resp. strong) passive responsibility attribution on histories: given an LTLf formula φ, an LTLf environment specification E, an agent strategy σag, and an history h, we want to decide whether the agent has weak (resp. strong) passive responsibility for φ under E, σag and h or not. The computational complexity of the problems is established in the following.

Theorem 7. Checking if the agent has weak passive responsibility for φ under σag, E, and h is: PSPACE-complete wrt φ; 2EXPTIME-complete wrt E; polynomial wrt σag; and polynomial wrt h.

Theorem 8. Checking if the agent has strong passive responsibility for φ under σag, E, and h is: 2EXPTIME-complete wrt φ and E; polynomial wrt σag; and polynomial wrt h.

Based on Theorem 6, we can reduce checking if the agent has weak (resp. strong) passive responsibility for φ under E, σag, and h to checking whether σag is not dominant (resp. best-effort) for ¬φ under E ∧ Eh. We can do so by adapting the algorithms in Section 4, written ¬CHECKDOM(¬φ, E ∧ Eh, σag) (resp. ¬CHECKBE(¬φ, E∧Eh, σag)). The complexity of such algorithms establish membership of weak (resp. strong) passive responsibility attribution wrt φ, E, and σag. To obtain polynomial polynomial complexity wrt h, observe that DFA AE∧Eh can be constructed in polynomial time as the product AE × AEh . In turn, AEh can be constructed in polynomial time in the length of h as in Figure 2. To see why AEh captures exactly the environment strategies consistent with h = (Y0∪X0) · · · (Yn∪Xn), observe that transitions of the form Yi ∧¬Xi lead to a non-final sink state, as no environment strategy σenv consistent with h plays ¬Xi when the agent plays Y0 · · · Yi. Hardness of weak (resp. strong) passive responsibility attribution follows by its relation with dominant (resp. best-effort) strategies, established in Theorem 6, and hardness of checking if a strategy is dominant (resp. besteffort), established in Lemma 3 (resp. Lemma 4). Putting together membership and hardness of weak (resp. strong) passive responsibility attribution, we get the complexity characterization in Theorem 7 (resp. Theorem 8).

6 Conclusion

We observe that once these responsibility notions are characterized, they can be used not only to assess responsibility but also during strategy synthesis. This ensures the generation of strategies that avoid unintended responsibility, opening a research avenue into responsibility-aware strategy synthesis.

We focused on a single agent with a first-person perspective, examining responsibility from the agent's viewpoint rather than any third-person perspective. However, our work could be extended to a multi-agent setting, where each agent operates within an environment shaped by both the environment itself and the actions of other agents. We plan to explore these directions further in the future.

Acknowledgments

This work is supported in part by the ERC Advanced Grant WhiteMech (No. 834228), the PRIN project RIPER (No. 20203FFYLK), the PNRR MUR project FAIR (No.PE0000013), and the UKRI Erlangen AI Hub on Mathematical and Computational Foundations of AI. Emiliano Lorini is supported by the ANR projects EpiRL (grant number ANR-22-CE23-0029) and ALoRS (grant number ANR21-CE23-0018-01). Gianmarco Parretti is supported by the Italian National Ph.D. on AI at "La Sapienza".