Publication Type

Journal Article

Version

publishedVersion

Publication Date

1-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.

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Formal Methods in System Design

Volume

44

Issue

2

First Page

176

Last Page

202

ISSN

0925-9856

Identifier

10.1007/s10703-013-0197-1

Publisher

Springer Verlag (Germany)

Additional URL

https://doi.org/10.1007/s10703-013-0197-1

Download

Share

COinS