Global and local views of state fairness

AbstractIn this paper, we compare global and local versions of state fairness for systems of concurrent programs and Petri nets. We then investigate complexity and decidability issues for the fair nontermination problem. It turns out that for systems of concurrent Boolean programs and 1-bounded Petri nets, the problem is PSPACE-complete with respect to global state fairness, but EXPTIME-complete with respect to local state fairness. For general systems of concurrent programs, both the globally and locally state fair nontermination problems are undecidable. (In fact, they are Π1-complete and Σ|-complete, respectively.1) On the other hand, the problem is decidable for general Petri nets with respect to global state fairness, and undecidable (Σ1-complete) with respect to local state fairness