Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

Kazuki Watanabe

TL;DR

This paper addresses solving string diagrams of parity games by introducing Pareto fronts for open parity games (oPGs) to handle multi-objective considerations. The core approach is a loop-construction that translates an oPG into a single-objective parity game, enabling the use of established quasi-polynomial parity-game solvers and yielding a simple, scalable algorithm whose complexity grows with the number of exits rather than the total node count. A key contribution is proving positional determinacy for Pareto fronts, ensuring that optimal results can be achieved by positional strategies, and the development of shortcut oPGs to compose Pareto fronts efficiently within string diagrams. The result is a compositional algorithm for string diagrams of parity games, facilitating divide-and-conquer solving of large, structured parity games with multi-objective considerations and potential applicability to higher-order model checking and compositional verification workflows.

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.

Pareto Fronts for Compositionally Solving String Diagrams of Parity Games

TL;DR

This paper addresses solving string diagrams of parity games by introducing Pareto fronts for open parity games (oPGs) to handle multi-objective considerations. The core approach is a loop-construction that translates an oPG into a single-objective parity game, enabling the use of established quasi-polynomial parity-game solvers and yielding a simple, scalable algorithm whose complexity grows with the number of exits rather than the total node count. A key contribution is proving positional determinacy for Pareto fronts, ensuring that optimal results can be achieved by positional strategies, and the development of shortcut oPGs to compose Pareto fronts efficiently within string diagrams. The result is a compositional algorithm for string diagrams of parity games, facilitating divide-and-conquer solving of large, structured parity games with multi-objective considerations and potential applicability to higher-order model checking and compositional verification workflows.

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.
Paper Structure (13 sections, 12 theorems, 9 equations, 5 figures, 1 algorithm)

This paper contains 13 sections, 12 theorems, 9 equations, 5 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Formal Problem Statement
  4. Parity Games
  5. String Diagrams of Parity Games
  6. Denotations, Optimal Strategies, and Pareto Fronts
  7. Denotation of Open Parity Games
  8. Optimal Strategies of Open Parity Games
  9. Pareto Fronts of Open Parity Games
  10. Solving Open Parity Games
  11. Positional Determinacy of Pareto Fronts
  12. The Loop Construction and the Algorithm
  13. Solving String Diagrams of Parity Games

Key Result

Lemma 15

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.

Figures (5)

  • 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}$.
  • Figure 2: The parity game $\mathcal{A}\fatsemi \mathcal{B}$. Every node is owned by Player $\exists$.
  • 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.
  • 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$,
  • 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 $\{ \{ (o_{\mathbf{l}, 1}, 1)\},\, \{ (o_{\mathbf{r}, 1}, 1) \},\, \{ (o_{\mathbf{r}, 1}, 2), (o_{\mathbf{l}, 1}, 2) \} \}$. 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$.

Theorems & Definitions (43)

  • Definition 1: parity game
  • Definition 2: open parity game DBLP:journals/corr/abs-2112-14058
  • Definition 3: sequential composition
  • Definition 4: sum
  • Definition 5: string diagram
  • Remark 6: trace operator
  • Definition 7: domain
  • Definition 8: denotation of play
  • Definition 9: denotation of entrance
  • Definition 10: denotation of oPGs DBLP:journals/corr/abs-2112-14058
  • ...and 33 more