Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
7-2012
Abstract
Model checking provides a way to automatically verify hardware and software systems, whereas the goal of planning is to produce a sequence of actions that leads from the initial state to the desired goal state. Recently research indicates that there is a strong connection between model checking and planning problem solving. In this paper, we investigate the feasibility of using a newly developed model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. We first carried out a number of experiments on different planning tools in order to compare their performance and capabilities. Our experimental results showed that the performance of the PAT model checker is comparable to that of state-of-art planners for certain categories of problems. We further propose a set of translation rules for mapping from a commonly used planning notation – PDDL into the CSP# modeling language of PAT. Finally, we provide evaluations on the translated models against other approaches in the planning domain to demonstrate the effectiveness of using the PAT model checker for planning.
Keywords
Formal Verification, Model Checking, Planning
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012, Paris, France, July 18-20
First Page
240
Last Page
249
ISBN
9782954181004
Identifier
10.1109/ICECCS20050.2012.6299219
Publisher
IEEE
City or Country
France
Citation
LI, Yi; SUN, Jing; DONG, Jin Song; LIU, Yang; and SUN, Jun.
Translating PDDL into CSP# - The PAT approach. (2012). Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2012, Paris, France, July 18-20. 240-249.
Available at: https://ink.library.smu.edu.sg/sis_research/5019
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/ICECCS20050.2012.6299219