Explaining the Space of SSP Policies via Policy-Property Dependencies: Complexity, Algorithms, and Relation to Multi-Objective Planning

Venue: icaps-conference_org_ICAPS_2024_Conference
Published: 2023-12-07 11:07:19

Abstract: Stochastic shortest path (SSP) problems are a common framework for planning under uncertainty. However, the reactive structure of their solution policies is typically not easily comprehensible by an end-user, while planners neither justify the reasons behind their choice of a particular policy over others. To strengthen confidence in the planner's decision-making, recent work in classical planning has introduced a framework for explaining to the user the possible solution space in terms of necessary trade-offs between user-provided plan properties. Here, we extend this framework to SSPs. We introduce a notion of policy properties taking into account action-outcome uncertainty. We analyze formally the computational problem of identifying the exclusion relationships between policy properties, showing that this problem is in fact harder than SSP planning in a complexity theoretical sense. We show that all the relationships can be identified through a series of heuristic searches, which, if ordered in a clever way, yields an anytime algorithm. Further, we introduce an alternative method, which leverages a connection to multi-objective probabilistic planning to move all the computational burden to a pre-process. Finally, we explore empirically the feasibility of the proposed explanation methodology on a range of adapted IPPC benchmarks.

Main paper: 
 introduction: 
 Stochastic shortest path (SSP) problems (Bertsekas and Tsitsiklis 1991) are a common framework for planning under action-outcome uncertainty. SSP solutions take into account arising contingencies by means of policies deciding what action to take next as a function of what happened in the past. This complex structure, however, leads to an astronomically large space Π of different possible solutions, a direct overview of which is beyond the capability of actual end-users of planning technology. At the same time, current SSP solution methods lack functionality for providing reasons behind the choice of a particular policy over others. Krarup et al.'s (2021) introduced a generic iterative planning framework aiming at helping a user to interactively explore and comprehend the solution space Π. The goal of the user-planner interactions is to arrive at a solution that is in line with the user's preferences. Eifler et al. (2020a,b) proposed an instantiation of this framework for classical planning. The user-planner interactions are based on a set of user-provided plan properties Ω, i.e. Boolean functions on plans. The plan space is explained by identifying trade-offs between the given properties, i.e., the relationships between property subsets Φ and Ψ that are not simultaneously achievable. This gives rise to a contrastive question-answer kind of dialog (Miller 2019) , where the user specifies preferences Φ ⊆ Ω and is then confronted with the implied exclusion of other property subsets Ψ. This has proved highly beneficial in strengthening the user's understanding of the solution space (Eifler et al. 2022) .While explaining solutions to probabilistic planning models is by no means a novel topic, most prior work deals with the explanation of individual solutions. With the recognition of the importance of explainable AI, the sub-field of explainable reinforcement learning is increasingly gaining attention, yet its primary focus lies in tracing a policy's decision back to input features (Milani et al. 2023) . Topin and Veloso (2019) attempted to summarize a single policy via state abstraction. Juozapaitis et al. (2019) and Khan, Poupart, and Black (2009) explain single action-decisions of a given policy by contrasting them to all available options by exposing trade-offs between different reward or cost objectives.Building on Eifler et al.'s (2020a) explanation methodology, we propose a novel approach to explaining the global space of all SSP policies, or a local user-chosen subset. We introduce a notion of policy properties, taking into account action-outcome uncertainty, and formally study the computational problem of identifying their exclusion relationships. In order to compute the explanations, we devise two approaches that relate to constrained SSPs (Altman 1999) and multi-objective SSPs (Chen, Trevizan, and Thiébaux 2023) , respectively. We show that both approaches can be efficiently realized by adapting the heuristic search algorithm I-DUAL (Trevizan et al. 2016) , which embeds occupation-measure heuristics for effective guidance (Trevizan, Thiébaux, and Haslum 2017) . Finally, we explore the feasibility of the proposed explanation methodology empirically on a range of adapted IPPC and new benchmarks. 
