Forward Conformant Planning via Symbolic 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 planing domain. In this paper we present a new algorithm for conformant planning, returning conformant plans of minimal length if the problem admits a solution, otherwise returning with failure. This work extends previous work on conformant planning, based on model checking techniques. The algorithm presented in this paper takes full advantage of the symbolic representation based on Binary Decision Diagrams (BDDs). in particular, it proceeds forwards, from the initial states towards the goal. it is thus able to exploit forward computation steps, which some times can be significantly more efficient than the corresponding backwards. Furthermore, it implements a new simplification technique which also significantly improves the performance, by containing the combinatorial explosion of the number of explored plans due to the use of a serial encoding. Experimental results suggest that our conformant planner CMBP, besides being strictly more expressive that the state of the art conformant planner CGP, is also able to deal with uncertainties more efficiently