Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Watanabe, Kazuki

doi:10.4230/LIPIcs.CALCO.2025.14

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Kazuki Watanabe

National Institute of Informatics, Tokyo, Japan
The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan

Abstract

Open parity games are proposed as a compositional extension of parity games with algebraic operations, forming string diagrams of parity games. A potential application of string diagrams of parity games is to describe a large parity game with a given compositional structure and solve it efficiently as a divide-and-conquer algorithm by exploiting its compositional structure.

Building on our recent progress in open Markov decision processes, we introduce Pareto fronts of open parity games, offering a framework for multi-objective solutions. We establish the positional determinacy of open parity games with respect to their Pareto fronts through a novel translation method. Our translation converts an open parity game into a parity game tailored to a given single-objective. Furthermore, we present a simple algorithm for solving open parity games, derived from this translation that allows the application of existing efficient algorithms for parity games. Expanding on this foundation, we develop a compositional algorithm for string diagrams of parity games.

Keywords and phrases:

parity game, compositionality, string diagram

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Verification by model checking

Acknowledgements:

We would like to thank the anonymous referees for their helpful suggestions, which have enabled us to improve this article.

Funding:

We are supported by the JST grant No. JPMJAX23CU.

DOI:

10.4230/LIPIcs.CALCO.2025.14

Event:

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Parity games (on finite graphs) have been actively studied, and the search for efficient algorithms is a central topic for parity games. A key property of parity games is positional determinacy [15, 16], which underpins their decidability by ensuring that positional strategies suffice to determine the winner at any node. Calude et al. [10] show that parity games are solvable in quasi-polynomial-time, leading to the development of subsequent quasi-polynomial-time algorithms [25, 19, 32]. The significance of these advancements extends beyond theoretical interest; they have practical applications in various verification problems. Notably, many verification problems can be reduced to solving parity games, including model checking with temporal specifications [28, 29, 17, 35, 27].

Refer to caption — Figure 1: (i) an open parity game (oPG), (ii) the sequential composition $\mathcal{A}\fatsemi\mathcal{B}$ of oPGs $\mathcal{A},\mathcal{B}$ , and (iii) the sum $\mathcal{A}\oplus\mathcal{B}$ of oPGs $\mathcal{A},\mathcal{B}$ .

Compositionality in verification is a property that enables divide-and-conquer algorithms by exploiting compositional structures, aiming to solve the notorious state space explosion problem. Clarke et al. [12] provided the first compositional model checking algorithm, and since then, many compositional model checking algorithms have been proposed for LTL [26], Markov decision processes [30, 46, 44], and higher-order model checking [40]. Recently, we introduced string diagrams of parity games [43] as a compositional extension of parity games. We proposed open parity games that can be composed using two algebraic operations: the (bidirectional) sequential composition and the sum. Fig. 1 shows an open parity game and illustrates two algebraic operations over open parity games $\mathcal{A},\mathcal{B}$ in string diagrams of parity games. Although we did not provide a compositional algorithm in the original work [43], we developed one for string diagrams of mean payoff games [45]. The methodology developed is also adaptable to string diagrams of parity games.

A major difficulty for compositional algorithms arises from the multi-objective perspective¹¹1This differs from having several parity objectives. on individual components: typically, even if a given “global” objective is single-objective, which is the parity condition for parity games, “local” objectives on components become multi-objective.

Figure 2: The parity game

\mathcal{A}\fatsemi\mathcal{B}

. Every node is owned by Player

\exists

.

For instance, Fig. 2 shows a parity game $\mathcal{A}\fatsemi\mathcal{B}$ consisting of open parity games $\mathcal{A}$ and $\mathcal{B}$ . In the open parity game $\mathcal{A}$ , the Player $\exists$ has the choice of moving from the node $a$ to either the node $o_{\mathbf{r},1}$ or the node $o_{\mathbf{r},2}$ . However, the optimal $\exists$ -strategies in $\mathcal{A}\fatsemi\mathcal{B}$ may vary, depending on the priorities $m_{1}$ and $m_{2}$ in the open parity game $\mathcal{B}$ . Consequently, it is necessary to compute all “potentially” optimal strategies on $\mathcal{A}$ without any prior knowledge of $\mathcal{B}$ in order to solve the parity game $\mathcal{A}\fatsemi\mathcal{B}$ compositionally. Our previous work on string diagrams of mean payoff games [45] tackled this by enumerating such potentially optimal strategies in open mean payoff games. The enumeration algorithm requires exponential time in the number of nodes of the given open mean payoff game, which is infeasible in practice.

By following our recent progress on string diagrams of Markov decision processes (MDPs) [46], we introduce Pareto fronts of open parity games, which are intuitively sets of optimal results on open parity games. We prove positional determinacy of open parity games, that is, positional strategies suffice to achieve Pareto fronts (Thm. 28). Our proof method involves selecting a “single-objective”, the number of which is finite, and we show that positional strategies suffice to satisfy the given single-objective. This procedure is repeated for each possible single-objective. In the proof, we propose a novel translation that converts an open parity game into a (non-open) parity game tailored to a given single-objective (Def. 32). Moreover, our translation leads to a simple algorithm for open parity games that requires exponential time only in the number of exits, not in the number of whole nodes as in our previous algorithm [45]: here our algorithm use known quasi-polynomial-time algorithms (Alg. 1 and Prop. 40). On top of these developments, we provide a compositional algorithm of string diagrams of parity games by composing Pareto fronts of open parity games (Alg. 2).

Contributions.

$\blacksquare$

we introduce Pareto fronts of open parity games in Section 3.3,
$\blacksquare$

we prove the positional determinacy of Pareto fronts of open parity games, which is stated in Section 4.1, by a novel translation from an open parity game to a parity game with a given single-objective in Section 4.2,
$\blacksquare$

we present a simple algorithm that computes Pareto fronts of open parity games, and provide an upper bound of its time complexity in Section 4.2, which shows improvements over our previous algorithm [45],
$\blacksquare$

we provide a compositional algorithm of string diagrams of parity games in Section 5.

1.1 Related Work

String diagrams are a graphical language, which is mostly described in category theory. They effectively model signal flow diagrams [5, 7, 8, 2], quantum processes [13, 14], Petri nets [6, 3], and games for economics [23, 31]. Rathke et al. [38] derive a divide-and-conquer algorithm for reachability analysis of Petri nets, and we provide a compositional algorithm for string diagrams of mean payoff games in [45], which can be readily adapted to string diagrams of parity games [43]. Recently, Piedeleu [37] provides a sound and complete diagrammatic language of parity games w.r.t. the semantics of open parity games [43]. In this paper, we propose a compositional algorithm for string diagrams of parity games based on a rather efficient semantics, focusing on the positional determinacy of open parity games.

Pareto fronts [36, 18] offer a well-formulated solution for multi-objective optimization problems. They enhance the performance of compositional probabilistic model checking [46]. A crucial property of Pareto fronts in [46] is again positional determinacy: each point on Pareto fronts is induced by a positional scheduler, which can be computed using standard algorithms for (non-open) MDPs [21].

In [46], we propose a compositional probabilistic model checking of string diagrams of MDPs with Pareto fronts: we introduce shortcut MDPs and prove their compositionality, analogous to Props 42 and 43. A major contribution of this paper, compared to [46], is the introduction of a novel translation from open parity games to parity games, designed to efficiently compute Pareto fronts. This stands in contrast to the already established translation for open MDPs [21].

Multi-objectives in games have been well-studied in the literature. Velner et al. [41] study the complexity of multi-mean-payoff and multi-energy games. Chen et al. [11] develop an approximation method for Pareto fronts of stochastic games. Recently, a Pareto-based rational verification problem, which interacts with the environment, is introduced in [9].

Obdržálek [34], and Fearnley and Schewe [20] provide polynomial time algorithms for parity games on graphs of bounded tree-width. Berwanger et al. [4] show that parity games on graphs of bounded DAG-width can be solved in polynomial time. The notion of result in [4] gathers optimal results of Player $\forall$ for each strategy employed by Player $\exists$ , regardless of its optimality. In contrast, our Pareto fronts collect optimal results not only from Player $\forall$ , but also from Player $\exists$ , and are positionally determined. Although our compositional algorithm is not a polynomial time algorithm for string diagrams of parity games, it does not require assumptions such as bounded tree- or DAG-widths.

Compositionality in parity games seems to be linked to higher-order model checking [35, 27], a model checking method of higher-order programs. In higher-order model checking, specifications are given as parity tree automata, which are equivalent to modal $\mu$ -calculus [16]. In fact, the semantics of string diagrams of parity games [43] is based on the semantics of higher-order model checking [24]. Unlike [24] that employs the trivial discrete order on priorities, we utilize the sub-priority order [4, 22], which is central to our development. Fujima et al. [22] introduce the subtype relation in the intersection type, which corresponds to our order for results of games defined in Def. 22. Tsukada and Ong [40] present a compositional higher-order model checking over the composition of Böhm trees. We employ the dual of priorities (Def. 34), which in [40] is called the left-residual of $0$ . The duality of queries shown in Lem. 37 is conceptually similar to the notion of the complementarity predicate in [39]. They utilize the property for showing the relationship between a game and its dual in the context of higher-order model checking.

2 Formal Problem Statement

We revisit parity games and string diagrams of parity games [43], and we formally state our target problem. Throughout this paper, we fix the finite set $\mathbb{P}:=\{0,1,\dots,M\}$ of priorities. We assume that the maximum priority $M$ is even and $M\geq 2$ without loss of generality.

2.1 Parity Games

Definition 1 (parity game).

A parity game (PG) $\mathcal{G}$ is a tuple $(V,V_{\exists},V_{\forall},E,\Omega)$ , where the set $V$ is a non-empty finite set of nodes, the sets $V_{\exists},V_{\forall}$ are a partition of $V$ such that $V_{\exists}$ is owned by Player $\exists$ and $V_{\forall}$ is owned by Player $\forall$ , the set $E$ is a set of edges $E\subseteq V\times V$ , and the function $\Omega$ is a labelling function $\Omega\colon E\rightarrow\mathbb{P}$ , assigning priorities to edges.

We assume that every node has a successor in PGs. A play $p$ is an infinite path $(v_{i})_{i\in\mathbb{N}}$ such that $(v_{i},v_{i+1})\in E$ , for any $i\in\mathbb{N}$ . A play $p$ is winning (for Player $\exists$ ) if the maximum priority that occurs in $p$ infinitely often is even. Otherwise, the play $p$ is losing (for Player $\exists$ ). We also call the winning condition as the parity condition. An $\exists$ -strategy $\sigma_{\exists}$ (of Player $\exists$ ) is a function $\sigma_{\exists}\colon V^{\ast}\cdot V_{\exists}\rightarrow V$ such that for any finite path $v_{1}\cdots v_{n}$ , if $v_{n}\in V_{\exists}$ , then $\big{(}v_{n},\sigma_{\exists}(v_{1}\cdots v_{n})\big{)}\in E$ . A $\forall$ -strategy $\sigma_{\forall}$ (of Player $\forall$ ) is analogously defined. An $\exists$ -strategy $\sigma_{\exists}$ is a positional strategy if for any $v_{1}\cdots v_{m}$ and $v^{\prime}_{1}\dots v^{\prime}_{n}$ such that $v_{m}=v^{\prime}_{n}\in V_{\exists}$ , their successors coincide $\sigma_{\exists}(v_{1}\cdots v_{m})=\sigma_{\exists}(v^{\prime}_{1}\cdots v^{% \prime}_{n})$ ; positional $\forall$ -strategies are defined in the same way. We write $\sigma_{\exists}\colon V_{\exists}\rightarrow V$ (and $\sigma_{\forall}\colon V_{\forall}\rightarrow V$ ) for a positional $\exists$ -strategy (and a positional $\forall$ -strategy). Given a pair $(\sigma_{\exists},\sigma_{\forall})$ of $\exists$ - and $\forall$ -strategies, and a node $v$ , a play $p_{\sigma_{\exists},\sigma_{\forall};v}$ from $v$ that is induced by $(\sigma_{\exists},\sigma_{\forall})$ is the play $(v_{i})_{i\in\mathbb{N}}$ such that $v_{1}=v$ , and for any index $i$ , if $v_{i}\in V_{\exists}$ , then $\sigma_{\exists}(v_{1}\cdots v_{i})=v_{i+1}$ , and if $v_{i}\in V_{\forall}$ , then $\sigma_{\forall}(v_{1}\cdots v_{i})=v_{i+1}$ . PGs are positionally determined [15, 16], that is, there is a partition $(W_{\exists},W_{\forall})$ of $V$ , called winning regions, such that $v\in W_{\exists}$ iff there is a winning positional strategy $\sigma_{\exists}\colon V_{\exists}\rightarrow V$ for Player $\exists$ , and $v\in W_{\forall}$ iff there is a winning positional strategy $\sigma_{\forall}\colon V_{\forall}\rightarrow V$ for Player $\forall$ .

2.2 String Diagrams of Parity Games

String diagrams of parity games [43] consist of open parity games (oPGs), which are a compositional extension of PGs. OPGs have open ends that are entrances and exits. We illustrate an oPG in Fig. 3 as a running example, and will continue to refer to this example until Section 4.1. It is important to note that oPGs without exits can be regarded as PGs.

Definition 2 (open parity game [43]).

An open parity game (oPG) $\mathcal{A}$ is a pair $(\mathcal{G},\mathsf{IO})$ of a PG $\mathcal{G}=(V,V_{\exists},V_{\forall},E,\Omega)$ and open ends $\mathsf{IO}=(I_{\mathbf{r}},I_{\mathbf{l}},O_{\mathbf{r}},O_{\mathbf{l}})$ , where $I_{\mathbf{r}},I_{\mathbf{l}},O_{\mathbf{r}},O_{\mathbf{l}}$ are nodes $I_{\mathbf{r}},I_{\mathbf{l}},O_{\mathbf{r}},O_{\mathbf{l}}\subseteq V_{\exists}$ that are totally ordered, respectively, and each pair of them is disjoint. Open ends in $I_{\mathbf{r}},O_{\mathbf{r}}$ are rightward, and open ends in $I_{\mathbf{l}},O_{\mathbf{l}}$ are leftward. We call $I:=I_{\mathbf{r}}\cup I_{\mathbf{l}}$ entrances, and $O:=O_{\mathbf{r}}\cup O_{\mathbf{l}}$ exits, respectively. We also write $\mathcal{A}\colon(m_{\mathbf{r}},m_{\mathbf{l}})\rightarrow(n_{\mathbf{r}},n_{% \mathbf{l}})$ for the oPG $\mathcal{A}$ with the type of open ends, where $m_{\mathbf{r}}:=|I_{\mathbf{r}}|$ , $m_{\mathbf{l}}:=|I_{\mathbf{l}}|$ , $n_{\mathbf{r}}:=|O_{\mathbf{r}}|$ , and $n_{\mathbf{l}}:=|O_{\mathbf{l}}|$ . We additionally impose that every exit $o\in O_{\mathbf{r}}\cup O_{\mathbf{l}}$ is a sink node, that is, for any $v\in V$ , $(o,v)\in E$ implies $v=o$ and $\Omega(o,o)=0$ .

