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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.351.17 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |