pddl2hoa is a Python tool that converts PDDL (Planning Domain Definition Language) planning problems into HOA (Hanoi Omega Automata) format. This enables downstream analysis with formal methods tools and automata-based verification frameworks.
- Parse and analyze PDDL domain and problem files
- Convert planning goals into equivalent HOA automata
- Generate Strategy Templates for PDDL domains and problems (must install Pestel seperately)
- Compatible with tools that support HOA format (e.g., Spot, Pestel)
- Designed for integration into formal methods pipelines
Install via uv (recommended):
uv pip install pddl2hoaOr from source:
git clone https://github.com/yourusername/pddl2hoa.git
cd pddl2hoa
uv pip install .After installation, use the CLI tool:
pddl2hoa domain.pddl problem.pddl > edge_labeled_HOA.hoaOr use it as a Python library:
from pddl2hoa import convert_pddl_to_hoa
convert_pddl_to_hoa("domain.pddl", "problem.pddl")This library is designed to be extensible. You can convert almost any domain with a graph-based structure into an HOA representation by subclassing the TurnBasedGame abstract base class in game.py. Once your game format is implemented, you can call the format_hoa method from generate_hoa.py to produce a corresponding HOA graph.
Pull requests are welcome! For major changes, please open an issue first to discuss what you’d like to change.
- Github
- PyPi
- PDDLGym, the PDDL utility that this package uses under the hood
- HOA Format Spec