Planning as Model Checking Tasks

Yi Li, Jing Sun, Jin Song Dong, Yang Liu, and Jun Sun

In Proceedings of the 35th Annual IEEE Software Engineering Workshop (SEW-35), 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 states. 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 different model checking tools and techniques for solving classic planning problems. To achieve this, we carried out a number of experiments on different planning domains in order to compare the performance and capabilities of various tools. Our experimental results indicate that the performance of some model checkers is comparable to that of state-of-the-art planners for certain categories of problems. In particular, a new planning module with specifically designed searching algorithm is implemented on top of the established model checking framework, Process Analysis Toolkit (PAT), to serve as a planning solution provider for upper layer applications. A case study on a public transportation management system has been developed to demonstrate the idea of using the PAT model checker as a planning service.

Cite:

@inproceedings{Li2012PMC,
  author = {Li, Yi and Sun, Jing and Dong, Jin Song and Liu, Yang and Sun, Jun},
  booktitle = {Proceedings of the 35th Annual IEEE Software Engineering Workshop (SEW-35)},
  month = oct,
  pages = {177--186},
  title = {Planning as Model Checking Tasks},
  year = {2012}
}