Figure 3: An oPG

\mathcal{C}\colon(1,1)\rightarrow(1,0)

. The node

i_{\mathbf{r},1}

is the entrance, and the nodes

o_{\mathbf{r},1},o_{\mathbf{l},1}

are exits. The open ends

i_{\mathbf{r},1}

and

o_{\mathbf{r},1}

are rightward, and the exit

o_{\mathbf{l},1}

is leftward. The shape of each (internal) node represents the owner, that is, circles are owned by Player

\exists

, and diamonds are owned by Player

\forall

. The labels on the edges are the assigned priorities.

Algebraic operations, namely the (bidirectional) sequential composition $\mathcal{A}\fatsemi\mathcal{B}$ and the sum $\mathcal{A}\oplus\mathcal{B}$ , are defined as illustrated in Fig. 1. The sequential composition $\mathcal{A}\fatsemi\mathcal{B}$ of $\mathcal{A}$ and $\mathcal{B}$ is given by connecting their open ends, assuming their arities are consistent. Note that the sequential composition can create a cycle along open ends.

Definition 3 (sequential composition).

Let $\mathcal{A}\colon(m_{\mathbf{r}},m_{\mathbf{l}})\rightarrow(l_{\mathbf{r}},l_{% \mathbf{l}})$ and $\mathcal{B}\colon(l_{\mathbf{r}},l_{\mathbf{l}})\rightarrow(n_{\mathbf{r}},n_{% \mathbf{l}})$ . Their (bidirectional) sequential composition $\mathcal{A}\fatsemi\mathcal{B}\colon(m_{\mathbf{r}},m_{\mathbf{l}})\rightarrow% (n_{\mathbf{r}},n_{\mathbf{l}})$ is an oPG $(V^{\mathcal{A}}\uplus V^{\mathcal{B}},V^{\mathcal{A}}_{\exists}\uplus V^{% \mathcal{B}}_{\exists},V^{\mathcal{A}}_{\forall}\uplus V^{\mathcal{B}}_{% \forall},E^{\mathcal{A}\fatsemi\mathcal{B}},\Omega^{\mathcal{A}\fatsemi% \mathcal{B}})$ , where the set $E^{\mathcal{A}\fatsemi\mathcal{B}}$ of edges is the least relation and $\Omega^{\mathcal{A}\fatsemi\mathcal{B}}$ is the function that satisfy the following conditions:

$\blacksquare$

if $(v,v^{\prime})\in E^{\mathcal{A}}$ and $v\not\in O_{\mathbf{r}}^{\mathcal{A}}$ , then $(v,v^{\prime})\in E$ and $\Omega^{\mathcal{A}\fatsemi\mathcal{B}}(v,v^{\prime}):=\Omega^{\mathcal{A}}(v,% v^{\prime})$ ,
$\blacksquare$

if $(v,v^{\prime})\in E^{\mathcal{B}}$ and $v\not\in O_{\mathbf{l}}^{\mathcal{B}}$ , then $(v,v^{\prime})\in E$ and $\Omega^{\mathcal{A}\fatsemi\mathcal{B}}(v,v^{\prime}):=\Omega^{\mathcal{B}}(v,% v^{\prime})$ ,
$\blacksquare$

$(o_{\mathbf{r},i}^{\mathcal{A}},i_{\mathbf{r},i}^{\mathcal{B}})\in E$ and $\Omega^{\mathcal{A}\fatsemi\mathcal{B}}(o_{\mathbf{r},i}^{\mathcal{A}},i_{% \mathbf{r},i}^{\mathcal{B}}):=0$ , for any $i\in[1,l_{\mathbf{r}}]$ , and
$\blacksquare$

$(o_{\mathbf{l},j}^{\mathcal{B}},i_{\mathbf{l},j}^{\mathcal{A}})\in E$ and $\Omega^{\mathcal{A}\fatsemi\mathcal{B}}(o_{\mathbf{l},j}^{\mathcal{B}},i_{% \mathbf{l},j}^{\mathcal{A}}):=0$ , for any $j\in[1,l_{\mathbf{l}}]$ .

We also define the sum $\mathcal{A}\oplus\mathcal{B}$ of $\mathcal{A}$ and $\mathcal{B}$ : see Fig. 1 for an illustration.

Definition 4 (sum).

Let $\mathcal{A}\colon(m_{\mathbf{r}},m_{\mathbf{l}})\rightarrow(n_{\mathbf{r}},n_{% \mathbf{l}})$ and $\mathcal{B}\colon(k_{\mathbf{r}},k_{\mathbf{l}})\rightarrow(l_{\mathbf{r}},l_{% \mathbf{l}})$ . Their sum $\mathcal{A}\oplus\mathcal{B}\colon(m_{\mathbf{r}}+k_{\mathbf{r}},m_{\mathbf{l}% }+k_{\mathbf{l}})\rightarrow(n_{\mathbf{r}}+l_{\mathbf{r}},n_{\mathbf{l}}+l_{% \mathbf{l}})$ is an oPG $(V^{\mathcal{A}}\uplus V^{\mathcal{B}},V^{\mathcal{A}}_{\exists}\uplus V^{% \mathcal{B}}_{\exists},V^{\mathcal{A}}_{\forall}\uplus V^{\mathcal{B}}_{% \forall},E^{\mathcal{A}\oplus\mathcal{B}},\Omega^{\mathcal{A}}\uplus\Omega^{% \mathcal{B}})$ , where the set $E^{\mathcal{A}\oplus\mathcal{B}}$ of edges is the least relation that satisfies the following condition:

$\blacksquare$

if $(v,v^{\prime})\in E^{\mathcal{A}}$ , then $(v,v^{\prime})\in E^{\mathcal{A}\oplus\mathcal{B}}$ , and if $(v,v^{\prime})\in E^{\mathcal{B}}$ , then $(v,v^{\prime})\in E^{\mathcal{A}\oplus\mathcal{B}}$ .

We define string diagrams of PGs as a syntax of compositional PGs: we also introduce operational semantics of string diagrams of PGs as oPGs induced by string diagrams.

Definition 5 (string diagram).

A string diagram $\mathbb{D}$ of parity games is a term inductively generated by $\mathbb{D}::=\mathcal{A}\mid\mathbb{D}\fatsemi\mathbb{D}\mid\mathbb{D}\oplus% \mathbb{D}$ where $\mathcal{A}$ ranges over oPGs. The operational semantics $\llbracket\mathbb{D}\rrbracket$ of a string diagram $\mathbb{D}$ is the oPG inductively given by Defs 3 and 4.

Finally, we state the target problem, that is, deciding the winner for each entrance on a given string diagram $\mathbb{D}$ whose operational semantics is a PG (oPG that has no exits).

Problem Statement: Let $\mathbb{D}$ be a string diagram such that the operational semantics $\llbracket\mathbb{D}\rrbracket$ can be naturally considered as a PG, that is, $\llbracket\mathbb{D}\rrbracket$ has no exits. Compute the winning region $(W_{\exists},W_{\forall})$ on entrances $I^{\llbracket\mathbb{D}\rrbracket}$ , that is, decide the winner of each entrance.

$\blacktriangleright$ Remark 6 (trace operator).

In [43, 44, 45], we support the trace operator that makes loops by connecting exits to the corresponding entrances, respectively. We can encode the trace operator by the (bidirectional) sequential composition and the sum, as in [46, 47].

3 Denotations, Optimal Strategies, and Pareto Fronts

In this section, we recap denotations [43] and introduce Pareto fronts for oPGs, which are a compositional extension of winning and losing for PGs.

3.1 Denotation of Open Parity Games

Strategies and plays in oPGs are defined in exactly the same way as in PGs; note that oPGs are PGs with open ends. Unlike PGs, where the winning condition is qualitative, the winning condition in oPGs is quantitative due to the openness of oPGs, which induces pending states between two extremes of winning and losing. Specifically, we show denotations of oPGs [43] with denotations of plays and entrances. Given a play $p$ , the denotation $\llparenthesis p\rrparenthesis$ of the play $p$ is winning ( $\top$ ), losing ( $\bot$ ), or reaching an exit $o$ with the priority $m$ that is the maximum priority that occurred during the play. Importantly, all exits are sinks, meaning that once we enter an exit, we stay there forever.

Definition 7 (domain).

Let $\mathcal{A}$ be an oPG. The domain $\mathcal{D}_{\mathcal{A}}$ of $\mathcal{A}$ is the set $\mathcal{D}_{\mathcal{A}}:=\{\bot,\top\}\cup\{(o,m)\mid\text{$o$ is an exit $(% o\in O^{\mathcal{A}})$},\ m\text{ is a priority }(m\in\mathbb{P})\}$ .

Definition 8 (denotation of play).

Let $p=(v_{j})_{j\in\mathbb{N}}$ be a (necessarily infinite) play on an oPG $\mathcal{A}$ . The denotation $\llparenthesis p\rrparenthesis\in\mathcal{D}_{\mathcal{A}}$ of $p$ is given by the following:

\displaystyle\llparenthesis p\rrparenthesis:=\begin{cases}\top&\text{ if $v_{j% }\not\in O^{\mathcal{A}}$ for any $j\in\mathbb{N}$, and $p$ satisfies the % parity condition,}\\ (o,m)&\text{ if $v_{j}=o\in O^{\mathcal{A}}$ for some $j\in\mathbb{N}$,}\\ &\text{ and $m:=\max\big{\{}\Omega\big{(}(v_{k},v_{k+1})\big{)}\ \big{|}\ k\in% \{1,\dots,j-1\}\big{\}}$, }\\ \bot&\text{ if $v_{j}\not\in O^{\mathcal{A}}$ for any $j\in\mathbb{N}$, and $p% $ does not satisfy the parity condition.}\end{cases}

Note that the condition in the second case distinction is well-defined because we assume every exit is a sink state (Def. 2).

The denotation $\llparenthesis i\rrparenthesis$ of an entrance $i$ is the set of denotations of plays from $i$ that are induced by $\exists$ - and $\forall$ -strategies. Specifically, for each $\exists$ -strategy $\sigma_{\exists}$ , the denotation $\llparenthesis i\rrparenthesis$ contains the set of denotations $\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ of plays $p_{\sigma_{\exists},\sigma_{\forall};i}$ that are induced by some $\forall$ -strategy $\sigma_{\forall}$ . Note that $\sigma_{\exists}$ and $\sigma_{\forall}$ may not be positional.

Definition 9 (denotation of entrance).

Let $\mathcal{A}$ be an oPG and $i$ be an entrance. The denotation $\llparenthesis i\rrparenthesis$ is given by

