Automatic Planning: From Event-B to PDDL

Automatic planning is a separate discipline of Artificial Intelligence (AI). It aims to formalize the planning problems described by the concept of state space. The Planning Domain Definition Language (PDDL) is a de facto standard language in the field of automatic planning. PDDL-related dynamic analysis tools, namely planners and validators, are insufficient for verifying and validating PDDL descriptions. Such tools make it possible to detect errors a posteriori by means of a test activity. In this article, we recommend a rigorous approach coupling Event-B and PDDL for automatic planning. Event-B is used for formal modeling by stepwise refinement with mathematical proofs of planning problems. A refinement strategy appropriate to planning problems is, then, proposed. The ultimate Event-B model, correct by construction, supposed to be translatable into PDDL, is automatically translated into PDDL using our MDE Event-B2PDDL tool. The obtained PDDL description is submitted to efficient planners for generation of solution plans.