Conformant Planning via Symbolic Model Checking
Alessandro Cimatti, Marco Roveri · 2000
We tackle the problem of planning in nondeterministic domains, by presenting a new approach to conformant planning. Conformant planning is the problem of nding a sequence of actions that is guaranteed to achieve the goal despite the nondeterminism of the domain. Our approach is based on the representation of the planning domain as a nite state automaton. We use Symbolic Model Checking techniques, in particular Binary Decision Diagrams, to compactly represent and eciently search the automaton. In this paper we make the following contributions. First, we present a general planning algorithm for conformant planning, which applies to fully nondeterministic domains, with uncertainty in the initial condition and in action eects. The algorithm is based on a breadth-rst, backward search, and returns conformant plans of minimal length, if a solution to the planning problem exists, otherwise it terminates concluding that the problem admits no conformant solution. Second, we provid...