\displaystyle\llparenthesis i\rrparenthesis:=\Big{\{}\big{\{}\llparenthesis p_% {\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis\ \big{|}\ \text{$\sigma_{% \forall}$ is a $\forall$-strategy}\big{\}}\ \Big{|}\ \text{$\sigma_{\exists}$ % is an $\exists$-strategy}\Big{\}}.

We call the entrance $i$ winning if $\{\top\}\in\llparenthesis i\rrparenthesis$ , losing if $\bot\in T$ holds for any $T\in\llparenthesis i\rrparenthesis$ , and pending otherwise.

The denotations of entrances are indeed a compositional extension of winning regions of PGs: in fact, for oPG $\mathcal{A}$ with no exits, the entrance is winning if $\{\top\}\in\llparenthesis i\rrparenthesis$ , which is consistent with winning regions on PGs, and otherwise the entrance is losing.

Definition 10 (denotation of oPGs [43]).

Let $\mathcal{A}$ be an oPG. The denotation $\llparenthesis\mathcal{A}\rrparenthesis$ of $\mathcal{A}$ is the indexed family $\big{(}\llparenthesis i\rrparenthesis\big{)}_{i\in I^{\mathcal{A}}}$ of denotations of entrances.

Example 11.

Consider the oPG $\mathcal{C}\colon(1,1)\rightarrow(1,0)$ presented in Fig. 3. Since there is the unique entrance $i_{\mathbf{r},1}$ , the denotation $\llparenthesis\mathcal{C}\rrparenthesis$ is essentially same as the denotation $\llparenthesis i_{\mathbf{r},1}\rrparenthesis$ . Every play that starts from the entrance reaches the node $c$ : if Player $\exists$ decides to move the exit $o_{\mathbf{r},1}$ , then the denotation of the play is $(o_{\mathbf{r},1},1)$ , and otherwise, the play reaches the node $d$ . By similar arguments, we can conclude that the denotation $\llparenthesis i_{\mathbf{r},1}\rrparenthesis$ is the following:

	$\displaystyle\llparenthesis i_{\mathbf{r},1}\rrparenthesis=\Big{\{}$	$\displaystyle\big{\{}(o_{\mathbf{r},1},1)\big{\}},\,\big{\{}(o_{\mathbf{r},1},% 2),(o_{\mathbf{r},1},3),(o_{\mathbf{l},1},1),(o_{\mathbf{l},1},3),\bot\big{\}}% ,\,\big{\{}(o_{\mathbf{r},1},2),(o_{\mathbf{r},1},3),(o_{\mathbf{l},1},1)\big{% \}},\,$
		$\displaystyle\big{\{}(o_{\mathbf{r},1},2),(o_{\mathbf{r},1},3),(o_{\mathbf{l},% 1},1),(o_{\mathbf{l},1},3)\big{\}}\Big{\}}.$

$\blacktriangleright$ Remark 12.

Our denotation of entrances implicitly requires that an $\exists$ -strategy $\sigma_{\exists}$ is always chosen at first, and later a $\forall$ -strategy is chosen with respect to $\sigma_{\exists}$ . This order of choices by Players $\exists$ and $\forall$ does not matter for parity games because parity games are positionally determined [15, 16].

3.2 Optimal Strategies of Open Parity Games

For deciding the winning region of the entrances in the operational semantics $\llbracket\mathbb{D}\rrbracket$ , as stated in Section 2.2, the denotation $\llparenthesis\mathcal{A}\rrparenthesis$ defined in Def. 10 may contain redundant information: for example, suppose we fix an $\exists$ -strategy $\sigma_{\exists}$ . If there is a $\forall$ -strategy $\sigma_{\forall}$ such that $\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis:=\bot$ , that is, the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ is losing for Player $\exists$ , then we can exclude other $\forall$ -strategies $\tau_{\forall}$ because choosing $\sigma_{\forall}$ is optimal for Player $\forall$ when Player $\exists$ chooses $\sigma_{\exists}$ . We generalize this elimination of sub-optimal strategies by introducing orders on plays and strategies.

Specifically, we use the sub-priority order [22, 4] on priorities: the intuition is that Player $\exists$ favors larger even priorities, and Player $\forall$ favors larger odd priorities.

Definition 13 (sub-priority order [22, 4]).

The sub-priority order $\preceq_{\mathbb{P}}$ on the set $\mathbb{P}$ of priorities is the total order defined by $M-1\prec_{\mathbb{P}}M-3\prec_{\mathbb{P}}\dots\prec_{\mathbb{P}}1\prec_{% \mathbb{P}}0\prec_{\mathbb{P}}2\prec_{\mathbb{P}}\dots\prec_{\mathbb{P}}M-2% \prec_{\mathbb{P}}M$ . Recall that we assume that the maximum priority $M$ is even.

$\blacktriangleright$ Remark 14.

The existing semantics [24, 43] uses the trivial discrete order on the set $\mathbb{P}$ , that is, $m_{1}\preceq_{\mathbb{P}}m_{2}$ iff $m_{1}=m_{2}$ . This difference is crucial for our development.

The operation $\max\colon\mathbb{P}\times\mathbb{P}\rightarrow\mathbb{P}$ that returns a bigger number with respect to the standard order on natural numbers is (also) monotone with respect to the sub-priority order.

Lemma 15 (monotonicity [40]).

Let $m_{1},m_{2},m_{3}\in\mathbb{P}$ . If the inequality $m_{1}\preceq_{\mathbb{P}}m_{2}$ holds, then the inequality $\max(m_{1},m_{3})\preceq_{\mathbb{P}}\max(m_{2},m_{3})$ holds.

We extend the sub-priority order to a partial order on the domain $\mathcal{D}_{\mathcal{A}}$ considering exits.

Definition 16 (domain order).

The domain order $\preceq_{\mathbf{D}}$ on the domain $\mathcal{D}_{\mathcal{A}}$ (defined in Def. 7) is the partial order such that $d_{1}\preceq_{\mathbf{D}}d_{2}$ iff (i) $d_{1}=\bot$ , (ii) $d_{2}=\top$ , or (iii) $d_{1}:=(o_{1},m_{1})$ and $d_{2}:=(o_{2},m_{2})$ such that $o_{1}=o_{2}$ and $m_{1}\preceq_{\mathbb{P}}m_{2}$ .

Given an $\exists$ -strategy $\sigma_{\exists}$ , we define optimal $\forall$ -strategies w.r.t. $\sigma_{\exists}$ as $\forall$ -strategies that induce plays whose denotations are minimal.

Definition 17 (minimal).

For a set $T\subseteq\mathcal{D}_{\mathcal{A}}$ , the set $T^{\mathrm{min}}$ is the set of minimal elements in $T$ w.r.t. the domain order $\preceq_{\mathbf{D}}$ .

Definition 18 (optimal $\forall$ -strategy).

Let $\mathcal{A}$ be an oPG, $i$ be an entrance, and $\sigma_{\exists}$ be an $\exists$ -strategy. A $\forall$ -strategy $\sigma_{\forall}$ is optimal on $i$ w.r.t. $\sigma_{\exists}$ if the following condition holds:

\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis\in\big{\{% }\llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}\rrparenthesis\ \big{|}\ % \tau_{\forall}\text{ is a $\forall$-strategy}\big{\}}^{\mathrm{min}}.

We further define optimal $\exists$ -strategies; here we do not fix a $\forall$ -strategy. Specifically, we use the upper preorder [1].

Definition 19 (upper preorder [1]).

The upper preorder $\preceq_{\mathbf{U}}$ on the powerset $\mathcal{P}(\mathcal{D}_{\mathcal{A}})$ of $\mathcal{D}_{\mathcal{A}}$ is given by $T_{1}\preceq_{\mathbf{U}}T_{2}$ if for any $d_{2}\in T_{2}$ , there is $d_{1}\in T_{1}$ such that $d_{1}\preceq_{\mathbf{D}}d_{2}$ .

The intuition is the following: we fix an entrance $i$ and suppose that there are two $\exists$ -strategies $\sigma_{\exists}$ and $\tau_{\exists}$ . The $\exists$ -strategy $\sigma_{\exists}$ is “better” than $\tau_{\exists}$ if for any $\forall$ -strategy $\sigma_{\forall}$ , there is a $\forall$ -strategy $\tau_{\forall}$ such that $p_{\tau_{\exists},\tau_{\forall};i}\preceq_{\mathbf{P}}p_{\sigma_{\exists},% \sigma_{\forall};i}$ .

Definition 20 (maximal).

For a set $S\subseteq\mathcal{P}(\mathcal{D}_{\mathcal{A}})$ , the set $S^{\mathrm{max}}$ is the set of maximal elements in $S$ w.r.t. the upper preorder $\preceq_{\mathbf{U}}$ .

Definition 21 (optimal $\exists$ -strategy).

Let $\mathcal{A}$ be an oPG, and $i$ be an entrance. An $\exists$ -strategy $\sigma_{\exists}$ is optimal on $i$ if the following condition holds:

\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis\ % \big{|}\ \text{a $\forall$-strategy }\sigma_{\forall}\big{\}}^{\mathrm{min}}% \in\Big{\{}\big{\{}\llparenthesis p_{\tau_{\exists},\tau_{\forall};i}% \rrparenthesis\ \big{|}\ \text{a $\forall$-strategy }\tau_{\forall}\big{\}}^{% \mathrm{min}}\ \Big{|}\ \text{an $\exists$-strategy }\tau_{\exists}\Big{\}}^{% \mathrm{max}}.

We show an example of optimal $\exists$ -strategies in Example 25 later.

3.3 Pareto Fronts of Open Parity Games

We conclude this section by introducing Pareto fronts of oPGs. Roughly speaking, Pareto fronts are the set of results that are induced by optimal strategies.

Definition 22 (results, result order [22]).

Let $\mathcal{A}$ be an oPG. The set $\mathbf{R}_{\mathcal{A}}$ of results is the set of non-empty antichains $\mathbf{r}$ on the domain $\mathcal{D}_{\mathcal{A}}$ , that is, $\mathbf{r}\subseteq\mathcal{D}_{\mathcal{A}}$ and $\mathbf{r}^{\mathrm{min}}=\mathbf{r}$ . The result order $\preceq_{\mathbf{R}_{\mathcal{A}}}$ on $\mathbf{R}_{\mathcal{A}}$ is the partial order that is given by the upper preorder $\preceq_{\mathbf{U}}$ .

The result order is indeed a partial order because of the minimality of results.

Proposition 23.

The result order is a partial order.

Proof.

Suppose that $\mathbf{r}\preceq_{\mathbf{R}_{\mathcal{A}}}\mathbf{r}^{\prime}$ and $\mathbf{r}^{\prime}\preceq_{\mathbf{R}_{\mathcal{A}}}\mathbf{r}$ . It suffices to prove that $\mathbf{r}\subseteq\mathbf{r}^{\prime}$ due to the symmetry of $\mathbf{r}$ and $\mathbf{r}^{\prime}$ . For any $d_{1}\in\mathbf{r}$ , there is $d_{2}\in\mathbf{r}^{\prime}$ such that $d_{2}\preceq_{\mathbf{D}}d_{1}$ . Similarly, there is $d_{3}\in\mathbf{r}$ such that $d_{3}\preceq_{\mathbf{D}}d_{2}$ . Thus, we have $d_{3}\preceq_{\mathbf{D}}d_{1}$ and we see $d_{3}=d_{1}$ due to the minimality of $\mathbf{r}$ . Thus, $d_{1}=d_{2}=d_{3}$ holds and $\mathbf{r}\subseteq\mathbf{r}^{\prime}$ holds. $\hfill\blacktriangleleft$ We finally define Pareto fronts of oPGs by optimal $\exists$ - and $\forall$ -strategies.

Definition 24 (Pareto front, Pareto-optimal).

Let $\mathcal{A}$ be an oPG, and $i$ be an entrance. The Pareto front $\mathcal{S}(\mathcal{A},i)$ is the set of denotations of plays that are induced by optimal $\exists$ -strategies and optimal $\forall$ -strategies on $i$ , that is,

\displaystyle\mathcal{S}(\mathcal{A},i):=\Big{\{}\big{\{}\llparenthesis p_{% \sigma_{\exists},\sigma_{\forall};i}\rrparenthesis\ \big{|}\ \sigma_{\forall}% \text{ is a $\forall$-strategy}\big{\}}^{\mathrm{min}}\ \Big{|}\ \sigma_{% \exists}\text{ is an $\exists$-strategy}\Big{\}}^{\mathrm{max}}\subseteq% \mathbf{R}_{\mathcal{A}}.

We call results $\mathbf{r}$ in $\mathcal{S}(\mathcal{A},i)$ Pareto-optimal. We write $\mathcal{S}(\mathcal{A})$ for the indexed family $\big{(}\mathcal{S}(\mathcal{A},i)\big{)}_{i\in I^{\mathcal{A}}}$ of Pareto fronts. Note that $\mathcal{S}(\mathcal{A},i)\not=\emptyset$ and $\emptyset\not\in\mathcal{S}(\mathcal{A},i)$ hold by definition.

Example 25.

Consider the oPG $\mathcal{C}\colon(1,1)\rightarrow(1,0)$ presented in Fig. 3. The denotation $\llparenthesis i_{\mathbf{r},1}\rrparenthesis$ contains $\big{\{}(o_{\mathbf{r},1},2),(o_{\mathbf{r},1},3),(o_{\mathbf{l},1},1)\big{\}}$ . Since $(o_{\mathbf{r},1},3)\preceq_{\mathbf{D}}(o_{\mathbf{r},1},2)$ , we have a result $\big{\{}(o_{\mathbf{r},1},2),(o_{\mathbf{r},1},3),(o_{\mathbf{l},1},1)\big{\}}% ^{\mathrm{min}}=\big{\{}(o_{\mathbf{r},1},3),(o_{\mathbf{l},1},1)\big{\}}$ . This result is not Pareto-optimal because the inequality $\big{\{}(o_{\mathbf{r},1},3),(o_{\mathbf{l},1},1)\big{\}}\preceq_{\mathbf{U}}% \big{\{}(o_{\mathbf{r},1},1)\big{\}}$ holds, where $\big{\{}(o_{\mathbf{r},1},1)\big{\}}\in\llparenthesis i_{\mathbf{r},1}\rrparenthesis$ . By continuing similar arguments, we can show that the Pareto front $\mathcal{S}(\mathcal{C},i_{\mathbf{r},1})$ is $\Big{\{}\big{\{}(o_{\mathbf{r},1},1)\big{\}}\Big{\}}.$ Thus, an optimal $\exists$ -strategy on $\mathcal{C}$ is positionally moving from $c$ to $o_{\mathbf{r},1}$ .

$\blacktriangleright$ Remark 26 (meager semantics).

In [45], we introduce meager semantics to eliminate sub-optimal strategies. Meager semantics is defined globally, meaning that optimal strategies are uniformly defined over entrances. Pareto fronts are defined locally, with optimal strategies tailored specifically for each entrance. This locality is essential for our technical development in Sections 4 and 5.

Pareto fronts of oPGs characterise the winning condition of oPGs defined in Def. 9.

Lemma 27.

Let $\mathcal{A}$ be an oPG, and $i$ be an entrance. The Pareto front $\mathcal{S}(\mathcal{A},i)$ satisfies the following properties:

1.

the entrance $i$ is winning iff $\mathcal{S}(\mathcal{A},i)=\big{\{}\{\top\}\big{\}}$ ,
2.

the entrance $i$ is losing iff $\mathcal{S}(\mathcal{A},i)=\big{\{}\{\bot\}\big{\}}$ , and
3.

the entrance $i$ is pending iff for any $T\in\mathcal{S}(\mathcal{A},i)$ , $\top,\bot\not\in T$ , and for any $(o_{1},m_{1}),(o_{2},m_{2})\in T$ , if $o_{1}=o_{2}$ , then $m_{1}=m_{2}$ .

Proof.

Suppose that the entrance $i$ is winning. By definition, $\{\top\}\in\llparenthesis i\rrparenthesis$ holds. Since $\{\top\}$ is the greatest element, $\mathcal{S}(\mathcal{A},i)=\big{\{}\{\top\}\big{\}}$ .

Suppose that the entrance $i$ is losing. By definition, $\bot\in T$ holds for any $T\in\llparenthesis i\rrparenthesis$ . This means that for any optimal $\forall$ -strategy $\sigma_{\forall}$ of a given $\exists$ -strategy $\sigma_{\exists}$ , the denotation $\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ is $\bot$ because $\bot$ is the least element in the domain, which proves $\mathcal{S}(\mathcal{A},i)=\big{\{}\{\bot\}\big{\}}$ .

Suppose that the entrance $i$ is pending. For any $T\in\mathcal{S}(\mathcal{A},i)$ , $\top\not\in T$ because $\top$ is the greatest element. Similarly, $\bot\not\in T$ because $T=\{\bot\}$ leads to the contradiction. If $(o,m_{1}),(o,m_{2})\in T$ , $m_{1}=m_{2}$ holds because of the minimality of $T$ . $\hfill\blacktriangleleft$

