Introduction

Traditionally, the field of Automated Planning [17,18] deals with the problem of generating a sequence of actions-a plan-that transforms an initial state of the environment to some goal state. Actions, in plain words, stand for modifiers of the environment. One interesting question is whether the effects of an action are reversible (by other actions), or in other words, whether the action effects can be undone. Notions of reversibility have previously been investigated; cf. e.g., works by Eiter et al. [12] or by Daum et al. [9].

Studying action reversibility is important for several reasons. Intuitively, actions whose effects cannot be reversed might lead to dead-end states from which the goal state is no longer reachable. Early detection of a dead-end state is beneficial in a plan generation process [20]. Reasoning in more complex structures such as Agent Planning Programs [10] which represent networks of planning tasks where a goal state of one task is an initial state of another is even more prone to dead-ends [6]. Concerning non-deterministic planning, for instance Fully Observable Non-Deterministic (FOND) Planning, where actions have non-deterministic effects, determining reversibility or irreversibility of each set of effects of the action can contribute to early dead-end detection, or to generalizing recovery from undesirable action effects which is important for efficient computation of strong (cyclic) plans [5]. Concerning online planning, we can observe that applying reversible actions is safe and hence we might not need to explicitly provide the information about safe states of the environment [8]. Another, although not very obvious, benefit of action reversibility is in plan optimization. If the effects of an action are later reversed by a sequence of other actions in a plan, these actions might be removed from the plan, potentially shortening it significantly. It has been shown that under such circumstances, pairs of inverse actions, which are a special case of action reversibility, can be removed from plans [7].

In [21] we have introduced a general framework for action reversibility that offers a broad definition of the term, and generalizes many of the already proposed notions of reversibility, like "undoability" proposed in [9], or the concept of "reverse plans" as introduced in [12]. The concept of reversibility in [21] directly incorporates the set of states in which a given action should be reversible. We call these notions S-reversibility and ϕ-reversibility, where the set S contains states, and the formula ϕ describes a set of states in terms of propositional logic. These notions are then further refined to universal reversibility (referring to the set of all states) and to reversibility in some planning task Π (referring to the set of all reachable states w.r.t. the initial state specified in Π). These last two versions match the ones proposed in [9]. Furthermore, our notions can be further restricted to require that some action is reversible by a single "reverse plan" that is not dependent of the state for which the action is reversible. For single actions, this matches the concept of the same name proposed in [12].

The complexity analyses in [21] indicate that several of these tasks can be solved by means of Answer Set Programming (ASP). In this paper, we leverage the translations implemented in plasp [11] and produce encodings to effectively solve some reversibility tasks on PDDL domains, for now restricted to the STRIPS [14] fragment.

Structure. The remainder of the paper is organized as follows. In Section 2, we introduce basic concepts; Section 3 then reviews definitions and properties of different versions of reversibility from [21]; in Section 4 we review the plasp format and present some ASP encodings for reversibility tasks before concluding in Section 5.

2 Background STRIPS Planning. Let F be a set of facts, that is, atomic statements about the world. Then, a subset s ⊆ F is called a state, which intuitively represents a set of facts considered to be true. An action is a tuple a = pre(a), add (a), del (a) , where pre(a) ⊆ F is the set of preconditions of a, and add (a) ⊆ F and del (a) ⊆ F are the add and delete effects of a, respectively. W.l.o.g., we assume actions to be well-formed, that is, add (a) ∩ del (a) = ∅ and pre(a) ∩ add (a) = ∅. An action a is applicable in a state s iff pre(a) ⊆ s. The result of applying an action a in a state s, given that a is applicable in s, is the state a[s] = (s \ del (a)) ∪ add (a). A sequence of actions π = a 1 , . . . , a n is applicable in a state s 0 iff there is a sequence of states s 1 , . . . , s n such that, for 0 < i ≤ n, it holds that a i is applicable in s i−1 and a i [s i−1 ] = s i . Applying the action sequence π on s 0 is denoted π[s 0 ], with π[s 0 ] = s n . The length of action sequence π is denoted |π|.

