Counterfactual Scenarios for Automated Planning

TL;DR

This paper introduces a new explanation approach for automated planning using counterfactual scenarios, which identify minimal modifications to planning problems to achieve desired properties, enhancing interpretability beyond traditional plan modifications.

Contribution

It proposes a novel counterfactual scenario framework for planning explanations based on properties specified by extless ltlf extgreater formulas, with complexity analysis and practical viability.

Findings

Counterfactual scenarios can be generated with complexity comparable to plan computation.

The framework captures higher-level properties of planning problems.

Practical algorithms are feasible based on the complexity results.

Abstract

Counterfactual Explanations (CEs) are a powerful technique used to explain Machine Learning models by showing how the input to a model should be minimally changed for the model to produce a different output. Similar proposals have been made in the context of Automated Planning, where CEs have been characterised in terms of minimal modifications to an existing plan that would result in the satisfaction of a different goal. While such explanations may help diagnose faults and reason about the characteristics of a plan, they fail to capture higher-level properties of the problem being solved. To address this limitation, we propose a novel explanation paradigm that is based on counterfactual scenarios. In particular, given a planning problem $P$ and an \ltlf formula $\psi$ defining desired properties of a plan, counterfactual scenarios identify minimal modifications to $P$ such that it admits plans that comply with $\psi$. In this paper, we present two qualitative instantiations of counterfactual scenarios based on an explicit quantification over plans that must satisfy $\psi$. We then characterise the computational complexity of generating such counterfactual scenarios when different types of changes are allowed on $P$. We show that producing counterfactual scenarios is often only as expensive as computing a plan for $P$, thus demonstrating the practical viability of our proposal and ultimately providing a framework to construct practical algorithms in this area.

Tables

Table 1. Table 1: Overview of the computational complexity results.

	Initial State	Goals	Action Preconditions
	$C_{\mathrm{𝑖𝑛𝑖𝑡}}$	$C_{\mathrm{𝑔𝑜𝑎𝑙}}$	$C_{\mathrm{𝑎𝑐𝑡}}$
${\Xi }_{\exists }$	PSPACE-c.	PSPACE-c.	PSPACE-c.
	Theorem 2	Theorem 3	Theorem 5
${\Xi }_{\forall }$	PSPACE-c.	PSPACE-c.	$\in$ NEXPNP
	Theorem 2	Theorem 4	Theorem 6

Equations

$$\displaystyle\begin{aligned} \psi\coloneqq\mathop{\Box}&\bigl{(}\mathtt{at(truck,coffee{-}shop)}\rightarrow\mathop{\bigcirc}\mathtt{at(truck,butchery)}\bigr{)}\\ {}\land{}&\bigl{(}\neg\mathtt{at(truck,butchery)}\mathrel{\mathcal{U}}\mathtt{at(truck,coffee{-}shop)}\bigr{)}\end{aligned}$$

$$\left\{\begin{array}{rl}& \mathtt{at}(\mathtt{driver},\mathtt{coffee}-\mathtt{shop})\wedge \\ & \mathtt{at}(\mathtt{truck},\mathtt{coffee}-\mathtt{shop})\wedge \\ & \mathtt{link}(\mathtt{coffee}-\mathtt{shop},\mathtt{butchery})\end{array}\right\}$$

$$\psi :=\square \left[\begin{array}{rl}& \left(\begin{array}{rl}& \mathtt{at}(\mathtt{meat},\mathtt{butchery})\wedge \\ & \mathtt{at}(\mathtt{coffee},\mathtt{coffee}-\mathtt{shop})\end{array}\right)\to \\ \to & ◊\mathtt{at}(\mathtt{truck},\mathtt{depot})\end{array}\right]$$

$$\left\{\begin{array}{rl}& \mathtt{at}(\mathtt{meat},\mathtt{butchery})\wedge \\ & \mathtt{at}(\mathtt{coffee},\mathtt{coffee}-\mathtt{shop})\wedge \\ & \mathtt{at}(\mathtt{truck},\mathtt{depot})\end{array}\right\}$$