By the characterisation shown in Lem. 27, it suffices to compute the Pareto fronts of operational semantics of string diagrams of parity games for solving our target problem shown in Section 2.2. We thus extend our target problem as follows:

Compositional Problem Statement: Let $\mathbb{D}$ be a string diagram of PGs, and $i$ be an entrance. Compute the Pareto front $\mathcal{S}(\llbracket\mathbb{D}\rrbracket,i)$ of the operational semantics $\llbracket\mathbb{D}\rrbracket$ .

4 Solving Open Parity Games

In this section, we prove the positional determinacy of Pareto fronts through a novel translation from an oPG to a PG specified by a given query, a method we call the loop construction. Utilizing the loop construction, we provide a simple algorithm for computing Pareto fronts. Additionally, we present an analysis of the upper-bound of its time complexity.

4.1 Positional Determinacy of Pareto Fronts

We begin by stating the positional determinacy of Pareto fronts: positional strategies suffice to determine Pareto fronts.

Theorem 28 (positional determinacy).

Pareto fronts are positionally determined, that is, for any entrance $i$ , the following equality holds:

\displaystyle\mathcal{S}(\mathcal{A},i)=\Big{\{}\big{\{}\llparenthesis p_{% \sigma_{\exists},\sigma_{\forall};i}\rrparenthesis\ \big{|}\ \text{a % positional $\forall$-strategy }\sigma_{\forall}\big{\}}^{\mathrm{min}}\ \Big{|% }\ \text{a positional $\exists$-strategy }\sigma_{\exists}\Big{\}}^{\mathrm{% max}}.

Once we establish the positional determinacy of Pareto fronts, it becomes clear that solving Pareto fronts is decidable through the enumeration of all positional strategies.

We use the following weaker property for proving Thm. 28.

Lemma 29.

Let $\mathcal{A}$ be an oPG, $i$ be an entrance, and $\sigma_{\exists}$ be a positional $\exists$ -strategy. Then, positional $\forall$ -strategies suffice, that is, the following equality holds:

\displaystyle\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}% \rrparenthesis\ \big{|}\ \sigma_{\forall}\text{ is a $\forall$-strategy}\big{% \}}^{\mathrm{min}}=\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall}% ;i}\rrparenthesis\ \big{|}\ \sigma_{\forall}\text{ is a positional $\forall$-% strategy}\big{\}}^{\mathrm{min}}.

Proof.

We take a (finite) oPG $\mathcal{A}[\sigma_{\exists}]$ that is induced by the positional $\exists$ -strategy $\sigma_{\exists}$ ; the nodes and edges of $\mathcal{A}[\sigma_{\exists}]$ are the same of $\mathcal{A}$ , except the edges from nodes of Player $\exists$ are determined by $\sigma_{\exists}$ . Take an optimal $\forall$ -strategy $\sigma_{\forall}$ on $\mathcal{A}[\sigma_{\exists}]$ from $i$ , which is also optimal on $\mathcal{A}$ w.r.t. $\sigma_{\exists}$ . If the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ is losing, then there is a positional optimal $\forall$ strategy by the positional determinacy of PGs.

Suppose that the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ reaches an exit $o$ . We write the sequence $v_{1},v_{2},\dots,v_{n}$ of nodes for the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ , where $n$ is the smallest index such that $v_{n}=o$ . If the equality $v_{j}=v_{j}$ implies $i=j$ , then we can easily construct a positional $\forall$ -strategy $\tau_{\forall}$ such that $p_{\sigma_{\exists},\sigma_{\forall};i}=p_{\sigma_{\exists},\tau_{\forall};i}$ .

The remaining case is that there are $v_{i}=v_{j}$ such that $i\not=j$ . Since $\sigma_{\exists}$ is positional, we can assume that $v_{i}$ and $v_{j}$ are owned by Player $\forall$ : if every $v_{i}=v_{j}$ such that $i\not=j$ is owned by Player $\exists$ , it will not reach an exit, which leads to the contradiction. We assume that $i<j$ without loss of generality. If the maximum priority $m$ occurs in $v_{i},\dots,v_{j}$ is odd, then it contradicts to the fact that $\sigma_{\forall}$ is optimal. If the maximum priority $m$ occurs in $v_{i},\dots,v_{j}$ is even, then the shortcut play $p:=v_{1},\dots,v_{i},v_{j+1},\dots,v_{n}$ has the same denotation. In fact, if the maximum priority in $p_{\sigma_{\exists},\sigma_{\forall};i}$ is $m$ , then the maximum priority in $p$ is also $m$ ; otherwise, it contradicts to the fact that $\sigma_{\forall}$ is optimal. If the maximum priority in $p_{\sigma_{\exists},\sigma_{\forall};i}$ is strictly greater than $m$ , then the denotation of $p$ does not change because removing $v_{i+1},\dots,v_{j}$ does not matter. By iterating this shortcut construction, we can finally obtain a play $p^{\prime}=v^{\prime}_{1},\dots,v^{\prime}_{l}$ such that $v^{\prime}_{i}=v^{\prime}_{j}$ implies $i=j$ and the equality $\llparenthesis p^{\prime}\rrparenthesis=\llparenthesis p_{\sigma_{\exists},% \sigma_{\forall};i}\rrparenthesis$ holds in finite steps. Thus, we can construct a positional $\forall$ -strategy $\tau_{\forall}$ such that $\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis=% \llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}\rrparenthesis$ . $\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 30.

The assumption that the $\exists$ -strategy $\sigma_{\exists}$ in Lem. 29 is positional is indispensable. Consider the oPG shown in Fig. 3, and an $\exists$ -strategy such that the Player $\exists$ repeatedly moves from $c$ to $d$ until she reaches $c$ twice, and then moves to $o_{\mathbf{r},1}$ . Then there is an optimal $\forall$ -strategy that moves first from $b$ to $a$ , and later from $b$ to $o_{\mathbf{l},1}$ , which is not positional.

4.2 The Loop Construction and the Algorithm

In this section, we introduce our loop construction and we prove the positional determinacy of Pareto fronts. The parameter of the loop construction is a pair of an entrance and a query for oPGs. Informally, we show that positional strategies are sufficient to achieve any Pareto-optimal result on the Pareto front, and with the loop construction they can be specified by “minimal” queries, the number of which is finite. In addition, we present a simple but efficient algorithm based on the loop construction, which shows improvements over our previous algorithm [45].

Definition 31 (query).

Let $\mathcal{A}$ be an oPG. A query²²2We call $q$ query because $q$ asks whether there is an $\exists$ -strategy that leads to a better result than the dual of $q$ (see Lem. 38). $q$ is a function $q\colon O^{\mathcal{A}}\rightarrow\mathbb{P}\uplus\{\bot\}$ . We write $\mathbb{Q}_{\mathcal{A}}$ for the set of queries on $\mathcal{A}$ .

Figure 4: The loop constructions

\mathbb{G}(\mathcal{A},i_{1},q_{1})

and

\mathbb{G}(\mathcal{A},i_{1},q_{2})

that add white edges, where queries

q_{1},q_{2}

are given by (i)

q_{1}(o_{1}):=3

and

q_{1}(o_{2}):=\bot

, and (ii)

q_{2}(o_{1}):=0

and

q_{2}(o_{2}):=2

.

Given an oPG $\mathcal{A}$ , a pair $(i,q)$ of an entrance $i$ and a query $q$ induces a PG $\mathbb{G}(\mathcal{A},i,q)$ by the loop construction.

Definition 32 (loop construction).

Let $\mathcal{A}:=(\mathcal{G}^{\mathcal{A}},\mathsf{IO}^{\mathcal{A}})$ be an oPG, $i$ be an entrance, and $q$ be a query. The loop construction $\mathbb{G}(\mathcal{A},i,q)$ builds a PG $(V^{\mathcal{A}},V^{\mathcal{A}}_{\exists},V^{\mathcal{A}}_{\forall},E,\Omega)$ , where $E$ is the least relation and $\Omega$ is the function such that

	$\displaystyle\big{(}(v,v^{\prime})\in E^{\mathcal{A}}\text{ and }v\not\in O^{% \mathcal{A}}\big{)}\Longrightarrow\big{(}(v,v^{\prime})\in E,\text{ and }\ % \Omega(v,v^{\prime}):=\Omega^{\mathcal{A}}(v,v^{\prime})\big{)},$
	$\displaystyle\big{(}o\in O^{\mathcal{A}}\text{ and }q(o)\in\mathbb{P}\big{)}% \Longrightarrow\big{(}(o,i)\in E,\text{ and }\ \Omega(o,i):=q(o)\big{)},\text{% and }$
	$\displaystyle\big{(}o\in O^{\mathcal{A}}\text{ and }q(o)=\bot\big{)}% \Longrightarrow\big{(}(o,o)\in E,\text{ and }\ \Omega(o,o):=1\big{)}.$

We present two examples in Fig. 4: for each exit $o$ , the loop construction $\mathbb{G}(\mathcal{A},i,q)$ adds (i) an edge to the specified entrance $i$ whose assigned priority is $q(o)$ , or (ii) makes a self loop with the priority $1$ if $q(o)=\bot$ .

The loop construction is closely related with Pareto fronts of oPGs via dual of queries. Firstly, we extend the sub-priority order $\preceq_{\mathbb{P}}$ to the functorial order of queries. We write $\preceq_{\overline{\mathbb{P}}}$ for the total order on $\mathbb{P}\uplus\{\top,\bot\}$ such that $m\preceq_{\overline{\mathbb{P}}}m^{\prime}$ iff (i) $m$ is the least element $\bot$ , (ii) $m\preceq_{\mathbb{P}}m^{\prime}$ , or (iii) $m^{\prime}$ is the greatest element $\top$ .

Definition 33 (query order).

Let $\mathcal{A}$ be an oPG. The query order $\preceq_{\mathbb{Q}_{\mathcal{A}}}$ on $\mathbb{Q}_{\mathcal{A}}$ is the functorial order w.r.t. the (restricted) total order $\preceq_{\overline{\mathbb{P}}}$ on $\mathbb{P}\uplus\{\bot\}$ , that is, the inequality $q\preceq_{\mathbb{Q}_{\mathcal{A}}}q^{\prime}$ holds if $q(o)\preceq_{\overline{\mathbb{P}}}q^{\prime}(o)$ for each $o\in O^{\mathcal{A}}$ .

Given a query $q$ and assuming $q(o)=m\in\mathbb{P}$ , the dual $m^{d}$ of $m$ , which is also called the left-residual of $0$ in [40], reveals the relationship between queries and Pareto fronts. We define the dual $m^{d}$ as the lowest priority such that priorities that occur infinitely often are only $m$ and $m^{d}$ , and it satisfies the parity condition (see Lem. 35).

Definition 34 (dual).

Let $m\in\mathbb{P}$ . The dual $m^{d}\in\mathbb{P}$ is given by (i) $m^{d}:=m+1$ if $m$ is odd, (ii) $m^{d}:=0$ if $m=0$ , and (iii) $m^{d}:=m-1$ if $m$ is even and $m>0$ .

Lemma 35 ([40]).

Let $m,m^{\prime}\in\mathbb{P}$ . The max priority $\max(m,m^{\prime})$ is even iff $m^{d}\preceq_{\mathbb{P}}m^{\prime}$ .

We define the dual of queries based on the dual of priorities.

Definition 36 (dual of query).

Let $\mathcal{A}$ be an oPG, $i$ be an entrance, and $q$ be a query. The dual $r(q)$ of the query $q$ is the result $r(q)\in\mathbf{R}_{\mathcal{A}}$ that is defined as follows:

$\blacksquare$

if $q(o)=\bot$ for any $o\in O^{\mathcal{A}}$ , then $r(q):=\{\top\}$ , and
$\blacksquare$

otherwise, $r(q):=\{(o,q(o)^{d})\mid o\in O^{\mathcal{A}},q(o)\in\mathbb{P}\}$ .

Note that for any result $\mathbf{r}\in\mathbf{R}_{\mathcal{A}}$ unless $\mathbf{r}=\{\bot\}$ , there is a query $q$ such that $r(q)=\mathbf{r}$ .

Lemma 37 (duality).

Let $\mathcal{A}$ be an oPG, $i$ be an entrance, and $q,q^{\prime}$ be queries. The equality $q=q^{\prime}$ holds iff the equality $r(q)=r(q^{\prime})$ holds. Moreover, the inequality $q\preceq_{\mathbb{Q}_{\mathcal{A}}}q^{\prime}$ holds iff the inequality $r(q)\succeq_{\mathbf{R}_{\mathcal{A}}}r(q^{\prime})$ holds.

Proof.

Clearly, the equality $q=q^{\prime}$ holds iff the equality $r(q)=r(q^{\prime})$ holds.

Suppose that $q\preceq_{\mathbb{Q}_{\mathcal{A}}}q^{\prime}$ holds. Then, either $q(o)=\bot$ or $q(o)\preceq_{\mathbb{P}}q^{\prime}(o)$ hold for each $o\in O$ . For any $(o,m)\in r(q)$ , the equality $m=q(o)^{d}$ holds by definition, and $q^{\prime}(o)^{d}\preceq_{\mathbb{P}}m$ . We thus conclude $r(q)\succeq_{\mathbf{R}_{\mathcal{A}}}r(q^{\prime})$ . The converse direction holds in the same way. $\hfill\blacktriangleleft$ The lemma presented below is crucial for proving the correctness of the loop construction (Prop. 39). This, in turn, directly contributes to the proof of the positional determinacy of Pareto fronts.

Lemma 38.

Let $\mathcal{A}:=(\mathcal{G}^{\mathcal{A}},\mathsf{IO}^{\mathcal{A}})$ be an oPG, $i$ be an entrance, and $q$ be a query. Then, the following conditions are equivalent:

1.

the node $i$ on the PG $\mathbb{G}(\mathcal{A},i,q)$ is winning,
2.

there is a result $\mathbf{r}$ such that $r(q)\preceq_{\mathbf{R}_{\mathcal{A}}}\mathbf{r}$ and $\mathbf{r}\in\mathcal{S}(\mathcal{A},i)$ .

Proof.

