Probabilistic termination versus fair termination
The probabilistic almost everywhere termination of concurrent programs is proved to be expressible by a \(\Pi^ 0_ 2\) arithmetic formula and hence it has the complexity equivalent to that of deterministic program termination. This is much simpler then the \(\Pi^ 1_ 1\) complexity of ``fair'' termination.
scientific article; zbMATH DE number 4113954