A STRIPS planning task Π = F, A, s 0 , G is a tuple consisting of a set of facts F = {f 1 , . . . , f n }, a set of (ground) actions A = {a 1 , . . . , a m }, an initial state s 0 ⊆ F, and a goal specification (or, simply, goal

) G ⊆ F. A state s ⊆ F is a goal state (for Π) iff G ⊆ s. An action sequence π is called a plan iff π[s 0 ] ⊇ G.

We further define several relevant notions w.r.t. a planning task Π. A state s is reachable from state s iff there exists an applicable action sequence π such that π[s ] = s. A state s ∈ 2 F is simply called reachable iff it is reachable from the initial state s 0 . The set of all reachable states in Π is denoted by R Π . An action a is reachable iff there is some state s ∈ R Π such that a is applicable in s.

Deciding whether a STRIPS planning task has a plan is known to be PSpacecomplete in general and it is NP-complete if the length of the plan is polynomially bounded [3].

Answer Set Programming (ASP). We assume the reader is familiar with ASP and will only give a very brief overview of the core language. For more information, we refer to standard literature [2,15,19], and, in our case, the ASP-Core-2 input language format [4].

Briefly, ASP programs consist of sets of rules of the form

a 1 | • • • | a n ← b 1 , . . . , b , ¬b +1 , . . . , ¬b m .

In these rules, all a i and b i are atoms of the form p(t 1 , . . . , t n ), where p is a predicate name, and t 1 , . . . , t n are terms, that is, either variables or constants. The domain of constants in an ASP program P is given implicitly by the set of all constants that appear in it. Generally, before evaluating an ASP program, variables are removed by a process called grounding, that is, for every rule, each variable is replaced by all possible combination of constants, and appropriate ground copies of the rule are added to the resulting program ground (P ). In practice, several optimizations have been implemented in state-of-the-art grounders that try to minimize the size of the grounding. The result of a (ground) ASP program P is calculated as follows [16]. An interpretation I (i.e., a set of ground atoms appearing in P ) is called a model of P iff it satisfies all the rules in P in the sense of classical logic. It is further called an answer set of P iff there is no proper subset I ⊂ I that is a model of the so-called reduct P I of P w.r.t. I. P I is defined as the set of rules obtained from P where all negated atoms on the right-hand side of the rules are evaluated over I and replaced by or ⊥ accordingly. The main decision problem for ASP is deciding whether a program has at least one answer set. This has been shown to be Σ P 2 -complete [13].

Reversibility of Actions

In this section, we describe the notion of reversibility of actions. In particular, we focus on the notion of uniform reversibility, but note that there are other notions of reversibility which are lied out and explained in detail by Morak et al. [21]. Intuitively, we call an action reversible if there is a way to undo all the effects that this action caused, and we call an action uniformly reversible if its effects can be undone by a single sequence of actions irrespective of the state where the action was applied. While this intuition is fairly straightforward, when formally defining this concept, we also need to take several other factors into account-in particular, the set of possible states where an action is considered plays an important role [21].

Definition 1. Let F be a set of facts, A be a set of actions, S ⊆ 2 F be a set of states, and a ∈ A be an action. We call a uniformly S-reversible iff there exists a sequence of actions π = a 1 , . . . , a n ∈ A n such that for each s ∈ S wherein a is applicable it holds that π is applicable in a[s] and π[a[s]] = s.

The notion of uniform reversibility in the most general sense does not depend on a concrete STRIPS planning task, but only on a set of possible actions and states w.r.t. a set of facts. Note that the set of states S is an explicit part of the notion of uniform S-reversibility.