Let $q(o)=\bot$ for any $o\in O^{\mathcal{A}}$ . Since $r(q):=\{\top\}$ is the greatest element, it suffices to prove that the following conditions are equivalent:

1.

the node $i$ on the PG $\mathbb{G}(\mathcal{A},i,q)$ is winning,
2.

$\mathcal{S}(\mathcal{A},i)=\big{\{}\{\top\}\big{\}}$ .

Suppose Item 1 holds, then there is an optimal $\exists$ -strategy such that every play that is induced by a $\forall$ -strategy can not reach any exit $o\in O^{\mathcal{A}}$ because of the loop construction: every exit has a self-loop with the priority $1$ . Therefore, the optimal $\exists$ -strategy is also optimal for $\mathcal{A}$ from $i$ as well, and Item 2 holds. The converse direction holds by the same argument.

Let $q(o)\not=\bot$ for some $o\in O^{\mathcal{A}}$ . Suppose that the node $i$ on the $\mathbb{G}(\mathcal{A},i,q)$ is winning. Because of the positional determinacy of PGs, there is a winning positional $\exists$ -strategy $\sigma^{\exists}$ on $\mathbb{G}(\mathcal{A},i,q)$ . By Lem. 29, we only consider positional $\forall$ -strategies. For any positional $\forall$ -strategy $\tau^{\forall}$ on $\mathcal{A}$ , the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ that is induced by $\sigma_{\exists}$ and $\sigma_{\forall}$ satisfies the following condition: if $p_{\sigma_{\exists},\sigma_{\forall};i}$ does not reach any exits $o\in O^{\mathcal{A}}$ , then $p_{\sigma_{\exists},\sigma_{\forall};i}$ is winning. This is because $\sigma_{\exists}$ is winning on $\mathbb{G}(\mathcal{A},i,q)$ . If $p_{\sigma_{\exists},\sigma_{\forall};i}$ reaches an exit $o\in O^{\mathcal{A}}$ , then the maximal priority $m$ that occurs in $p_{\sigma_{\exists},\sigma_{\forall};i}$ until reaching $o$ satisfies that $\max\big{(}q(o),m\big{)}$ is even; here $q(o)\in\mathbb{P}$ because $\sigma_{\exists}$ is winning on $\mathbb{G}(\mathcal{A},i,q)$ . This is equivalent to $q(o)^{d}\preceq_{\mathbb{P}}m$ by Lem. 35. Thus, we conclude that $r(q)\preceq_{\mathbf{R}_{\mathcal{A}}}\big{\{}\llparenthesis p_{\sigma_{% \exists},\sigma_{\forall};i}\rrparenthesis\ \big{|}\ \sigma_{\forall}\text{ is% a $\forall$-strategy}\big{\}}^{\mathrm{min}}$ , which proves Item 2.

Conversely, suppose that there is a result $\mathbf{r}$ such that $r(q)\preceq_{\mathbf{R}_{\mathcal{A}}}\mathbf{r}$ and $\mathbf{r}\in\mathcal{S}(\mathcal{A},i)$ . Take an $\exists$ -strategy $\sigma_{\exists}$ such that $\mathbf{r}=\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}% \rrparenthesis\ \big{|}\ \sigma_{\forall}\text{ is a $\forall$-strategy}\big{% \}}^{\mathrm{min}}$ ; note that $\sigma_{\exists}$ may not be positional. Then, the $\exists$ -strategy $\sigma_{\exists}$ natually induces an $\exists$ -strategy $\sigma^{\prime}_{\exists}$ on $\mathbb{G}(\mathcal{A},i,q)$ that mimicks $\sigma_{\exists}$ . It is easy to show that the $\exists$ -strategy $\sigma^{\prime}_{\exists}$ is indeed winning by a similar argument. $\hfill\blacktriangleleft$

The following proposition is a direct consequence of Lemmas 37 and 38.

Proposition 39.

Let $\mathcal{A}$ be an oPG, $i$ be an entrance, and $q$ be a query. The following conditions are equivalent:

1.

the query $q$ is minimal such that the entrance $i$ on the PG $\mathbb{G}(\mathcal{A},i,q)$ is winning,
2.

the dual $r(q)$ is Pareto-optimal, that is, $r(q)\in\mathcal{S}(\mathcal{A},i)$ .

Finally, we prove the positional determinacy of Pareto fronts.

Proof of Thm. 28.

Suppose that the entrance $i$ of $\mathcal{A}$ is not losing, that is, $\mathcal{S}(\mathcal{A},i)\not=\big{\{}\{\bot\}\big{\}}$ . By Prop. 39 (and its proof), every Pareto-optimal result $\mathbf{r}$ induces the corresponding minimal query $q$ such that the PG $\mathbb{G}(\mathcal{A},i,q)$ is winning. Since the PG $\mathbb{G}(\mathcal{A},i,q)$ is positionally determined, there is a positional winning $\exists$ -strategy $\tau_{\exists}$ on $\mathbb{G}(\mathcal{A},i,q)$ ; we also regard $\tau_{\exists}$ as a positional $\exists$ -strategy on $\mathcal{A}$ . By Lem. 29, we only consider positional optimal $\forall$ -strategies $\tau_{\forall}$ w.r.t. $\tau_{\exists}$ . If the play $p_{\tau_{\exists},\tau_{\forall};i}$ does not reach an exit, then the play $p_{\tau_{\exists},\tau_{\forall};i}$ is winning. If the play $p_{\tau_{\exists},\tau_{\forall};i}$ reach an exit $o$ , then the equality $q(o)^{d}=m$ hold, where $m$ is the maximum priority that occurs in the play $p_{\tau_{\exists},\tau_{\forall};i}$ ; here we use the mimality of $q$ and $\tau_{\forall}$ . Thus, we can conclude that $\big{\{}\llparenthesis p_{\tau_{\exists},\sigma_{\tau};i}\rrparenthesis\ \big{% |}\ \tau_{\forall}\text{ is a positional $\forall$-strategy}\big{\}}^{\mathrm{% min}}=r(q)$ .

The case that the entrance $i$ of $\mathcal{A}$ is losing is easy to show. This is because of the positional determinacy of parity games. $\hfill\blacktriangleleft$

Algorithm and Time Complexity.

The positional determinacy of oPGs that is shown in Thm. 28 implies that solving oPGs is decidable by enumerating positional strategies. Furthermore, Prop. 39 suggests that there is an efficient algorithm based on the loop construction when the number of exists are small. Specifically, we evaluate whether the PG $\mathbb{G}(\mathcal{A},i,q)$ is winning for each query $q$ , and we keep only those minimal queries that are wininng, whose duals are Pareto-optimal. Notably, we can use well-studied algorithms of PGs to solve the PG $\mathbb{G}(\mathcal{A},i,q)$ without the need to enumerate positional strategies. Alg. 1 shows the details of our algorithm.

Algorithm 1 solveParetoFront: Solving Pareto fronts for oPGs.

Proposition 40.

Alg. 1 requires time $\mathcal{O}\big{(}(M+2)^{N}\cdot L+N\cdot(M+2)^{2N}\big{)}$ to compute the Pareto front $\mathcal{S}(\mathcal{A},i)$ of an oPG $\mathcal{A}$ and an entrance $i$ , where $N$ is the number of exits, $M$ is the largest priority, and $L$ is the required time for a given algorithm to solve PGs that are built by the loop construction.

Proof.

Since the number of queries $Q$ is $(M+2)^{N}$ , we solve PGs $Q$ times, which requires time $\mathcal{O}\big{(}Q\cdot L\big{)}$ . Removing sub-optimal results can be done in $\mathcal{O}\big{(}N\cdot Q^{2})$ by comparing all results: for comparing two results, we see exits at most $N$ times. $\hfill\blacktriangleleft$ Note that Alg. 1 requires an exponential memory to the number of exists since the size of Pareto fronts itself can be exponential. A variant of our previous algorithm [45], designed for open parity games, involves enumerating all positional strategies, the number of which is $\mathcal{O}\big{(}(M_{E})^{|V|}\big{)}$ , where $M_{E}$ represents the maximum number of the outgoing edges, and $V$ is the set of nodes. In contrast, Alg. 1 is exponential only in the number of exits, benefiting from the quasi-polymial-time algorithms for parity games (e.g. [10, 25, 19, 32]).

5 Solving String Diagrams of Parity Games

We apply Alg. 1 that solves oPGs for compositionally solving string diagrams of PGs.

For compositionally solving a given PG $\llbracket\mathbb{D}\rrbracket$ , which is defined in Def. 5, we translate Pareto fronts of oPGs into shortcut oPGs. A similar shortcut construction is introduced for MDPs [46], where there is the unique Player.

Definition 41 (shortcut oPG).

Let $\mathcal{A}:=(\mathcal{G}^{\mathcal{A}},\mathsf{IO}^{\mathcal{A}})$ be an oPG. The shortcut oPG $\mathcal{C}(\mathcal{A})$ of $\mathcal{A}$ is the oPG $(\mathcal{G},\mathsf{IO}^{\mathcal{A}})$ , where the parity game $\mathcal{G}:=(V,V_{\exists},V_{\forall},E,\Omega)$ is defined by

$\blacksquare$

$V:=\mathsf{IO}^{\mathcal{A}}\uplus\coprod_{i\in I^{\mathcal{A}}}\mathcal{S}(% \mathcal{A},i)$ , $V_{\exists}:=\mathsf{IO}^{\mathcal{A}}$ , and $V_{\forall}:=\coprod_{i\in I^{\mathcal{A}}}\mathcal{S}(\mathcal{A},i)$ , and
$\blacksquare$
we simultaneously define $E$ and $\Omega$ : for any $\mathbf{r}\in\mathcal{S}(\mathcal{A},i)$ , $\big{(}i,\mathbf{r}\big{)}\in E$ and $\Omega\big{(}i,\mathbf{r}\big{)}:=0$ , and for any $d\in\mathbf{r}$ ,
- –
  
  if $d=\top$ , then $(\mathbf{r},\mathbf{r})\in E$ and $\Omega(\mathbf{r},\mathbf{r}):=0$ ,
- –
  
  if $d=(o,m)$ , then $(\mathbf{r},o\big{)}\in E$ and $\Omega(\mathbf{r},o\big{)}:=m$ , and
- –
  
  if $d=\bot$ , then $(\mathbf{r},\mathbf{r})\in E$ and $\Omega(\mathbf{r},\mathbf{r}):=1$ .

Figure 5: The shortcut oPG

\mathcal{C}(\mathcal{A})

of an oPG

\mathcal{A}

whose Pareto front

\mathcal{S}(\mathcal{A},i_{\mathbf{r},1})

is

\Big{\{}\big{\{}(o_{\mathbf{l},1},1)\big{\}},\,\big{\{}(o_{\mathbf{r},1},1)% \big{\}},\,\big{\{}(o_{\mathbf{r},1},2),(o_{\mathbf{l},1},2)\big{\}}\Big{\}}

. We write

\mathbf{r}_{1}

,

\mathbf{r}_{2}

, and

\mathbf{r}_{3}

for

\{(o_{\mathbf{l},1},1)\}

,

\{(o_{\mathbf{r},1},1)\}

, and

\{(o_{\mathbf{r},1},2),(o_{\mathbf{l},1},2)\}

, respectively. Note that the entrance

i_{\mathbf{r},1}

is owned by Player

\exists

.

We present an example to illustrate this shortcut construction in Fig. 5. Given an oPG $\mathcal{A}$ and its Pareto fronts $\mathcal{S}(\mathcal{A})$ , the shortcut oPG $\mathcal{C}(\mathcal{A})$ is a summary of $\mathcal{A}$ , that is, it eliminates internal nodes in $\mathcal{A}$ , and keeps only optimal results that are stored in the Pareto fronts $\mathcal{S}(\mathcal{A})$ . This shortcut construction allows us to reuse the Pareto fronts for different appearances in a given string diagram with a reduced number of nodes.

Formally, the following two propositions ensure the correctness of this shortcut construction, that is, the compositionality of Pareto fronts with the shortcut construction.

Proposition 42.

Let $\mathcal{A}$ be an oPG. The Pareto front $\mathcal{S}(\mathcal{A},i)$ of $\mathcal{A}$ coincides with the Pareto front $\mathcal{S}(\mathcal{C}(\mathcal{A}),i)$ of the shortcut oPG $\mathcal{C}(\mathcal{A})$ .

Prop. 42 is easy to prove by the definition of the shortcut construction.

Proposition 43.

Let $\ast\in\{\fatsemi,\oplus\}$ , $\mathcal{A}\ast\mathcal{B}$ be an oPG, and $i$ be an entrance. The Pareto front $\mathcal{S}(\mathcal{A}\ast\mathcal{B},i)$ of $\mathcal{A}\ast\mathcal{B}$ coincides with the Pareto front $\mathcal{S}(\mathcal{C}(\mathcal{A})\ast\mathcal{C}(\mathcal{B}),i)$ of $\mathcal{C}(\mathcal{A})\ast\mathcal{C}(\mathcal{B})$ .

Proof Sketch.

For $\ast=\oplus$ , Prop. 43 is easy to prove because there is no interaction between $\mathcal{A}$ and $\mathcal{B}$ . For $\ast=\fatsemi$ , we focus on “entrance-dependent” strategies, and prove the monotonicity of entrance-dependent strategies. Furthermore, we can see that entrance-dependent $\forall$ -strategies suffice for entrance-dependent $\exists$ -strategies, like Lem. 29. Using these facts and the positional determinacy (Thm. 28), we can prove the compositionality of the Pareto front. We present formal definitions and proofs in Appendix A. $\hfill\blacktriangleleft$

Algorithm 2 solveStringDiagrams: Solving String Diagrams of PGs.

By Props 42 and 43, we can compositionally solve string diagrams for PGs: we show a pseudocode in Alg. 2. For a given string diagram $\mathbb{D}$ , we inductively solve $\mathbb{D}$ : for the base case, that is, $\mathbb{D}=\mathcal{A}$ , we directly apply Alg. 1 for $\mathcal{A}$ . For the step case, that is, $\mathbb{D}=\mathbb{D}_{1}\ast\mathbb{D}_{2}$ for $\ast\in\{\fatsemi,\oplus\}$ , we recursively solve $\mathbb{D}_{1}$ and $\mathbb{D}_{2}$ , and construct their shortcut oPGs. By Prop. 43, solving $\mathcal{S}(\mathcal{C}(\mathbb{D}_{1})\ast\mathcal{C}(\mathbb{D}_{2}))$ leads to the Pareto front of $\llbracket\mathbb{D}\rrbracket$ .

