Planning via Model Checking: A Decision Procedure for AR

In this paper we propose a new approach to planning based on a `high level action language`, called AR, and `model checking`. AR is an expressive formalism which is able to handle, among other things, ramifications and non-deterministic effects. We define a decision procedure for planning in AR which is based on `symbolic model checking`, a technique which has been sucessfully applied in hardware and software verification. The decision procedure always terminates with an optimal solution or with failure if no solution exists. We have constructed a planner, called MBP, which implements the decision procedure