Interleaving Execution and Planning via Symbolic Model Checking

Interleaving planning and execution is the practical alternative to the problem of planning off-line with large state spaces. While planning via symbolic model checking has been extensively studied for off-line planning, no framework for interleaving it with execution has been ever devised. In this paper, we extend planning via symbolic model checking with the ability of interleaving planning and execution in the case of nondeterministic domains and partial observability, one of the most challenging and complex planning problems. We build a planning algorithm such that the interleaving of planning and execution is guaranteed to terminate, either because the goal is achieved, or since there is no longer chance to find a plan leading to the goal. We experiment with the planner and show that it can solve planning problems that cannot be tackled by the off-line symbolic model checking techniques