= Strong planning winning-set iteration
{title2=$W_{t+1}=W_t\cup\operatorname{Pre}_{\forall}(W_t)$}
For a finite <nondeterministic planning> problem with goal <set> $G$, initialize $W_0=G$ and put
$$
W_{t+1}=W_t\cup\{s:\exists a,\ \varnothing\ne\operatorname{Results}(s,a)\subseteq W_t\}.
$$
A 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.
Back to article page