background: 
 For a finite set X, we refer with ∆(X) to the set of all probability distributions over X. For δ ∈ ∆(X), supp(δ) := {x ∈ X | δ(x) > 0} gives the support of δ.We consider probabilistic planning tasks in a SAS + -like notation (Bäckström and Nebel 1995) . A planning task is given by a tuple τ = V, A, s 0 , G, c , where V is a finite set of state variables, each v ∈ V having a finite domain D v ; A is a finite set of actions; s 0 is the initial state (a complete variable assignment); G is a conjunctive goal (a variable assignment); and c : A → R + 0 is the cost function. Pairs v, d of variables v ∈ V and values d ∈ D v are called facts. The set of all facts is denoted with F. The states of τ are the complete variable assignments. The set of all states is denoted with S. For a (partial) variable assignment G, we denote with S G := {s ∈ S | G ⊆ s} the subset of states satisfying G. Each action a is associated with a precondition pre a (a variable assignment) and a probability distribution Out a over probabilistic outcomes (variable assignments). An action a is applicable in a state s if s ∈ S pre a . The set of all actions applicable in s is denoted with A(s).o ∈ supp(Out a ) is s o [v] = o[v] if o[v] is defined, else s o [v] = s[v].A task τ induces the stochastic shortest path (SSP)problem Θ τ = S, A, T , s 0 , S G , c with same states, actions, initial state, goal states, and cost function, and the transition probability function T : S ×A → ∆(S). Unless important, we treat τ and Θ τ interchangeably. We are interested in deterministic policies (policies for short), which are (partial) functions π : S A such that π(s) ∈ A(s) if π(s) is defined. For a policy π, we write π(s) = ⊥ if π(s) is not defined. The terminal states S π ⊥ ⊆ S under π are those s where π(s) = ⊥. A state s is reachable from a state s via π if there are states s 1 , . . . , s n with π(s i-1 ) = ⊥ and T (s i-1 , π(s i-1 ), s i ) > 0, for all 1 < i ≤ n, such that s 1 = s and s n = s . The set of all states reachable from s via π is denoted with S π (s); the reachable terminal states with S π ⊥ (s). Let G be a variable assignment. The G-reachability probabilities of a policy π is denoted with P G,π The Greachability probabilities are also called goal probabilities. We say that a policy π is s-proper if P G,π (s) = 1. We denote the set of all s-proper policies with Π(s). The expected cost of a policy π under the cost function c is denoted J c,π , where J c,π (s) = ∞ iff π is not s-proper. The optimal value for a state s under c is given by J c, * (s) := inf π∈Π(s) J c,π (s). An s-proper policy π is optimal for s under c if J c,π (s) = J c, * (s). When c is omitted, we refer to the task's cost function.Classical planning is special case of probabilistic planning where all actions have a single outcome. For brevity, we denote the unique resulting state of applying a in a state s by s a , and extend this to action sequences in the obvious manner. Given a state s, an action sequence a 1 , . . . , a n is called an s-plan if it is applicable in s and G ⊆ s a 1 , . . . , a n . The set of all s 0 -plans, also called plan space, is denoted Π(s 0 ).A plan property (Eifler et al. 2020a) (Giacomo and Vardi 2013) , can 145 be compiled into this format (Eifler et al. 2020b) .Let Ω ⊆ F be a set of user-provided plan properties. Let Φ ⊆ Ω be a subset of properties. Φ is solvable if there is a plan π ∈ Π(s 0 ) such that Φ ⊆ s 0 π . In this case, we also say π satisfies Φ. Φ is unsolvable if it is not satisfied by 150 any plan. Φ is a minimal unsolvable subset (MUS Eifler et al. (2020a) distinguish local and global expla-160 nations. The former assume a given subset of properties Φ ⊆ Ω, and aim at explaining the subspace of plans which satisfy Φ. The Φ-explanation gives the consequences of this plan-space restriction in terms of the set {Ψ ⊆ Ω | Φ ⇒ Π ¬Ψ is a non-rhs-dominated exclusion}. In contrast, 165 the global explanation provides a view on the entire plan space by means of a directed graph over property sets with an arc from Φ to Ψ if Φ ⇒ Π ¬Ψ is a non-dominated exclusion relation. Computing either type of explanations boils down to solving AllMUSes, i.e., computing the set of all 170 MUSes. For global explanations, this is inherent from the definition. For local explanations, this follows from the fact that the non-rhs-dominated exclusions of any Φ correspond exactly to AllMUSes in the task with goal G := G ∪ Φ.) if Φ is unsolvable but every Φ ⊂ Φ is solvable. Φ excludes another Ψ ⊆ Ω, denoted with Φ ⇒ Π ¬Ψ, if all plans π ∈ Π(s 0 ) that satisfy Φ violate Ψ. An exclusion Φ ⇒ Π ¬Ψ is non- dominated if there is no exclusion Φ ⇒ Π ¬Ψ such that 155 Φ ⊆ Φ and Ψ ⊆ Ψ while one of the subset relations is proper. Φ ⇒ Π ¬Ψ is non-rhs-dominated if no Ψ ⊂ Ψ is excluded by Φ. Observe that Φ ⇒ Π ¬Ψ iff Φ ∪ Ψ is unsolvable, and it is non-dominated iff Φ ∪ Ψ is a MUS.3 Exclusion-Based Explanations for SSPs 175 
