Formal Semantics and Formally Verified Validation for Temporal Planning
Mohammad Abdulaziz, Lukas Koller
2022Year
4Citations
1Top-tier citations
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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext f4bc5bf8-6cef-4132-af10-22934cfe741fCited by top-tier papers1
Ask how each one uses itBuilds on1
Related papers
- Deciding Unsolvability in Temporal Planning under Action Non-Self-OverlappingStefan Panjkovic, Andrea Micheli, Alessandro CimattiAAAI 2022 · 1 citation
- Temporal Numeric Planning with PatternsMatteo Cardellini, Enrico GiunchigliaAAAI 2025 · 4 citations
- Efficient Formally Verified Maximal End Component Decomposition for MDPsArnd Hartmanns, Bram Kohlen, Peter LammichFM 2024 · 2 citations
- Abstract Action Scheduling for Optimal Temporal Planning via OMTStefan Panjkovic, Andrea MicheliAAAI 2024 · 3 citations
- Verifying Secure Speculation in Isabelle/HOLMatt Griffin, Brijesh DongolFM 2021 · 6 citations
