Probabilistic termination versus fair termination

AbstractIn this note we show that probabilistic termination of concurrent programs is in many cases much simpler than the “fair” one. For a wide class of definitions of probabilistic termination we may express termination by π02 arithmetic formula, whereas the “fair” termination can be expressed only by Π| second-order arithmetic formula. Proof of “fair” termination usually needs induction on recursive ordinals, but proof of probabilistic termination has the complexity equivalent to that of deterministic program termination