# Practical applications of parity games

Are there examples of practical applications of parity games, ie systems, in the real world, that can be represented as parity games ?

Usually related documentation on parity games has almost never a practical example of this application.

• The game semantics of modal μ-calculus is related to two-player games with perfect information, particularly infinite parity games. See also section Relation with logic and automata theory in the wikipedia article on parity games. Jan 29 '15 at 16:14
• It is not really meant to be directly applied, but rather as an important part of theories (automata,games,logics) having other applications. Jan 30 '15 at 13:42

Here is a rather different application from what you may have had in mind. Linear programming has many practical applications. There are many algorithms for linear programming and those based on George Dantzig's simplex method are among the most commonly implemented. An important parameter of simplex is called the pivoting rule. Victor Klee and George Minty provides a set of polytopes on which the pivoting rule suggested by Dantzig would require an exponential number of pivoting steps. Since then, examples demonstrating an exponential lower bound have been discovered for nearly every deterministic pivoting rule.

Simplex can however use randomized pivoting rules. Gil Kalai in 1992 introduced a randomized pivoting rule and proved a sub-exponential upper bound for simplex with this rule. Also in 1992, Micha Sharir and Emo Welzl defined LP-type problems which include standard linear programming and with Jiří Matoušek also proposed randomized variants of simplex and proved subexponential upper bounds for this variant. Subexponential lower bounds were also discovered on LP-type problems, but till about 2010 there were no concrete examples of linear programs on which these lower bounds could be demonstrated. See these two posts on Gil Kalai's blog for another telling of this story, the connection to the Hirsch conjecture and links to the literature.

What does any of this have to do with parity games? A couple of steps are required to set up a connection. An open problem in parity games research till about 2009 was to determine if certain policy iteration algorithms for solving parity games might have exponential behaviour. See the papers of Marcin Jurdziński for more on this. Oliver Friedmann, starting in 2009, exhibited examples of parity games on which certain policy iteration algorithms required exponential time. By exploiting a connection between parity games and certain LP-type problems he derived sub-exponential lower bounds for various pivoting rules for simplex. (Note however that one of the results, which concerned the Random Facet algorithm was shown by Oliver Friedmann, Thomas Hansen and Uri Zwick to be erroneous.)

I hope you'll agree that's a pretty fascinating and convincing example of an application of parity games.

There is a more direct answer to your question as well. Suppose one wants to design a discrete controller that regulates how some physical system (thermostat, chemical plant, etc.) behaves based on the state of the system and the state of the environment. The question of whether a controller exists to provide the guarantees a designer wants can be reduced to solving parity games. So you can think of a parity game in terms of systems, environments and controllers.

Another setting is program analysis. Suppose you want to automatically determine if a program satisfies some correctness property in the modal $\mu$-calculus. Model checking is one approach to solving this problem and $\mu$-calculus model checking is deeply connected to parity games.

• The papers that introduced random facet proved subexponential upper bounds on the (expected) number of pivoting steps (currently the answer says lower bounds). The new lower bounds are of a similar form, i.e. subexponential, not exponential. Feb 1 '15 at 13:34
• It may be worth pointing out that some of the lower bounds by Friedmann, Hansen, and Zwick are flawed: arxiv.org/abs/1410.7871 Feb 2 '15 at 3:49
• Thanks Sasho. This is what happens when I stop following the literature! Feb 3 '15 at 4:14