Unbounded Nondeterminism - Indeterminacy Versus Nondeterministic Automata

Indeterminacy Versus Nondeterministic Automata

William Clinger provided the following analysis of the above proof by Plotkin:

This proof depends upon the premise that if every node x of a certain infinite branch can be reached by some computation c, then there exists a computation c that visits every node x on the branch. ... Clearly this premise follows not from logic but rather from the interpretation given to choice points. This premise fails for arrival nondeterminism because of finite delay . Though each node on an infinite branch must lie on a branch with a limit, the infinite branch need not itself have a limit. Thus the existence of an infinite branch does not necessarily imply a nonterminating computation.