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

Full description

Saved in:
Bibliographic Details
Published in:Journal of logic and computation 2024-04
Main Authors: Ammar, Sabrine, Sakka Rouis, Taoufik, Bhiri, Mohamed Tahar
Format: Article
Language:English
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0955-792X
1465-363X
DOI:10.1093/logcom/exae016