Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formally Verified Certification of Unsolvability of Temporal Planning Problems

David Wang, Mohammad Abdulaziz

TL;DR

This work addresses certifying the unsolvability of temporal planning by encoding planning problems as a network of timed automata and validating results with a formally verified certificate checker embedded in Isabelle/HOL. The encoding introduces per-action clocks, invariants, and mutex-like constraints to translate temporal planning constructs into a TA network, enabling a certificate-based verification pathway via TA model checking. A central correctness result shows that a valid plan implies the TA encoding has a reachable accepting configuration, expressed as $EF(loc(A_M) = goal_M)$, thereby providing a sound basis for unsolvability certificates and a foundation for executable certification pipelines. The study advances trustworthy certification for temporal planning and outlines concrete future work toward executable tooling, grounding, and semantic equivalence results.

Abstract

We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.

Formally Verified Certification of Unsolvability of Temporal Planning Problems

TL;DR

This work addresses certifying the unsolvability of temporal planning by encoding planning problems as a network of timed automata and validating results with a formally verified certificate checker embedded in Isabelle/HOL. The encoding introduces per-action clocks, invariants, and mutex-like constraints to translate temporal planning constructs into a TA network, enabling a certificate-based verification pathway via TA model checking. A central correctness result shows that a valid plan implies the TA encoding has a reachable accepting configuration, expressed as , thereby providing a sound basis for unsolvability certificates and a foundation for executable certification pipelines. The study advances trustworthy certification for temporal planning and outlines concrete future work toward executable tooling, grounding, and semantic equivalence results.

Abstract

We present an approach to unsolvability certification of temporal planning. Our approach is based on encoding the planning problem into a network of timed automata, and then using an efficient model checker on the network followed by a certificate checker to certify the output of the model checker. Our approach prioritises trustworthiness of the certification: we formally verify our implementation of the encoding to timed automata using the theorem prover Isabelle/HOL and we use an existing certificate checker (also formally verified in Isabelle/HOL) to certify the model checking result.

Paper Structure

This paper contains 20 sections, 4 theorems, 6 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Background and Definitions
  3. Temporal Planning
  4. Timed Automata
  5. Isabelle and Higher-Order Logic
  6. Encoding
  7. Correctness
  8. Discussion
  9. Related Work
  10. Planning and Timed Automata
  11. Certification
  12. Planning as Model Checking
  13. Size
  14. Future Work
  15. Detailed proofs
  16. ...and 5 more sections

Key Result

Lemma 1

Given a configuration $\mathit{encodes\_after}(\langle {L}{_I}, {v}{_I}, {c}{_I} \rangle,0,\langle {L}{_0}, {v}{_0}, {c}{_0} \rangle)$, it is possible to prove the existence of a configuration $\langle {L}{_k}, {v}{_k}, {c}{_k} \rangle$ and a run $[\langle {L}{_0}, {v}{_0}, {c}{_0} \rangle, \dots, \

Figures (6)

  • Figure 1: The verified planner architecture proposed by Abdulaziz and Kurz, combining verified (solid) and unverified (dotted) modules.
  • Figure 2: Interfering actions in \ref{['ex:robots_blocks_doors']}. Two robots picking up the same block.
  • Figure 3: Parts of candidate plans for \ref{['ex:robots_blocks_doors']}.
  • Figure 4: A timed automaton with named locations. The action transition checks the condition $(y = 2)? \land \top$ and the guard $\{x \ge 1?\}$, applies the update $\{ y := y - 1 \}$, and resets $\{ x \}$.
  • Figure 5: An automaton for an action $\mathcal{A}_a$ from temporalPlanningRefinementMC and the main automaton $\mathcal{A}_M$. The network of timed automata to encode a planning problem contains a copy of $\mathcal{A}_a$ for each action $\underline{a}$ in the problem.
  • ...and 1 more figures

Theorems & Definitions (47)

  • Definition 1: Snap action
  • Definition 2: Durative action
  • Example 1: Rooms, Robots, Doors, Blocks
  • Definition 3: Propositional state
  • Definition 4: Temporal planning problem
  • Example 1: Rooms, Robots, Doors, Blocks (continued)
  • Definition 5: Mutex Snap Actions
  • Definition 6: Plan
  • Definition 7: Induced parallel plan
  • Definition 8: Happening time point sequence
  • ...and 37 more