$$a(s)(f):=\{\begin{array}{ll}v& \text{if f:=v∈mboxeffa}\\ s(f)& \text{otherwise}\end{array}$$

$$\psi :=p$$

$$\mid ◯\psi \mid \sim ◯\psi \mid \psi \mathcal{U}\psi \mid ◊\psi \mid \square \psi$$

$${\Xi }_{\exists }(P,\psi ,C):=\underset{\begin{array}{c}\text{P′∈P s.t.}\\ \text{∃π′∈ΠP′ s.t.}\\ {\pi }^{\prime }\models \psi \end{array}}{\mathrm{argmin}}{\Delta }_C^P(P^{\prime })$$

$${\Xi }_{\forall }(P,\psi ,C):=\underset{\begin{array}{c}\text{P′∈P s.t.}\\ \text{ΠP′=∅ and}\\ \forall {\pi }^{\prime }\in {\Pi }_{P^{\prime }}{\pi }^{\prime }\models \psi \end{array}}{\mathrm{argmin}}{\Delta }_C^P(P^{\prime })$$

$$C_{\mathit{init}}\coloneqq\left\{(P,P^{\prime})\middle|\begin{array}[]{@{}c@{}}P=\langle F,A,I,G\rangle,\,P^{\prime}=\langle F,A,I^{\prime},G\rangle\\[5.0pt] \text{$I=I^{\prime}$ except at most one fluent}\end{array}\right\}$$

$$C_{\mathit{goal}}\coloneqq\left\{(P,P^{\prime})\middle|\begin{array}[]{@{}c@{}}P=\langle F,A,I,G\rangle,\,P^{\prime}=\langle F,A,I,G^{\prime}\rangle\\[5.0pt] \#\bigl{[}(G\wedge\neg G^{\prime})\vee(G^{\prime}\wedge\neg G)\bigr{]}=1\end{array}\right\}$$

$$C_{\mathit{act}}\coloneqq\left\{\!(P,P^{\prime})\middle|\begin{array}[]{@{}c@{}}P=\langle F,A,I,G\rangle,\,P^{\prime}=\langle F,A^{\prime},I,G\rangle\\[5.0pt] A\setminus A^{\prime}=A^{\prime}\setminus A=\{a\}\\[5.0pt] \mbox{eff}_{a}=\mbox{eff}_{a^{\prime}}\\[5.0pt] \#\left[{}\lor{}\begin{aligned} &(\mbox{pre}_{a}\land\neg\mbox{pre}_{a^{\prime}})\\ &(\mbox{pre}_{a^{\prime}}\land\neg\mbox{pre}_{a})\end{aligned}\right]=1\end{array}\right\}$$

Full text

1 Introduction

The widespread adoption of AI solutions for consequential decision-making tasks has fuelled considerable interest in Explainable AI (XAI). This is particularly true in the area of Machine Learning (ML), where black-box models are often deployed in applications such as credit risk analysis (?) or bail approval (?). In these settings, most approaches focus on explaining single-shot decisions (\iepredictions) produced by ML models but are often unable to explain more sophisticated decision-making tasks involving multiple reasoning steps.

The planning community has long recognised the importance of providing explanations for sequential decision-making tasks (?). As a result, a host of explainability approaches have been proposed. Examples include model reconciliation (?; ?), which focuses on resolving potential discrepancies between an AI agent’s internal model and a human’s mental model, and contrastive explanations (?; ?; ?), which highlight differences between a plan generated by an AI and a user-suggested alternative, showing why the former was preferred.

Much less attention has been devoted to counterfactual explanations, a popular explanation framework that is favoured in XAI due to its intelligibility and alignment with human reasoning (?). Counterfactuals are actively studied in ML, where they are typically defined in terms of minimally altered inputs for which the ML model gives a different, more desirable output from that of the original input (?). Echoing this idea, recent work in planning proposed to characterise counterfactuals in terms of minimal modifications to an existing plan that would result in the satisfaction of a different goal (?).

Counterfactuals defined in this way are well suited to reason about local properties of a plan, \iediagnose faults in it and potentially identify avenues for repair showing how a plan would need to change for a desired outcome to be attained. However, in many practical applications, users are often interested in understanding how characteristics of a planning problem may affect the quality of plans that can be produced. In such cases, local counterfactual explanations are of little use as they fail to capture properties of the planning problem being solved, leaving many unanswered questions about the fundamental relationships between problem structure and plan properties.

Contributions. In this paper, we fill this gap and propose a novel explanation paradigm based on the concept of counterfactual scenarios for automated planning problems. Differently from existing proposals, our explanations rely on counterfactual modifications of the planning problem itself, thus pointing users of planning software to what would need to be changed in the original problem formulation for a given course of action to be observed. More formally, given a planning problem $P$ and an LTLf (?) formula $\psi$ defining desired properties of a plan, counterfactual scenarios identify minimal modifications to $P$ such that it admits plans that comply with $\psi$. We investigate the computational complexity of generating such explanations under counterfactual modifications that can alter the initial state of $P$, the structure of its actions or its goals. We focus our analysis on two qualitative variants of counterfactuals scenarios: existential counterfactual scenarios ($\exists$), which identify modifications to $P$ such that it admits at least one plan satisfying $\psi$, and universal counterfactual scenarios ($\forall$), which modify $P$ in such a way that all its valid plans satisfy $\psi$. We demonstrate the feasibility of our proposal by showing that generating $\exists$ and $\forall$ counterfactual scenarios often has a computational complexity comparable to finding a plan for the original problem, thus providing a foundation for developing practical algorithms in this domain.

Related work. The challenge of explaining AI behaviours in sequential decision-making settings has gained considerable attention (see, \eg (?) for a recent account). As a result, a host of approaches have been proposed both in model-based and model-free settings (see, \eg ? (?) and ? (?) for a general overview). In the following, we focus on counterfactual explanations for sequential decision-making tasks, but refer the reader to Section 7 for a broader discussion of related work in the planning literature.

While research on counterfactuals for sequential decision-making is still in its infancy, several proposals have already been put forward. For instance, counterfactuals for automated planning problems have been defined by ? (?) as minimal modifications to an existing plan that would result in the satisfaction of a different goal. This definition echoes existing characterisations of counterfactuals in ML (?) and is closely related to the literature on plan repair (?). However, differently from the aforementioned definition, our counterfactuals identify changes in the planning problem itself and can thus be used to point to how changes in the structure of a problem may affect plan properties.

Counterfactuals have also been investigated in the context of sequential decision-making problems modelled by Markov Decision Processes (MDPs). For instance, ? (?) studied the problem of generating counterfactual strategies for MDPs by computing minimal modifications to an original strategy that would lead to reaching desirable states high probability. Similar efforts have been made in the Reinforcement Learning arena, as summarised by ? (?). While the works above propose notions that vary based on the specific changes that can be effected on a policy, they still frame counterfactuals as minimally altered policies, differently from our counterfactual scenarios. Finally, causality-based counterfactuals for MDPs have been investigated (?; ?). In this line of work, counterfactual explanations are defined in terms of paths that diverge by at most $k$ actions from a given initial path in the MDP, again marking a key difference from our proposal.

Structure of the paper. In the next section, we motivate and explain the need for counterfactual explanations whose scope extends beyond existing proposals, while Section 3 provides some background concepts on planning and LTLf. Then, Section 4 presents our novel notion of counterfactual scenarios, and in Section 5 we present three concrete classes of counterfactuals that we are interested in analysing. Section 6 proves computational complexity results for such classes. Finally, we discuss the implications of our results and draw our conclusions in Section 7 and Section 8.

2 A motivating example

To see what makes counterfactual scenarios interesting and useful, let us consider an example based on the food delivery domain originally formulated by ? (?).

Example 1**.**

The domain features one driver, one truck and three locations: a depot, a butchery, and a coffee shop. All locations are connected by roads with no pedestrian access, modelled by a predicate link(?from,?to) (links are directed). Both the goods and the truck are initially located at the depot (at(coffee,depot), at(meat,depot), at(truck,depot)), while the driver is located at the coffee shop (at(driver,coffee shop)). The goal is for the driver to deliver meat to the butchery and coffee beans to the coffee shop ($\texttt{at(meat,butchery) }\wedge\texttt{ at(coffee,coffee shop)}$). To achieve this goal, the following actions can be performed:

• •

load(?item,?truck,?loc)**: loads an item onto the truck, provided both are at the same location. When an item is loaded, it is removed from its location and is marked as stored inside the truck ($\neg\texttt{at(?item,?truck)}\wedge\texttt{in(?item,?truck)}$);

• •

unload(?item,?truck,?loc)**: removes an item from the truck, making it available at the location where it was unloaded;

• •

drive(?truck,?from,?to,?driver): allows to drive the truck between two specified locations, provided that they are connected by a road, \ielink(?from, ?to) is true. The driver and the truck must start from the same location for this action to be executable.

A visual representation of this problem is shown in Figure 1.

Existing approaches to define counterfactual explanations for sequential problems assume the availability of an initial action sequence from which the counterfactual explanation can be obtained. However, there may be cases where the planning problem does not admit a solution and the problem of generating counterfactuals for such instances becomes ill-defined. For instance, the planning problem described in Example 1 does not admit a solution, as the driver has no way to reach the truck and carry out deliveries. As a consequence, no initial action sequence can be determined to seed the search for a counterfactual explanation. In situations where a solution is unattainable, our existential counterfactual scenarios can help identify modifications to the planning problem that would make the problem solvable, as demonstrated in Example 2

Example 2**.**

The planning problem described in Example 1 does not admit a solution, as the driver is initially located away from the truck with no way to reach it. In such cases, an existential counterfactual scenario highlights how the initial problem should be changed for it to admit a solution. A possible existential counterfactual scenario can therefore be obtained by changing the initial location of the driver from at(driver, coffee-shop) to at(driver, depot). As a result, the new planning problem obtained by implementing this change admits (at least) one plan:

• •

load(meat,truck,depot)**

• •

load(coffee,truck,depot)**

• •

drive(truck,depot,butchery,driver)**

• •

unload(meat,truck,butchery)**

• •

drive(truck,butchery,coffee-shop,driver)**

• •

unload(coffee,truck,coffee shop)**

The counterfactual scenario in Example 2 helps users of planning software deal with unsolvable planning problems, potentially identifying changes in the problem formulation that determined unsolvability. These kind of explanations can be used to complement existing efforts, \eg (?; ?) and improve the user experience, debugging process, or overall effectiveness of planning tools. However, existential counterfactual scenarios also prove useful when planning problems are solvable to begin with, as discussed in Example 3.

Example 3**.**

Consider the planning problem given by the existential counterfactual scenario in Example 2. Suppose now that the user requires that in some plans, the truck visits the coffee shop before making a delivery to the butchery. This can be captured by the following logical specification:

[TABLE]

Satisfying this requirement is impossible in the original domain, as driving from the coffee shop to the butchery would require a (directed) connection between the two locations. This fact can be highlighted by means of an existential counterfactual scenario, showing how the preconditions of the action drive should be minimally changed for some valid plans to satisfy $\psi$. A possible solution to the problem corresponds to a modified planning problem where the precondition of the action is weakened to:

[TABLE]

With this change, the truck is allowed to visit the butchery after the coffee shop in some of the plans admitted by the existential counterfactual scenario.

Example 3 showed how existential counterfactual scenarios can result in changes that bring about at least one plan satisfying user requirements. However, depending on the application, users may be interested in changes that constrain the planning problem to have all its valid solutions comply with a specification. Our universal counterfactual scenarios can achieve this, as demonstrated in Example 4.

Example 4**.**

Consider the existential counterfactual scenario from Example 2. Suppose now that the user requires that in all plans, the truck should always go back to the depot (eventually) after completing all deliveries. This can be expressed by the following logical specification:

[TABLE]

Universal counterfactual scenarios can help identifying changes in the planning problem that would satisfy the requirement above. For instance, strengthening the goal to:

[TABLE]

would result in the the truck eventually visiting the depot in all plans admitted by the modified planning problem.

This section introduced the intuition behind counterfactual scenarios, highlighting some use cases. What follows will formally define our explanation framework and present a detailed analysis of the computational complexity of deciding the existence of such explanations.

3 Preliminaries

For the sake of this paper, we focus on classical planning, adopting a general formulation with arbitrary formulae as preconditions. While the definitions below easily generalize to numeric planning, we restrict ourselves to the classical, finite-state case because numeric planning is in general undecidable thus making all the explainability problems addressed in this paper trivially undecidable as well.

Definition 1** (Planning problem).**

A (ground) planning problem is a tuple $P=\langle F,A,I,G\rangle$ where:

$F$* is a set of Boolean fluents;* 2. 2.

$A$* is a set of actions, where each $a\in A$ comes with:*

1. (a)

a precondition $\mbox{pre}_{a}$ expressed as a formula over $F$; and 2. (b)

a set of effects $\mbox{eff}_{a}$ of the form $f:=v$ where $f\in F$ and $v\in\{\top,\bot\}$;111For the sake of simplicity, we assume that in every action there is at most one effect for a fluent $f$. 3. 3.

$I:F\rightarrow\{\top,\bot\}$* is the initial state encoded as a total assignment of truth values to fluents in $F$;* 4. 4.

$G$* is the goal condition expressed as a formula over $F$.*

We indicate with $\mathcal{P}$ the set of all possible planning problems.

Definition 2** (Plan state).**

A state for a planning problem $P=\langle F,A,I,G\rangle$ is a total assignment $s:F\rightarrow\{\top,\bot\}$ of values to fluents.

Definition 3** (Applicable action).**

Given a planning problem $P=\langle F,A,I,G\rangle$, an action $a\in A$ is applicable in state $s$ if the formula $\mbox{pre}_{a}$ is satisfied by the assignment of $s$.

Definition 4** (Successor state).**

Given a planning problem $P=\langle F,A,I,G\rangle$ and a state $s$, the successor $a(s)$ of an applicable action $a\in A$ is a state such that:

[TABLE]

Definition 5** (Sequential plan).**

A sequential plan for a planning problem $P=\langle F,A,I,G\rangle$ is a sequence of actions $\pi=\langle a_{0},\ldots,a_{n-1}\rangle$ where $a_{i}\in A$. When denoting $s_{0}=I$ and $s_{i+1}=a_{i}(s_{i})$, we say $\pi$ is valid if every $a_{i}$ is applicable in $s_{i-1}$ and $s_{n}\models G$.

Given a planning problem $P=\langle F,A,I,G\rangle$, we write $\Pi_{P}$ for the set of all valid plans. Note that there is no reason for a plan in classical planning for visiting twice the same state, as any such plan can be cut into a shorter one that does not. For this reason, we assume w.l.o.g. all plans in $\Pi_{P}$ to be devoid of state loops.

Our counterfactual scenarios are based on the notion of satisfaction of an LTLf formula (?). LTLf is a propositional modal logic interpreted over finite words. We consider here the standard syntax of LTLf where a formula $\psi$ is defined by the following grammar:

[TABLE]

where $p\in F$ with $F$ being some finite set of propositions.

The semantics is defined as usual in the literature (we omit the formal definition because of space concerns), where: $\mathop{\bigcirc}\psi$ and $\mathrlap{\hskip 1.0pt\sim}{\mathop{\bigcirc}}\psi$ are the strong and weak tomorrow operators which state the truth of $\psi$ at the next state (only if it exists, in the case of the weak operator); $\psi_{1}\mathrel{\mathcal{U}}\psi_{2}$ is the until operator stating that $\psi_{2}$ will happen in the future and $\psi_{1}$ holds everywhere until then; $\mathop{\Diamond}\psi$ and $\mathop{\Box}\psi$ are the eventually and globally operators, definable respectively as $\mathop{\Diamond}\psi\equiv\top\mathrel{\mathcal{U}}\psi$ and $\mathop{\Box}\psi\equiv\neg\Diamond\neg\psi$, which mandates $\psi$ to hold somewhere in the future or always in the future.

We recall that the satisfiability and validity problems for LTLf, \iedeciding respectively whether there exists a word satisfying a given formula or whether all words satisfy a given formula, are both PSPACE-complete (?), which also happens to be the same computational complexity of the plan existence problem in classical planning (?).

With a slight abuse of notation, we say that a plan $\pi$ satisfies an LTLf formula $\psi$ if $\langle s_{0},s_{1},\ldots,s_{n}\rangle\models\psi$, where the $s_{i}$ are defined as in Definition 5.

4 Abstract Counterfactual Scenarios

In this section, we introduce a general and abstract formulation of our counterfactual scenarios which can be instantiated into several different kind of explanations depending on the case at hand. In Section 5 we instantiate the framework considering some interesting concrete classes of counterfactuals which then will be studied in Section 6 from a computational complexity perspective.

In the following, let $\mathbb{P}$ denote the class of all the possible planning problems as in Definition 1.

Definition 6** (Possible changes).**

A possible-change relation is a relation $C\subseteq\mathbb{P}\times\mathbb{P}$.

Intuitively, a possible-change relation describes abstractly which classes of changes are admitted. Then, a counterfactual scenario can be defined as a planning problem that can be obtained by a minimal sequence of admitted changes. This notion is formally defined by introducing an abstract transition system whose worlds are planning problems.

Definition 7** (Counterfactual transition system).**

Let $P$ be a classical planning problem, and let $C$ be a possible-change relation. A counterfactual transition system for $P$ and $C$ is the transition system $\mathcal{C}(P,C)\coloneqq\langle\mathbb{P},P,C\rangle$ where:

$\mathbb{P}$* is the set of worlds of the transition system;* 2. 2.

$P$* is the initial world of the system.* 3. 3.

$C$* is the accessibility relation of the system;*

A path $\gamma$ in $\mathcal{C}(P,C)$ is a sequence of problems $\langle P_{0},P_{1},\ldots,P_{n}\rangle$ where $P_{0}=P$ and $(P_{i},P_{i+1})\in C$ for each $i\in[0,n-1]$. The cost of a path is its length $\left|\gamma\right|$.

Given a planning problem $P^{\prime}$ and a possible-change relation $C$, we denote as $\Gamma_{C}(P^{\prime})$ all the paths ending in $P^{\prime}$ in $\mathcal{C}(P,C)$. We denote as $\Delta^{P}_{C}(P^{\prime})=\min_{\gamma\in\Gamma_{C}(P^{\prime})}\left|\gamma\right|$ the minimum cost of reaching $P^{\prime}$.

Definition 8**.**

Given a planning problem $P=\langle F,A,I,G\rangle$, an LTLf formula $\psi$ defined over the alphabet $F$ and a possible-change relation $C$, an existential counterfactual scenario is a planning problem $\Xi_{\exists}(P,\psi,C)$ such that:

[TABLE]

Similarly, a universal counterfactual scenario is a planning problem $\Xi_{\forall}(P,\psi,C)$ such that:

[TABLE]

Note that existential and universal counterfactuals might not exist if there is no problem $P^{\prime}$ reachable in $\mathcal{C}(P,C)$ admitting a valid plan that satisfies $\psi$.

Moreover, our definitions do not rule out the possibility that a counterfactual scenario for a problem $P$ is $P$ itself. However, this behaviour is unlikely to happen in practical settings and depends on the type of counterfactual scenario being sought. Typically, users of planning tools are interested in explaining a plan $\pi$ after it has been generated by a planner. When searching for an existential counterfactual scenario, it is possible for $\Xi_{\exists}(P,\psi,C)$ to be equal to $P$, because the planner might have picked a plan not satisfying $\psi$ non-deterministically from the pool of existing plans. However, if the user is interested in universal counterfactual scenarios, then $\Xi_{\forall}(P,\psi,C)$ for $P$ cannot be $P$ itself since the existence of $\pi$ would violate Definition 8.

5 Concrete Classes of Counterfactuals

The definitions of existential and universal counterfactual scenarios given in the previous section are intentionally quite abstract and general, and in applications they need to be instantiated over concrete classes of possible-change relations. In this section, we describe three possible such instantiations, which define as many different classes of counterfactual scenarios that are interesting in practice. Then, Section 6 will study the associated decision problems from a complexity-theoretic standpoint. In particular, we focus on counterfactuals where we allow changes in the initial state, the goal conditions or the action preconditions. For the sake of this paper, we exclude the possibility of modifying the effects of actions for two reasons. First, for counterfactuals to be useful in practice, they need to be plausible: they should represent scenarios that could realistically occur or be implemented, rather than propose unachievable changes to an action’s effects (\eg, proposing the complete removal of all resource consumption following the execution of an action, which might be practically impossible). Second, from a technical standpoint, one needs to be very careful when choosing which effects are allowed to be changed to avoid constructing trivial counterfactuals (\eg, achieving the goal from the first action by adding a goal state itself goal as an effect). Nonetheless, the framework introduced in the previous section can easily accommodate the change of effects and one can describe the plausibility constraints in the possible-change relation.

We start from the simplest instance of our framework, where only changes to the initial state are allowed. To formalise this requirement, we define a possible-change relation that admits problems that differ for the initial state only. Let $F$ be a set of fluents, then:

[TABLE]

Note that single edits can change the assignment of at most one single fluent in the initial state, so the distance between two different initial states is the minimum number of edits needed to change one into the other.

A slightly more involved definition arises when one wants to admit changes to the goal conditions. In contrast to initial states, goals are expressed as arbitrary Boolean formulas, therefore a slight change may be more semantically relevant than it appears. To capture this nuance, when comparing two different goal conditions we count the number of differing truth assignments of the conditions, and we only admit to add or remove one truth assignment at a time, obtaining the following definition:

[TABLE]

where $\#[\phi]$ is the number of truth assignments of $\phi$.

Note that the definition of $C_{\mathit{goal}}$ considers both changes that strengthen the goal condition, \iethat remove goal states, and those that weaken the condition, \iethat add goal states. However, note that, for existential counterfactuals, strengthening the goal is never useful, because if a plan satisfying $\psi$ does not exist, removing goal states will not help. Conversely, weakening the goal is always sufficient, because adding a state reachable by a valid plan always costs less than adding it and removing something else.

For universal counterfactuals, instead, weakening is never useful, because if a plan not satisfying $\psi$ exists, it cannot disappear by adding goal states. However, note that strengthening the goal is not the only option in the universal case, because a counterfactual may be found by considering an entirely disjoint set of goal states.

A class of counterfactual scenarios that is apparently similar to the latter is that obtained by admitting changes to actions’ preconditions. In this case we define a possible-change relation that admits only problems where the only change is the precondition of a single action where a single truth assignment has been added or removed.

[TABLE]

Note that for this class of counterfactuals we can observe, similarly to the previous case, that in the existential case only weakening the preconditions make sense. Although the definitions of $C_{\mathit{goal}}$ and $C_{\mathit{act}}$ present many similarities, shortly we will see in Section 6 that they are computationally quite different.

Defining plausible scenarios. In concrete applications, not all possible changes in either the initial state, the goal or the action preconditions might be acceptable. For instance, in Example 1, at(truck, depot) and at(truck, butchery) cannot be both initially true, otherwise the model would allow the truck to be in two locations at the same time. Hence, one needs to impose additional plausibility constraints to control which changes are allowed to the planning problem. This can be easily achieved by leveraging the expressive power of LTLf. In the following, let $\phi_{init},\phi_{act},\phi_{goal}$ denote three propositional formulae defining plausibility constraints for the initial state, action preconditions and goal conditions respectively. To limit the changes in $C_{\mathit{init}}$, we simply conjoin the plausibility constraints (without temporal operators) in $\phi_{init}$ with $\psi$; in this way, we obviously constrain the possible initial states, because of the semantics of LTLf. For $C_{\mathit{goal}}$, we conjoin the formula $\Diamond(\mathrlap{\hskip 1.0pt\sim}{\mathop{\bigcirc}}\bot\land\phi_{goal})$ into $\psi$. Essentially, we are forcing $\phi_{goal}$ to hold on all the final states of a plan (where $\mathrlap{\hskip 1.0pt\sim}{\mathop{\bigcirc}}\bot$ holds). Finally, if we want to impose a propositional plausibility constraint on the precondition of an action $a$, we assume w.l.o.g. that there exists a fluent $f_{a}$ that is set to true by the effects of action $a$ and falsified by the effects of all the other actions. Then, we add the formula $\Box(\mathop{\bigcirc}f_{a}\rightarrow\phi_{act})$, forcing the formula $\phi_{act}$ to hold in the state where action $a$ has been applied. In all three cases above, imposing plausibility constraints can be done by simply extending the formula $\psi$ without complicating the problem further. As such, we do not need to explicitly consider plausibility constraints in the theoretical analysis presented in the next section.

6 The Hardness of Finding Counterfactuals

In this section we study the computational complexity of finding counterfactuals of the kinds introduced in Section 5. We will see that the decision problem for most of them surprisingly remains PSPACE-complete, which is the same complexity as finding a plan in the first place. A complete picture of the results is available in Table 1.

In our framework, the quality of plans is evaluated in terms of the satisfaction of an LTLf formula $\psi$ over the fluents $F$. Therefore, we need a way to link the two worlds of planning and LTLf. To this end, we can leverage a well-known result stating that any classical planning problem can be translated into a suitable LTLf formula that represents the plans of the problem and the states visited by those plans.

Proposition 1** (?** (?)).

For any classical planning problem $P=\langle F,A,I,G\rangle$ there exist:

an LTLf formula $[P]$ over the alphabet $A\cup F$ such that from any model of $[P]$ one can extract in polynomial time a plan for $P$ (not necessarily reaching the goal); 2. 2.

an LTLf formula $[P]_{G}$ over the alphabet $A\cup F$ such that from any model of $[P]_{G}$ one can extract in polynomial time a solution plan for $P$ (\iereaching the goal);

The extraction in polynomial time is actually a simple projection of the propositions from $A$ in the model of the LTLf formula: if proposition $a$ is true at a given time point it means action $a$ is executed in that step. Similarly, the propositions from $F$ encode the states visited by the plan.

Since the counterfactual scenarios are minimal objects, minimizing the number of edits, finding one is an optimization problem. Therefore, as is customary in complexity theory, our analysis is concerned with the decision problem associated with such an optimization problem.

Definition 9** (Counterfactual scenario existence problem).**

Let $C\subseteq\mathbb{P}\times\mathbb{P}$ be a possible-change relation. The existential counterfactual scenario existence problem under $C$, denoted $\operatorname{CSEP}_{\exists}(C)$, is the problem of deciding, given a planning problem $P$, an LTLf formula $\psi$, and a budget $K\geq 0$, whether $\Xi_{\exists}(P,\psi,C)$ exists and $\Delta^{P}_{C}(\Xi_{\exists}(P,\psi,C))\leq K$.

The universal counterfactual scenario existence problem under $C$, denoted $\operatorname{CSEP}_{\forall}(C)$, is defined similarly over $\Xi_{\forall}(P,\psi,C)$.

Our first result is that counterfactual scenario existence problems are, in general, PSPACE-hard.

Theorem 1**.**

Let $F$ be a set of fluents and $C\subseteq\mathbb{P}\times\mathbb{P}$ be a possible-change relation over $F$. Then, both $\operatorname{CSEP}_{\exists}(C)$ and $\operatorname{CSEP}_{\forall}(C)$ are PSPACE-hard.

Proof.

We go by reduction from the plan existence problem of classical planning which is known to be PSPACE-complete (?). Given $P=\langle F,A,I,G\rangle$, it is sufficient to ask for an existential or universal counterfactual scenario for a trivial formula $\psi\coloneqq\top$ and a cost $K=0$. The formula is trivially always satisfied, and the zero cost ensure to be unable to make any change to $P$. Then, since both the existential and the universal definitions require the counterfactual to have at least a solution, the counterfactual exists if and only if $P$ has a solution in the first place. ∎

Following Theorem 1, we can now focus specifically on showing that the decision problems for most of our particular classes of counterfactual scenarios belong to PSPACE and are therefore PSPACE-complete.

As in Section 5, we start from the class of counterfactuals where only changes to the initial state are admitted.

Theorem 2**.**

Both $\operatorname{CSEP}_{\exists}(C_{\mathit{init}})$ and $\operatorname{CSEP}_{\forall}(C_{\mathit{init}})$ are PSPACE-complete.

Proof.

Let $P=\langle F,A,I,G\rangle$, $\psi$ an LTLf formula, and let $K\geq 0$ be the cost. We proceed as follows. If $K=0$, we define $I^{\prime}=I$. Otherwise, we loop through all the possible alternative initial states $I^{\prime}$ which differs from $I$ of at most $K$ fluents. In both cases, for all the considered $I^{\prime}$, we test the satisfiability of $\psi\land[P]_{G}$, in the case of $\operatorname{CSEP}_{\exists}(C_{\mathit{init}})$, or the validity of $[P]_{G}\to\psi$ in the case of $\operatorname{CSEP}_{\forall}(C_{\mathit{init}})$ (see also Proposition 1). If we find any $I^{\prime}$ for which the test is successful, we found an existential (or universal) counterfactual, otherwise we reply negatively. Since satisfiability and validity for LTLf is PSPACE-complete, and we only need an additional polynomial number of bits to count all the possible exponential initial states $I^{\prime}$, the above procedure uses polynomial space, so $\operatorname{CSEP}_{\exists}(C_{\mathit{init}})$ and $\operatorname{CSEP}_{\forall}(C_{\mathit{init}})$ are PSPACE-complete. ∎

Let us now consider counterfactuals where the goal condition can be edited. Here, the existential and universal counterfactuals need to be addressed separately.

Theorem 3**.**

$\operatorname{CSEP}_{\exists}(C_{\mathit{goal}})$* is PSPACE-complete.*

Proof.

In this class of counterfactuals, changing the goal can be done by adding or removing truth assignments of the goal condition. Recall that, as observed in Section 5, for the existential counterfactuals, only weakening the goal makes sense, \ieadding truth assignments.

Let $\theta\coloneqq\psi\land[P]$ (see Proposition 1), and we test the satisfiability of $\theta$ (which can be done in polynomial space, as we recall). Then:

if $K=0$, and $\theta$ is satisfiable, $P$ is an existential counterfactual for itself of cost zero, so we reply positively; otherwise, we reply negatively; 2. 2.

if $K>0$, and $\theta$ is satisfiable, then we extract the last state $s$ reached by the corresponding model of $\theta$, and we define $P^{\prime}=\langle F,A,I,G^{\prime}\rangle$ where $G^{\prime}\coloneqq G\lor s$; then we know a plan for $P^{\prime}$ satisfying $\psi$ exists; if $\theta$ is unsatisfiable, we reply negatively.

All of the above can be done in polynomial space, therefore $\operatorname{CSEP}_{\exists}(C_{\mathit{goal}})$ is PSPACE-complete. ∎

The case of $\operatorname{CSEP}_{\forall}(C_{\mathit{goal}})$ is a bit more involved. Our solution is shown in Algorithm 1. Intuitively, the algorithm counts how many goal states are reachable by plans that do not satisfy $\psi$ (lines 3 to 7). This amount of goal states have to be removed from the goal in any case, so we do not actually store them, we only count how many they are. Then, if the amount is greater than the maximum allowed cost, we reply negatively (line 8). Otherwise, we have to be careful. The definition of universal counterfactual (Definition 8) forbids trivial solutions where the problem has no plans at all (and hence trivially all their plans would satisfy $\psi$). So we need to check whether there actually exists at least a plan satisfying $\psi$. However, if we already reached the maximum allowed cost (line 10), such a plan must reach the original goal condition, because we do not have margin to add anything within the cost, so return positively if and only if a plan of the original problem exists that satisfies $\psi$ (line 11). If instead the amount of assignments to be removed is strictly below the allowed cost (line 12), we have margin to ensure the set of solution plans is not empty, so we reply positively if and only if there is a plan reaching any goal state while satisfying $\psi$ (line 13). Let us now prove formally the soundness of Algorithm 1.

Theorem 4**.**

$\operatorname{CSEP}_{\forall}(C_{\mathit{goal}})$* is PSPACE-complete.*

Proof.

We want to prove that Algorithm 1 returns true if and only if there exists a universal counterfactual scenario $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})$ of cost less than or equal to $K$. So suppose that the latter is the case and let $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})=\langle F,A,I,G^{\prime}\rangle$. In this proof, with some abuse of notation, we will denote as $G$ and $G^{\prime}$ the set of goal states that satisfy the $G$ and $G^{\prime}$ formulas. As one can easily go from one representation to the other, this should not cause any ambiguity.