We remark that for a string diagram $\mathbb{D}$ such that $\llbracket\mathbb{D}\rrbracket$ has no exists, Alg. 2 runs in exponential-time, whereas monolithic algorithms – obtained by disregarding the compositional structure – can run in quasi-polynomial time (e.g. [10]). Nevertheless, Alg. 2 can reuse the solutions of individual components across multiple occurrences, which is particularly beneficial when the system contains duplicate subsystems. For instance, [46, 47] exploit such duplication to verify hierarchical systems, where reusability is key to achieving high performance.

6 Conclusion

We introduce Pareto fronts of oPGs as a multi-objective solution. Positional determinacy holds for our multi-objective solution of oPGs, which leads to our novel algorithm for solving open parity games with the loop construction. We propose the shortcut construction for open parity games, and we provide a compositional algorithm for string diagrams of parity games by composing Pareto fronts.

A future work is to support the mean-payoff objective, where we have to consider the sum of weights along plays. Although we expect that positional determinacy also holds for a similar semantics for open mean-payoff (or energy) games, the number of objectives may become huge because we believe that we have to consider the sum of weights along plays. This is challenging to achieve an efficient compositional algorithm for string diagrams of mean-payoff games. For this, we believe that an efficient approximation algorithm for Pareto fronts of open mean-payoff games is needed.

It would be interesting to investigate whether strategy improvement algorithms for parity games (e.g. [42, 33]) can be lifted to the setting of string diagrams of parity games. In this context, a strategy improvement algorithm for string diagrams would maintain a strategy throughout the iteration process – one that is not yet winning due to the openness of the system, but still encodes essential information for obtaining the compositional solution. Pursuing this direction and comparing our algorithm with such strategy improvement approaches is an exciting future direction.

Extending the diagrammatic language for parity games [37] to our semantics is another interesting future direction. In our work we use the sub-priority order on priorities, while they use the trivial discrete order on priorities. This difference is essential, since positional strategies are sufficient for our semantics, while they are not sufficient for their semantics (of oPGs).

References

[1] Samson Abramsky. Domain theory in logical form. In LICS, pages 47–53. IEEE Computer Society, 1987.
[2] John C Baez and Jason Erbele. Categories in control. arXiv preprint arXiv:1405.6881, 2014.
[3] John C. Baez, Fabrizio Genovese, Jade Master, and Michael Shulman. Categories of nets. In LICS, pages 1–13. IEEE, 2021. doi:10.1109/LICS52264.2021.9470566.
[4] Dietmar Berwanger, Anuj Dawar, Paul Hunter, and Stephan Kreutzer. Dag-width and parity games. In STACS, volume 3884 of Lecture Notes in Computer Science, pages 524–536. Springer, 2006. doi:10.1007/11672142_43.
[5] Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with Frobenius structure. J. ACM, 69(2):14:1–14:58, 2022. doi:10.1145/3502719.
[6] Filippo Bonchi, Joshua Holland, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Diagrammatic algebra: from linear to concurrent systems. Proc. ACM Program. Lang., 3(POPL):25:1–25:28, 2019. doi:10.1145/3290338.
[7] Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In POPL, pages 515–526. ACM, 2015. doi:10.1145/2676726.2676993.
[8] Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. The calculus of signal flow diagrams I: linear relations on streams. Inf. Comput., 252:2–29, 2017. doi:10.1016/J.IC.2016.03.002.
[9] Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-rational verification. In CONCUR, volume 243 of LIPIcs, pages 33:1–33:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.CONCUR.2022.33.
[10] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM J. Comput., 51(2):17–152, 2022. doi:10.1137/17M1145288.
[11] Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. On stochastic games with multiple objectives. In MFCS, volume 8087 of Lecture Notes in Computer Science, pages 266–277. Springer, 2013. doi:10.1007/978-3-642-40313-2_25.
[12] Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In LICS, pages 353–362. IEEE Computer Society, 1989. doi:10.1109/LICS.1989.39190.
[13] Bob Coecke and Ross Duncan. Interacting quantum observables. In ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages 298–310. Springer, 2008. doi:10.1007/978-3-540-70583-3_25.
[14] Bob Coecke and Aleks Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. doi:10.1017/9781316219317.
[15] E. Allen Emerson. Automata, tableaux and temporal logics (extended abstract). In Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79–88. Springer, 1985. doi:10.1007/3-540-15648-8_7.
[16] E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS, pages 368–377. IEEE Computer Society, 1991. doi:10.1109/SFCS.1991.185392.
[17] E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model checking for the $\mathrm{\mu}$ -calculus and its fragments. Theor. Comput. Sci., 258(1-2):491–522, 2001. doi:10.1016/S0304-3975(00)00034-7.
[18] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci., 4(4), 2008. doi:10.2168/LMCS-4(4:8)2008.
[19] John Fearnley, Sanjay Jain, Bart de Keijzer, Sven Schewe, Frank Stephan, and Dominik Wojtczak. An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. Int. J. Softw. Tools Technol. Transf., 21(3):325–349, 2019. doi:10.1007/S10009-019-00509-3.
[20] John Fearnley and Sven Schewe. Time and space results for parity games with bounded treewidth. Log. Methods Comput. Sci., 9(2), 2013. doi:10.2168/LMCS-9(2:6)2013.
[21] Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. Pareto curves for probabilistic model checking. In ATVA, volume 7561 of Lecture Notes in Computer Science, pages 317–332. Springer, 2012. doi:10.1007/978-3-642-33386-6_25.
[22] Koichi Fujima, Sohei Ito, and Naoki Kobayashi. Practical alternating parity tree automata model checking of higher-order recursion schemes. In APLAS, volume 8301 of Lecture Notes in Computer Science, pages 17–32. Springer, 2013. doi:10.1007/978-3-319-03542-0_2.
[23] Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn. Compositional game theory. In LICS, pages 472–481. ACM, 2018. doi:10.1145/3209108.3209165.
[24] Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order model-checking. In MFCS (1), volume 9234 of Lecture Notes in Computer Science, pages 256–268. Springer, 2015. doi:10.1007/978-3-662-48057-1_20.
[25] Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In LICS, pages 1–9. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005092.
[26] Roope Kaivola. Compositional model checking for linear-time temporal logic. In CAV, volume 663 of Lecture Notes in Computer Science, pages 248–259. Springer, 1992. doi:10.1007/3-540-56496-9_20.
[27] Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS, pages 179–188. IEEE Computer Society, 2009. doi:10.1109/LICS.2009.29.
[28] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.
[29] Orna Kupferman and Moshe Y. Vardi. Weak alternating automata and tree automata emptiness. In STOC, pages 224–233. ACM, 1998. doi:10.1145/276698.276748.
[30] Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38–65, 2013. doi:10.1016/J.IC.2013.10.001.
[31] Elena Di Lavore, Jules Hedges, and Pawel Sobocinski. Compositional modelling of network games. In CSL, volume 183 of LIPIcs, pages 30:1–30:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CSL.2021.30.
[32] Karoliina Lehtinen. A modal $\mu$ perspective on solving parity games in quasi-polynomial time. In LICS, pages 639–648. ACM, 2018. doi:10.1145/3209108.3209115.
[33] Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57(1-2):3–36, 2020. doi:10.1007/S00236-019-00349-3.
[34] Jan Obdrzálek. Fast mu-calculus model checking when tree-width is bounded. In CAV, volume 2725 of Lecture Notes in Computer Science, pages 80–92. Springer, 2003. doi:10.1007/978-3-540-45069-6_7.
[35] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.
[36] Christos H. Papadimitriou and Mihalis Yannakakis. On the approximability of trade-offs and optimal access of web sources. In FOCS, pages 86–92. IEEE Computer Society, 2000. doi:10.1109/SFCS.2000.892068.
[37] Robin Piedeleu. The algebra of parity games. CoRR, abs/2501.18499, 2025. doi:10.48550/arXiv.2501.18499.
[38] Julian Rathke, Pawel Sobocinski, and Owen Stephens. Compositional reachability in Petri nets. In RP, volume 8762 of Lecture Notes in Computer Science, pages 230–243. Springer, 2014. doi:10.1007/978-3-319-11439-2_18.
[39] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340–355, 2014. doi:10.1016/J.IC.2014.07.012.
[40] Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking via $\omega$ -regular games over Böhm trees. In CSL-LICS, pages 78:1–78:10. ACM, 2014. doi:10.1145/2603088.2603133.
[41] Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177–196, 2015. doi:10.1016/J.IC.2015.03.001.
[42] Jens Vöge and Marcin Jurdzinski. A discrete strategy improvement algorithm for solving parity games. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 202–215. Springer, 2000. doi:10.1007/10722167_18.
[43] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. A compositional approach to parity games. In MFPS, volume 351 of EPTCS, pages 278–295, 2021. doi:10.4204/EPTCS.351.17.
[44] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional probabilistic model checking with string diagrams of MDPs. In CAV (3), volume 13966 of Lecture Notes in Computer Science, pages 40–61. Springer, 2023. doi:10.1007/978-3-031-37709-9_3.
[45] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Principles of Verification (3), volume 15262 of Lecture Notes in Computer Science, pages 423–445. Springer, 2024. doi:10.1007/978-3-031-75778-5_20.
[46] Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, and Sebastian Junges. Pareto curves for compositionally model checking string diagrams of MDPs. In TACAS (2), volume 14571 of Lecture Notes in Computer Science, pages 279–298. Springer, 2024. doi:10.1007/978-3-031-57249-4_14.
[47] Kazuki Watanabe, Marck van der Vegt, Sebastian Junges, and Ichiro Hasuo. Compositional value iteration with pareto caching. In CAV (3), volume 14683 of Lecture Notes in Computer Science, pages 467–491. Springer, 2024. doi:10.1007/978-3-031-65633-0_21.

Appendix A Proof of Prop. 43 for $\ast=\fatsemi$

In this section, we additionally assume that every entrance on a given oPG is not reachable except as an initial node, that is, $(v,v^{\prime})\in E$ implies $v^{\prime}\not\in I$ without loss of generality. We fix oPGs $\mathcal{A},\mathcal{B}$ , and an entrance $i$ on $\mathcal{A}\fatsemi\mathcal{B}$ . Here, we only consider plays that start from the specified entrance $i\in\mathcal{A}$ ; note that the sequential composition is bidirectional and the ordering between $\mathcal{A}$ and $\mathcal{B}$ is not essential. Firstly, we introduce entrance-dependent strategies on $\mathcal{A}\fatsemi\mathcal{B}$ : intuitively, for each play, they behave positionally depending on the last entrance that appears in the play.

Definition 44 (entrance-dependent strategy).

Let $\sigma_{\exists}$ be an $\exists$ -strategy on $\mathcal{A}\fatsemi\mathcal{B}$ . We write $\Sigma^{\mathcal{A}}_{\exists,\mathrm{p}}$ and $\Sigma^{\mathcal{B}}_{\exists,\mathrm{p}}$ for the set of positional $\exists$ -strategies on $\mathcal{A}$ and $\mathcal{B}$ , respectively. The $\exists$ -strategy $\sigma_{\exists}$ is entrance-dependent if there are assignments $\sigma^{\mathcal{A}}_{\exists,\_}\colon I^{\mathcal{A}}\rightarrow\Sigma^{% \mathcal{A}}_{\exists,\mathrm{p}}$ and $\sigma^{\mathcal{B}}_{\exists,\_}\colon I^{\mathcal{B}}\rightarrow\Sigma^{% \mathcal{B}}_{\exists,\mathrm{p}}$ such that for any play $p=p_{1}\cdots p_{n}\in V^{\ast}\times V_{\exists}$ , if the last entrance $i^{\prime}$ that appears in $p$ is $i^{\prime}\in I^{\mathcal{A}}$ , then the $\exists$ -strategy $\sigma_{\exists}$ is given by $\sigma_{\exists}(p)=\sigma^{\mathcal{A}}_{\exists,i^{\prime}}(p_{n})$ , and same for the case of $i^{\prime}\in I^{\mathcal{B}}$ .

We also define entrance-dependent $\forall$ -strategies in the same manner.

Entrance-dependent strategies consist of positional strategies and monotonicity of positional strategies holds. Intuitively, if we use better (or worse) positional strategies for entrance-dependent strategies, then their entrance-dependent strategies are also better (or worse).

Lemma 45 ( $\forall$ -monotonicity).

Let $\sigma_{\exists}$ be an entrance-dependent $\exists$ -strategy and $\sigma_{\forall},\tau_{\forall}$ be entrance-dependent $\forall$ -strategies. Suppose that for each $i^{\prime}\in I^{\mathcal{A}}$ , the inequality $\llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\tau^{\mathcal{A}}% _{\forall,i^{\prime}};i^{\prime}}\rrparenthesis\preceq_{\mathbf{D}}% \llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\sigma^{\mathcal{A% }}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ holds, and same for $i^{\prime}\in I^{\mathcal{B}}$ . Then, the inequality $\llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}\rrparenthesis\preceq_{% \mathbf{D}}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ holds.

Proof.

We prove the inequality $\llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}\rrparenthesis\preceq_{% \mathbf{D}}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ . If the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ is winning, then obviously the inequality holds.

Suppose that the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ reaches an exit $o$ (of $\mathcal{A}\fatsemi\mathcal{B}$ ) with the maximum priority $m$ , that is, $\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis=(o,m)$ . By the assumption and the monotonicity of priorities (Lem. 15), the play $p_{\sigma_{\exists},\tau_{\forall};i}$ is either losing, or reaching the same exit with a potentially different maximum priority $m^{\prime}$ such that $m^{\prime}\preceq_{\mathbb{P}}m$ . Thus, the desired inequality also holds.

Suppose that the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ is losing. By collecting the denotations of $\llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\sigma^{\mathcal{A% }}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ and $\llparenthesis p_{\sigma^{\mathcal{B}}_{\exists,i^{\prime}},\sigma^{\mathcal{B% }}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ , we obtain an infinte sequence $m_{1}\cdot m_{2}\cdots$ of priorities for $p_{\sigma_{\exists},\sigma_{\forall};i}$ such that the maximum priorities that occurs infinitely often in this sequence is odd. By the assumption, the corresponding infinite sequence $m^{\prime}_{1}\cdot m^{\prime}_{2}\cdots$ of priorities for $p_{\sigma_{\exists},\tau_{\forall};i}$ satisfies that $m^{\prime}_{j}\preceq_{\mathbb{P}}m_{j}$ for each $j\in\mathbb{N}$ . For each $j\in\mathbb{N}$ , if $m_{j}$ is the maximum priority $m$ that occurs infinitely often in the sequence $m_{1}\cdot m_{2}\cdots$ , then $m^{\prime}_{j}$ is a bigger or the same odd number, and at least one of the such odd number occurs infinitely often in the sequence $m^{\prime}_{1}\cdot m^{\prime}_{2}\cdots$ because the size of priorities is finite. If $m_{j}$ is even, then $m^{\prime}_{j}$ is a smaller or the same even number, therefore, the maximum even number that occurs infinitely often in the sequence $m^{\prime}_{1}\cdot m^{\prime}_{2}\cdots$ is strictly smaller than $m$ . Therefore, the maximum number that occurs infinitely often in $m^{\prime}_{1}\cdot m^{\prime}_{2}\cdots$ is again odd, which means that the desired inequality holds. $\hfill\blacktriangleleft$

Lemma 46 ( $\exists$ -monotonicity).

Let $\sigma_{\exists},\tau_{\exists}$ be entrance-dependent $\exists$ -strategies. Suppose that for each $i^{\prime}\in I^{\mathcal{A}}$ , the following inequality holds:

\displaystyle\big{\{}\llparenthesis p_{\tau^{\mathcal{A}}_{\exists,i^{\prime}}% ,\tau_{\forall};i^{\prime}}\rrparenthesis\ \big{|}\ \tau^{\mathcal{A}}_{% \forall}\text{ is a $\forall$-strategy}\big{\}}^{\mathrm{min}}\preceq_{\mathbf% {R}_{\mathcal{A}}}\big{\{}\llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{% \prime}},\sigma_{\forall};i^{\prime}}\rrparenthesis\ \big{|}\ \sigma^{\mathcal% {A}}_{\forall}\text{ is a $\forall$-strategy}\big{\}}^{\mathrm{min}},

and same for $i^{\prime}\in I^{\mathcal{B}}$ . Then, for any entrance-dependent $\forall$ -strategy $\sigma_{\forall}$ , there is an entrance-dependent $\forall$ -strategy $\tau_{\forall}$ such that $\llparenthesis p_{\tau_{\exists},\tau_{\forall};i}\rrparenthesis\preceq_{% \mathbf{D}}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ .

Proof.

For any entrance-dependent $\forall$ -strategy $\sigma_{\forall}$ , we construct an entrance-dependent $\forall$ -strategy $\tau_{\forall}$ such that the inequality $\llparenthesis p_{\tau_{\exists},\tau_{\forall};i}\rrparenthesis\preceq_{% \mathbf{D}}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ holds. For each entrance $i^{\prime}\in I^{\mathcal{A}}$ , there is a positional optimal $\forall$ -strategy $\sigma^{\prime\mathcal{A}}_{\forall,i^{\prime}}$ such that the inequality $\llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\sigma^{\prime% \mathcal{A}}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis\preceq_{\mathbf{D}% }\llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\sigma^{\mathcal{% A}}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ holds. By the assumption, we can take a positional optimal $\forall$ -strategy $\tau^{\mathcal{A}}_{\forall,i^{\prime}}$ such that $\llparenthesis p_{\tau^{\mathcal{A}}_{\exists,i^{\prime}},\tau^{\mathcal{A}}_{% \forall,i^{\prime}};i^{\prime}}\rrparenthesis\preceq_{\mathbf{D}}% \llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\sigma^{\prime% \mathcal{A}}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ , thus the inequality $\llparenthesis p_{\tau^{\mathcal{A}}_{\exists,i^{\prime}},\tau^{\mathcal{A}}_{% \forall,i^{\prime}};i^{\prime}}\rrparenthesis\preceq_{\mathbf{D}}% \llparenthesis p_{\sigma^{\mathcal{A}}_{\exists,i^{\prime}},\sigma^{\mathcal{A% }}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ holds. Similarly, we can take a positional optimal $\forall$ -strategy $\tau^{\mathcal{B}}_{\forall,i^{\prime}}$ for each entrance $i^{\prime}\in I^{\mathcal{B}}$ such that the inequality $\llparenthesis p_{\tau^{\mathcal{B}}_{\exists,i^{\prime}},\tau^{\mathcal{B}}_{% \forall,i^{\prime}};i^{\prime}}\rrparenthesis\preceq_{\mathbf{D}}% \llparenthesis p_{\sigma^{\mathcal{B}}_{\exists,i^{\prime}},\sigma^{\mathcal{B% }}_{\forall,i^{\prime}};i^{\prime}}\rrparenthesis$ holds. By the almost same argument used in the proof of Lem. 45, we can conclude that the inequality $\llparenthesis p_{\tau_{\exists},\tau_{\forall};i}\rrparenthesis\preceq_{% \mathbf{D}}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ holds, where $\tau_{\forall}$ is the entrance-dependent $\forall$ -strategy that consists of these positional optimal $\forall$ -strategies $\tau^{\mathcal{A}}_{\forall,i^{\prime}}$ and $\tau^{\mathcal{B}}_{\forall,i^{\prime}}$ . $\hfill\blacktriangleleft$

The last ingredient for proving Prop. 43 is the fact that entrance-dependent $\forall$ -strategies suffice for entrance-dependent $\exists$ -strategies.

Lemma 47.

Let $\sigma_{\exists}$ be an entrance-dependent $\exists$ -strategy. Then, entrance-dependent $\forall$ -strategies suffice, that is, the following equality holds:

\displaystyle\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}% \rrparenthesis\ \big{|}\ \text{a $\forall$-strategy }\sigma_{\forall}\big{\}}^% {\mathrm{min}}=\big{\{}\llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}% \rrparenthesis\ \big{|}\ \text{an entrance-dependent $\forall$-strategy }\tau_% {\forall}\big{\}}^{\mathrm{min}}.

Proof.

Let $\sigma_{\forall}$ be an optimal $\forall$ -strategy. If the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ is losing, it is straightforward to construct a losing entrance-dependent $\forall$ -strategy by distinguishing last entrances, and positional determinacy of PGs.

Suppose that the play $p_{\sigma_{\exists},\sigma_{\forall};i}$ reaches an exit $o$ on $\mathcal{A}\fatsemi\mathcal{B}$ . Let $i_{1}\cdots i_{n}$ be the (finite) sequence of entrances in $I^{\mathcal{A}}\uplus I^{\mathcal{B}}$ that occurs in $p_{\sigma_{\exists},\sigma_{\forall};i}$ , where the ordering is the order of their appearance. Then, we can take a positioal $\forall$ -strategy $\tau^{\mathcal{A}}_{\forall,j}$ for each entrances $i_{j}$ such that the constructed $\forall$ -strategy $\tau_{\forall}$ from these $\tau^{\mathcal{A}}_{\forall,j}$ satisfies that $\llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}\rrparenthesis\preceq_{% \mathbf{D}}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ . Since $\sigma_{\forall}$ is optimal, the equality $\llparenthesis p_{\sigma_{\exists},\tau_{\forall};i}\rrparenthesis=% \llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}\rrparenthesis$ holds.

Here, $\tau_{\forall}$ may not be an entrance-dependent, that is, there are $j\not=j^{\prime}$ such that $i_{j}=i_{j^{\prime}}$ and $\tau^{\mathcal{A}}_{\forall,j}\not=\tau^{\mathcal{A}}_{\forall,j^{\prime}}$ in general. If $\tau_{\forall}$ is not an entrance-dependent, we construct an $\forall$ -entrance-dependent strategy by a similar argument of the proof of Lem. 29; note that we assume $\sigma_{\exists}$ is entrance-dependent. $\hfill\blacktriangleleft$

Definition 48 (lower preorder).

Let $\mathbf{T}$ be a set such that $\mathbf{T}:=\{T^{\mathrm{max}}\mid T\subseteq\mathbf{R}_{\mathcal{A}\fatsemi% \mathcal{B}},\text{and $T\not=\emptyset$}\}$ . Then, the lower preorder $\preceq_{\mathbf{L}}$ on $\mathbf{T}$ is defined as follows: $T_{1}^{\mathrm{max}}\preceq_{\mathbf{L}}T_{2}^{\mathrm{max}}$ if for any result $\mathbf{r}_{1}\in T_{1}^{\mathrm{max}}$ , there is a result $\mathbf{r}_{2}\in T_{2}^{\mathrm{max}}$ such that $\mathbf{r}_{1}\preceq_{\mathbf{R}_{\mathcal{A}\fatsemi\mathcal{B}}}\mathbf{r}_% {2}$ .

Lemma 49.

The preorder $\preceq_{\mathbf{L}}$ is a partial order.

Proof.

It suffices to prove that $T_{1}^{\mathrm{max}}\preceq_{\mathbf{L}}T_{2}^{\mathrm{max}}$ and $T_{2}^{\mathrm{max}}\preceq_{\mathbf{L}}T_{1}^{\mathrm{max}}$ imply that $T_{1}^{\mathrm{max}}\subseteq T_{2}^{\mathrm{max}}$ . For any result $\mathbf{r}_{1}\in T_{1}^{\mathrm{max}}$ , there is a result $\mathbf{r}_{2}\in T_{2}^{\mathrm{max}}$ such that $\mathbf{r}_{1}\preceq_{\mathbf{R}_{\mathcal{A}\fatsemi\mathcal{B}}}\mathbf{r}_% {2}$ . Similarly, there is a $\mathbf{r}_{3}\in T_{1}^{\mathrm{max}}$ such that $\mathbf{r}_{2}\preceq_{\mathbf{R}_{\mathcal{A}\fatsemi\mathcal{B}}}\mathbf{r}_% {3}$ . Thus, we can conclude that $\mathbf{r}_{1}=\mathbf{r}_{3}$ because of the maximality of $T_{1}^{\mathrm{max}}$ . Since the result order is a partial order, we can conclude that $\mathbf{r}_{1}=\mathbf{r}_{2}$ , thus the desired $T_{1}^{\mathrm{max}}\subseteq T_{2}^{\mathrm{max}}$ holds. $\hfill\blacktriangleleft$

We conclude this section by showing our proof of Prop. 43.

Proof of Prop. 43 for $\ast=\fatsemi$ .

By definition and Thm. 28, the Pareto front $\mathcal{S}(\mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{B}),i)$ is given by

\displaystyle\Big{\{}\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{% \forall};i}\rrparenthesis\ \big{|}\ \text{a positional $\sigma_{\forall}$ on $% \mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{B})$}\big{\}}^{\mathrm{% min}}\ \Big{|}\ \text{a positional $\sigma_{\exists}$ on $\mathcal{C}(\mathcal% {A})\fatsemi\mathcal{C}(\mathcal{B})$}\Big{\}}^{\mathrm{max}}.

For a positional $\exists$ -strategy $\sigma_{\exists}$ on $\mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{B})$ , there is a corresponding entrance-dependent $\exists$ -strategy $\tilde{\sigma_{\exists}}$ on $\mathcal{A}\fatsemi\mathcal{B}$ by mimicking $\sigma_{\exists}$ . Similarly, the following equality holds:

		$\displaystyle\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{\forall};i}% \rrparenthesis\ \big{\|}\ \text{a positional $\sigma_{\forall}$ on $\mathcal{C}% (\mathcal{A})\fatsemi\mathcal{C}(\mathcal{B})$}\big{\}}^{\mathrm{min}}$
	$\displaystyle=$	$\displaystyle\big{\{}\llparenthesis p_{\tilde{\sigma_{\exists}},\tilde{\sigma_% {\forall}};i}\rrparenthesis\ \big{\|}\ \text{a positional $\sigma_{\forall}$ on% $\mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{B})$}\big{\}}^{\mathrm{% min}},$

where the $\forall$ -strategy $\tilde{\sigma_{\forall}}$ is the corresponding entrance-dependent $\forall$ -strategy of a positional $\forall$ -strategy $\sigma_{\forall}$ , and the play $p_{\tilde{\sigma_{\exists}},\tilde{\sigma_{\forall}};i}$ is on $\mathcal{A}\fatsemi\mathcal{B}$ . By Lemmas 45 and 47, we can further say that the Pareto front $\mathcal{S}(\mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{B}),i)$ is given by

\displaystyle\Big{\{}\big{\{}\llparenthesis p_{\tilde{\sigma_{\exists}},\sigma% _{\forall};i}\rrparenthesis\ \big{|}\ \text{a $\forall$-strategy $\sigma_{% \forall}$ on $\mathcal{A}\fatsemi\mathcal{B}$}\big{\}}^{\mathrm{min}}\ \Big{|}% \ \text{a positional $\sigma_{\exists}$ on $\mathcal{C}(\mathcal{A})\fatsemi% \mathcal{C}(\mathcal{B})$}\Big{\}}^{\mathrm{max}},

By using the lower preorder $\preceq_{\mathbf{L}}$ on the sets of maximal results, which is a partial order (Lem. 49), we obtain the following inequality:

		$\displaystyle\mathcal{S}(\mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{% B}),i)$
	$\displaystyle\preceq_{\mathbf{L}}$	$\displaystyle\Big{\{}\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{% \forall};i}\rrparenthesis\ \big{\|}\ \text{a $\forall$-strategy $\sigma_{% \forall}$ on $\mathcal{A}\fatsemi\mathcal{B}$}\big{\}}^{\mathrm{min}}\ \Big{\|}% \ \text{an $\exists$-strategy $\sigma_{\exists}$ on $\mathcal{A}\fatsemi% \mathcal{B}$}\Big{\}}^{\mathrm{max}}.$

