A Compositional Approach to Parity Games

Kazuki Watanabe
(The Graduate University for Advanced Studies (SOKENDAI) and National Institute of Informatics)
Clovis Eberhart
(National Institute of Informatics and Japanese-French Laboratory of Informatics)
Kazuyuki Asada
(Tohoku University)
Ichiro Hasuo
(The Graduate University for Advanced Studies (SOKENDAI), National Institute of Informatics, and Ritsumeikan University)

In this paper, we introduce open parity games, which is a compositional approach to parity games. This is achieved by adding open ends to the usual notion of parity games. We introduce the category of open parity games, which is defined using standard definitions for graph games. We also define a graphical language for open parity games as a prop, which have recently been used in many applications as graphical languages. We introduce a suitable semantic category inspired by the work by Grellois and Melliès on the semantics of higher-order model checking. Computing the set of winning positions in open parity games yields a functor to the semantic category. Finally, by interpreting the graphical language in the semantic category, we show that this computation can be carried out compositionally.

In Ana Sokolova: Proceedings 37th Conference on Mathematical Foundations of Programming Semantics (MFPS 2021), Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, Electronic Proceedings in Theoretical Computer Science 351, pp. 278–295.
Published: 29th December 2021.

ArXived at: http://dx.doi.org/10.4204/EPTCS.351.17 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org