policy properties: 
 We generalize Eifler et al.'s (2020a) concept of plan properties to SSPs. The exclusion-based explanation framework requires properties to be Boolean predicates. In classical planning, each plan π uniquely determines an execution trace 180 along with the resulting outcome state s 0 π . This makes the evaluation of every condition on π's execution inherently Boolean: either the condition is satisfied by π (e.g., s 0 π [v φ ] = t φ for the plan property φ) or it is violated (s 0 π [v φ ] = t φ ). One of the two cases definitely applies. 185 In the probabilistic setting, this is more complicated given that policies no longer induce a unique outcome but instead give rise to probability distributions over potentially even infinitely many possible executions, while conditions on individual executions may be satisfied in some but not all the 190 possible executions. Properties expressing characteristics of policies need to take into account this uncertainty, and therewith need to reason over the expectation of the properties' objectives. In the remainder of this paper, we will specifically consider two classes of such policy properties, one 195 based on state reachability and one based on cost.Reachability policy properties extend Eifler et al.'s (2020a) plan properties as introduced above.Definition 1 (Policy Reachability Property). A policy reachability property φ consists of a variable assignment G φ and a lower bound α φ ∈ (0, 1]. A policy π satisfies φ iff P G φ ,π (s 0 ) ≥ α φ .Cost properties allow the user to explore trade-offs between different cost functions and reachability properties: Definition 2 (Policy Cost Properties). A policy cost property φ consists of a cost function c φ and an upper boundβ φ ∈ R + 0 . A policy π satisfies φ iff J c φ ,π (s 0 ) ≤ β φ .As in Eifler et al.'s (2020a) framework, we assume the user specifies the relevant policy properties Ω, where Ω = Ω R Ω C is partitioned into reachability Ω R and cost properties Ω C . For a policy-property subset Φ ⊆ Ω, we similarly use Φ = Φ R Φ C . We explain Π(s 0 ) via the induced property-subset exclusion relationships. To this end, the concepts of solvable and unsolvable property subsets, propertysubset exclusions, and local and global explanations are accordingly extended to policy properties. We slightly adapt the conditions of minimal unsolvable subset and exclusion dominance, taking into account the policy properties' flexibility in the threshold choice. In general, it can be desirable to have in Ω multiple policy properties φ 1 , . . . , φ k with the same base objective (i.e., same reachability objective G φi = G φj , respectively same cost function c φi = c φj ) but different threshold values. This is useful, in particular, for exploring the effect of different property relaxations on the solvability of other properties.We say that a reachability property φ ∈ Ω R is a relaxation of another reachability propertyψ ∈ Ω R , denoted φ ψ, if G φ = G ψ and α φ ≤ α ψ ; and, similarly, a cost property φ ∈ Ω C is a relaxation of another cost property ψ ∈ Ω C (φ ψ) if c φ = c ψ and β φ ≥ β ψ . A relaxation φ ψ with φ = ψ is called strict (denoted φ ψ). A property subset Φ is a relaxation of another property subset Ψ, written Φ Ψ if every φ ∈ Φ relaxes some ψ ∈ Ψ. Φ is a strict relaxation of Ψ (Φ Ψ), if Φ Ψ and Φ = Ψ.To define MUSes and policy-property subset exclusion dominance, we substitute the subset relation by relaxation: Definition 3 (Minimal unsolvable policy-property subset).Φ ⊆ Ω is a MUS if it is unsolvable but each of its strict relaxations Φ ⊆ Ω, i.e., Φ Φ, is solvable. Definition 4 (Policy-property exclusion dominance). A policy-property subset exclusion Φ ⇒ Π ¬Ψ is non- dominated if there is no other exclusion Φ ⇒ Π ¬Ψ such that Φ Φ and Ψ Ψ and at least one of the relaxations is strict. Similarly, Φ ⇒ Π ¬Ψ is non-rhs-dominated if there is no Ψ ⊆ Ω such that Ψ Ψ and Φ ⇒ Π ¬Ψ .Note that both definitions subsume their original counterparts. This follows directly from the observation that if Φ ⊆ Φ for any two policy-property subsets, then it also holds that Φ Φ. Vice versa, however, there can be nonminimal unsolvable policy-property subsets Φ (respectively, dominated exclusions Φ ⇒ Π ¬Ψ ), although every subset of Φ is solvable (respectively, no exclusion satisfies the subset-based dominance criterion). Also note that it is still the case that an exclusion Φ ⇒ Π ¬Ψ is non-dominated iff the combined property set Φ ∪ Ψ is a MUS, and thatΦ ⇒ Π ¬Ψ is non-rhs-dominated iff every relaxation Φ ⊆ Ω of Φ ∪ Ψ with Φ ⊆ Φ is solvable.Finally, observe that for every non-dominated exclusion Φ ⇒ Π ¬Ψ, both Φ and Ψ must be unambiguous in that neither of them can contain two properties φ and φ such that φ φ . 260With the ability to express the satisfaction of plan properties as properties on states, the computation of AllMUSes in classical planning degenerates to standard goal reachability questions for different goal sets. Eifler et al. (2020b) showed 265 that these different questions can be solved even with just a single state-space search, resulting in a method offering similar scalability than that of optimal classical planners. Unfortunately, conditions on the expected behavior of policies can no longer be expressed as properties on states. This has two 270 consequences. First, AllMUSes can no longer be computed via methods similar to the algorithm just sketched. Second, whereas in classical planning, a local Φ-explanation could be computed by solving AllMUSes for a goal-extended task, this is no longer possible for SSPs.Property-Subset Lattice Exploration Algorithm 1 depicts our general algorithm for computing local Φexplanations, and closely resembles previous algorithms for computing minimal unsolvable goal/constraint subsets (Eifler et al. 2020a; Liffiton et al. 2016) with the difference of 280 using property-subset relaxation in place of the subset relation. At its core, Algorithm 1 conducts an exhaustive exploration of the space of all property subsets, testing the solvability of the combined set Φ ∪ Ψ for each visited Ψ. As Φ ⇒ Π ¬Ψ holds iff Φ ∪ Ψ is unsolvable, Φ's non-rhs-285 dominated exclusions are given exactly by the non-relaxable Ψ for which the combined set was found unsolvable (line 6). To avoid the complete enumeration of all the property subsets, Algorithm 1 utilizes the relaxation relationships with already tested property subsets. The specific choice of Ψ is 290 not important for correctness. In our implementation, we use MARCO (Liffiton et al. 2016) , which chooses Ψ in a way guaranteeing that each Ψ added to Unsolvable yields a nonrhs-dominated exclusion. Finally, note that by setting Φ = ∅, min Unsolvable will be exactly the set of all MUSes.295 Theorem 1. Algorithm 1 terminates with the Φ-explanation.If Φ = ∅ it returns all MUSes.The Property-Subset Solvability Problem Algorithm 1 relies on a sub-procedure deciding the property subsets' solvability. Before discussing possible implementations of 300 this sub-procedure, here we define and analyze this problem formally. Definition 5 (PSS). The property-subset solvability problem (PSS) is that of deciding, given a probabilistic planning task τ and a non-empty set of policy properties Φ, whether 305 there exists an s 0 -proper policy π that satisfies Φ.To analyze its complexity, we distinguish decision problems along three lines: (1) classical and probabilistic planning, (2) whether considering the factored planning task description or the flat state space as input, and (3) in the 310 probabilistic case, whether to allow stochastic policies or Algorithm 1: Generic property-subset lattice exploration for computing the Φ-explanation for a given property subset Φ. end if 13: end while whether to constrain the solution space to the deterministic policies. It is well-known that with flat representations, the standard plan/policy existence problems can be decided in polynomial time (e.g., Puterman 1994) . The policy type does not make a difference. For factored representations, classical planning becomes PSPACE-COMPLETE (Bylander 1994) and probabilistic-planning EXP-COMPLETE (Littman, Goldsmith, and Mundhenk 1998) .Moving to PSS, the additional constraints imposed by the properties have an impact on the complexity in some but not all cases. PSS for the classical-planning flat case is already NP-COMPLETE, being a generalization of the weight-limited shortest-path problem (Garey and Johnson 1979) . For the factored representation, PSS stays in the same complexity class of classical planning due to the ability of compiling the properties into facts. PSS for flat SSPs with stochastic policies can still be solved in time polynomial in the size of the SSP via an extension of the standard SSP linear program (as we will see in the next section). For deterministic policies, however, PSS becomes NP-COMPLETE, given the classical planning result. That PSS for factored SSPs is in EXP follows via the approach for the flat variant.Given that standard SSP policy existence is a special case of PSS, the latter therefore remains EXP-COMPLETE when stochastic policies are allowed. However, as in the flat case, the restriction to deterministic policies again raises the complexity by the "non-deterministic" factor. Therefore, and this is in contrast to classical planning, generating explanations for SSPs becomes computationally more demanding than Finding a policy that satisfies a given property subset Φ boils down to solving the SSP under additional policy constraints.This relates to the class of constrained SSPs (CSSPs) (Altman 1999). This section develops an extension of I-DUAL (Trevizan et al. 2016 ) -the so far only known heuristicsearch algorithm for solving CSSPs-to solving PSS. To this end, we start with a brief recap of the CSSPs and I-DUAL, then introduce a mixed-integer linear program (MIP) characterization of PSS, and finally show how to adapt I-DUAL to solve this integer program efficiently. 
