Automated planning as an early verification tool for distributed control

Abstract

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.