The Algebra of Parity Games

TL;DR

This paper develops an algebraic framework for parity games using string diagrams, providing a complete set of axioms for reasoning about and solving these games compositionally.

Contribution

It introduces a sound and complete axiomatisation of parity games as string diagrams, enabling algebraic and equational reasoning for solving games.

Findings

Parity games can be represented as morphisms in a symmetric monoidal category.

A complete axiomatisation allows solving parity games through equational reasoning.

A symbolic calculus with fixpoints is developed, mirroring the diagrammatic language.

Abstract

In recent work, Watanabe, Eberhart, Asada, and Hasuo have shown that parity games can be seen as string diagrams, that is, as the morphisms of a symmetric monoidal category, an algebraic structure with two different operations of composition. Furthermore, they have shown that the winning regions associated to a given game can be computed functorially, i.e. compositionally. Building on their results, this paper focuses on the equational properties of parity games, giving them a sound and complete axiomatisation. The payoff is that any parity game can be solved using equational reasoning directly at the level of the string diagram that represents it. Finally, we translate the diagrammatic language of parity games to an equally expressive symbolic calculus with fixpoints, and equip it with its own equational theory.