background: cssps and i-dual: 
 CSSPs extend SSPs with a list of additional cost functions c 1 , . . . , c k and accompanying bounds β 1 , . . . , β k on the policies' corresponding expected costs. Unlike in the unconstrained version, optimally solving CSSPs in general requires stochastic policies, i.e., ones mapping states to probability distributions over actions. The optimal solutions are characterized exactly by the linear program (LP) depicted in Figure 1 (cf., e.g., Altman 1999) .The basis of the encoding are the occupation-measure (OM) variables X s,a which represent the expected number of times action a is to be executed in state s. The expected cost of the policy represented by the OM variables is given by the linear combination with the cost function (cf. def. of cost[c ]). The objective function (C1) asks for minimizing the expected cost under the SSP's primary cost function. The bounds on secondary cost functions map into additional constraints (C3). (C4) bounds the states' flow, asserting that the expected numbers of times a non-goal state is entered (the in-flow) and exited (the out-flow) to be the same. A flow surplus of 1 is inserted at the initial state. (C5) implements the s 0 -proper policy requirement by asserting that the entire inserted flow sinks at the SSP's goal states eventually.The LP necessitates building the entire state space Θ τ . I-DUAL (Trevizan et al. 2016 ) aims to avoid this by iteratively solving progressively larger sub-SSPs Θ = Ŝ, A, T , s 0 , ŜG of Θ τ . One iteration of I-DUAL consists of solving the CSSP LP for the current sub-SSP and subsequently expanding Θ at the fringe states visited by the found solution, where Θ's fringe F ⊆ Ŝ is the set of non-goal states whose transitions from Θ τ are not present in Θ yet. An optimal CSSP solution is found when all flow is sinking at goal states. To guide the exploration, I-DUAL leverages heuristics to estimate the expected remaining cost-togoal, for each cost function, depending on the reached fringe states. The estimates become additional summands in the objective respectively the cost constraints. Solution optimality is preserved if the heuristics provide are admissible. Trevizan, Thiébaux, and Haslum (2017) presented an extension of I-DUAL, baptized I 2 -DUAL, which integrates the computation of a particular heuristic, the projection occupation-measure (POM) heuristic h pom , directly in I-DUAL's LP. This has the advantage over using cost-function individual heuristics in being able to jointly consider all CSSP's cost constraints inside the heuristic computation. The blue parts in Figure 1 summarize the integration. In brief, h pom is based on the projections of τ onto the individual state variables V, where the v-projection is the simplified task obtained from τ by discarding all other variables. the OM-based representation of the projections' SSPs, tying together the OM variables between the projections by enforcing that each projection executes every action overall exactly the same number of times. By inserting flow into the projections according to the probabilities of reaching frontier states, the projections' OM variables yield the heuristic summands for (C1) and (C3). CSSPs differ from PSS in two regards: CSSPs (1) consider solely constraints on secondary cost functions; and (2) assume stochastic policies. In the presence of a single goalreachability objective, i.e., assumption (1), one can assume w.l.o.g. that goal states are absorbing, forcing policies to immediately terminate once reaching those states. This assumption allows to exclude in the LP (a) the trivial special case s 0 ∈ S G , (b) omit goal-state leaving transitions, setting out[s G ] = 0 implicitly for all goal states s G , and (c) ignore flow constraints for the goal states.Minimize cost[c]+ cost v [c] (C1) Subject to Xs,a ≥ 0, s ∈ S \ SG, a ∈ A(s) (C2) cost[ci]+ cost v [ci] ≤ βi, 1 ≤ i ≤ k (C3) out[s] -in[s] = [s = s0], s ∈ S \ SG (C4) s∈S G in[s] = 1 (C5) cost[c ] := s∈S,a∈A(s) Xs,ac (a), c ∈ {c, c1, . . . , cn} out[s] := a∈A(s) Xs,a, s ∈ S in[s] := s ∈S,a∈A(s ) X s ,a T (s , a, s), s ∈ S X v d,a ≥ 0, v ∈ V, d ∈ Dv, a ∈ A (C6) v-projection OM constraints, v ∈ V (C7) constraints tying X v •,a with X v •,a , v ∈ V \ {v}, a ∈ A (C8)In contrast, in the presence of multiple reachability constraints, continuing the execution in the SSP's goal states might be necessary for achieving the other reachability objectives. Figure 2 accounts for additional reachability objectives by introducing occupation-measure variables also for goal-leaving transitions. Thus, the flow constraints (C11) need to be defined for all states, while to allow flow sinking at some states, the equality needs to be changed to an upperbound constraint. As flow may now escape from goal states, (C5) is no longer a sufficient proper policy condition. (C12) in Figure 2 instead ensures that all the flow enters and resides in the SSP's goal states eventually. Furthermore, (C12) handles the case s 0 ∈ S G by taking into account the initial flow inserted at s 0 if s 0 is a goal state. Reachability property can now be encoded as flow-residual constraints (C13).The second source of complication arises from the factMinimize (C1) Subject to (C2) for all s ∈ S, a ∈ A(s) (C9) (C3) for each φ ∈ Φ C (C10) out[s] -in[s] ≤ [s = s0], s ∈ S (C11) res[SG]+PG = 1 -[s0 ∈ SG] (C12) res[SG φ ]+PG φ ≥ α φ -[s0 ∈ SG φ ], φ ∈ Φ R (C13) Ds,aK -Xs,a ≥ 0, s ∈ S, a ∈ A(s) (C14) a∈A(s) Da,s + Ts ≤ 1, s ∈ S (C15) out[s] -in[s] + Ts ≥ [s = s0], s ∈ S (C16) Ds,a ∈ {0, 1}, s ∈ S, a ∈ A(s) (C17) Ts ∈ {0, 1}, s ∈ S (C18) res[S] := s∈S (in[s] -out[s]),S ⊆ S POM extensions (C6) -(C8) with adaptations as discussed in the text, (C19) that PSS talks about deterministic policies, which in the presence of additional policy constraints are no longer equally expressive than stochastic policies, as previously mentioned. We implement that requirement by binary integer decision variables D s,a for each state-action pair. (C14) 445 ensures that D s,a is set if the corresponding transition is assigned a positive occupation measure, while (C15) insists on setting at most one D s,a per state. The additional binary integer variables T s are explicit indicators of the policy terminating in s. These are necessary because with the policy's 450 termination being no longer determined by the satisfaction of the SSP's goal, termination becomes a deliberative policy choice. (C15) makes sure that this choice remains deterministic. (C16) ensures that the termination indicator T s is set whenever some flow is sinking in state s.PG ≥ 0, G ∈ {G φ | φ ∈ Φ R } ∪ {G} (C20) PG ≤ res v [G[v]], v ∈ V s.t. G[v] is defined (C21)Putting everything together, we conclude:Theorem 3. Figure 2 is feasible iff Φ is solvable.The principles of I-DUAL can be applied directly to solving PSS. The main change required is, obviously, the substitu-460 tion of the CSSP LP by the MIP from Figure 2 . Some care must be taken to correctly handle the subtle differences between PSS and CSSPs. First, given that goal states can no longer be assumed to be absorbing, goal states must now be included in I-DUAL's fringe (and thus possibly expanded). 465 Second, given that goal states may now be contained in the fringe, we must extend I-DUAL's termination condition testing explicitly that no flow is sinking in the fringe. Lastly, the fringe states must be handled appropriately in PSS's reachability constraints. This is, we must make sure to optimistically (hence upper) bound the expected achievement of the individual reachability properties given the fringe states reached. This can be done, in the same vein as for the cost constraints, with the help of admissible goal-probability heuristics. After these changes, I-DUAL's original correctness arguments can be carried over to show that our adapted variant correctly solves PSS.To complete the adaptation of I 2 -DUAL, it only remains to extend the h pom part to deliver the necessary optimistic reachability-probability bounds. The blue parts in Figure 2 highlight the main changes. In summary, we discard h pom 's proper policy constraint. h pom 's reachabilityprobability bounds are represented through additional variables P G for each relevant G, cf. (C20), which become additional summands in the proper-policy (C12) and the reachability-property constraints (C13) of the overall MIP. The constraints (C21) synchronize the values of those reachability variables with the actual probability of residing in the projections' G-achieving states. That this indeed yields an upper bound on the probability of achieving G from the fringe states follows similarly to the cost bounds from the fact that projections are solution preserving. Theorem 4. Run I 2 -DUAL or I-DUAL with admissible heuristics. If at any point in time, the MIP for one of the sub-SSPs Θ becomes infeasible, then Φ is unsolvable. If they return π, then π is s 0 -proper and π satisfies Φ.Note that the h pom modifications sketched so far do not ensure that the projection's OM variables resemble a deterministic policy. One might be tempted to enforce determinism within every projection via additional integer variables.This however breaks h pom 's admissibility property, because due to the tying of the projections, different actions might need to be applied in a single projection state. 
