TLDR
- Undo means exact state restoration. A reverse plan must be applicable after the target action and return the resulting state to its original set of true facts.
- Uniform means one plan for every state. The reverse sequence cannot be chosen separately after seeing which relevant starting state supplied the action.
- The state set changes the question. Reversibility may range over every state, states satisfying a formula, or states reachable in one planning task.
- ASP guesses and filters candidates. A bounded reverse sequence is chosen, executed with inertia and rejected when preconditions or final-state equality fail.
- ELP states the universal layer directly. Multiple answer sets inside one world view represent starting states, trading a clearer quantifier structure for weaker experimental performance in the tested solvers.
A reversible step carries its own route out
Planning usually asks for a sequence from an initial state to a goal. Action reversibility asks a different question: after applying one action, can some further sequence restore the state from which it was taken?
The distinction matters before a goal is known. An irreversible action may enter a dead end from which a desired state becomes unreachable. Early recognition can guide search away from traps. In online planning, a reversible action can be comparatively safe because the agent has a certified recovery sequence. In non-deterministic planning, reasoning about whether each possible effect can be reversed can support strong or cyclic recovery policies.
Reversibility can also expose redundancy after a plan is found. If one action’s effects are later undone, the intervening fragment may sometimes be removable, shortening the plan. This is not automatic: other actions may depend on transient effects, and inverse pairs are only a special case. The paper’s definition gives a precise object that optimisation rules can reference.
The authors build on a broader framework developed with Chrpa and Fišer. It distinguishes a set of states in which reversal is required and whether one fixed reverse plan must serve them all. This prevents “reversible” from hiding crucial quantifiers. An action might be undoable from one state but not another, or undoable everywhere only when the recovery is allowed to depend on the starting state.
The paper’s contribution is computational. It encodes several bounded uniform-reversibility problems for the STRIPS fragment of PDDL. A translator called plasp turns planning-domain descriptions into answer-set facts. ASP and epistemic logic programmes then generate actions and reverse-plan candidates, simulate them, and eliminate failures. The comparison examines expressiveness, extensibility and preliminary runtime and memory behaviour.
Worked example 1 · opening versus breaking
Opening an unlocked door may be reversed by closing it. Breaking a sealed door can produce the same immediate accessibility but lacks a route back to the original intact state. Goal progress alone does not reveal the difference; exact restoration does.
Causal probe 1 · why is returning to some safe state insufficient?
That would define recoverability, not reversal. Exact equality protects facts unrelated to the current goal and lets the certificate transfer across tasks. It is deliberately stronger than merely reaching another acceptable condition.
Preconditions gate an action; add and delete lists rewrite truth
The paper restricts itself to propositional STRIPS. That narrow language makes every transition finite and explicit enough to encode in logic programmes and to exhaust in the companion laboratory.
Let F be a finite set of facts. A state s is a subset of F containing exactly the facts treated as true. An action a is a triple: pre(a), add(a) and del(a). Preconditions must hold before execution. Add effects become true; delete effects become false. Actions are assumed well formed: no fact is both added and deleted, and no added fact is already required as a positive precondition.
The action is applicable when pre(a) is a subset of s. Its deterministic successor is a[s]=(s\del(a))∪add(a). Every unmentioned fact persists through set difference and union. A sequence is applicable only if every member’s preconditions hold in the state produced by its predecessors. Applying the sequence returns its last state.
A planning task combines F, an action set A, an initial state s₀ and a goal set G. Any state containing all goal facts is a goal state. Reachability is relative to s₀ and A: a state is reachable when some applicable sequence produces it. The paper uses the full reachable set RΠ to define one task-specific variant of reversibility.
Positive-only preconditions deserve attention. A missing fact is treated as false in the state, but an action cannot directly require that absence in elementary STRIPS. Richer PDDL fragments support more forms, but the encodings here deliberately stay within STRIPS. This scope keeps the action application equation and plasp translation clean.
Worked example 2 · delete everything, then rebuild
In the appendix domain, del-all requires f0 and f1 and deletes both. add-f0 restores f0 without a precondition. add-f1 requires f0 and restores f1. Starting from {f0,f1}, the sequence del-all, add-f0, add-f1 returns exactly to {f0,f1}.
Causal probe 2 · why must reverse-plan applicability be checked?
A sequence can have the right final add and delete sets on paper yet fail midway. Here add-f1 cannot precede add-f0 after del-all because its f0 precondition is false. A certificate must be executable, not merely algebraically suggestive.
One reverse plan must work after every applicable start
Uniform reversibility is not “for every state, some recovery exists”. It is “there exists one recovery sequence such that, for every relevant state where the action applies, that same sequence is applicable and restores the state”.
Definition 1 begins with a fact set F, action set A, relevant state set S and target action a. The action is uniformly S-reversible when some fixed sequence π from A works for each s in S where a is applicable. Two tests are required on every such state: π must be applicable in a[s], and π[a[s]]=s.
The restriction to states where a applies avoids demanding a result for an undefined transition. It does not weaken the restoration requirement. If the target action is applicable in ten relevant states, the reverse sequence must survive ten executions and reproduce ten potentially different originals without observing which one it received.
Moving the existential quantifier inside would permit a separate reverse plan πs for each state. That is non-uniform reversibility. It may be practically useful when the agent can observe the state and choose a recovery, but it is a different certificate. Uniformity supplies a context-independent macro: after a, execute π.
Reverse-plan length is externally bounded by a horizon. The encodings described return plans of exactly that length. Iterative deepening can search shorter lengths when the answer is not known. Complexity statements in the paper assume polynomially bounded reverse plans: universal uniform reversibility is NP-complete, while formula-restricted uniform reversibility reaches the second level of the polynomial hierarchy under the cited framework.
Worked example 3 · state-specific recovery is not uniform
Suppose an action forces a lamp on whether it began on or off. If it began off, switch-off restores it; if it began on, doing nothing restores it. A state-aware agent has a recovery for either case, but there is no single blind sequence satisfying both unless another action records or reconstructs the lost initial value.
Causal probe 3 · why is exact equality hard after information-destroying effects?
If two distinct starting states collapse to the same successor, a fixed deterministic reverse sequence sees identical input in both cases and produces one output. It cannot equal two different originals. Uniform reversibility therefore depends on whether the target action erases distinctions relevant to S.
Universal, formula-restricted and task-reachable reversal
The same action and sequence can pass or fail depending on S. The paper therefore names several state sets rather than treating reversibility as a property of action syntax alone.
Universal uniform reversibility sets S to the full powerset 2F. The reverse plan must work from every conceivable state in which the action’s preconditions hold. It is independent of a concrete initial state or goal and transfers across all planning tasks sharing the domain. This is the strongest of the variants considered.
Uniform φ-reversibility lets a propositional formula describe S. Domain constraints can exclude impossible combinations. If a robot can never simultaneously hold two bulky objects, the formula can omit those valuations. The reverse plan is still one sequence, but it need only serve models of φ.
Uniform reversibility in a planning task sets S to RΠ, the states reachable from that task’s initial state. This can be weaker still. A troublesome valuation may be expressible and satisfy static constraints yet remain unreachable under the action dynamics. Task-relative certification can accept a plan rejected by universal checking.
The implication flows from stronger state coverage to weaker: a universally uniform reverse plan also works in every subset S, including formula models and reachable states. The reverse implication need not hold. The computational encoding must therefore know whether it can exploit a universal shortcut or must represent a compact family of states and check them all.
Worked example 4 · an impossible valuation
An action may be unrecoverable only when both grippers are occupied. If the robot’s invariant forbids that state, universal checking rejects while φ-reversibility under the invariant may accept. The difference is not a solver error; it is a different S.
Causal probe 4 · why prefer the stronger notion?
A universal certificate is reusable before initial state and goal are fixed. That portability costs conservatism: it must defend against syntactically possible states that a particular task can never reach.
plasp turns action syntax into a database for solving
The encodings do not parse PDDL themselves. They consume plasp’s translation of variables, actions, preconditions and unconditional postconditions into ASP facts and rules.
A STRIPS predicate becomes a Boolean variable. Each action receives an action fact. Positive preconditions become precondition records whose value is true. Add effects become postconditions assigning true; delete effects assign false. A contains predicate records the possible Boolean values. The resulting representation can be joined with generic ASP or ELP rules.
The appendix domain uses facts f0 and f1. del-all requires both and sets both false. add-f0 sets f0 true without a precondition. add-f1 requires f0 and sets f1 true. plasp emits a small relational description of this domain rather than a custom procedural simulator.
This separation matters for reuse. The same solver encoding can process different STRIPS domains because domain data and reversal logic occupy different layers. It also inherits plasp’s planning vocabulary and implementation, allowing the work to focus on quantifier modelling and candidate validation.
The scope is narrower than full PDDL. Conditional effects, negative preconditions, numeric fluents and non-deterministic effects are not addressed by the paper’s present encodings. The conclusion names lifted representations, non-determinism and exogenous events as future directions, not completed features.
Worked example 5 · one delete effect as data
The PDDL effect “not f0” for del-all becomes a postcondition record assigning the Boolean value false to variable f0. Generic transition rules later derive that f0 is caused false at the action’s time step.
Causal probe 5 · why translate rather than compile a bespoke checker?
A declarative domain database keeps the action model inspectable and lets alternative encodings share identical input. Performance and expressiveness differences can then be attributed more cleanly to ASP, ELP and the selected technique.
Guess an action, guess a plan, execute, reject failure
Universal uniform reversibility admits a key shortcut: it is sufficient to inspect facts appearing in the target action’s precondition. Any target or reverse action touching another fact prevents a universal reverse plan under the cited characterisation.
The encoding chooses exactly one target action. Its precondition facts define the initial valuation and the relevant set. The target occurs at time 1. One action is guessed for every later time up to the supplied horizon. The full occurrence sequence therefore contains the target followed by a reverse plan of exactly horizon steps.
Execution derives caused values from postconditions. A modified marker identifies variables affected at a step. Caused values become the new holdings; unmodified values persist by inertia. Constraints reject a candidate when a precondition is absent at the preceding step or when any selected action mentions a variable outside the relevant set.
Two directional equality checks compare time 0 with horizon+1. A value present initially must appear finally, and a final value must have been present initially. Both directions matter because restoration means set equality, not containment. The ELP encoding wraps failure in an epistemic check; the simple ASP version replaces modal guesses with ordinary choice rules and expresses equality with constraints.
Theorem 4 states that the ELP encoding produces exactly one world view for each universally uniformly reversible action and reverse plan of the fixed length. Each such world view contains precisely one answer set because the universal shortcut reduces the state check to one constructed valuation. Theorem 5 gives the parallel one-answer-set-per-plan result for ASP.
Worked example 6 · the only length-two answer
For the appendix domain and horizon 2, del-all followed by add-f0 and add-f1 succeeds. Repeating add-f0 leaves f1 false. Reversing the restore order makes add-f1 inapplicable. The unique valid occurrence sequence therefore identifies del-all and its two-step reverse plan.
Causal probe 6 · why compare final to initial in both directions?
Checking only that every initial truth is restored would tolerate new facts accidentally left true. Checking only that every final truth was initial would tolerate lost facts. Equality requires both no omissions and no additions.
Let answer sets stand for states inside one world view
Formula-restricted and arbitrary S-reversibility cannot use the simple relevant-precondition shortcut. The encoding must expose every starting state while holding the target and reverse plan fixed across them.
The general ELP encoding uses epistemic choices to select one target and one occurrence at each time. It then guesses truth values for every fact at time 0, creating multiple answer sets. A rule can restrict those guesses to the selected state set S, for example by checking that the valuation models φ.
Within each answer set, ordinary rules execute the common plan. An inapplicable atom marks a failed precondition. A noreversal atom marks disagreement between the initial and final states. Epistemic constraints demand that neither failure occurs in any answer set of the world view. The world view therefore represents one existential plan surrounding a universal family of state executions.
This is close to the mathematical statement: choose π once; verify every s. Modal operators make the division visible. In the universal special case, adding a state-membership filter is unnecessary. For φ-reversibility, the same structure accepts a rule that discards initial guesses outside the models of φ.
Plain ASP lacks a direct world-view layer, so the general encoding uses saturation to simulate universal quantification. It guesses a starting valuation, derives whether the plan is applicable and restores the state, then inflates a successful candidate with all fact–value–time combinations. Stable-model minimality eliminates an inflated model if any counterexample interpretation survives. The technique is powerful but less transparent to a reader.
Worked example 7 · four states in one world view
With f0 and f1, the general ELP encoding can contain answer sets for {}, {f0}, {f1} and {f0,f1}. The chosen action and reverse sequence are shared epistemically. A failure in even one applicable branch makes the world-view constraint reject the plan.
Causal probe 7 · why can ordinary answer-set guessing be insufficient?
One answer set naturally chooses one state and one plan, expressing ∃s∃π. Uniform checking needs one π held constant while all s are inspected. ELP world views provide that outer grouping directly; ASP saturation reconstructs the grouping indirectly.
Uniform reversal laboratory
The laboratory exhaustively evaluates the appendix’s two-fact domain. Choose a target action and exact reverse-plan horizon; every action sequence of that length is tested against every state in which the target applies.
Green candidates are uniformly valid. A rejected sequence reports the first starting state in which it becomes inapplicable or fails exact restoration.
The executor implements the paper’s transition equation directly. A state is a set of f0 and f1. An action fires only when all preconditions are present, then deletes its delete set and adds its add set. Candidate sequences are Cartesian products of the three domain actions at the selected horizon.
For each starting state where the target applies, the engine first applies the target. It then tries the same candidate sequence. Any failed precondition rejects the candidate. If execution finishes, the final state must equal the original in both directions. The first witness of failure is displayed so that non-reversibility is explanatory rather than a bare “no”.
At horizon 2, del-all has exactly the appendix plan: add-f0 followed by add-f1. The reverse order fails because f0 is required before add-f1. Two add-f0 actions fail to restore f1. At horizon 3, longer certificates can appear through redundant actions, illustrating why the paper fixes exact length and suggests iterative deepening for shortest plans.
The laboratory evaluates the definition by brute force rather than reproducing ASP or ELP solver internals. That makes it an independent oracle for this finite domain. It confirms the same valid histories that a correct encoding should represent as answer sets or world views.
Worked example 8 · one counterexample defeats uniformity
Select add-f0. It applies in all four states. From a state where f0 was false, a reverse must remove f0; from one where f0 was already true, it must preserve f0. Because both inputs become identical after add-f0 when f1 agrees, no fixed deterministic sequence can restore both.
Causal probe 8 · why display the first failing state?
Uniformity is a universal claim, so one witness is a complete refutation of a candidate plan. Showing it exposes whether failure came from applicability or state inequality and mirrors the counterexample logic behind the general encodings.
The clearer general encoding pays for its quantifiers
The experiments are preliminary and synthetic. They compare four encodings on domains constructed to have one long reverse plan or no plan one step below the necessary horizon.
In rev-i, del-all requires and deletes f0 through fi. A chain of add actions restores the facts in order, with each later addition depending on its predecessor. The unique reverse plan has length equal to the number of facts. Instances range from small cases through up to 200 facts for the existence task; the non-existence series extends to 250 in the text.
The toolchain used plasp 3.1.1, eclingo 0.2.0 and clingo 5.4.0 on a 2.3 GHz AMD EPYC 7601 machine running CentOS 8. Each run had a twenty-minute timeout and sixteen-gigabyte memory limit, which was not exceeded. Runtime and memory are plotted rather than reduced to one aggregate score.
For finding the unique plan, the general ELP encoding timed out already at seven facts. The simple ELP solved up to 150 facts within the limit. Both ASP variants outperformed their ELP counterparts, while the simple ELP performed better than the saturation-based general ASP. For proving no plan at the too-short horizon, all approaches did better; general ELP still timed out at seven facts and general ASP at fifty, while simple variants reached all tested instances up to 250.
The authors interpret the broad result cautiously. General encodings must evaluate all answer sets in a world view or perform saturation, so worse scaling is expected. ELP solvers were far less mature than optimised ASP systems. The experiment indicates an expressiveness–performance trade-off on one controlled family, not a universal solver ranking.
Worked example 9 · proving absence can be easier here
With horizon i−1, the chain lacks one slot needed to restore all i facts. Propagation can expose failure without finding and then excluding a full unique plan. The observed speed-up belongs to these structured instances and encodings; it is not a general theorem that non-existence is easy.
Causal probe 9 · why compare simple and general encodings separately?
The simple variants exploit a theorem specific to universal uniform reversal. The general variants retain an explicit all-states mechanism and can accept other S descriptions. Pooling them would confound language choice with a substantial change in modelling generality.
Four encodings, one narrow language, several open directions
The paper contributes executable logical encodings and correctness correspondences. It does not claim a complete treatment of reversibility across PDDL or superiority on representative planning benchmarks.
Two encodings are simple and specialised to universal uniform reversibility. Two are general enough to represent arbitrary compact state sets, with ELP world views or ASP saturation carrying universal quantification. Theorems connect simple encoding solutions to target-action and fixed-length reverse-plan pairs. The appendix walks all four encodings through the two-fact witness.
The experiments use artificial chain domains. They reveal scaling differences cleanly but do not capture rich action interactions, grounding structure or real benchmark distributions. The versions and hardware are reported, the timeout is explicit, and the authors call the experiments preliminary. Memory never crosses the imposed limit, though it grows with problem size.
Future work includes optimising ELP encodings, testing other ELP solvers and semantics, comparing declarative methods with procedural algorithms, and comparing existing RevPlan and undoability tools. The authors also identify lifted, more expressive and non-deterministic domains plus exogenous events. These are research directions, not implied support.
The larger lesson is a modelling one. ASP elegantly captures bounded existential search through choice and constraints. When one plan must satisfy a set of possible worlds, ELP exposes the two levels directly. Plain ASP can still express the condition, but its saturation idiom is less immediately aligned with the specification. Declarative closeness and operational efficiency need not coincide.
Evidence boundary
The primary is the 2021 arXiv version marked under consideration for TPLP. Placeholder submission dates in its header are publication-template artefacts and are not treated as historical facts. Claims here follow its definitions, theorems, appendix and reported setup without upgrading preliminary experiments into broad performance guarantees.
Worked example 10 · a longer plan is not automatically better
At horizon 3, the finite laboratory may find a reversal containing a redundant repeat. The encoding is correct for exact length, but a user seeking the shortest certificate must run increasing horizons or add optimisation. The paper mentions iterative deepening rather than claiming minimality by default.
Causal probe 10 · why retain a slower general encoding?
It can change S without redesigning the quantifier mechanism. A formula, reachability approximation or other compact state representation can be inserted as a filter. That modelling flexibility may outweigh runtime on problems where the simple universal theorem does not apply.
| Claim | Supported status | Boundary |
|---|---|---|
| Uniform reversal uses one sequence over every applicable state in S. | Definition 1. | Not state-dependent recovery. |
| Universal uniform reversal implies restricted variants. | Immediate relation after Definition 2. | The converse need not hold. |
| Simple ELP and ASP solutions correspond to fixed-length reverse plans. | Theorems 4 and 5. | Under STRIPS input and the stated encoding assumptions. |
| General ELP is more declaratively aligned with all-state checking. | Structural comparison by the authors. | Not a claim of faster execution. |
| ASP outperformed ELP overall in the experiments. | Reported synthetic benchmark result. | Version-, hardware- and instance-family-specific. |
Twelve retrieval hooks
Scholarly and publication gates
Review A · fidelity, teaching and evidential fairness
The companion was checked against all nineteen pages of arXiv:2108.05428v1, including the motivation, STRIPS and ELP preliminaries, Definitions 1–2, complexity qualifications, plasp facts, Observation (*), simple ELP rules, Theorem 4 and proof sketch, ASP replacements and Theorem 5, general ELP state enumeration, general ASP saturation, experimental domain, tool versions, hardware, limits, both qualitative result discussions, conclusions, future work and the detailed appendix. The title’s missing visual space in “ActionReversibility” and placeholder 2003 submission dates are treated as source-layout artefacts, not repeated as findings.
Fidelity review passed. Reversal is exact state equality, not goal recovery. Uniformity fixes one sequence outside the state quantifier. Universal, formula-restricted and task-reachable state sets remain distinct. The simple relevant-precondition shortcut is not attributed to arbitrary S. ELP world views and ASP answer sets are not conflated. Saturation is described at the level justified by the paper and appendix. Exact-horizon output is separated from shortest-plan search.
Teaching review passed. Ten worked examples and ten causal probes separate transition correctness, applicability, equality, quantifier order, state-set choice, translation, candidate search, universal counterexamples and benchmark interpretation. The laboratory independently enumerates all action sequences for the appendix domain and exposes a failing state for each rejected candidate. It does not pretend to benchmark clingo or eclingo in the browser.
Review B · language, accessibility, responsive layout and execution
The prose was reviewed for inflated novelty, causal overreach from experiments, vague authority, anthropomorphic solver language, retrospective terminology and AI-telltale scaffolding. British English is consistent. Each of ten figures has a unique title, description, caption and source note. Shapes, labels and order carry meaning beyond colour. Animation is non-essential and disabled by reduced-motion settings. The document has a skip link, ordered headings, labelled native controls, a live candidate report and explicit table headers.
Responsive review covers 1440, 768 and 390 pixels. The hero, five orientation cards, prose columns, all diagrams, three-control laboratory, memory studio and sequence navigation collapse without viewport overflow; the evidence table remains independently scrollable if necessary. Executable review enumerates all three targets at horizons zero through three. Three invariants must pass: each transition equals the STRIPS add/delete equation, every accepted plan is applicable in every tested branch, and every accepted endpoint equals its corresponding start. The appendix’s unique length-two witness is asserted as an exact regression test.
From the frame problem to verified return
Paper 0101 exposed the persistence burden in reasoning about action: a theory must say what changes and what remains. Paper 0102 adopts STRIPS, where inertia is built into the set update, and asks a sharper question about action histories. Can one bounded sequence restore every relevant starting state exactly after a target action? The emphasis moves from founding a calculus of change to deciding a quantified property of its transitions.
Paper 0103 turns to Eiter, Faber, Leone, Pfeifer and Polleres on knowledge-state planning. The next work makes information-producing actions and epistemic states central to planning semantics and complexity. This extends the present paper’s use of epistemic logic programming from quantifying over candidate worlds towards planning where what is known is itself part of the evolving state.
Sources and audit trail
- Faber, W., Morak, M., & Chrpa, L. (2021). “Determining Action Reversibility in STRIPS Using Answer Set and Epistemic Logic Programming.” arXiv:2108.05428. Primary source, including appendix and experimental setup.
- Morak, M., Chrpa, L., Faber, W., & Fišer, D. (2020). “On the Reversibility of Actions in Planning.” KR 2020, 652–661. General state-indexed framework and complexity results used by the primary paper.
- Eiter, T., Erdem, E., & Faber, W. (2008). “Undoing the Effects of Action Sequences.” Journal of Applied Logic, 6(3), 380–415. Earlier reverse-plan framework cited and compared by the primary paper.
- Daum, J., Torralba, Á., Hoffmann, J., Haslum, P., & Weber, I. (2016). “Practical Undoability Checking via Contingent Planning.” ICAPS, 106–114. Competing undoability approach named in the paper’s comparisons and future work.
- Dimopoulos, Y., Gebser, M., Lühne, P., Romero, J., & Schaub, T. (2019). “plasp 3: Towards Effective ASP Planning.” Theory and Practice of Logic Programming, 19(3), 477–504. arXiv:1812.04491. Translation substrate used by all four encodings.
- Gelfond, M. (1991). “Strong Introspection.” AAAI, 386–391. Epistemic-specification semantics selected by the primary paper.
- Cabalar, P., Fandinno, J., & Fariñas del Cerro, L. (2019). “Founded World Views with Autoepistemic Equilibrium Logic.” Later ELP-semantic context; the primary explicitly notes competing semantics for future testing.
What ships with Paper 0102
Title: When one sequence must undo every start: Faber, Morak and Chrpa’s reversible actions. Standfirst: A visual, executable reconstruction of STRIPS transitions, exact reversal, uniform quantifiers, state-set variants, plasp translation, ASP guessing, ELP world views, saturation and the reported scaling trade-off. Search terms: action reversibility, STRIPS, reverse plan, answer set programming, epistemic logic programming, plasp, saturation, uniform reversibility. Demonstration: an exhaustive oracle for the paper’s two-fact appendix domain across three actions and four exact horizons. Accessibility promise: ten titled and described SVG figures, reduced-motion support, labelled controls, keyboard operation and responsive layouts.