Conformant Planning via Model Checking

Conformant planning is the problem of finding a sequence of actions that is guaranteed to achieve the goal for any possible initial state and non-deterministic behavior of the planning domain. In this paper we present a new approach to conformant planning. We propose an algorithm that returns the set of all conformant plans of minimal length if the problem admits a solution, otherwise it returns with failure. Our work is based on the planning via model checking paradigm, and relies on symbolic techniques such as Binary Decision Diagrams to compactly represent and efficiently analyze the planning domain. The algorithm, called CMBP, has been implemented in the MBP planner. CMBP is strictly more expressive than the state of the art conformant planner CGP. Furthermore, an experimental evaluation suggests that CMBP is able to deal with uncertainties more efficiently than CGP.