Parity Games: Intro
With computer software becoming more important and complex, finding and solving bugs is more critical and difficult than ever. But why must this be? Surely computer programs, running as they do on deterministic machines powered by pure math, can be checked automatically. Well, in general, no. The space of programs, as a whole, is so wild that there exists no algorithm to answer even simple questions such as "will this get stuck in an endless loop". But, if we only need to look at restricted classes of programs, there are mathematical methods to guarantee correctness, or automatically construct a correct program -- where "correct" of course depends on our application. Formal verification is the home of such nifty mathematics and in this post we will be looking at a beautiful slice of it: parity games . Plus, parity games are the home of a tantalizing open question: are they solvable in polynomial time? We'll define what "parity gam