A Compositional Approach to Parity Games

TL;DR

This paper introduces open parity games, a compositional framework that extends traditional parity games with open ends, enabling modular analysis through a graphical language and semantic interpretation.

Contribution

It develops a category of open parity games and a graphical language as a prop, allowing compositional computation of winning positions in parity games.

Findings

Open parity games form a new compositional framework.

The graphical language is interpreted in a semantic category.

Winning positions can be computed compositionally.

Abstract

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\`es 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.