Let us now define as $S\subseteq G$ the subset of goal states reached by any plan of $P$ that does not satisfy $\psi$. Note that such goal states must in any case be removed from $G$ so the cost of $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})$ is at least $\left|S\right|$. Since the cost of $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})$ stays within $K$ we know $\left|S\right|\leq K$, otherwise we would need to overflow the cost to edit $G$ to $G^{\prime}$. Therefore the $\mathrm{counter}$ variable at the end of the for loop in Algorithm 1 must be less than or equal to $K$ so the algorithm does not reply false in 9. So now we have two cases:

if $\left|S\right|=K$, we know $G^{\prime}=G\setminus S$, because we can only afford to remove $S$ and not to edit $G$ in any other way. Now, since $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})$ is a universal counterfactual and by definition it has at least one plan satisfying $\psi$, the check at 11 returns true. 2. 2.

If $\left|S\right|<K$, then $G^{\prime}=G\setminus S\cup S^{\prime}$ where $S^{\prime}$ is some set of goal states that $G^{\prime}$ adds with regards to $G$. Then, since $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})$ is a universal counterfactual and by definition it has at least one plan satisfying $\psi$, the check at 13 returns true.

\Viceversa

, suppose Algorithm 1 returns true. We build a set $G^{\prime}$ of goal states that will define the counterfactual $\Xi_{\forall}(P,\psi,C_{\mathit{goal}})=\langle F,A,I,G^{\prime}\rangle$. Let $S\subseteq G$ be the subset of goal states reached by any plan of $P$ that does not satisfy $\psi$. Its size $\left|S\right|$ is the value the variable $\mathrm{counter}$ holds at line 7. Since we return true we know $\left|S\right|\leq K$, so we have two cases:

