Strong Cyclic Planning Revisited

Several realistic non-deterministic planning domains require plans that encode iterative trial-and-error strategies, e.g., `pick up a block until succeed`. In such domains, a certain effect (e.g., action success) might never be guaranteed a priori of execution and, in principle, iterative plans might loop forever. Here, the planner should generate iterative plans whose executions always have a possibility of terminating and, when they do, they are guaranteed to achieve the goal. In this paper, we define the notion of strong cyclic plan, which formalizes in temporal logic the above informal requirements for iterative plans, define a planning algorithm based on model-checking techniques, and prove that the algorithm is guaranteed to return strong cyclic plans when they exist or to terminate with failure when they do not. We show how this approach can be extended to formalize plans that are guaranteed to achieve the goal and do not involve iterations (strong plans) and plans that have a possibility (but are not guaranteed) to achieve the goal (weak plans). The results presented in this paper constitute a formal account for `planning via model checking` in non-deterministic domains, which has never been provided before