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