Based on this general notion, it is then possible to define several concrete sets of states S that are useful to consider when considering whether an action is reversible. For instance, S could be defined via a propositional formula over the facts in F. Or we can consider a set of all possible states (2 F ) which gives us a notion of uniform reversibility that applies to all possible planning tasks that share the same set of facts and actions (i.e., the tasks that differ only in the initial state or goals). Or we can move our attention to a specific STRIPS instance and ask whether a certain action is uniformly reversible for all states reachable from the initial state. Definition 2. Let F, A, S, and a be as in Definition 1. We call the action a 1. uniformly ϕ-reversible iff a is uniformly S-reversible in the set S of models of the propositional formula ϕ over F; 2. uniformly reversible in Π iff a is uniformly R Π -reversible for some STRIPS planning task Π; and 3. universally uniformly reversible, or, simply, uniformly reversible, iff a is uniformly 2 F -reversible.

Given the above definitions, we can already observe some interrelationships. In particular, universal uniform reversibility (that is, uniform reversibility in the set of all possible states) is obviously the strongest notion, implying all the other, weaker notions. It may be particularly important when one wants to establish uniform reversibility irrespective of the concrete STRIPS instance.

The notion of uniform reversibility naturally gives rise to the notion of the reverse plan. We say that some action a has an (S-)reverse plan π iff a is uniformly (S-)reversible using the sequence of actions π. It is interesting to note that this definition of the reverse plan based on uniform reversibility now coincides with the same notion as defined by [12]. Note, however, that in that paper the authors use a much more general planning language.

Even if the length of the reverse plan is polynomially bounded, the problem of deciding whether an action is uniformly (ϕ-)reversible is intractable. In particular, deciding whether an action is universally uniformly reversible (resp. uniformly ϕ-reversible) by a polynomial length reverse plan is NP-complete (resp. in Σ P

2 ) [21].

Methods

After reviewing the relevant features of plasp [11] in Section 4.1, we present our encodings for determining reversibility in Section 4.2.

The plasp Format

The system plasp [11] transforms PDDL domains and problems into facts. Together with suitable programs, plans can then be computed using ASP solvers. Given a STRIPS domain with facts F and actions A, the following relevant facts and rules will be created by plasp:

variable(variable("f")). for all f ∈ F action(action("a")). for all a ∈ A precondition(action("a"),variable("f"),value(variable("f"),true)) :-action(action("a")).

for each a ∈ A and f ∈ pre(a) postcondition(action("a"),effect(unconditional),variable("f"), value(variable("f"),true)) :-action(action("a")). for each a ∈ A and f ∈ add (a) postcondition(action("a"),effect(unconditional),variable("f"), value(variable("f"),false)) :-action(action("a")). for each a ∈ A and f ∈ del (a)

Example 1. The STRIPS domain with F = {f } and actions del−f = {f }, ∅, {f } and add − f = ∅, {f }, ∅ is written in PDDL as follows:

(define (domain example1 ) (:requirements :strips) (:predicates (f) ) (:action del-f :precondition (f) :effect (not (f))) (:action add-f :effect (f)))

plasp translates this domain to the following ASP code (plus a few technical facts and rules):

variable(variable("f")). action(action("del-f")). precondition(action("del-f"), variable("f"), value(variable("f"), true)) :-action(action("del-f")). postcondition(action("del-f"), effect(unconditional), variable("f"), value(variable("f"), false)) :-action(action("del-f")). action(action("add-f")). postcondition(action("add-f"), effect(unconditional), variable("f"), value(variable("f"), true)) :-action(action("add-f")).

Reversibility Encodings in ASP

In this section, we present our ASP encoding for checking whether, in a given domain, there is an action that is uniformly reversible. As we have seen in Section 4.1, the plasp tool is able to rewrite STRIPS domains into ASP even when no concrete planning instance for that domain is given. We will present two encodings, one for (universal) uniform reversibility, and one that can be used for uniform ϕ-reversibility.

