Please use this identifier to cite or link to this item:
Title: Model checking approach to automated planning
Authors: Li, Y.
Dong, J.S. 
Sun, J.
Liu, Y.
Sun, J.
Keywords: Deterministic planning
Formal specification & verification
Model checking
Issue Date: 2014
Citation: Li, Y., Dong, J.S., Sun, J., Liu, Y., Sun, J. (2014). Model checking approach to automated planning. Formal Methods in System Design 44 (2) : 176-202. ScholarBank@NUS Repository.
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. © 2013 Springer Science+Business Media New York.
Source Title: Formal Methods in System Design
ISSN: 09259856
DOI: 10.1007/s10703-013-0197-1
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Sep 24, 2020


checked on Sep 24, 2020

Page view(s)

checked on Sep 27, 2020

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.