allmuses via mo optimization: 
 Ignoring the properties' thresholds, one is left with a set of policy metrics whose simultaneous optimization becomes a variant of multi-objective (MO) SSPs (Chen, Trevizan, and Thiébaux 2023) . In the following, we leverage this connection, showing that the solution to this MOSSP variant contains all the relevant information to decide any PSS. Multi-objective SSPs (Roijers and Whiteson 2017; Chen, Trevizan, and Thiébaux 2023) differ from regular SSPs in optimizing a cost-function vector c = (c1 ... cn) T rather than a single cost function. Optimality in the MO setting is 515 defined via a dominance order between real vectors, where for two real vectors x = (x1 ... xn) T and y = (y1 ... yn) T , x weakly dominates y ( x y) if x i ≤ y i holds for all i. x dominates y ( x ≺ y) if x y and x = y. Associating each policy π with the vector of expected-cost functions 520 J c,π := (J c 1 ,π ... J cn,π ) T , the optimal MOSSP policies are those s 0 -proper policies π where J c,π (s 0 ) is not dominated by J c,π (s 0 ) for any other π . Since is no longer a total order, different optimal policies can in general have different value vectors. The optimal MO-value function J * assigns every state to the set of all these optimal cost vectors. Like constrained SSPs, MOSSPs assume stochastic policies, and there can exist J * ∈ J * (s) that are not achievable by any deterministic policy. |J * (s)| is in general infinite but can be represented as the convex hull of a finite coverage set (Roijers and Whiteson 2017).To be able to translate the policy property set Ω into a multiobjective optimization problem, we introduce a slight variation of MOSSPs that supports multiple cost as well as goal objectives. Concretely, let c = (c1 ... cn) T be a cost-function vector, as before, and let G = (G1 ... Gm) T be a vector of variable assignments. For simplicity's sake, we denote for every policy π the combined policy value vector with V π = (J c 1 ,π ... J cn ,π -P G 1 ,π ... -P G 2 ,π ) T (note the negation of the reachability probabilities). A deterministic policy π ∈ Π(s 0 ) is deterministic optimal if V π is not dominated by V π of any π ∈ Π(s 0 ). The deterministic-optimal MOvalue function is given byV * d (s) := min { V π (s) | π ∈ Π(s)}. Note that |V * d (s)| is always guaranteed to be finite. Let c = (c0 ... cn) T and G = (G1 ... Gm) T where c 0 denotes the SSP's main cost function, c 1 , . . . , c n are the cost functions underlying the cost properties Ω C , and G 1 , . . . , G m are the goal sets underlying Ω R . Let Φ ⊆ Ω be an unambiguous property subset. We associate with β Φ (c i ) := β φ the cost threshold assigned by the property φ ∈ Φ C with c φ = c i if it exists, and define β Φ (c i ) := ∞ otherwise. α Φ (G i ) is defined accordingly. Suppose we are given V * d (s 0 ) for these objectives. Then Theorem 5. Let Φ ⊆ Ω be an unambiguous property subset. Let v Φ := (∞ βΦ(c1) ... βΦ(cn) -αΦ(G1) ... -αΦ(Gm)) T . v Φ is dominated by one of the vectors in V * d (s 0 ) iff Φ is solvable.Plugged into Algorithm 1, this yields an alternative approach to computing the exclusions, where all propertysubset solvability tests boil down to lookups; in particular no additional MIPs need to be solved. For any Φ, the domination condition on v Φ can obviously be checked in time linear in the number of entries in V * d (s 0 ). Therefore, if the size of V * d (s 0 ) is small compared to the number of possible property subsets, then this approach can be expected to be more effective than solving the requested property subsets via individual planner calls -provided that the overhead of the V * d (s 0 ) precomputation does not outweigh this benefit.The decision-problem formulation asking whether V π ∈ V * d (s 0 ), for a given V π , is equivalent to the definition of PSS (Definition 5). Hence, as a corollary from Theorem 2, this decision problem is NEXP-COMPLETE, which, unfortunately, excludes the use of existing MOSSP techniques.Let c = (c1 ... cn) T be the cost-function and G = (G1 ... Gm) T be the goal vector. The non-dominated solu- The MIP is iteratively refined taking into account the set Incumbent of policies computed so far. During the course of all iterations, it is guaranteed that (1) only deterministic-optimal policies are ever added to Incumbent, and (2) that for each value vector V * ∈ V * d (s 0 ), there is at most one policy π ∈ Incumbent such that V π (s 0 ) = V * . V * d (s 0 ) is found when the MIP becomes infeasible. Since the number of policies satisfying (1) and ( 2) is exactly |V * d (s 0 )|, termination must happen after the claimed number of iterations.EQUATIONEQUATIONThe encoding is based on Figure 2 , dropping the policyproperty constraints. The optimization function is a linear scalarization of all objectives, i.e., any choice of weights ω > 0 such that n i=1 ω ci + m j=1 ω Gj = 1. This suffices to guarantee (1), which can be shown straightforwardly 595 by contraposition. The bulk of the MIP deals with ensuring progress in the sense of forbidding finding the same solutions again. This is accomplished through constraints (C24), which require improving over the previously computed policy in at least one objective. The selection of this improving 600 objective is implemented via binary integer wildcard variables W π O , for each policy π ∈ Incumbent and objective O. When set, W π O = 1, the MIP solution may perform worse than π wrt. O. However, due to (C25), it is not possible to wildcard all objectives. In other words, each iteration finds a non-dominated π whose value vector V π (s 0 ) differs from all the previous ones; yielding property (2). There is a little caveat, however. To model strict inequality constraints, enforcing strict improvement in at least one objective, (C24) has to include a non-zero ε summand. Nevertheless: Theorem 6. There always exists ε ∈ (0, ∞] such that the sketched algorithm terminates with V * d (s 0 ). In practice, the exact value of ε is task specific and may be difficult to find. The ε parameter can be used to control the precision, and therewith size of the computed solution 615 set, at the cost of losing the formal correctness guarantee.As before, it is possible to leverage the principles of I-DUAL, solving each MIP in multiple iterations, while expanding the state space incrementally. Along the lines, and in addition to our adaptations from the previous section, this requires taking into account the fringe states' optimistic heuristic estimates in the ensure-progress constraints (C24); and, to foster finding non-dominated solutions, in the optimization function (C22). Figure 3 illustrates the changes for I 2 -DUAL's h pom representation. Correctness follows with similar arguments as before. 