Note that universal uniform reversibility is computationally easier than ϕuniform reversibility (under standard complexity-theoretic assumptions). For a given action (and polynomial-length reverse plans), the former can be decided in NP, while the latter is harder [21,Theorem 18 and 20]. We will hence start with the encoding for the former problem, which follows a standard guess-and-check pattern.

Universal Uniform Reversibility. As a "database" the encoding takes the output of plasp's translate action [11]. The problem can be solved in NP due to the following Observation (*): in any (universal) reverse plan for some action a, it is sufficient to consider only the set of facts that appear in the precondition of a. If any action in a candidate reverse plan π for a (resp. a itself) contains any other fact than those in pre(a), then π cannot be a reverse plan for a (resp. a is not uniformly reversible) [21,Theorem 18]. With this observation in mind, we can now describe the (core parts of) our encoding 3 .

The encoding makes use of the following main predicates (in addition to several auxiliary predicates, as well as those imported from plasp):

chosen/1 holds the action to be tested for reversibility.

holds/3 encodes that some fact (or variable, as they are called in plasp parlance) is set to a certain value at a given time step. occurs/2 encodes the candidate reverse plan, saying which action occurs at which time step.

With the intuitive meaning of the predicates defined, firstly, we chose an action from the available actions and set the initial state as the facts in the precondition of the chosen action. We also say, in line with the Observation (*) above, that only those variables in the precondition are relevant to check for a reverse plan.

1 {chosen(A) : action(action(A))} 1. holds(V, Val, 0) :chosen(A), precondition(action(A), variable(V), value(variable(V), Val)). relevant(V) :-holds(V, _, 0). These rules set the stage for the inherent planning problem to be solved to find a reverse plan. In fact, from the initial state defined above, we need to find a plan π that starts with action a (the chosen action), such that after executing π we end up in the initial state again. Such a plan is a (universal) reverse plan. This idea is encoded in the following: time(0..horizon+1).

occurs(A, 1) :-chosen(A). 1 {occurs(A, T) : action(action(A))} 1 :-time(T), T > 1.

caused(V, Val, T) :occurs(A, T), postcondition(action(A), _, variable(V), value(variable(V), Val)), holds(V2, Val2, T -1) : precondition(action(A), variable(V2), value(variable(V2), Val2)). modified(V, T) :-caused(V, _, T).

holds(V, Val, T) :-caused(V, Val, T). holds(V, Val, T) :-holds(V, Val, T -1), not modified(V, T), time(T).

The above rules guess a potential plan π as described above, and then execute the plan on the initial state (changing facts if this is caused by the application of a rule, and keeping the same facts if they were not modified). The notation in the rule body for caused is an abbreviation for requiring holds for each precondition. Finally, we simply need to check that the plan is (a) executable, and (b) leads from the initial state back to the initial state. This can be done with the following constraints:

:-occurs(A, T), precondition(action(A), variable(V), value(variable(V), Val)), not holds(V, Val, T -1).

:-occurs(A, T), precondition(action(A), variable(V), _), not relevant(V). :-occurs(A, T), postcondition(action(A), _, variable(V), _), not relevant(V).

:-holds(V, Val, 0), not holds(V, Val, horizon+1). :-holds(V, Val, horizon+1), not holds(V, Val, 0).

The first rule checks that rules in the candidate plan are actually applicable. The next two check that the rules do not contain any facts other than those that are relevant (cf. Observation (*) above). Finally, the last two rules make sure that at the maximum time point (i.e., the one given by the externally defined constant "horizon") the initial state and the resulting state of plan π are the same. It is not difficult to verify that any answer set of the above program (combined with the plasp translation of a STRIPS problem domain) will yield a plan π (encoded by the occurs predicate) that contains the sequence a, a 1 , . . . , a n of actions, where a 1 , . . . , a n is a (universal) reverse plan for the action a. Note that our encoding yields reverse plans of length exactly as long as set in the "horizon" constant. This completes our encoding for the problem of deciding universal uniform reversibility.

