Model Checking Approach to Automated Planning

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

Formal Methods in System Design, 2014

Abstract: Model checking provides a way to automatically explore the state space of a finite state system based on desired properties, whereas planning is to produce a sequence of actions that leads from the initial state to the target goal states. Previous research in this field proposed a number of approaches for connecting model checking with planning problem solving. In this paper, we investigate the feasibility of using an established model checking framework, Process Analysis Toolkit (PAT), as a planning solution provider for upper layer applications. To achieve this, we first carry out a number of experiments on different model checking tools in order to compare their performance and capabilities on planning problem solving. Our experimental results suggest that solving planning problems using model checkers is not only possible but also practical. We then propose a formal semantic mapping from the standard Planning Domain Description Language (PDDL) to the Labeled Transition System (LTS), based on which a planning module was implemented as a part of the PAT framework. Lastly, we demonstrate and evaluate the approach of using PAT as planning service via a case study on a public transportation management system.

Cite:

@article{Li2014MCA,
  author = {Li, Yi and Dong, Jin Song and Sun, Jing and Liu, Yang and Sun, Jun},
  journal = {Formal Methods in System Design},
  number = {2},
  pages = {176--202},
  publisher = {Springer US},
  title = {Model Checking Approach to Automated Planning},
  volume = {44},
  year = {2014}
}