A Verified Compositional Algorithm for AI Planning
From MaRDI portal
Publication:5875407
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
Uses Software
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