we return true at line 11, hence $\left|S\right|=K$ and $[P]_{G}\land\psi$ is satisfiable. So we set $G^{\prime}=G\setminus S$ to build our counterfactual: any plan reaching a goal state in $G^{\prime}$ must satisfy $\psi$ (because it does not satisfy $\neg\psi$), and we know the set of plans is not empty because $[P]_{G}\land\psi$ is satisfiable. 2. 2.

We return true at line 13, hence $\left|S\right|<K$ and $[P]\land\psi$ is satisfiable. So there exists a plan of $P$ (not necessarily reaching $G$, see Proposition 1) that satisfies $\psi$. Let $s$ be the goal state reached by such a plan. We set $G^{\prime}=G\setminus S\cup\{s\}$ to build our counterfactual: in this way we ensure the set of plans satisfying $\psi$ is not empty, and we stay below the cost $K$.∎

Let us now focus on the last class of counterfactuals considered in Section 5, namely those where actions’ preconditions are allowed to change. As we will see, even though the existential counterfactuals are again relatively easy to find (\iestill in polynomial space), universal counterfactuals may be more involved. We start with the easier case, which nevertheless requires some additional background. Given a finite set of propositions $F$, let $\omega:F\to\mathbb{N}$ be a weighting function for $F$. Then, given an LTLf formula over $F$, one may ask for a word of minimum weight, where the weight of a word is the sum of the weights of all the propositions true in any time step. Then, the following is known:

