Accès ouvert

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

Article scientifique 2023 Anglais

Résumé

Abstract 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.

Citer ce document

Ammar, S., Rouis, T., Bhiri, M. (2023). A correct-by-construction approach for development of reliable planning problems. https://doi.org/10.21203/rs.3.rs-2621444/v1

Accès au document

Voir sur le dépôt source

Ce document est hébergé sur son dépôt institutionnel d'origine.

Auteur(s)

Sabrine Ammar Taoufik Sakka Rouis Mohamed Tahar Bhiri

Statistiques

Consultations : 1

Téléchargements : 0