experimental evaluation: 
 The focus of our experiments is evaluating the feasibility of the proposed explanation architecture. Our implementation is based on Probabilistic Fast Downward (Helmert 2006; Steinmetz, Hoffmann, and Buffet 2016) . Code and benchmarks will be made publicly available. All experiments were run on a cluster with Intel Xeon E5-2695v4 CPUs, using runtime and memory limits of 30 minutes and 4 GB.Setup We implemented Algorithm 1 via MARCO (Liffiton et al. 2016), using MiniSAT 2.2 (Eén and Sörensson 2003) as the SAT solver. The LPs/MIPs were solved using CPLEX 22.11. We compare 6 PSS methods: PSS-MIP via the MIP encoding of PSS, either (F) building and solving the MIP over the full (reachable) state space directly, or (I) solving the MIP incrementally via our I-DUAL variant using as heuristic the state-of-the-art canonical PPDB heuristic over all patterns of size 2 (Klößner and Hoffmann 2021; Klößner et al. 2021) , or (I 2 ) solving the MIP with our I 2 -DUAL variant. The other three configurations (MO) compute up front the optimal MO value function, using either F, I, or I 2 for enumerating the non-dominated solution vectors. We set ε = 0.05. As a reference, we also experimented with LP relaxations of the PSS-MIP methods, which compute the non-dominated exclusions for the space of stochastic policies. This is not possible for the MO methods as the size of the stochastic MO value function might not be finite. We cannot compare to other MOSSP solvers (e.g., Chen, Trevizan, and Thiébaux 2023) due to the lack of support of goal reachability objectives. As an additional reference, we experiment with a state-of-the-art MaxProb heuristic search configuration using iLAO * (Hansen and Zilberstein 2001) and FRET-π (Steinmetz, Hoffmann, and Buffet 2016) .Benchmarks Our benchmark set is based on existing and new PPDDL benchmarks. A benchmark instance here consists of a PPDDL task τ , a set of properties Ω, and a property subset Φ ⊂ Ω for computing local explanations. The benchmark set is composed of three parts. We leave Φ empty except in the first part:• OSP Following Eifler et al. (2020a) , we generate "OSP" variants of existing benchmarks from the IPPCs and other sources (Steinmetz, Hoffmann, and Buffet 2016; Klößner et al. 2021) that have more than one goal fact. We use Ω as the representation of "soft goals" and Φ to enforce the cost bound. Specifically, for each PPDDL base task τ , we generate for each combination of p ∈ {0.6, 0.75, 0.9} and c ∈ {0.25, 0.5, 0.75} a benchmark instance (1) making the goal of the task empty, (2) each original goal fact g becomes a reachability property φ g with G φg = {g} and α φg = p • P G * where P G * is the MaxProb of τ ; (3) Φ = {φ} where φ is the cost property enforcing as bound β φ = c • h * on τ 's cost function, where h * is the minimal path cost required to reach τ 's goal (J * cannot be used as some benchmarks have no proper policy).• Search and Rescue An adaptation of Trevizan, Thiébaux, and Haslum's (2017) CSSP benchmark. m cells of an n-by-n grid can possibly hold a victim. The agent must navigate through the grid in order to find, and as necessary, rescue the victims, while there are bounds on the total time and fuel consumption. We created 75 instances, randomly generating 5 instances for each combination of n ∈ {5, . . . , 10} and m ∈ {2, 3, 4}. Ω includes the reachability properties φ x requiring the victim from cell x being rescued with probability of 1; and for the time and fuel cost functions, the cost properties φ c,c with β φc,c = c • J c, * , where J c, * is the minimal expected cost under c of rescuing all victims, and c ∈ {0.5, 0.75, 1.0, 1.25, 1.5}. Note that c > 1 makes sense, because being optimal wrt. one cost function does not mean being optimal wrt. the other cost function. • Factory A use-case of an actual company. Incoming product components must be stashed in first-in-first-out storage racks, and taken out of the racks as requested by the production lines. There is uncertainty about the component requested next. Components can be moved between racks. Ideally, all production lines should be served while using as few racks as possible and moving as few components between the racks as possible. We generated 90 random instances with {3, 4, 5, 6} incoming components, {2, 3} available racks, and {2, 3} production lines. We encode the three different preferences as properties: the probability p of successfully serving all production lines, considering p ∈ {0.5, 0.6, . . . , 1.0}; a reachability property φ n where G φn encodes that n racks have not been used and α G φn = 1; and bounds on component movements between racks, modeled as the cost property φ m where β φm = m and m ∈ {1, . . . , 5}.The left-hand side of Once computed, the generation of the explanation only takes a split second. This can become an advantage for computing multiple local explanations in a row, which we did not 735 evaluate here. Compared to the references, the theoretical complexity results are partially reflected in the data. Overall, explanations could be computed in only a fraction of the instances feasible for MaxProb. However, PSS-MIP I 2 's close performance to its LP-relaxed counterpart suggests that the 740 reason of this discrepancy already lies in the secondary constraints and objectives rather than the original source of the complexity increase (deterministic policies). 