Proposition 2** (?** (?)).

Deciding whether an LTLf formula has a model of weight at most $k$ is PSPACE-complete. A minimal model can be produced in polynomial space as well.

The above proposition is at the core of the following solution for $\operatorname{CSEP}_{\exists}(C_{\mathit{act}})$.

Theorem 5**.**

$\operatorname{CSEP}_{\exists}(C_{\mathit{act}})$* is PSPACE-complete.*

Proof.

Let $P=\langle F,A,I,G\rangle$ be a planning problem, $\psi$ an LTLf formula, and $K\geq 0$. Recall from an observation in Section 5 that it only makes sense to look for counterfactuals that weaken the precondition of some actions. We proceed as follows. We define $A_{\mathit{relax}}$ as a set of actions equal to $A$ except that each action has its precondition set to true. Then, we let $P_{\mathit{relax}}=\langle F,A\cup A_{\mathit{relax}},I,G\rangle$, and we define a weighting function $\omega$ such that $\omega(a)=0$ for all $a\in A$ and $\omega(a)=1$ for all $a\in A_{\mathit{relax}}$. Then, we consider the formula $\theta\coloneqq[P_{\mathit{relax}}]_{G}\land\psi$, and look for a model of minimal weight according to $\omega$. Recall from Section 3 that this can be done in polynomial space. Then, we return true if and only if $\theta$ is satisfiable and the minimal model has weight at most $K$.

