# Formal Semantics and Formally Verified Validation for Temporal Planning

arXiv: https://arxiv.org/abs/2203.13604 · HTML: https://mlsanity.com/paper/2203.13604/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 0 of its 34 references that are in the map.
- First posted on arXiv 25 Mar 2022.

## Built on by (most cited first, 3 of 3)

- [HDDL 2.1: Towards Defining a Formalism and a Semantics for Temporal HTN Planning](https://mlsanity.com/paper/2306.07353/) (2023)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [On Guiding Search in HTN Temporal Planning with non Temporal Heuristics](https://mlsanity.com/paper/2306.07638/) (2023)

## Abstract (arXiv)

We present a simple and concise semantics for temporal planning. Our semantics are developed and formalised in the logic of the interactive theorem prover Isabelle/HOL. We derive from those semantics a validation algorithm for temporal planning and show, using a formal proof in Isabelle/HOL, that this validation algorithm implements our semantics. We experimentally evaluate our verified validation algorithm and show that it is practical.