Recent contributions to advancing planning from the classical model to more realistic problems include using temporal logic such as LTL to express desired properties of a solution plan. This paper introduces a planning model that combines temporally extended goals and uncontrollable events. The planning task is to reach a state such that all event sequences generated from that state satisfy the problem's temporally extended goal. A real-life application that motivates this work is to use planning to configure a system in such a way that its subsequent, non-deterministic internal evolution (nominal behavior) is guaranteed to satisfy a condition expressed in temporal logic.

A solving architecture is presented that combines planning, model checking and learning. An online learning process incrementally discovers information about the problem instance at hand. The learned information is useful both to guide the search in planning and to safely avoid unnecessary calls to the model checking module. A detailed experimental analysis of the approach presented in this paper is included. The new method for online learning is shown to greatly improve the system performance.