To see that the above procedure is correct, suppose on one hand that $\theta$ is indeed satisfiable with a minimal model of weight $L\leq K$. We can extract each occurrence of an action $a$ from $A_{\mathit{relax}}$ in the model, and define as $S_{a}$ the set of all the states the action $a$ was applied to in the model. We then define our counterfactual $\Xi_{\exists}(P,\psi,C_{\mathit{act}})=\langle F,A^{\prime},I,G\rangle$ where $A^{\prime}$ is defined as $A$ except that the precondition of each $a\in A$ is disjuncted with all the states in $S_{a}$. Now, note that this is an existential counterfactual because, by construction, there is a plan of $\Xi_{\exists}(P,\psi,C_{\mathit{act}})$ satisfying $\psi$. It also has cost $L\leq K$, by the way we defined $\omega$.

\Viceversa

, suppose a counterfactual $\Xi_{\exists}(P,\psi,C_{\mathit{act}})=\langle F,A^{\prime},I,G\rangle$ exists with cost $L\leq K$. Then, let $S_{a}$ be the set of states added to $\mbox{pre}_{a}$ in $A^{\prime}$. Let $\pi$ be the plan that witnesses the counterfactual, \iea plan that satisfies $\psi$. We can assume w.l.o.g. that $\pi$ visits all the states in $S_{a}$ at least once, otherwise there would be a counterfactual of lower cost built by not adding the non-visited state to $\mbox{pre}_{a}$. Then, we can construct a model of $\theta$ of minimum weight by setting proposition $a_{\mathit{relax}}$ or $a$ to true respectively each time an action $a$ is applied in $\pi$ to a state $s\in S_{a}$ or $s\not\in S_{a}$. Since each usage of an $a_{\mathit{relax}}$ has cost $1$, the cost of the model is $L\leq K$. ∎

