A Verified Compositional Algorithm for AI Planning

DOI10.4230/LIPIcs.ITP.2019.4OpenAlexW2977387023MaRDI QIDQ5875407

Michael Norrish, Charles Gretton, Mohammad Abdulaziz

Publication date: 3 February 2023

Full work available at URL: https://doi.org/10.4230/LIPIcs.ITP.2019.4

zbMATH Keywords

transition systemsAI planningcompositional algorithmsalgorithm verification

Mathematics Subject Classification ID

Uses Software

• Coq
• HOL
• nuXmv
• Myhill-Nerode

Cites Work

• Unnamed Item
• Formal verification of an executable LTL model checker with partial order reduction
• Automatically generating abstractions for planning
• Stochastic dynamic programming with factored representations
• Formally verified algorithms for upper-bounding state space diameters
• Robot task planning and explanation in open and uncertain worlds
• STRIPS: A new approach to the application of theorem proving to problem solving
• A Constructive Theory of Regular Languages in Coq
• Verified Over-Approximation of the Diameter of Propositionally Factored Transition Systems
• A Formalisation of the Myhill-Nerode Theorem Based on Regular Expressions (Proof Pearl)
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• A Formalisation of Finite Automata Using Hereditarily Finite Sets
• A Brief Overview of HOL4

This page was built for publication: A Verified Compositional Algorithm for AI Planning