But It Was True When I Checked: Compiling SHOP-Style Method Preconditions into Partially-Ordered HTN Planning
Harrison Oates
cs.AI
Nov 8, 2026 · v1
TL;DR
The definitions, key lemmas and main correctness theorem of the HTN precondition compilation are formalised in Lean 4 with Mathlib, with a public repository.
Abstract
Method preconditions specify when a method may be applied in hierarchical task network (HTN) planning, but their meaning differs under two established semantics. The SHOP planners, like the classical HTN formalism of Erol, Hendler and Nau, require the precondition to hold immediately before the method's first action. HDDL, the input language of the International Planning Competition's HTN track, instead introduces an auxiliary action to check it; under partial order, unrelated actions may invalidate the precondition before the method starts. HDDL's designers adopted this weaker semantics because the first-action reading could not easily be compiled. Subsequent work has repeatedly identified its compilation under partial order as an open question, with existing transformations limited to total order. We give a compilation of the first-action semantics into standard partially ordered HTN planning without method preconditions using only two additional facts, thereby resolving a longstanding question in the HTN planning community.
Problem
In HTN planning, SHOP planners require method preconditions to hold immediately before the method's first action. HDDL instead checks them with an auxiliary action, which under partial order lets unrelated actions invalidate the precondition beforehand. Compiling the first-action semantics into partially ordered HTN planning had remained an open question.
Approach
Each method gets a check action ordered before its subtasks, plus variants that mark which minimal subtask produces the method's first action. Compound tasks get normal and 'first' copies. Two extra facts (free and lock) form a lock window, so no unrelated action can execute between a check and the release action of its marked chain. Soundness and completeness are proved, and the definitions, lemmas and main theorem are formalised in Lean 4 with Mathlib.
Results
The compilation is polynomial: quadratic size in general and linear for totally ordered methods. It preserves total order, acyclicity, tail recursion and regularity, which makes HDDL planners and complexity results applicable to SHOP-style semantics. The correctness results are machine-checked in Lean.