The complexity of $\operatorname{CSEP}_{\forall}(C_{\mathit{act}})$ concludes this section. However, this case is more involved. To proceed, let us recall a standard ingredient of complexity theory. Oracle machines are a standard tool (see \eg ? (?)) for the study of the relationship between complexity classes. An Oracle machine is a Turing machine with an associated oracle language $O$. At any time, the machine can query whether $s\in O$ for some string $s$ and get the answer in constant time. When we study the computational complexity of a problem, by counting the oracle computation as a single computation step we isolate the main algorithm solving the problem from its sub-problems, clarifying the relationship between them.

What we can show here is that $\operatorname{CSEP}_{\forall}(C_{\mathit{act}})$ belongs to the class NEXPNP, which is the class of problems solvable in nondeterministic exponential time when given access to an oracle for an NP problem. This class is also often denoted as $\Sigma^{EXP}_{2}$, referring to its second place in the exponential hierarchy. Note that $\text{NEXP}\subseteq\text{NEXP\textsuperscript{NP}}\subseteq\text{EXPSPACE}$ but it is not known whether $\text{NEXP}=\text{NEXP\textsuperscript{NP}}$ unless $\text{P}=\text{NP}$.

In our case, the NP problem to be used as oracle is SAT, \iepropositional satisfiability, the prototypical NP-complete problem. We use a call to a SAT oracle to test bounded LTLf satisfiability, \iesatisfiability of an LTLf formula restricted to models of bounded length. Many approaches exist in literature to solve LTL and LTLf satisfiability (or equivalently model checking) through an iteration of SAT queries (?; ?). In particular, we can state the following.

Proposition 3** (?** (?)).

Given an LTLf formula $\psi$ and a bound $B>0$, in time polynomial in $B$ and in the size of $\psi$ one can produce a propositional formula $\operatorname{enc}(\psi,B)$ such that $\operatorname{enc}(\psi,B)$ is satisfiable if and only if $\psi$ has a model of length at most $B$.

