Most research in planning focuses on generating a plan to achieve a desired set of goals. However, a goal specification can also be used to encode a property that should never hold, allowing a planner to identify a trace that would reach a flawed state. In such cases, the objective may shift to modifying the planning task to ensure that the flawed state is never reached, in other words, to make the planning task unsolvable. In this paper we introduce planning task shielding: the problem of detecting and repairing flaws in planning tasks. We propose three different approaches to solve these tasks, each aiming to minimize the number of modifications to the original actions that render the planning task unsolvable.
Figures & tables
Listing 1 Approval workflow described as PDDL actions.
Figure 1: aga succeeds on all instances with faster runtime, \textscallmin100 and \textscdfs15 follow.
Figure 2: Experimental results on the 90 benchmark problems. Each column denotes one of the 10 problems for each domain.
Figure 3: Execution time split into the time to compute the set of plans with symk (blue) and the time to compute the minimum number of modifications with the MILP (orange).
Figure 4: Number of modifications per benchmark and method. While aga successfully renders unsolvable all benchmarks, the average number of modifications is higher.
Figure 5: Mean execution time per benchmark and method. aga is consistently faster, while mcts shows the higher variance across the search-based methods.
Config
SYNTH4
SYNTH8
SYNTH16
T
C
S
∣M∣
Time
T
C
S
∣M∣
Time
T
C
S
∣M∣
Time
allmin 10
10
10
10
6.0±0.0
1.1±0.3
10
10
0
-
-
10
10
0
-
-
allmin 100
10
10
10
6.0±0.0
1.1±0.1
10
10
10
11.0±0.0
5.6±0.7
10
10
10
21.0±0.0
69.6±10.1
allmin
10
10
10
6.0±0.0
1.1±0.1
10
10
10
11.0±0.0
5.6±0.8
10
10
10
21.0±0.0
68.6±8.7
aga
10
10
10
8.0±0.0
0.6±0.2
10
10
10
16.0±0.0
1.1±0.2
10
10
10
32.0±0.0
2.7±0.5
bfs
10
10
10
6.0±0.0
134.2±23.7
10
0
0
-
-
10
0
0
-
-
Table 1: Outcome breakdown and modification counts per method and benchmark. T= total problems; C=completed, S=success. T-C=out of memory or timeout, C-S=modifications do not render the task unsolvable.
Plans often change due to changes in the situation or our understanding of the situation. Sometimes, a feasible plan may not even exist, and identifying such infeasibilities is useful to determine when requirements need adjustment. Common planning approaches focus on efficient one-shot planning in feasible cases rather than updating domains or detecting infeasibility. We propose a Petri net reachability relaxation to enable robust invariant synthesis, efficient goal-unreachability detection, and helpful infeasibility explanations. We further leverage incremental constraint solvers to support goal and constraint updates. Empirically, compared to baselines, our system produces a comparable number of invariants, detects up to 2 times more infeasibilities, performs competitively in one-shot planning, and outperforms in sequential plan updates in the tested domains.
Nguyen Cong Nhat Le, John G. Rogers, Claire N. Bonial +1
Colorado School of Mines, Golden CO 80401, USA · DEVCOM Army Research Laboratory, Adelphi, MD, USA
Automated planning traditionally assumes that all aspects of a planning task (initial state, goals, and available actions) are fully specified in advance, an approach well-suited to domains with fixed rules and deterministic execution. However, real-world planning often requires flexibility, allowing for deviations from the original task parameters in response to unforeseen circumstances or to improve outcomes. This paper surveys existing works on counterfactual reasoning in automated planning, categorizing them by what elements are changed, when the reasoning is triggered, and why and how these changes are made. We conclude by discussing key findings and outlining open research questions to guide future work in this area.
Frontier large language models (LLMs) can generate heuristic functions that guide search to achieve state-of-the-art performance in satisficing planning, where any plan is acceptable. However, these heuristics are not guaranteed to be admissible and can lead to suboptimal plans. We introduce LeanPlan, the first planning system that finds optimal plans with LLM-generated heuristics whose admissibility is machine-checked. Given a domain description and training tasks, an agentic loop uses planner feedback to iteratively improve a reusable domain-specific heuristic, its admissibility proof and the required domain assumptions. LeanPlan implements the heuristic, its proof and an efficient planner with machine-checked grounding and search in Lean 4. We evaluate LeanPlan on ten domains from the International Planning Competition and three new domains, using test tasks with up to 57 times as many objects as the training tasks. With GPT-5.6 Sol in the agentic loop, we successfully generate heuristics and admissibility proofs for all these domains. With the resulting heuristics, LeanPlan usually expands fewer states than the state-of-the-art Scorpion planner and solves more tasks overall.
André G. Pereira, Augusto B. Corrêa, Felipe Meneguzzi +1
Federal University of Rio Grande do Sul Brazil · University of Oxford United Kingdom · University of Aberdeen United Kingdom +1