
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Advanced Database Systems and Queries · Game Theory and Applications
