Practical applications of parity games

Question

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.

Answer 1

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.