Nondeterministic planning

Automated planning with several possible successors for an action and no specified probabilities for choosing between them. A plan must say how to act after observed outcomes. A strong plan guarantees eventual success for every possible outcome history; a favorable outcome on just one branch does not establish that guarantee.

A plan or policy that reaches a goal after finitely many steps under every permitted outcome sequence. In a finite state space with finite outcome sets, a terminating finitely branching plan tree has bounded depth. Strong planning winning-set iteration constructs exactly the states from which such finite guaranteed-success plans exist. A repeated state cannot be accepted merely because repeated attempts might eventually succeed: without a fairness or probability assumption, an unfavorable outcome can recur forever.

For a finite nondeterministic planning problem with goal set $G$, initialize $W_0=G$ and putA state in $W_t$ has a strong plan reaching $G$ within $t$ steps. The proof is mathematical induction: an action witnessing admission to $W_{t+1}$ has only successors with plans of depth at most $t$. Conversely, the first action of any guaranteed plan of depth $t+1$ has every successor in $W_t$, again by mathematical induction. Since $W_t$ only grows inside a finite state space, the iteration stabilizes after at most the number of states many strict expansions. Recording a witnessing action at first admission gives a policy whose rank decreases at every nonterminal step.