conclusion: 
 In the presence of action-outcome uncertainty, characteris-745 tics of solution policies are defined by the expectation over the policies' executions. We introduced accordingly policy reachability and cost variants of Eifler et al.'s (2020a) plan properties. The analysis of mutual relationships between user-provided properties can comprehensibly summa-750 rize trade-offs in the infeasibly large space of all (global) or selected (local) policies. We showed that under the restriction to deterministic policies, this analysis is however computationally more difficult than the computation of a single solution policy. Our empirical results reflected to an ex-755 tent this complexity, but also showed that proposed explanation methodology can be feasible. We introduced two algorithm variants identifying the properties' exclusion relationships. While analyzing property combinations individually tends to be more efficient in computing a single explana-760 tion, taking the detour via multi-objective optimization can have strengths in an interactive setting where a user might request a series of local explanations. The adaptation of multiobjective heuristics (Geißer et al. 2022 ) is a promising direction to improve scalability of the proposed methods. 
: 
 others. To strengthen confidence in the planner's decisionmaking, recent work in classical planning has introduced a framework for explaining to the user the possible solution space in terms of necessary trade-offs between user-provided plan properties. Here, we extend this framework to SSPs. We introduce a notion of policy properties taking into account action-outcome uncertainty. We analyze formally the computational problem of identifying the exclusion relationships between policy properties, showing that this problem is in fact harder than SSP planning in a complexity theoretical sense.We show that all the relationships can be identified through a series of heuristic searches, which, if ordered in a clever way, yields an anytime algorithm. Further, we introduce an alternative method, which leverages a connection to multi-objective probabilistic planning to move all the computational burden to a pre-process. Finally, we explore empirically the feasibility of the proposed explanation methodology on a range of adapted IPPC benchmarks. 
 
 Appendix:  


