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

The automatic planning community has developed a defacto standard planning language called PDDL. Using the PDDL tools, the reliability of PDDL descriptions can only be posteriori examined. However, the Event-B method supports a rich refinement technique that is mathematically proven. This allows the step-by-step correct construction of Event-B models. In order to specify and solve the planning problems, a development process based on the combination of Event-B and PDDL is proposed. Our development process begins with modeling the planning problem by an Event-B abstract model. Through successive refinements, an Event-B ultimate model correct by construction is obtained. Then, using our Event-B2PDDL Eclipce plugin, the Event-B ultimate model can be automatically translated into a PDDL description. Thus, the resulting PDDL description can be considered correct by construction. Finally, using the PDDL planner tool on this generated PDDL description, plan-solutions related to the planning problems initially described by an Event-B model can be produced. Our process is successfully experimented on a set of representative case studies.