Formal Semantics and Formally Verified Validation for Temporal Planning
This work addresses the need for rigorous verification in temporal planning, which is incremental as it builds on existing formal methods.
The authors tackled the problem of providing a formal semantics for temporal planning and developed a formally verified validation algorithm using Isabelle/HOL, showing through experiments that it is practical.
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.