Other Forms of Uniform Reversibility. Using a similar guess-and-check idea as in the previous encoding, we can also check for uniform reversibility for a specified set of states (that is, uniform S-reversibility). Generally, the set S of relevant states is encoded in some compact form, and our encoding therefore, intentionally, does not assume anything about this representation, but leaves the precise checking of the set S open for implementations of a concrete use case. The predicates used in this more advanced encoding are similar to the ones used in the previous for the universal case above, and hence we will not list them here again. However, in order to encode the for-all-states check (i.e., the check that the candidate reverse plan works in all states inside the set S), we now need an advanced ASP encoding technique called saturation [13].

The encoding starts off much like the previous one:

Note that we no longer need to keep track of any set of "relevant" facts, since we now need to consider all the facts that appear inside the actions and in the set S of states. However, we need to keep track of those facts that are affected (i.e., potentially changed) by the application of an action. We assume that a predicate opposites/2 exists that holds, in both possible orders, the values "true" and "false". This will later be used to find the opposite value of some fact at a particular time step.

Next, we again guess and execute a plan, keeping track of whether the actions were able to be applied at each particular time step: occurs(A, 1) :-chosen(A). 1 {occurs(A, T) : action(action(A))} 1 :-time(T), T > 1. applied(0). % no action needs to be applied at time step 0 applicable(A, T) :occurs(A, T), applied(T -1), holds(V, Val, T -1) : precondition(action(A), variable(V), value(variable(V), Val)). applied(T) :-applicable(_, T). holds(V, Val, T) :applicable(A, T), postcondition(action(A), _, variable(V), value(variable(V), Val)). holds(V, Val, T) :holds(V, Val, T -1), occurs(A, T), applied(T), not affected(A, V).

Again, the rules above choose a candidate reverse plan π, starting with the action-to-be-checked a, as before. Furthermore, we set up the goal conditions: π should be applicable (i.e., at each time step, the relevant action must have been applied), and furthermore, the state at the beginning must be equal to the state at the end. same(V) :-holds(V, Val, 0), holds(V, Val, horizon + 1). samestate :-same(V) : variable(variable(V)). planvalid :-applied(horizon + 1). reversePlan :-samestate, planvalid.

Finally, we need to specify that for all the states specified in the set S the candidate reverse plan must work. This is done as follows:

holds(V, Val1, 0) | holds(V, Val2, 0) :- variable(variable(V)), opposites(Val1, Val2), Val1 < Val2. holds(V, Val, T) :- reversePlan, contains(variable(V), value(variable(V), Val)), time(

T). :-not reversePlan.

As stated above, this is done using the technique of saturation [13]. We encourage the reader to refer to the relevant publication for more details on the "inner workings" of this encoding technique. In our case, intuitively, the rules state the following:

The first rule above specifies that some initial state should be guessed where the candidate reverse plan π is to be checked. The second and third rule together say that, for each such possible guess (i.e., for each possible initial state), the atom reversePlan must be derived for that particular guess. This concludes the main part of our encoding. In its current form, the encoding given above produces exactly the same results as the first encoding given in this section; that is, it checks for universal uniform reversibility. However, the second encoding can be easily modified in order to check uniform S-reversibility. Simply add a rule of the following form to it: reversePlan :-< check guess against set S > This rule should derive the atom reversePlan precisely when the current guess (that is, the currently considered starting state) does not belong to the set S. This can of course be generalized easily. For example, if set S is given as a formula ϕ, then the rule should check whether the current guess conforms to formula ϕ (i.e., encodes a model of ϕ). Other compact representations of S can be similarly checked at this point. Hence, we have a flexible encoding for uniform S-reversibility that is easy to extend with various forms of representations of set S4 . This concludes the description of our encodings.

Experiments

