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 as 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 to Answer Set Programming (ASP), which we then use to solve the problem via epistemic logic programs (ELPs). This work provides a sound and complete system for determining reversibility of PDDL actions (restricted to the STRIPS fragment), while also providing insight into the performance of state-ofthe-art ELP solvers.
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 [
Epistemic Logic Programs (ELPs) and Answer Set Programming (ASP). We
assume the reader is familiar with ELPs and will only give a very brief overview of
the core language. For more information, we refer to the original paper proposing
ELPs [
Brie y, ELPs consist of sets of rules of the form a1 _ : : : _ an `1; : : : ; `m: In these rules, all ai 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. Each ` is either an objective or subjective literal, where objective literals are of the form a or :a (for a an atom), and subjective literals are of the form K l or :K l, where l is an objective literal. Note that often the operator M is also used, which we will simply treat as a shorthand for :K :.
The domain of constants in an ELP P is given implicitly by the set of all constants that appear in it. Generally, before evaluating an ELP 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 systems that try to minimize the size of the grounding.
The result of a (ground) ELP 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 set of rules (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 ELP encodings 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 rules 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 [17, 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 a single 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. chosen(A) :- action(action(A)), not &k{-chosen(A)}. -chosen(A) :- action(action(A)), not &k{ chosen(A)}. :- chosen(A), chosen(B), A!=B. onechosen :- chosen(A). :- not onechosen. 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). occurs(A, T) :- action(action(A)),time(T), T > 1, not &k{-occurs(A, T)}. -occurs(A, T) :- action(action(A)),time(T), T > 1, not &k{occurs(A, T)}. :- occurs(A,T), occurs(B,T), A!=B. oneoccurs(T) :- occurs(A,T), time(T), T > 0. :- time(T), T>0, not oneoccurs(T). 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)). 1 The full encoding is available here: https://sea le.aau.at/d/373cd25718dc4377afec/. 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, 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). noreversal :- holds(V, Val, 0), not holds(V, Val, H+1), horizon(H). noreversal :- holds(V, Val, H+1), not holds(V, Val, 0), horizon(H). :- not &k{ ~ noreversal}.
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 three 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 world view of the above ELP (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 (each world view consists of precisely one answer set). 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 our world views to contain multiple answer sets: one for each state in S.
The encoding starts o much like the previous one: chosen(A) :- action(action(A)), not &k{-chosen(A)}. -chosen(A) :- action(action(A)), not &k{ chosen(A)}. :- chosen(A), chosen(B), A!=B. onechosen :- chosen(A). :- not onechosen. holds(V, Val, 0) :chosen(A), precondition(action(A), variable(V), value(variable(V), Val)).
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 open up several answer sets, one for each state. This is done by guessing a truth value for each fact at time step 0. holds(V,Val,0) | -holds(V,Val,0) :
variable(variable(V)), contains(variable(V),value(variable(V),Val)). oneholds(V,0) :- holds(V,Val,0). :- variable(variable(V)), not oneholds(V,0). :- holds(V,Val,0), holds(V,Val1,0), Val != Val1.
Next, we again guess and execute a plan, keeping track of whether the actions were able to be applied at each particular time step: ccurs(A, 1) :- chosen(A). occurs(A, T) :- action(action(A)),time(T), T > 1, not &k{-occurs(A, T)}. -occurs(A, T) :- action(action(A)),time(T), T > 1, not &k{occurs(A, T)}. :- occurs(A,T), occurs(B,T), A!=B. oneoccurs(T) :- occurs(A,T), time(T), T > 0. :- time(T), T>0, not oneoccurs(T). inapplicable :occurs(A, T), precondition(action(A), variable(V), value(variable(V), Val)), not holds(V, Val, T - 1). :- not &k{ ~ inapplicable}. caused(V, Val, T) :occurs(A, T), postcondition(action(A), E, variable(V), value(variable(V), Val)). 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).
Again, the rules above chose a candidate reverse plan , starting with the action-to-be-checked a, as before. Furthermore, we check applicability: should be applicable (i.e. at each time step, the relevant action must have been applied, encoded by the third block of rules above), and furthermore, only modi ed facts (i.e. those a ected by an action) can change their truth values from time step to time step. Finally, we again need to make sure that the guessed plan actually returns us to the original state at time step 0. noreversal :- holds(V, Val, 0), not holds(V, Val, H+1), horizon(H). noreversal :- holds(V, Val, H+1), not holds(V, Val, 0), horizon(H). :- not &k{ ~ noreversal}.
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: :- < check guessed state against set S >
This rule should re 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 S2. 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 2 The full encoding can be found at https://sea le.aau.at/d/373cd25718dc4377afec/.
The action del-all has a universal uniform reverse plan h add-f0, . . . , add-fi i. We have generated instances from i = 1 to i = 6 and from i = 10 to i = 200 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 general encoding.
We have used plasp 3.1.1 (https://potassco.org/labs/plasp/) and eclingo 0.2.0 (https://github.com/potassco/eclingo) [?] on a computer with a 2.3 GHz AMD EPYC 7601 CPU with 32 cores and 500 GB RAM running CentOS 8. We have set a timeout of 10 minutes and a memory limit of 16GB (which was never exceeded).
600 The results for problem (a) are plotted in Figure 1. The general encoding exceeded the time limit already at the problem with six facts, while the simple encoding could solve all problems with up to 120 facts within the time limit. The memory consumption increased with i for both encodings, proportional to the computation time.
The results for problem (b) are plotted in Figure 2. Interestingly, compared to (a), both the general and the simple encoding performed noticably faster. While the general encoding still hit the time limit for six facts, the simple encoding was able to solve all the instances up to our maximum of i = 200, but at the expense of increasing memory usage.
In total, the general encoding scales worse, as expected, since the ELP solver
needs to evaluate all answer sets inside each possible world view. However, for
the simple encoding, especially the task of testing for non-reversibility performed
surprisingly well. From all of our results, however, we can see that ELP solving
still severly trails, in terms of performance, encodings for plain ASP [
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 ELP community, it will not come as
a surprise that the general encoding was performing much more poorly than
the simple encoding, since it needs to deal with a large set of answer sets in
each world view. For such encodings to become practical, ELP solvers need to
be further optimized. However, the simple encoding showed some promise, but
needed an increasing amount of memory with increasing problem sizes, compared
to a plain ASP encoding [
For future work, we intend to optimize our encodings further, and test them
with other established ELP solvers. 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. [