Conformant Planning via Symbolic Model Checking and Heuristic Search

In this paper we tackle the problem of Conformant Planning: find a sequence of actions that guarantees goal achievement regardless of an uncertain initial condition and of nondeterminstic action effects. Our approach, recast as search in the belief space, is based on two main intuitions. First, symbolic model checking techniques, Binary Decision Diagrams in particular, can be used to represent and expand the search space, and to provide an efficient computational platform. Second, driving the search solely with reachability information is not effective, and the notion of knowledge has to be taken explicitly into account. We make the following contributions. First, we thoroughly analyze reachability heuristics: we formally prove their admissibility, we show how they can be implemented by means of symbolic techniques, and experimentally evaluate them. Second, we analyze the limitations of reachability heuristics, and propose more informed, yet admissible, heuristics, based on a formal notion of knowledge. Third, we present a practical conformant planning algorithm, where the search is explicitly based on the notion of target knowledge, i.e. the amount of information that has to be available in order to reach the goal. The search alternates between the `acquire knowledge` mode, where actions have the precise purpose of gathering necessary information, and the ``Reach Goal`` mode, where actions are directed towards the goal. Finally, we provide a thorough experimental comparison between several conformant planners. Our approach is sometimes able to outperform the competitor systems by orders of magnitude