Strong planning in non-deterministic domains via model checking
Alessandro Cimatti, Marco Roveri, Paolo Traverso · 1998
Most real world domains are non-deterministic: the state of the world can be incompletely known, the effect of actions can not be completely foreseen, and the environment can change in unpredictable ways. Automatic plan formation in non-deterministic domains is, however, still an open problem. In this paper we show how to do strong planning in non-deterministic domains, i.e. finding automatically plans which are guaranteed to achieve the goal regardless of nondeterminism. We define a notion of planning solution which is guaranteed to achieve the goal independently of non-determinism, a notion of plan including conditionals and iterations, and an automatic decision procedure for strong planning based on model checking techniques. The procedure is correct, complete and returns optimal plans. The work has been implemented in mbp, a planner based on model checking techniques.