A correct-by-construction approach for development of reliable planning problems

The automated planning community has developed a defacto standard planning language called PDDL. Using the PDDL tools, the reliability of PDDL descriptions can only be posterior examined. However, the Event-B method supports a rich refinement technique that is mathematically proven. Indeed, the Event-B method relies on a first-order predicates language and sets (including mathematical functions and relations) to model the data and on a simple action language to model the treatments. A model described in Event-B includes static modeling elements (sets, constants, axioms and theorems) and dynamic modeling elements (variables, invariant properties and events). Moreover, the Event-B method allows the step-by-step correct construction of Event-B models. To specify and solve the planning problems, a development process based on the combination of Event-B and PDDL is proposed. Our development process favors the obtaining of reliable PDDL description from an ultimate Event-B model using our Event-B2PDDL Eclipse plugin. Our process is successfully experimented on the sliding puzzle game.