On the other hand, since positional strategies are entrance-dependent, we obtain the following inequality by Lemmas 45 and 46:

		$\displaystyle\mathcal{S}(\mathcal{C}(\mathcal{A})\fatsemi\mathcal{C}(\mathcal{% B}),i)$
	$\displaystyle\succeq_{\mathbf{L}}$	$\displaystyle\Big{\{}\big{\{}\llparenthesis p_{\sigma_{\exists},\sigma_{% \forall};i}\rrparenthesis\ \big{\|}\ \text{entrance-dependent $\sigma_{\forall}% $ on $\mathcal{A}\fatsemi\mathcal{B}$}\big{\}}^{\mathrm{min}}\ \Big{\|}\ \text{% positional $\sigma_{\exists}$ on $\mathcal{A}\fatsemi\mathcal{B}$}\Big{\}}^{% \mathrm{max}}.$

By Thms 28 and 49, we can conclude that $\mathcal{S}(\mathcal{A}\ast\mathcal{B},i)=\mathcal{S}(\mathcal{C}(\mathcal{A})% \fatsemi\mathcal{C}(\mathcal{B}),i)$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Samson Abramsky. Domain theory in logical form. In LICS, pages 47–53. IEEE Computer Society, 1987.

[bib.bib2] [2] John C Baez and Jason Erbele. Categories in control. arXiv preprint arXiv:1405.6881, 2014.

[bib.bib3] [3] John C. Baez, Fabrizio Genovese, Jade Master, and Michael Shulman. Categories of nets. In LICS, pages 1–13. IEEE, 2021. doi:10.1109/LICS52264.2021.9470566.

[bib.bib4] [4] Dietmar Berwanger, Anuj Dawar, Paul Hunter, and Stephan Kreutzer. Dag-width and parity games. In STACS, volume 3884 of Lecture Notes in Computer Science, pages 524–536. Springer, 2006. doi:10.1007/11672142_43.

[bib.bib5] [5] Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. String diagram rewrite theory I: rewriting with Frobenius structure. J. ACM, 69(2):14:1–14:58, 2022. doi:10.1145/3502719.

[bib.bib6] [6] Filippo Bonchi, Joshua Holland, Robin Piedeleu, Pawel Sobocinski, and Fabio Zanasi. Diagrammatic algebra: from linear to concurrent systems. Proc. ACM Program. Lang., 3(POPL):25:1–25:28, 2019. doi:10.1145/3290338.

[bib.bib7] [7] Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In POPL, pages 515–526. ACM, 2015. doi:10.1145/2676726.2676993.

[bib.bib8] [8] Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. The calculus of signal flow diagrams I: linear relations on streams. Inf. Comput., 252:2–29, 2017. doi:10.1016/J.IC.2016.03.002.

[bib.bib9] [9] Véronique Bruyère, Jean-François Raskin, and Clément Tamines. Pareto-rational verification. In CONCUR, volume 243 of LIPIcs, pages 33:1–33:20. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPICS.CONCUR.2022.33.

[bib.bib10] [10] Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasi-polynomial time. SIAM J. Comput., 51(2):17–152, 2022. doi:10.1137/17M1145288.

[bib.bib11] [11] Taolue Chen, Vojtech Forejt, Marta Z. Kwiatkowska, Aistis Simaitis, and Clemens Wiltsche. On stochastic games with multiple objectives. In MFCS, volume 8087 of Lecture Notes in Computer Science, pages 266–277. Springer, 2013. doi:10.1007/978-3-642-40313-2_25.

[bib.bib12] [12] Edmund M. Clarke, David E. Long, and Kenneth L. McMillan. Compositional model checking. In LICS, pages 353–362. IEEE Computer Society, 1989. doi:10.1109/LICS.1989.39190.

[bib.bib13] [13] Bob Coecke and Ross Duncan. Interacting quantum observables. In ICALP (2), volume 5126 of Lecture Notes in Computer Science, pages 298–310. Springer, 2008. doi:10.1007/978-3-540-70583-3_25.

[bib.bib14] [14] Bob Coecke and Aleks Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. doi:10.1017/9781316219317.

[bib.bib15] [15] E. Allen Emerson. Automata, tableaux and temporal logics (extended abstract). In Logic of Programs, volume 193 of Lecture Notes in Computer Science, pages 79–88. Springer, 1985. doi:10.1007/3-540-15648-8_7.

[bib.bib16] [16] E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In FOCS, pages 368–377. IEEE Computer Society, 1991. doi:10.1109/SFCS.1991.185392.

[bib.bib17] [17] E. Allen Emerson, Charanjit S. Jutla, and A. Prasad Sistla. On model checking for the $\mathrm{\mu}$ -calculus and its fragments. Theor. Comput. Sci., 258(1-2):491–522, 2001. doi:10.1016/S0304-3975(00)00034-7.

[bib.bib18] [18] Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, and Mihalis Yannakakis. Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci., 4(4), 2008. doi:10.2168/LMCS-4(4:8)2008.

[bib.bib19] [19] John Fearnley, Sanjay Jain, Bart de Keijzer, Sven Schewe, Frank Stephan, and Dominik Wojtczak. An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space. Int. J. Softw. Tools Technol. Transf., 21(3):325–349, 2019. doi:10.1007/S10009-019-00509-3.

[bib.bib20] [20] John Fearnley and Sven Schewe. Time and space results for parity games with bounded treewidth. Log. Methods Comput. Sci., 9(2), 2013. doi:10.2168/LMCS-9(2:6)2013.

[bib.bib21] [21] Vojtech Forejt, Marta Z. Kwiatkowska, and David Parker. Pareto curves for probabilistic model checking. In ATVA, volume 7561 of Lecture Notes in Computer Science, pages 317–332. Springer, 2012. doi:10.1007/978-3-642-33386-6_25.

[bib.bib22] [22] Koichi Fujima, Sohei Ito, and Naoki Kobayashi. Practical alternating parity tree automata model checking of higher-order recursion schemes. In APLAS, volume 8301 of Lecture Notes in Computer Science, pages 17–32. Springer, 2013. doi:10.1007/978-3-319-03542-0_2.

[bib.bib23] [23] Neil Ghani, Jules Hedges, Viktor Winschel, and Philipp Zahn. Compositional game theory. In LICS, pages 472–481. ACM, 2018. doi:10.1145/3209108.3209165.

[bib.bib24] [24] Charles Grellois and Paul-André Melliès. Finitary semantics of linear logic and higher-order model-checking. In MFCS (1), volume 9234 of Lecture Notes in Computer Science, pages 256–268. Springer, 2015. doi:10.1007/978-3-662-48057-1_20.

[bib.bib25] [25] Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In LICS, pages 1–9. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005092.

[bib.bib26] [26] Roope Kaivola. Compositional model checking for linear-time temporal logic. In CAV, volume 663 of Lecture Notes in Computer Science, pages 248–259. Springer, 1992. doi:10.1007/3-540-56496-9_20.

[bib.bib27] [27] Naoki Kobayashi and C.-H. Luke Ong. A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In LICS, pages 179–188. IEEE Computer Society, 2009. doi:10.1109/LICS.2009.29.

[bib.bib28] [28] Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333–354, 1983. doi:10.1016/0304-3975(82)90125-6.

[bib.bib29] [29] Orna Kupferman and Moshe Y. Vardi. Weak alternating automata and tree automata emptiness. In STOC, pages 224–233. ACM, 1998. doi:10.1145/276698.276748.

[bib.bib30] [30] Marta Z. Kwiatkowska, Gethin Norman, David Parker, and Hongyang Qu. Compositional probabilistic verification through multi-objective model checking. Inf. Comput., 232:38–65, 2013. doi:10.1016/J.IC.2013.10.001.

[bib.bib31] [31] Elena Di Lavore, Jules Hedges, and Pawel Sobocinski. Compositional modelling of network games. In CSL, volume 183 of LIPIcs, pages 30:1–30:24. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021. doi:10.4230/LIPICS.CSL.2021.30.

[bib.bib32] [32] Karoliina Lehtinen. A modal $\mu$ perspective on solving parity games in quasi-polynomial time. In LICS, pages 639–648. ACM, 2018. doi:10.1145/3209108.3209115.

[bib.bib33] [33] Michael Luttenberger, Philipp J. Meyer, and Salomon Sickert. Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica, 57(1-2):3–36, 2020. doi:10.1007/S00236-019-00349-3.

[bib.bib34] [34] Jan Obdrzálek. Fast mu-calculus model checking when tree-width is bounded. In CAV, volume 2725 of Lecture Notes in Computer Science, pages 80–92. Springer, 2003. doi:10.1007/978-3-540-45069-6_7.

[bib.bib35] [35] C.-H. Luke Ong. On model-checking trees generated by higher-order recursion schemes. In LICS, pages 81–90. IEEE Computer Society, 2006. doi:10.1109/LICS.2006.38.

[bib.bib36] [36] Christos H. Papadimitriou and Mihalis Yannakakis. On the approximability of trade-offs and optimal access of web sources. In FOCS, pages 86–92. IEEE Computer Society, 2000. doi:10.1109/SFCS.2000.892068.

[bib.bib37] [37] Robin Piedeleu. The algebra of parity games. CoRR, abs/2501.18499, 2025. doi:10.48550/arXiv.2501.18499.

[bib.bib38] [38] Julian Rathke, Pawel Sobocinski, and Owen Stephens. Compositional reachability in Petri nets. In RP, volume 8762 of Lecture Notes in Computer Science, pages 230–243. Springer, 2014. doi:10.1007/978-3-319-11439-2_18.

[bib.bib39] [39] Sylvain Salvati and Igor Walukiewicz. Krivine machines and higher-order schemes. Inf. Comput., 239:340–355, 2014. doi:10.1016/J.IC.2014.07.012.

[bib.bib40] [40] Takeshi Tsukada and C.-H. Luke Ong. Compositional higher-order model checking via $\omega$ -regular games over Böhm trees. In CSL-LICS, pages 78:1–78:10. ACM, 2014. doi:10.1145/2603088.2603133.

[bib.bib41] [41] Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177–196, 2015. doi:10.1016/J.IC.2015.03.001.

[bib.bib42] [42] Jens Vöge and Marcin Jurdzinski. A discrete strategy improvement algorithm for solving parity games. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 202–215. Springer, 2000. doi:10.1007/10722167_18.

[bib.bib43] [43] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. A compositional approach to parity games. In MFPS, volume 351 of EPTCS, pages 278–295, 2021. doi:10.4204/EPTCS.351.17.

[bib.bib44] [44] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional probabilistic model checking with string diagrams of MDPs. In CAV (3), volume 13966 of Lecture Notes in Computer Science, pages 40–61. Springer, 2023. doi:10.1007/978-3-031-37709-9_3.

[bib.bib45] [45] Kazuki Watanabe, Clovis Eberhart, Kazuyuki Asada, and Ichiro Hasuo. Compositional solution of mean payoff games by string diagrams. In Principles of Verification (3), volume 15262 of Lecture Notes in Computer Science, pages 423–445. Springer, 2024. doi:10.1007/978-3-031-75778-5_20.

[bib.bib46] [46] Kazuki Watanabe, Marck van der Vegt, Ichiro Hasuo, Jurriaan Rot, and Sebastian Junges. Pareto curves for compositionally model checking string diagrams of MDPs. In TACAS (2), volume 14571 of Lecture Notes in Computer Science, pages 279–298. Springer, 2024. doi:10.1007/978-3-031-57249-4_14.

[bib.bib47] [47] Kazuki Watanabe, Marck van der Vegt, Sebastian Junges, and Ichiro Hasuo. Compositional value iteration with pareto caching. In CAV (3), volume 14683 of Lecture Notes in Computer Science, pages 467–491. Springer, 2024. doi:10.1007/978-3-031-65633-0_21.

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

Acknowledgements:

Funding:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Contributions.

1.1 Related Work

2 Formal Problem Statement

2.1 Parity Games

Definition 1 (parity game).

2.2 String Diagrams of Parity Games

Definition 2 (open parity game [43]).

Definition 3 (sequential composition).

Definition 4 (sum).

Definition 5 (string diagram).

▶ Remark 6 (trace operator).

3 Denotations, Optimal Strategies, and Pareto Fronts

3.1 Denotation of Open Parity Games

Definition 7 (domain).

Definition 8 (denotation of play).

Definition 9 (denotation of entrance).

Definition 10 (denotation of oPGs [43]).

Example 11.

▶ Remark 12.

3.2 Optimal Strategies of Open Parity Games

Definition 13 (sub-priority order [22, 4]).

▶ Remark 14.

Lemma 15 (monotonicity [40]).

Definition 16 (domain order).

Definition 17 (minimal).

Definition 18 (optimal ∀-strategy).

Definition 19 (upper preorder [1]).

Definition 20 (maximal).

Definition 21 (optimal ∃-strategy).

3.3 Pareto Fronts of Open Parity Games

Definition 22 (results, result order [22]).

Proposition 23.

Proof.

Definition 24 (Pareto front, Pareto-optimal).

Example 25.

▶ Remark 26 (meager semantics).

Lemma 27.

Proof.

4 Solving Open Parity Games

4.1 Positional Determinacy of Pareto Fronts

Theorem 28 (positional determinacy).

Lemma 29.

Proof.

▶ Remark 30.

4.2 The Loop Construction and the Algorithm

Definition 31 (query).

Definition 32 (loop construction).

Definition 33 (query order).

Definition 34 (dual).

Lemma 35 (​​[40]).

Definition 36 (dual of query).

Lemma 37 (duality).

Proof.

Lemma 38.

Proof.

Proposition 39.

Proof of Thm. 28.

Algorithm and Time Complexity.

Proposition 40.

Proof.

5 Solving String Diagrams of Parity Games

Definition 41 (shortcut oPG).

Proposition 42.

Proposition 43.

Proof Sketch.

6 Conclusion

References

Appendix A Proof of Prop. 43 for ∗⁣=⁣⨟

$\blacktriangleright$ Remark 6 (trace operator).

$\blacktriangleright$ Remark 12.

$\blacktriangleright$ Remark 14.

Definition 18 (optimal $\forall$ -strategy).

Definition 21 (optimal $\exists$ -strategy).

$\blacktriangleright$ Remark 26 (meager semantics).

$\blacktriangleright$ Remark 30.

Lemma 35 ([40]).

Appendix A Proof of Prop. 43 for $\ast=\fatsemi$

Lemma 45 ( $\forall$ -monotonicity).

Lemma 46 ( $\exists$ -monotonicity).

Proof of Prop. 43 for $\ast=\fatsemi$ .