We have conducted preliminary experiments with artificially constructed domains. The domains are as follows:

(define (domain rev-i) (:requirements :strips) (:predicates (f0) ... (fi)) (:action del-all :precondition (and (f0) ... (fi) ) :effect (and (not (f0)) ... (not (fi))))

(:action add-f0 :effect (f0))

...

(:action add-fi :precondition (fi-1) :effect (fi)))

The action del-all has a universal uniform reverse plan add-f0, . . . , add-fi . We have generated instances from i = 10 to i = 500 with step 10. We have analyzed runtime and memory consumption of two problems: (a) finding the reverse plan of size i (by setting the constant horizon to i) and proving that no other reverse plan exists, and (b) showing that no reverse plan of length i-1 exists (by setting the constant horizon to i-1). We compare the two encodings described in Section 4.2, we refer to the first one as simple encoding and the second one as saturation encoding.

We have used plasp 3.1.1 (https://potassco.org/labs/plasp/) and clingo 5.4.0 (https://potassco.org/clingo/) on a computer with a 3.1 GHz Intel Xeon Gold 6254 CPU with 18 cores and 128 GB RAM running CentOS 7. We have set a timeout of 10 minutes and a memory limit of 4GB (which was never exceeded). The results for problem (a) are plotted in Figure 1. The saturation encoding exceeded the time limit already at the problem with 50 facts, while the simple encoding could solve all problems in under 20 seconds. The memory consumption increased with i, but was relatively moderate, also for the saturation encoding. The results for problem (b) are plotted in Figure 2. While the simple encoding shows very similar behavior to problem (a), the saturation encoding took longer and had a time-out already at i = 40.

In total, the saturation encoding scales worse, as expected, but it can still solve problems of reasonable size. Another positive observation is that memory consumption does not appear to be an issue.

Conclusions

In this paper, we have given a review of several notions of action reversibility in STRIPS planning, as originally presented in [21]. We then proceeded, on the basis of the PDDL-to-ASP translation tool plasp [11], to present two ASP encodings to solve the task of universal uniform reversibility of STRIPS actions, given a corresponding planning domain. When given to an ASP solving system, these encodings, combined with the ASP translation of STRIPS planning domains produced by plasp, then yield a set of answer sets, each one representing a (universal) reverse plan for each action in the domain, for which such a reverse plan could be found.

The two encodings use two different approaches. The first encoding makes use of a shortcut that allows it to focus only on those facts that appear in the precondition of the action to check for reversibility [21]. The second encoding makes use of an advanced ASP encoding technique called saturation [13], which allows for the expression of universal quantifiers. It directly encodes the original definition of uniform reversibility: for an action to be uniformly reversible, there must exists a plan, and this plan must revert that action in all possible starting states (where it is applicable). This second encoding is more flexible insofar as it also allows for the checking of non-universal uniform reversibility (e.g., to check for uniform ϕ-reversibility, where the starting states are given via some formula ϕ).

In order to compare the two encodings, we performed some benchmarks on artificially generated instances by checking whether there is an action that is universally uniformly reversible. For the ASP community, it will not come as a surprise that the saturation-based encoding was performing much more poorly than the encoding without saturation. However, we found that, for our benchmark instances, both encodings were able to solve reasonably sized instances. Therefore, the encodings offer a trade-off: while the first encoding is clearly more efficient when checking for universal uniform reversibility, the saturation-based encoding is more flexible in that it can also be used to check more advanced versions where a given set of starting states needs to be considered.

For future work, we intend to optimize our encodings further, and see how they perform on real-world benchmark instances. It would also be interesting to see how they perform when compared to a procedural implementation of the algorithms proposed for reversibility checking by Morak et al. [21]. We would also like to compare our approach to existing tools RevPlan 5 (implementing tech-niques of [12]) and undoability (implementing techniques of [9]). Furthermore, we would also like to test other ASP systems such as DLV26 [1].