Automated planning as an early verification tool for distributed control

Ghosh, Kamalesh ; Dasgupta, Pallab ; Ramesh, S. (2015) Automated planning as an early verification tool for distributed control Journal of Automated Reasoning, 54 (1). pp. 31-68. ISSN 0168-7433

Full text not available from this repository.

Official URL:

Related URL:


We present a new modelling formalism which is suitable for capturing high level functional specifications and requirements of reactive control systems. This formalism is a simple extension of the classical planning formalism. We show that if specifications are thus formalized, then it is possible to use existing automated planners and model checkers to find logical faults in them. Our extension to classical planning consists of introducing a separate class of actions, referred as control actions, which have higher priority than regular actions.We present several illustrative examples of high-level modelling and verification of modern automotive features with our proposed formalism. We present several compilation schemes to solve the proposed problem using well-known planners and the model checkers. We present a comparative study of the performance of a number of well-known tools on our problem.We also present some novel optimization techniques which help the solution scale much better with most of the studied tools.

Item Type:Article
Source:Copyright of this article belongs to Springer Verlag.
Keywords:Automated Planning; Model Checking; Action Priority; Formal Verification; Early Verification; Distributed Control; Component Based Systems; Logical Faults; Automotive; Reactive Control; Requirements Engineering
ID Code:100840
Deposited On:12 Dec 2016 11:57
Last Modified:12 Dec 2016 11:57

Repository Staff Only: item control page