Formal Semantics and Formally Verified Validation for Temporal Planning

2022/03/25 by Mohammad Abdulaziz, Abdulaziz, Mohammad, Lukas Koller +1
Computer Science · #AI-based Problem Solving and Planning #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2203.13604

openalex publication_date 2022/03/25 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Related

• Formally Verified Certification of Unsolvability of Temporal Planning Problems
• Timeline-based Planning and Execution with Uncertainty: Theory, Modeling Methodologies and Practice
• Timeline-based planning: Expressiveness and Complexity
• Temporal Planning with Intermediate Conditions and Effects
• From TimeML to TPL