FormPlan

PDDL Plan Validator

Formally verified validators for planning problems and solutions specified in PDDL (supporting the STRIPS planning fragment) [github]

Papers:

M. Abdulaziz and P. Lammich, ‘A Formally Verified Validator for Classical Planning Problems and Solutions’, in the 30th International Conference on Tools with Artificial Intelligence (ICTAI), 2018. doi: 10.1609/aaai.v36i9.21197.

M. Abdulaziz and L. Koller, ‘Formal semantics and formally verified validation for temporal planning.’, in the 36th AAAI Conference on Artificial Intelligence (AAAI), 2022. doi: 10.1609/aaai.v36i9.21197.

SAS+ Plan Validator

Formally verified validators for planning problems and solutions specified in Fast-Downward’s translator format [Download]

SAT-Based Planner

A formally verified SAT-based planner for planning problems and solutions specified in Fast-Downward’s translator format [github]

Papers:

M. Abdulaziz and F. Kurz, ‘Formally verified SAT-Based AI planning’, in the 37th AAAI Conference on Artificial Intelligence (AAAI), 2023. doi: 10.1609/aaai.v37i12.26714.

Tabular MDP Solvers

Formally verfied implementations of (Gauss-Seidel) value iteration and (modified) policy iteration on MDPs [github]

Papers:

M. Schäffeler and M. Abdulaziz, ‘Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes’, in the 37th AAAI Conference on Artificial Intelligence (AAAI), 2023. doi: 10.1609/aaai.v37i12.26759.

Factored MDP Solver

Formally verfied approximate policy iteration on factored MDPs

M. Schäffeler and M. Abdulaziz, ‘Formally Verified Approximate Policy Iteration’. arXiv, Jun. 11, 2024. doi: 10.48550/arXiv.2406.07340.

Contributors

Mohammad Abdulaziz, Maximilian Schäffeler, Lukas Koller, Friedrich Kurz, Peter Lammich