Infinite trees, markings, and well-foundedness
Computations of nondeterministic programs are modelled by paths in trees. A necessary and sufficient condition is given for the existence of infinite paths in a (computation) tree. This yields a proof rule for fair termination and similar properties of nondeterministic programs.
scientific article; zbMATH DE number 4078764
scientific article