Group colloquium: Parity games are a distraction: how simple fixpoint iteration selects successful strategies

When: July 4, 2019, 15:45-16:30

Where: RA 3231

Who: Tom van Dijk

You can solve model-checking mu-calculus formulas with parity games, but did you know that you can solve parity games by model-checking a mu-calculus formula? It is true! The problems are linearly reducible to each other.

For mu-calculus model-checking, an extremely simple method directly computes the nested fixpoints of the second-order variables. Applying this method to parity games, we find an interesting optimization to the procedure that also trivializes finding the winning strategy for both players. The algorithm should be slow and inefficient but we find that it outperforms all other algorithms for practical model-checking games. Heck, why even bother with parity games in the first place?