page_title: Parity game
section_title: Relation with logic and automata theory
hierarchical_section_title: Parity game / Relation with logic and automata theory
caption_attribution_description: English: The image contains an overview over the most common use cases for parity game solving.
context_page_description: A parity game is played on a colored directed graph, where each node has been colored by a priority – one of finitely many natural numbers. Two players, 0 and 1, move a token along the edges of the graph. The owner of the node that the token falls on selects the successor node, resulting in a path, called the play.
  The winner of a finite play is the player whose opponent is unable to move. The winner of an infinite play is determined by the priorities appearing in the play. Typically, player 0 wins an infinite play if the largest priority that occurs infinitely often in the play is even. Player 1 wins otherwise. This explains the word "parity" in the title.
  Parity games lie in the third level of the Borel hierarchy, and are consequently determined.
  Games related to parity games were implicitly used in Rabin's
  proof of decidability of second-order theory of n successors, where determinacy of such games was
  proven. The Knaster–Tarski theorem leads to a relatively simple proof of determinacy of parity games.
  Moreover, parity games are history-free determined.
context_section_description: Despite its interesting complexity theoretic status, parity game solving can be seen as the algorithmic backend to problems in automated verification and controller synthesis. The model-checking problem for the modal μ-calculus for instance is known to be equivalent to parity game solving. Also, decision problems like validity or satisfiability for modal logics can be reduced to parity game solving.
caption: Most common applications of parity game solving.
exif: {}