Formal Semantics and Formally Verified Validation for Temporal Planning

Authors

  • Mohammad Abdulaziz Technische Universität München, Germany King's College London, United Kingdom
  • Lukas Koller Technische Universität München, Germany

DOI:

https://doi.org/10.1609/aaai.v36i9.21197

Keywords:

Planning, Routing, And Scheduling (PRS), Knowledge Representation And Reasoning (KRR)

Abstract

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.
AAAI-22 Proceedings Cover

Downloads

Published

2022-06-28

How to Cite

Abdulaziz, M., & Koller, L. (2022). Formal Semantics and Formally Verified Validation for Temporal Planning. Proceedings of the AAAI Conference on Artificial Intelligence, 36(9), 9635-9643. https://doi.org/10.1609/aaai.v36i9.21197

Issue

Vol. 36 No. 9: AAAI-22 Technical Tracks 9

Section

AAAI Technical Track on Planning, Routing, and Scheduling