This is a formally verified validator for planning problems specified in a fragment of PDDL. The supported PDDL features are :strips, :typing, :negative-preconditions, :disjunctive-preconditions, :equality, :constants, and :action-costs.

We formalised the semantics of that PDDL fragment in the theorem prover Isabelle/HOL and proved that the validator code implements these formal semantics. This archive includes:

• the PDDL semantics, which is in the Isabelle/HOL theory file PDDL_STRIPS_Semantics.thy

• soundness theorems in Isabelle/HOL for the specified semantics, a la Lifschitz's in Lifschitz_Consistency.thy

• the validator's specification and the proof of its equivalence to the semantics, which is in the Isabelle/HOL theory file PDDL_STRIPS_Checker.thy

• the validator's implementation in SML, which is in the file isabelle/code/PDDL_STRIPS_Checker_Exported.sml

• a PDDL parser implementation in SML, which is in the directory PDDL_val/codeBase/planning/pddlParser/

This validator was described in the following paper:

Mohammad Abdulaziz and Peter Lammich. A Formally Verified Validator for Classical Planning Problems and Solutions. In International Conference on Tools in Artificial Intelligence (ICTAI), 2018.

Building the validator

Note: if you do not want to replay the verification, start at step 4 (the code generated by isabelle is included in this tar ball).

1. Download and install Isabelle/HOL

2. Install the Archive of Formal Proofs as indicated in this page. We require version = Isabelle-2022, which, at the time of writing, is the current version.

3. Generate sml code equivalent to the Isabelle theories by running

   cd afp_download_path/thys/AI_Planning_Languages_Semantics/

   isabelle_download_directory/bin/isabelle build -ecv -d . -o document=pdf -o document_output=. AI_Planning_Languages_Semantics

This will invoke Isabelle to check all proofs and re-generate the exported code, which is written to afp_download_path/thys/AI_Planning_Languages_Semantics/code/PDDL_STRIPS_Checker_Exported.ML

4. Download and install MLton compiler version >= 20210117.

5. Build the generated sml code together with the pddl parser by running the following commands from the top directory

   mlton -mlb-path-var 'AFP_PATH afp_download_path' -cc-opt -O3 -cc-opt -g0 pddl_validate_plan.mlb

Validating plans

Given a pddl domain description file (e.g. examples/ged3-itt_no_invariants.pddl), a pddl instance (e.g. examples/d-1-2.pddl), and a plan file (e.g. examples/plan), from the top directory run:

cd bin

./validate_pddl_plan.sh ../examples/ged3-itt_no_invariants.pddl ../examples/d-1-2.pddl ../examples/plan

Note that the plan file has to have a plan in the IPC format, i.e. a list of action instances, each of which is as follows:

(act_name arg1 arg2 ...)

The validator will then give an output indicating the validation result.

Developers

Mohammad Abdulaziz and Peter Lammich (the name ordering is alphabetical)