Given an LTL formula, the tool encodes Deterministic Buchi Automata states and transitions into PDDL (FOND problems).
Example and benchmarks folders, illustrate how to use the tool to generate different FOND domains with LTL goals.
ltl2pddl takes an LTL formula, generates the BA, and provides a clean way to create the PDDL encoding of the BA. Then script generators are used for merging the planning domains with the buchi.
Each folder contains:
- .cxx file to generate either the planning problem, or to generate the planning domain. Domains are generated by combining the BA from the LTL goal and the FOND planning domain
- SConstruct script. To compile, just type: scons
- generate_domains.py script to run the domain/problem generator given the accepted parameters
The key element in the domain generator is the "ltl2pddl translator" class member. The main 3 functions are:
- translator.parse_ltl( ltl_formula ); // Parse an arbitrary LTL formula and generate the buchi automata. Generates a parse_ltl.log file with the Buchi Automata
- translator.generate_pddl_encoding( ... ) // generate pddl encoding of the Buchi automata, given a string that encode the prefix of a buchi_state, and common prec and eff of every buchi transition (can be empty)
- add_action () // to do the cross product representation
See ltl2pddl.hxx for more details.
More to come soon.
Dependencies: spot (https://spot.lrde.epita.fr/), boost and Scons
Have fun,
Nir Lipovetzky & Fabio Patrizi
Jan-2013