Decision: The paper applies the general idea behind a recent contribution to explainable AI from classical planning to SSPs. The approach from classical planning analysis user-given plan properties and identifies trade-offs between the given properties. The SSP setting is much more complicated. The authors generalize plan properties to policy properties, define and theoretically analyze the corresponding Property-Subset Solvability problem (called PSS) for SSPs, and propose and evaluate two approaches for solving the problem.
The reviewers are happy with the quality, originality and significance of the work. The paper is very dense and not always easy to follow.

Pros:
- highly non-incremental extension to SSPs
- the paper tackles a difficult and interesting problem
- promising approach
- sound and rigorous

Cons:
- the paper is very dense and some technical details like the full MIP encoding have been omitted.
- no examples
- one reviewer did not like the structure of the paper

Reviews: review: strength_weakness: strength_weakness: As I said above, the paper is quite well-written. However, the use of minimal examples along the way (e.g. a small problem + a possible set of policy properties one may want to check for) could enhance the paper even more.

L18 in the abstract mentions "anytime" algorithm -- however unless I missed it, I didn't see too much attention paid to that aspect in the empirical evaluation. Given the challenging nature of the problem, quantifying in some ways the quality of solutions built along the way would be useful to see. The empirical evaluation only focuses on
questions: questions: Could you elaborate on the anytime aspects you hinted at in the abstract?
strength_weakness: strength_weakness: - The paper organization is kind of chaotic. Between sections 3, 4, and 5, the authors interleave contributions and theoretical background, making it difficult for the reader to understand what is novel and what is background theory. Besides, the paper involves several non trivial and not sufficiently explained approaches such as how to make a MIP encoding of PSS for a property subset based on a MIP encoding of SSPs in the dual space (Trevizan et al). Another non trivial approach, and not well explained as well, is how to use iLAO  and FRET-\pi to solve multi-objective SSPs.

- Since the authors has focused on the theoretical aspects of the paper, the Experimentation section feels too summarized and missing discussions about the setups and results. 

- Some typos: 
    - Lines 91 and 120: the use of calligraphy G notation for a "conjunctive goal" and regular G notation later.
    - Line 157: an explanation for the meaning of "rhs" is missing. 
    - Line 170: is the term "AllMUSes" used as an abbreviation? or an algorithm? It is not clear if the authors are talking about an algorithm called "AllMUSes" (that is able to compute the set of all MUSes) or if it is a theoretical concept (like a group of algorithms that computes all MUSes).
questions: questions: 1. How difficult could b  for the user to specify the set of policy properties? 

2. Line 652: " We cannot compare to other MOSSP solvers (e.g., Chen, Trevizan, and Thiebaux 2023) due to the lack of support of goal reachability objectives."  See section 3 of the referred paper and comment. 

3. What possible adaptations can be done in the work of  Geißer et al. 2022, since you claim that this is a promising direction to improve scalability of the proposed method?
strength_weakness: strength_weakness: I would like to see more motivation for why this is an important problem to solve. Including an example would also help in this direction.

The ideas that are introduced are somewhat difficult to follow and visualize. Perhaps this is unavoidable given the complexity of the problem under consideration, but I think having a running example that is referred to with each new concept would be helpful. I would also suggest including more intuitions in the paper whenever possible to make it easy for the reader to follow.

A figure showing an example output for a small problem, or a part of the output, would be helpful.

Several of the concepts discussed in the paper are more readily understood by many researchers as "soft goals", "rewards", or "utilities" but these terms do not appear until much later in the paper if at all. I think making it clearer early in the paper that these are at least very similar concepts to what is being discussed would make the paper easier to follow for a larger audience.
questions: questions: As I understand it, non-deterministic policies might be able to satisfy preferences that deterministic policies are not able to, e.g. by trying an action that has a positive cost in a different cost function if the bound has already been reached for another one. Is this intuition correct? If so, why focus only on deterministic policies? Is this a limitation of the algorithms used to compute the solution or are there other reasons?

Would some sort of mutex computation improve performance by decreasing the sizes of the different sets that need to be considered? e.g. a fluent that is mutex with the goal could be ruled out directly instead of potentially requiring an iteration of the algorithm.

"too many non-dominated but almost indistinguishable value vectors" would some sort of binning scheme be helpful here to discard entries that are epsilon equal to existing values?

typos etc:

"while planners neither justify the reasons behind their choice of a particular policy over others" unclear what 'neither' refers to here, if meant to contrast with previous part of sentence I would say "nor do planners justify..."

"move all the computational burden to a pre-process" --> to a preprocessing step

"Krarup et al.’s (2021) introduced a generic iterative planning framework" awkward citation format, maybe remove possessive 's, as in the next sentence.

Classical planning is *a* special case of probabilistic planning

if the heuristics provide*d* are admissible

"equally expressive than stochastic policies" than --> as

This is, we must make sure --> That is, we must make sure... 

line 541 - using commas between entries in the vector would clarify that the terms are separate and there is no term that is the difference of two values. 

line 541 - last term should be −P^G_m,\pi, that is, m rather than 2, correct?

"We created 75 instances" I think the numbers given lead to 80 instances? 6 n values * 3 m values * 5 instances

"only half as many states than" than --> as