Planning under Uncertainty by Model Checking

"Planning under uncertainty" is one of the most significant
and challenging planning problems. Most realistic applications
need to deal with uncertainty about the domain and the environment,
and to deal with incomplete knowledge at planning time and
partial observability at execution time. The problem of planning
under uncertainty has been shown to be hard, both theoretically
and experimentally. "Planning as Model Checking" is a novel
approach to planning. We have shown that it is a general and
well-founded approach to the problem of planning under uncertainty.
We have built a planner, the Model Based Planner MBP
and we have shown with experimental evaluations that MBP can deal
in practice with domains of large size. In the talk we will introduce
the problem and the approach, and we will present
some recent results in planning in non-deterministic domains,
with partial information available at run time,
and for requirements expressed in temporal logic.