{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T12:07:04Z","timestamp":1753877224117,"version":"3.41.2"},"reference-count":33,"publisher":"Oxford University Press (OUP)","issue":"3","license":[{"start":{"date-parts":[[2024,4,2]],"date-time":"2024-04-02T00:00:00Z","timestamp":1712016000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/pages\/standard-publication-reuse-rights"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,3,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>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.<\/jats:p>","DOI":"10.1093\/logcom\/exae016","type":"journal-article","created":{"date-parts":[[2024,4,4]],"date-time":"2024-04-04T07:34:42Z","timestamp":1712216082000},"source":"Crossref","is-referenced-by-count":0,"title":["A correct-by-construction approach for development of reliable planning problems"],"prefix":"10.1093","volume":"35","author":[{"given":"Sabrine","family":"Ammar","sequence":"first","affiliation":[{"name":"Computer Science Department, Miracl Laboratory , Sfax, 3021,","place":["Tunisia"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Taoufik","family":"Sakka Rouis","sequence":"additional","affiliation":[{"name":"Computer Science Department, ISIMM , Monastir, 5000,","place":["Tunisia"]}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamed Tahar","family":"Bhiri","sequence":"additional","affiliation":[{"name":"Computer Science Department, Miracl Laboratory , Sfax, 3021,","place":["Tunisia"]}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2024,4,2]]},"reference":[{"key":"2025042210091632200_ref1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-031-01564-9","article-title":"A concise introduction to models and methods for automated planning","volume":"7","author":"Geffner","year":"2013","journal-title":"Synthesis Lectures on Artificial Intelligence and Machine Learning"},{"key":"2025042210091632200_ref2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-031-01584-7","article-title":"An introduction to the planning domain definition language","volume":"13","author":"Haslum","year":"2019","journal-title":"Synthesis Lectures on Artificial Intelligence and Machine Learning"},{"volume-title":"PDDL: the Planning Domain Definition Language","year":"1998","author":"Mcdermott","key":"2025042210091632200_ref3"},{"volume-title":"ICTAI16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2004), Boca Raton, FL, USA","year":"2004","author":"Howey","key":"2025042210091632200_ref4"},{"key":"2025042210091632200_ref5","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: Systems and Software Engineering","author":"Abrial","year":"2010"},{"key":"2025042210091632200_ref6","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1109\/MC.2009.283","article-title":"Faultless systems: yes we can!","volume":"42","author":"Abrial","year":"2009","journal-title":"Computer"},{"key":"2025042210091632200_ref7","first-page":"32","volume-title":"Proceedings of the Workshop on User Interfaces and Scheduling and Planning","author":"Magnaguagno","year":"2017"},{"key":"2025042210091632200_ref8","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/978-3-030-38561-3_5","article-title":"KEPS book: planning","author":"Muise","year":"2020","journal-title":"Domains. Knowledge Engineering Tools and Techniques for AI Planning"},{"key":"2025042210091632200_ref9","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1080\/0952813X.2017.1409278","article-title":"PDDL4J: a planning domain description library for java","volume":"30","author":"Pellier","year":"2018","journal-title":"Journal of Experimental and Theoretical Artificial Intelligence"},{"key":"2025042210091632200_ref10","first-page":"474","volume-title":"The IEEE 30th International Conference on Tools with Artificial Intelligence, ICTAI 2018, 5\u20137 November 2018","author":"Abdulaziz","year":"2018"},{"key":"2025042210091632200_ref11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1613\/jair.1705","article-title":"The fast downward planning system","volume":"26","author":"Helmert","year":"2006","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2025042210091632200_ref12","first-page":"114","article-title":"Planning as model checking: the performance of ProB vs NuSMV","volume":"338","author":"Horne","year":"2008","journal-title":"ACM International Conference Proceeding Series, Developing Countries, SAICSIT 2008, 6\u20138 October 2008, Wilderness, South Africa"},{"key":"2025042210091632200_ref13","first-page":"240","volume-title":"The 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012","author":"Li","year":"2012"},{"key":"2025042210091632200_ref14","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book: Assigning Programs to Meanings","author":"Abrial","year":"1996"},{"key":"2025042210091632200_ref15","first-page":"179","volume-title":"Symposium on Information and Communication Technology (SoICT)","author":"Mery","year":"2011"},{"key":"2025042210091632200_ref16","first-page":"313","volume-title":"The Proceedings of the ICFEM International Conference, ICFEM 2016: Formal Methods and Software Engineering","author":"Siala","year":"2016"},{"key":"2025042210091632200_ref17","first-page":"345","volume-title":"International Conference on Abstract State Machines, B and Z, ABZ 2008: Abstract State Machines, B and Z","author":"Requet","year":"2008"},{"key":"2025042210091632200_ref18","first-page":"287","volume-title":"The 25th Euromicro International Conference on Parallel, Distributed and Network-Based Processing, PDP 2017","author":"Siala","year":"2017"},{"key":"2025042210091632200_ref19","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1613\/jair.1129","article-title":"PDDL2.1: an extension to PDDL for expressing temporal planning domains","volume":"20","author":"Fox","year":"2003","journal-title":"Journal of Artificial Intelligence Research"},{"volume-title":"Plan Constraints and Preferences in PDDL3: The Language of the Fifth International Planning Competition","year":"2005","author":"Gerevini","key":"2025042210091632200_ref20"},{"key":"2025042210091632200_ref21"},{"key":"2025042210091632200_ref22","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1613\/jair.2044","article-title":"Modelling mixed discrete-continuous domains for planning","volume":"27","author":"Fox","year":"2006","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2025042210091632200_ref23","first-page":"288","article-title":"The power of reformulation: from validation to planning in PDDL+","volume":"32","author":"Percassi","year":"2022","journal-title":"Archives des sciences m\u00e9dicales"},{"key":"2025042210091632200_ref24","first-page":"655","volume-title":"Proceedings of the Twenty-Second European Conference on Artificial Intelligence, ECAI 2016, Volume 285","author":"Scala","year":"2016"},{"key":"2025042210091632200_ref25","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1613\/jair.1.11751","article-title":"Planning for hybrid systems via satisfiability modulo theories","volume":"67","author":"Cashmore","year":"2020","journal-title":"Journal of Artificial Intelligence Research"},{"key":"2025042210091632200_ref26","first-page":"252","volume-title":"Proceedings of the 31st International Conference on Automated Planning and Scheduling, ICAPS 2021","author":"Percassi","year":"2021"},{"key":"2025042210091632200_ref27","first-page":"436","volume-title":"International Conference on Computational Collective Intelligence","author":"Ammar","year":"2022"},{"key":"2025042210091632200_ref28","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1016\/j.artint.2008.11.009","article-title":"Learning from planner performance","volume":"173","author":"Roberts","year":"2009","journal-title":"Artificial Intelligence"},{"key":"2025042210091632200_ref29","first-page":"1","article-title":"The Rodin platform has turned ten","author":"Voisin","year":"2014","journal-title":"International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2014)"},{"key":"2025042210091632200_ref30","first-page":"199","volume-title":"The 13th SEFM International Conference","author":"Krings","year":"2015"},{"volume-title":"Event-B2PDDL\u2019s Inline Repository","author":"Ammar","key":"2025042210091632200_ref31"},{"key":"2025042210091632200_ref32","first-page":"2638","volume-title":"International Conference on Knowledge-Based Intelligent Information & Engineering Systems (KES), Verona, Italy, Procedia Computer Science","author":"Fourati","year":"2022"},{"key":"2025042210091632200_ref33","first-page":"1647","volume-title":"IEEE Systems Journal","author":"Sakka Rouis","year":"2020"}],"container-title":["Journal of Logic and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/3\/exae016\/57139863\/exae016.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/logcom\/article-pdf\/35\/3\/exae016\/57139863\/exae016.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,22]],"date-time":"2025-04-22T14:58:11Z","timestamp":1745333891000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/logcom\/article\/doi\/10.1093\/logcom\/exae016\/7639119"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,2]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,3,11]]}},"URL":"https:\/\/doi.org\/10.1093\/logcom\/exae016","relation":{},"ISSN":["0955-792X","1465-363X"],"issn-type":[{"type":"print","value":"0955-792X"},{"type":"electronic","value":"1465-363X"}],"subject":[],"published-other":{"date-parts":[[2025,4]]},"published":{"date-parts":[[2024,4,2]]},"article-number":"exae016"}}