A Verified Compositional Algorithm for AI Planning

DOI10.4230/LIPICS.ITP.2019.4MaRDI QIDQ5875407zbMATH OpenOpenAlexFDO

Authors Mohammad Abdulaziz, Charles Gretton, Michael Norrish

Publication date 3 February 2023

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

zbMATH Keywords

AI planningalgorithm verificationcompositional algorithmstransition systems

Mathematics Subject Classification ID

Recommendations

• Formally verified algorithms for upper-bounding state space diameters
• The classical AI planning problems in the mirror of Horn linear logic: semantics, expressibility, complexity
• A temporal logic programming approach to planning
• Proof systems for planning under 0-approximation semantics
• A new representation and associated algorithms for generalized planning

Cites work

• A Brief Overview of HOL4
• A constructive theory of regular languages in Coq
• A formalisation of finite automata using hereditarily finite sets
• A formalisation of the Myhill-Nerode theorem based on regular expressions (proof pearl)
• Automatically generating abstractions for planning
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Formal verification of an executable LTL model checker with partial order reduction
• Formally verified algorithms for upper-bounding state space diameters
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• Robot task planning and explanation in open and uncertain worlds
• Stochastic dynamic programming with factored representations
• STRIPS: A new approach to the application of theorem proving to problem solving
• Verified over-approximation of the diameter of propositionally factored transition systems

Describes a project that uses

Uses Software

• Myhill-Nerode
• Coq
• nuXmv
• HOL

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875407)