With Proposition 3 in place we can proceed.

Theorem 6**.**

$\operatorname{CSEP}_{\forall}(C_{\mathit{act}})$* belongs to NEXPNP.*

Proof.

The solution is shown in Algorithm 2. Following the definition of universal counterfactual, we non-deterministically guess a number of actions to be edited and the states to be added or removed and we build a candidate counterfactual $P^{\prime}$. Then we need to check first if the problem has any solution plan at all, and then if all its solution plans satisfy $\psi$. For both checks we invoke the NP oracle, whose calls are underlined in Algorithm 2:

the first check tests the satisfiability of $\operatorname{enc}([P^{\prime}]_{G},2^{\left|F\right|})$, which by Proposition 3 corresponds to testing the satisfiability of $[P^{\prime}]_{G}$ over models of length at most $2^{\left|F\right|}$. We know this bound is sufficient because solution plans of classical planning problems do not have any reason to visit the same state twice, and after $2^{\left|F\right|}$ steps we are sure to find a repetition. 2. 2.

the second check tests the satisfiability of the formula $\operatorname{enc}([P^{\prime}]_{G}\land\neg\psi,2^{\left|F\right|})$ which by Proposition 3 corresponds to the satisfiability of $[P^{\prime}]_{G}\land\neg\psi$ over models of length at most $2^{\left|F\right|}$, a bound that is chosen for the same reason outlined above. Since we accept when $[P^{\prime}]_{G}\land\neg\psi$ is not satisfiable this corresponds to checking the validity of $[P^{\prime}]_{G}\to\psi$, which corresponds to the fact that all solution plans of $P^{\prime}$ satisfy $\psi$.∎

Theorem 6 shows that $\operatorname{CSEP}_{\forall}(C_{\mathit{act}})$ has a NEXPNP upper bound, but a matching lower bound is still missing and not trivial to prove. Theorem 1 shows that the class of $\operatorname{CSEP}_{\exists}(C)$ and $\operatorname{CSEP}_{\forall}(C)$ problems have a PSPACE core that cannot be avoided, made of the interconnection of two PSPACE-complete problems, namely classical planning and LTLf satisfiability. However, the possible-change relation $C$ can be arbitrarily complex. For the practically relevant classes of counterfactuals that we chose to study, the complexity has turned out to be relatively low, but theoretically one may devise classes of possible-change relations that easily cause complexity to increase arbitrarily, as evidence of the formal flexibility of our framework.

7 Discussion

This paper introduced counterfactual scenarios, a novel explanation paradigm for automated planning problems. Differently from existing proposals, our explanations identify minimal modifications to a planning problem such that it admits plans that comply with user-specified requirements, here captured by means of LTLf formulae. Given that our proposal is the first of its kind, in this paper we set to investigate the computational complexity of generating this type of explanations and explored potential theoretical barriers to our proposal. Our analysis revealed that computing counterfactual scenarios is, in most cases, only as expensive as solving planning problems. This somewhat surprising result suggests that, for a significant class of problems, the additional step of identifying changes to a planning problem necessary to achieve a desired outcome does not introduce a prohibitive increase in complexity.

Our counterfactual scenarios are strongly related to the literature on model repair. For instance, work by Lin and Bercher addresses a setting where a flawed domain is repaired to fit a plan that serves as a witness (?; ?), often accounting for a notion of minimality of change (?). Although this line of work bears some similarities to our proposal, here we considered the more general problem of generating modifications that comply with an arbitrary LTLf formula, rather than fixing existing domains based on specific plan examples. This is a major departure point, as our counterfactual scenarios can accommodate complex behaviours captured by abstract and highly expressive LTLf formulae, and are guaranteed to return modified domains where all (or at least one) plans adhere to such behaviours. This profound technical difference is also reflected in the divergent computational complexities we obtained: most of our problems are PSPACE-complete, while the setting considered by Lin and Bercher typically yields NP-complete problems. Another critical difference between our work and model repair is the inherent plausibility requirement. Our counterfactuals are designed to generate actionable and plausible insights, pointing to what would need to be changed in a planning domain for a given behaviour to be observed. As such, changes suggested by our counterfactuals are not necessarily aimed at fixing a flawed domain; rather, they must be plausible (according to a domain-dependent notion of plausibility). This crucial requirement motivated our initial choice of using LTLf formulae to capture plausibility and marks another fundamental difference from work on model repair.

Our work fits within the broader scope of explainable automated planning and introduces a novel explanation paradigm that takes a fundamentally different approach than both model reconciliation and contrastive explanations. Unlike model reconciliation, our counterfactual scenarios do not operate on the premise of reconciling a human’s mental model with an agent’s. Our approach focuses on identifying systematic modifications to a planning problem that would enable or enforce specific properties on the resulting plans, as captured by an LTLf formula. As such, our counterfactuals are prescriptive and prospective, answering the question “How can I change the planning problem so that plans satisfying a given property become possible?”. This also marks a crucial difference from contrastive explanations, which have typically been defined to address the question: “Why did the agent choose action A instead of action B in a plan?”. Contrastive explanations are inherently local and retrospective, providing a justification for a specific choice made for a given planning problem. Our explanations have a global scope, identifying modifications that affect the entire planning problem space to enable or enforce a class of solutions characterized by an LTLf formula. This is particularly evident in the universal setting, where there is a sharp contrast with the local and specific comparison inherent in contrastive explanations.

8 Future work

The findings presented here have profound implications for the practical application of our counterfactuals, suggesting that existing planning algorithms could be leveraged to support the generation of counterfactual scenarios. Our future work will focus on the development of efficient algorithms for the generation of counterfactual scenarios. Our efforts will initially concentrate on the classical planning setting and the use of LTLf specifications as described in this paper. Given the strong link with model repair, we believe it would be interesting to investigate whether some of the algorithmic techniques developed in that space could be adapted to compute counterfactual scenarios, particularly if plausibility constraints could be integrated. Once a robust algorithmic foundation is established for this setting, it would be interesting to explore the generation of counterfactual scenarios for different planning formalisms, such as those addressing numeric domains, as well as considering alternative specification languages over finite traces, such as CTL for probabilistic systems (?).

Acknowledgments

Andrea Micheli has been supported by the STEP-RL project funded by the European Research Council under GA n. 101115870. Francesco Leofante was supported by Imperial College under the Imperial College Research Fellowship scheme. Nicola Gigante was partially funded by the NextGenerationEU FAIR PE0000013 project MAIPM (CUP C63C22000770006).