In planning and reasoning about action and change, reversibility of actions is the problem of deciding whether the e ects of an action can be reverted by applying other actions in order to return to the original state. While this problem has been studied for some time, recently there has been renewed interest in the context of the language PDDL. After reviewing the concepts, in this paper we propose a solution by leveraging an existing translation from PDDL domains and problems to Answer Set Programming (ASP). This work serves as the basis for the rst sound and complete system for determining reversibility of PDDL actions, for now restricted to the STRIPS fragment.
Traditionally, the eld of Automated Planning [
Studying action reversibility is important for several reasons. Intuitively,
actions whose e ects 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
bene cial in a plan generation process [
In [
The complexity analyses in [
Structure. The remainder of the paper is organized as follows. In Section 2,
we introduce basic concepts; Section 3 then reviews de nitions and properties
of di erent versions of reversibility from [
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 = hpre(a); add (a); del (a)i, where pre(a) F is the set of preconditions of a, and add (a) F and del (a) F are the add and delete e ects 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 i 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 n del (a)) [ add (a). A sequence of actions = ha1; : : : ; ani is applicable in a state s0 i there is a sequence of states hs1; : : : ; sni such that, for 0 < i n, it holds that ai is applicable in si 1 and ai[si 1] = si. Applying the action sequence on s0 is denoted [s0], with [s0] = sn. The length of action sequence is denoted j j.
A STRIPS planning task = hF ; A; s0; Gi is a tuple consisting of a set of facts F = ff1; : : : ; fng, a set of (ground) actions A = fa1; : : : ; amg, an initial state s0 F , and a goal speci cation (or, simply, goal ) G F . A state s F is a goal state (for ) i G s. An action sequence is called a plan i [s0] G. We further de ne several relevant notions w.r.t. a planning task . A state s is reachable from state s0 i there exists an applicable action sequence such that [s0] = s. A state s 2 2F is simply called reachable i it is reachable from the initial state s0. The set of all reachable states in is denoted by R . An action a is reachable i there is some state s 2 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 [
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 [
Brie y, ASP programs consist of sets of rules of the form a1 j j an
b1; : : : ; b`; :b`+1; : : : ; :bm: In these rules, all ai and bi are atoms of the form p(t1; : : : ; tn), where p is a predicate name, and t1; : : : ; tn 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 [
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. [
While this intuition is fairly straightforward, when formally de ning 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 [
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 de ne several concrete sets of states S that are useful to consider when considering whether an action is reversible. For instance, S could be de ned via a propositional formula over the facts in F . Or we can consider a set of all possible states (2F ) 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 di er only in the initial state or goals). Or we can move our attention to a speci c STRIPS instance and ask whether a certain action is uniformly reversible for all states reachable from the initial state.
De nition 2. Let F , A, S, and a be as in De nition 1. We call the action a 1. uniformly '-reversible i a is uniformly S-reversible in the set S of models of the propositional formula ' over F ; 2. uniformly reversible in i a is uniformly R -reversible for some STRIPS planning task ; and 3. universally uniformly reversible, or, simply, uniformly reversible, i a is uniformly 2F -reversible.
Given the above de nitions, 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 i a is
uniformly (S-)reversible using the sequence of actions . It is interesting to note
that this de nition of the reverse plan based on uniform reversibility now
coincides with the same notion as de ned by [
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 2P ) [
After reviewing the relevant features of plasp [
The system plasp [
for each a 2 A and f 2 pre(a) { postcondition(action("a"),effect(unconditional),variable("f"), value(variable("f"),true)) :- action(action("a")).
for each a 2 A and f 2 add (a) { postcondition(action("a"),effect(unconditional),variable("f"), value(variable("f"),false)) :- action(action("a")).
for each a 2 A and f 2 del (a) Example 1. The STRIPS domain with F = ff g and actions del f = hff g; ;; ff gi and add f = h;; ff g; ;i 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")). 4.2
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 [
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 de ned, rstly, 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.
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 nd a reverse plan. In fact, from the initial state de ned above, we need to nd 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 modi ed). 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, 3 The full encoding is available here: https://sea le.aau.at/d/e0aedc92b4c546d5bf9a/. 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 rst 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 de ned constant \horizon") the initial state and the resulting state of plan are the same. It is not di cult 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; a1; : : : ; an of actions, where a1; : : : ; an 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
speci ed 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 [
The encoding starts o much like the previous one:
holds(V, Val, 0) :chosen(A), precondition(action(A), variable(V), value(variable(V), Val)). affected(A, V) :- postcondition(action(A), _, variable(V), _).
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 a ected (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 nd 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:
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 speci ed 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 [
The rst rule above speci es 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 rst encoding given in this section; that is, it checks for universal uniform reversibility. However, the second encoding can be easily modi ed 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 exible 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. 4.3
We have conducted preliminary experiments with arti cially 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)) 4 The full encoding can be found at https://sea le.aau.at/d/e0aedc92b4c546d5bf9a/.
The action del-all has a universal uniform reverse plan h add-f0, . . . , add-fi i. We have generated instances from i = 10 to i = 500 with step 10. We have analyzed runtime and memory consumption of two problems: (a) nding 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 rst 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). simple encoding saturation encoding simple encoding saturation encoding 250 200 ()s 150 e m i tun 100 R 50 0 40 ) s (e m i tunR 20 0 0 0 100 200 300 400 500
Number of facts 100 200 300 400 500
Number of facts 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. simple encoding saturation encoding simple encoding saturation encoding ) 1;000 B M ( y r eom 500 M 0
0 ) 1;000 B M ( y r eom 500 M 0
0 100 200 300 400 500
Number of facts 100 200 300 400 500
Number of facts
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. 5
In this paper, we have given a review of several notions of action reversibility in
STRIPS planning, as originally presented in [
The two encodings use two di erent approaches. The rst 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 [
In order to compare the two encodings, we performed some benchmarks on arti cially 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 o er a trade-o : while the rst encoding is clearly more e cient when checking for universal uniform reversibility, the saturation-based encoding is more exible 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. [