Fast Symbolic Algorithms for Omega-Regular Games under Strong Transition Fairness

We consider fixpoint algorithms for two-player games on graphs with$\omega$-regular winning conditions, where the environment is constrained by astrong transition fairness assumption. Strong transition fairness is a widelyoccurring special case of strong fairness, which requires that any execution isstrongly fair with respect to a specified set of live edges: whenever thesource vertex of a live edge is visited infinitely often along a play, the edgeitself is traversed infinitely often along the play as well. We show that,surprisingly, strong transition fairness retains the algorithmiccharacteristics of the fixpoint algorithms for $\omega$-regular games -- thenew algorithms have the same alternation depth as the classical algorithms butinvoke a new type of predecessor operator. For Rabin games with $k$ pairs, thecomplexity of the new algorithm is $O(n^{k+2}k!)$ symbolic steps, which isindependent of the number of live edges in the strong transition fairnessassumption. Further, we show that GR(1) specifications with strong transitionfairness assumptions can be solved with a 3-nested fixpoint algorithm, same asthe usual algorithm. In contrast, strong fairness necessarily requiresincreasing the alternation depth depending on the number of fairnessassumptions. We get symbolic algorithms for (generalized) Rabin, parity andGR(1) objectives under strong transition fairness assumptions as well as adirect symbolic algorithm for qualitative winning in stochastic$\omega$-regular games that runs in $O(n^{k+2}k!)$ symbolic steps, improvingthe state of the art. Finally, we have implemented a BDD-based synthesis enginebased on our algorithm. We show on a set of synthetic and real benchmarks thatour algorithm is scalable, parallelizable, and outperforms previous algorithmsby orders of magnitude