Partial Solvers for Generalized Parity Games

TL;DR

This paper introduces an extension of partial solvers for generalized parity games, combining them with Zielonka's recursive algorithm, and evaluates their performance on benchmark sets from the LTL synthesis competition.

Contribution

It extends partial solvers to generalized parity games and integrates them with Zielonka's recursive algorithm, enhancing solving capabilities for complex game objectives.

Findings

Partial solvers efficiently solve most benchmark games.

Combined algorithms outperform classical methods in certain cases.

Extended solvers handle conjunctions of parity objectives effectively.

Abstract

Parity games have been broadly studied in recent years for their applications to controller synthesis and verification. In practice, partial solvers for parity games that execute in polynomial time, while incomplete, can solve most games in publicly available benchmark suites. In this paper, we combine those partial solvers with the classical recursive algorithm for parity games due to Zielonka. We also extend partial solvers to generalized parity games that are games with conjunction of parity objectives. We have implemented those algorithms and evaluated them on a large set of benchmarks proposed in the last LTL synthesis competition.

Tables

Table 1. Table 1: Statistics on the one dimensional benchmarks.

Solver	Solved	T.O.	Fastest	Mean time (233)
Zielonka	240 (100%)	0	150 (63 %)	272 ms
Ziel&BüchiSolver	240 (100%)	0	89 (37 %)	480 ms
Ziel&GoodEpSolver	233 (97%)	7	0 (0%)	1272 ms
Ziel&LaySolver	238 (99%)	2	1 (0%)	587 ms
BüchiSolver	203 (84%) - 37	0	-	-
GoodEpSolver	233 (97%) - 0	7	-	-
LaySolver	232 (97%) - 6	2	-	-

Table 2. Table 2: Statistics on the one dimensional benchmarks for the 20 most difficult instances for Algorithm Zielonka

Solver	Solved	T.O.	Fastest	Mean time (13)
Zielonka	20 (100%)	0	11 (55%)	451 ms
Ziel&BüchiSolver	20 (100%)	0	8 (40%)	7746 ms
Ziel&GoodEpSolver	13 (65%)	7	0 (0%)	20025 ms
Ziel&LaySolver	18 (99%)	2	1 (5%)	9079 ms
BüchiSolver	15 (75%) - 5	0	-	-
GoodEpSolver	13 (65%) - 0	7	-	-
LaySolver	18 (90%) - 0	2	-	-

Table 3. Table 3: Statistics on the multi-dimensional benchmarks.

Solver	Solved	T.O.	Fastest	Mean-Time (87)
GenZielonka	128 (84%)	24	33 (25%)	66 ms
GenZiel&GenBüchiSolver	130 (86%)	22	72 (55%)	56 ms
GenZiel&GenGoodEpSolver	112 (74%)	40	24 (18%)	644 ms
GenZiel&GenLaySolver	110 (72%)	42	3 (2%)	1133 ms
GenBüchiSolver	110 (72%) - 20	22	-	-
GenGoodEpSolver	112 (74%) - 0	40	-	-
GenLaySolver	104 (68%) - 6	42	-	-

Equations

$${\mathsf{Cpre}}_i(G,U)$$

$$X_0$$

$$X_{j+1}$$

$$X_0$$

$$X_{j+1}$$

$$v_0\in \mathsf{Win}(G,0,\mathsf{GenB}\ddot{\mathsf{u}}\mathsf{chi}(U_1,\dots ,U_k)\cap \mathsf{CoB}\ddot{\mathsf{u}}\mathsf{chi}(U^{\prime }))$$

$$⟹$$

$$v_0\in \mathsf{Win}(G,1,\mathsf{B}\ddot{\mathsf{u}}\mathsf{chi}(U)\cap \mathsf{CoB}\ddot{\mathsf{u}}\mathsf{chi}(U^{\prime }))$$

$$⟹$$

$$W^{\prime }=\mathsf{Win}(G,i,\mathsf{B}\ddot{\mathsf{u}}\mathsf{chi}(U)\cap \mathsf{Safe}(U^{\prime })),W={\mathsf{Attr}}_i(G,W^{\prime })$$

$$T_j$$

$$A_j$$

$$F_j$$

$$C_0$$

$$C_1$$

$$B_0$$

$$B_1$$

$$B_p$$

$$A_j$$

$$F_j$$

$$B_p$$

$$C_p$$

Full text

1 Introduction

Since the early nineties, parity games have been attracting a large attention in the formal methods and theoretical computer science communities for two main reasons. First, parity games are used as intermediary steps in the solution of several relevant problems like, among others, the reactive synthesis problem from LTL specifications [17] or the emptiness problem for tree automata [8]. Second, their exact complexity is a long standing open problem: while we know that they are in ${\sf NP}\cap{\sf coNP}$ [8] (and even in ${\sf UP}\cap{\sf coUP}$ [15]), we do not yet have a polynomial time algorithm to solve them. Indeed, the best known algorithm so far has a worst-case complexity which is quasi-polynomial [3].

The classical algorithm for reactive synthesis from LTL specifications is as follows: from an LTL formula $\phi$ whose propositional variables are partitioned into inputs (controllable by the environment) and outputs (controlled by the system), construct a deterministic parity automaton (DPA) $A_{\phi}$ that recognizes the set of traces that are models of $\phi$. This DPA can then be seen as a two player graph game where the two players choose in turn the values of the input variables (Player 1) and of the output variables (Player 0). The winning condition in this game is the parity acceptance condition of the DPA. The two main difficulties with this approach are that the DPA may be doubly exponential in the size of $\phi$ and that its parity condition may require exponentially many priorities. So the underlying parity game may be hard to solve with the existing algorithms (which are not polynomial time). These difficulties have triggered two series of results.

First, incomplete algorithms that partially solve parity games in polynomial time have been investigated in [12, 13, 1]. Although they are incomplete, experimental results show that they behave well on benchmarks generated with a random model and on examples that are forcing the worst-case behavior of the classical recursive algorithm for solving parity games due to Zielonka [19]. The latter algorithm has a worst-case complexity which is exponential in the number of priorities of the parity condition. Second, compositional approaches to generate the automata from LTL specifications have been advocated, when the LTL formula $\phi$ is a conjunction of smaller formulas, i.e., $\phi=\phi_{1}\land\phi_{2}\cdots\land\phi_{n}$. In this case, the procedure constructs a DPA $A_{i}$ for each subformula $\phi_{i}$. The underlying game is then the product of the automata $A_{i}$ and the winning condition is the conjunction (for Player 0) of the parity conditions of each automaton. Those games are thus generalized parity games, that are known to be $\mathsf{co}$-$\mathsf{NP}$-complete [6].

In this paper, we contribute to these two lines of research in several ways. First, we show how to extend the partial solvers for parity games to generalized parity games. In the generalized case, we also show how efficient data structures based on antichains can be used to retain efficiency. Second, we show how to combine partial solvers for parity games and generalized parity games with the classical recursive algorithms [19, 6]. In this combination, the recursive algorithm is only executed on the portion of the game graph that was not solved by the partial solver, and this is repeated at each recursive call. Third, we provide for the first time extensive experiments that compare all those algorithms on benchmarks that are generated from LTL specifications used in the LTL synthesis competition [14]. For parity games, our experiments show behaviors that differ largely from the behaviors observed on experiments done on random graphs only. Indeed Zielonka’s algorithm is faster than partial solvers on average which was not observed on random graphs in [13]. Equally interestingly, we show that there are instances of our benchmarks of generalized parity games that cannot be solved by the classical recursive algorithm or by any of the partial solvers alone, but that can be solved by algorithms that combine them. We also show that when combined with partial solvers, the performances of the classical recursive algorithms are improved on a large portion of our benchmarks for both the parity and generalized parity cases.

The structure of the paper is as follows. In Section 2, we recall the useful notions on two-player games played on graphs. In particular we recall the notions of parity game and generalized parity game. In Section 3, we explain how the classical recursive algorithms for parity games and generalized parity can be combined with partial solvers and under which hypothesis the resulting algorithm is correct. In Sections 4-6, we present the three partial solvers proposed in [12, 13] for parity games and we explain how to extend them to generalized parity games. For the extended partial solver of Section 5, we also explain how to transform it into an antichain-based algorithm. In the last Section 7, we present our experiments that compare the three partial solvers for both parity games and generalized parity games.

2 Preliminaries

Game structures.

A game structure is a tuple $G=(V_{0},V_{1},E)$ where

• •

$(V,E)$ is a finite directed graph, with $V=V_{0}\cup V_{1}$ the set of vertices and $E\subseteq V\times V$ the set of edges such that111This condition guarantees that there is no deadlock. for each $v\in V$, there exists $(v,v^{\prime})\in E$ for some $v^{\prime}\in V$,

• •

$(V_{0},V_{1})$ forms a partition of $V$ such that $V_{i}$ is the set of vertices controlled by player $i$ with $i\in\{0,1\}$.

Given $U\subseteq V$, if $G_{\restriction U}=(V_{0}\cap U,V_{1}\cap U,E\cap(U\times U))$ has no deadlock, then $G_{\restriction U}$ is called the subgame structure induced by $U$.

A play in $G$ is an infinite sequence of vertices $\pi=v_{0}v_{1}\ldots\in V^{\omega}$ such that $(v_{j},v_{j+1})\in E$ for all $j\in\mathbb{N}$. Histories in $G$ are finite sequences $h=v_{0}\ldots v_{j}\in V^{+}$ defined in the same way. We denote by $\mathsf{Plays}(G)$ the set of plays in $G$ and by $\mathsf{Plays}(v_{0})$ the set of plays starting in a given initial vertex $v_{0}$. Given a play $\pi=v_{0}v_{1}\ldots$, the set $\mathsf{Occ}(\pi)$ denotes the set of vertices that occur in $\pi$, and the set $\mathsf{Inf}(\pi)$ denotes the set of vertices that occur infinitely often in $\pi$, i.e., $\mathsf{Occ}(\pi)=\{v\in V\mid\exists j\geq 0,v_{j}=v\}$ and $\mathsf{Inf}(\pi)=\{v\in V\mid\forall j\geq 0,\exists k\geq j,\ v_{k}=v\}$.

Strategies.

A strategy $\sigma_{i}$ for player $i\in\{0,1\}$ is a function $\sigma_{i}\colon V^{*}V_{i}\rightarrow V$ assigning to each history $hv\in V^{*}V_{i}$ a vertex $v^{\prime}=\sigma_{i}(hv)$ such that $(v,v^{\prime})\in E$. It is memoryless if $\sigma_{i}(hv)=\sigma_{i}(h^{\prime}v)$ for all histories $hv,h^{\prime}v$ ending with the same vertex $v$, that is, $\sigma_{i}$ is a function $\sigma_{i}\colon V_{i}\rightarrow V$. More generally, it is finite-memory if $\sigma_{i}(hv)$ needs only a finite information out of the history $hv$. This is possible with a finite-state machine that keeps track of histories of plays (see [11] for a precise definition). Given a strategy $\sigma_{i}$ of player $i$, a play $\pi=v_{0}v_{1}\ldots$ of $G$ is consistent with $\sigma_{i}$ if $v_{j+1}=\sigma_{i}(v_{0}\ldots v_{j})$ for all $j\in\mathbb{N}$ such that $v_{j}\in V_{i}$. Consistency is naturally extended to histories in a similar way.

Objectives.

An objective for player $i$ is a set of plays $\Omega\subseteq\mathsf{Plays}(G)$. It is called prefix-independent whenever $\pi\in\Omega$ if and only if $h\pi\in\Omega$ for all plays $\pi,h\pi$. A game $(G,\Omega)$ is composed of a game structure $G$ and an objective $\Omega$ for player [math]. A play $\pi$ is winning for player [math] if $\pi\in\Omega$, and losing otherwise. The games that we here study are zero-sum: player $1$ has the opposite objective $\overline{\Omega}=V^{\omega}\setminus\Omega$, meaning that a play $\pi$ is winning for player [math] if and only if it is losing for player $1$. Given a game $(G,\Omega)$ and an initial vertex $v_{0}$, a strategy $\sigma_{0}$ for player [math] is winning from $v_{0}$ if all the plays $\pi\in\mathsf{Plays}(v_{0})$ consistent with $\sigma_{0}$ belong to $\Omega$. Vertex $v_{0}$ is thus called winning for player [math]. We also say that player [math] is winning from $v_{0}$. We denote by ${\mathsf{Win}}({G},{0},{\Omega})$ the set of such winning vertices $v_{0}$. Similarly we denote by ${\mathsf{Win}}({G},{1},{\overline{\Omega}})$ the set of vertices from which player $1$ can ensure his objective $\overline{\Omega}$. Thus given a player $i$ and an objective $\Omega$, ${\mathsf{Win}}({G},{i},{\Omega})$ is the set of vertices from which player $i$ can ensure $\Omega$ in the game structure $G$.

A game $(G,\Omega)$ is determined if each of its vertices belongs to ${\mathsf{Win}}({G},{0},{\Omega})$ or ${\mathsf{Win}}({G},{1},{\overline{\Omega}})$. Martin’s theorem [16] states that all games with Borel objectives are determined. The problem of solving a game $(G,\Omega)$ means to decide, given an initial vertex $v_{0}$, whether player [math] is winning from $v_{0}$ for $\Omega$ (or dually whether player $1$ is winning from $v_{0}$ for $\overline{\Omega}$ when the game is determined). The sets ${\mathsf{Win}}({G},{0},{\Omega})$ and ${\mathsf{Win}}({G},{1},{\overline{\Omega}})$ are also called the solutions of the game.

Parity and generalized parity objectives.

Let $G$ be a game structure and $d\in\mathbb{N}$ be an integer. Let $\alpha\colon V\rightarrow[d]$, with $[d]=\{0,1,\ldots,d\}$, be a priority function that associates a priority with each vertex. The parity objective $\Omega=\mathsf{EvenParity}(\alpha)$ asks that the maximum priority seen infinitely often along a play is even, i.e., $\mathsf{EvenParity}(\alpha)=\{\pi\in\mathsf{Plays}(G)\mid\max_{v\in\mathsf{Inf}(\pi)}\alpha(v)\mbox{ is even}\}$. Games $(G,\mathsf{EvenParity}(\alpha))$ are called parity games. In those games, player $1$ has the opposite objective $\overline{\Omega}$ equal to $\{\pi\in\mathsf{Plays}(G)\mid\max_{v\in\mathsf{Inf}(\pi)}\alpha(v)\mbox{ is odd}\}$. We denote $\overline{\Omega}$ by $\mathsf{OddParity}(\alpha)$. In the sequel, an $i$-priority means an even priority if $i=0$ and an odd priority if $i=1$. For convenience, we also use notation ${i}\mathsf{Parity}(\alpha)$ such that ${0}\mathsf{Parity}(\alpha)=\mathsf{EvenParity}(\alpha)$ and ${1}\mathsf{Parity}(\alpha)=\mathsf{OddParity}(\alpha)$. Notice that objective ${i}\mathsf{Parity}(\alpha)$ is prefix-independent.

We now consider $k\geq 1$ priority functions $\alpha_{\ell}\colon V\rightarrow[d_{\ell}]$, $\ell\in\{1,\ldots,k\}$. The generalized parity objective $\Omega=\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k})$ is the conjunction of the parity objectives defined by all $\alpha_{\ell}$, i.e., $\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k})=\bigcap_{\ell=1}^{k}\mathsf{EvenParity}(\alpha_{\ell})$. Thus the opposite objective $\overline{\Omega}$ for player $1$ is equal to $\mathsf{DisjOddParity}=\bigcup_{\ell=1}^{k}\mathsf{OddParity}(\alpha_{\ell})$. Games $(G,\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k}))$ are called generalized parity games.

Parity games and generalized parity games are determined because their objectives are $\omega$-regular and thus Borel. The complexity of solving those games is stated in the next theorem, as well as the memory requirements for the winning strategies.

Theorem 2.1

• •

Solving parity games is in $\mathsf{UP}\cap\mathsf{co}$-$\mathsf{UP}$* and both players have memoryless winning strategies [15].*

• •

Solving generalized parity games is $\mathsf{co}$-$\mathsf{NP}$-complete, player $1$ has memoryless winning strategies, and finite-memory strategies are necessary and sufficient for player [math] to win **[6]**.

Partial solvers.

In this paper, we study partial solvers for parity games and generalized parity games, that are algorithms that partially compute their solutions. A partial solver returns two partial sets of winning vertices $Z_{0}\subseteq{\mathsf{Win}}({G},{0},{\Omega})$ and $Z_{1}\subseteq{\mathsf{Win}}({G},{1},{\overline{\Omega}})$ such that $G_{\restriction U}$ is a subgame structure with $U=V\setminus(Z_{0}\cup Z_{1})$. In the next sections, we present the polynomial time partial solvers proposed in [12, 13] for parity games and show how to extend them to generalized parity games.

Other $\omega$-regular objectives.

We recall some other useful $\omega$-regular objectives. Given a game structure $G$ and subsets $U,U_{1},\ldots,U_{k}\subseteq V$:

• •

the reachability objective asks to visit $U$ (called target set) at least once, i.e. $\mathsf{Reach}(U)=\{\pi\in\mathsf{Plays}(G)\mid\mathsf{Occ}(\pi)\cap U\neq\emptyset\}$,

• •

the safety objective asks to avoid visiting $U$ (called bad set), i.e. $\mathsf{Safe}(U)=\{\pi\in\mathsf{Plays}(G)\mid\mathsf{Occ}(\pi)\cap U=\emptyset\}$,

• •

the Büchi objective asks to visit infinitely often a vertex of $U$, i.e. $\mathsf{B\ddot{u}chi}(U)=\{\pi\in\mathsf{Plays}(G)\mid\mathsf{Inf}(\pi)\cap U\neq\emptyset\}$,

• •

the co-Büchi objective asks to avoid visiting infinitely often $U$, i.e. $\mathsf{CoB\ddot{u}chi}(U)=\{\pi\in\mathsf{Plays}(G)\mid\mathsf{Inf}(\pi)\cap U=\emptyset\}$,

• •

the generalized Büchi objective $\mathsf{GenB\ddot{u}chi}(U_{1},\ldots,U_{k})$ is equal to the intersection $\bigcap_{\ell=1}^{k}\mathsf{B\ddot{u}chi}(U_{\ell})$.

The next theorem summarizes the time complexities for solving those games as implemented in our prototype tool.222A better algorithm in $O(|V|^{2})$ for Büchi objectives is proposed in [5], and in $O(k\cdot|V|^{2})$ for generalized Büchi objectives in [4].

Theorem 2.2

For solving games $(G,\Omega)$, we have the following time complexities.

• •

Reachability, safety objectives: $O(|E|)$ **[11]**.

• •

Büchi, co-Büchi, Büchi $\cap$ safety objectives: $O(|V|\cdot|E|)$ **[11]**.

• •

Generalized Büchi, generalized Büchi $\cap$ safety objectives: $O(k\cdot|V|\cdot|E|)$333This result is obtained thanks to a classical reduction to games with Büchi objectives [2]..

Attractors.

We conclude this section with some basic notions related to the concept of attractor. Let $G$ be a game structure. The controllable predecessors for player $i$ of a set $U\subseteq V$, denoted by ${\mathsf{Cpre}}_{i}({G},{U})$, is the set of vertices from which player $i$ can ensure to visit $U$ in one step. Formally,

[TABLE]

The attractor ${\mathsf{Attr}}_{i}({G},{U})$ for player $i$ is the set of vertices from which he can ensure to visit $U$ in any number of steps (including zero steps). It is constructed by induction as follows: ${\mathsf{Attr}}_{i}({G},{U})=\bigcup_{j\geq 0}X_{j}$ such that:

[TABLE]

It is therefore equivalent to the winning set ${\mathsf{Win}}({G},{i},{\mathsf{Reach}(U)})$. The positive attractor ${\mathsf{PAttr}}_{i}({G},{U})$ is the set of vertices from which player $i$ can ensure to visit $U$ in any positive number of steps, that is, ${\mathsf{PAttr}}_{i}({G},{U})=\bigcup_{j\geq 0}X_{j}$ such that:

[TABLE]

Given $U\subseteq V$, we say that $U$ is an $i$-trap if for all $v\in U\cap V_{i}$ and all $(v,v^{\prime})\in E$, we have $v^{\prime}\in U$ (player $i$ cannot leave $U$), and for all $v\in U\cap V_{1-i}$, there exists $(v,v^{\prime})\in E$ such that $v^{\prime}\in U$ (player $1-i$ can ensure to stay in $U$). Therefore $G_{\restriction U}$ is a subgame structure. When $V\setminus U$ is an $i$-trap, we also use the notation $G\setminus U$ (instead of $G_{\restriction V\setminus U}$) for the subgame structure induced by $V\setminus U$. The next properties are classical.

Theorem 2.3 ([11])

Let $G$ be a game structure, $i\in\{0,1\}$ be a player, and $U\subseteq V$ be a subset of vertices. Then

• •

the attractor ${\mathsf{Attr}}_{i}({G},{U})$ and the positive attractor ${\mathsf{PAttr}}_{i}({G},{U})$ can be computed in $O(|E|)$ time,

• •

the set $V\!\setminus\!{\mathsf{Attr}}_{i}({G},{U})$ is an $i$-trap.

3 Zielonka’s algorithm with partial solvers

The classical algorithm used to solve parity games is the recursive algorithm proposed by Zielonka in [19]. Despite its relatively bad theoretical $O(|V|^{d})$ time complexity, it is known to outperform other algorithms in practice [10, 18]. This algorithm solves parity games $(G,\mathsf{EvenParity}(\alpha))$ by working in a divide-and-conquer manner, combining solutions of subgames to obtain the solution of the whole game. It returns two sets $\{W_{0},W_{1}\}$ such that $W_{i}={\mathsf{Win}}({G},{i},{{i}\mathsf{Parity}(\alpha)})$ is the winning set for player $i$. The recursion in this algorithm is performed both on the number of priorities and of nodes in the game. See Algorithm 1 in which no call to a partial solver is performed (therefore line 4 is to be replaced by $\{Z_{0},Z_{1}\}=\{\emptyset,\emptyset\}$). This algorithm is called Algorithm Zielonka.

Let us explain how Zielonka’s algorithm can be combined with a partial solver for parity games (see Algorithm 1). When $V$ is not empty, we first execute the partial solver. If it solves completely the game, we are done. Otherwise, let $\overline{G}$ be the subgame of $G$ that was not solved. We then execute the Zielonka instructions on $\overline{G}$ and we return the union of the partial solutions obtained by the partial solver with the solutions obtained for $\overline{G}$. Proposition 1 below guarantees the soundness of this approach under the hypothesis that if some player wants to escape from $\overline{G}$, then he will necessarily go to the partial solution of the other player.

Proposition 1

Suppose that the partial solver used in Algorithm 1 computes partial solutions $Z_{0},Z_{1}$ such that for all $(v,v^{\prime})\in E$ and $i\in\{0,1\}$, if $v\in\overline{V}\cap V_{i}$ and $v^{\prime}\not\in\overline{V}$, then $v^{\prime}\in Z_{1-i}$. Then Algorithm Ziel&PSolver correctly computes the sets ${\mathsf{Win}}({G},{i},{{i}\mathsf{Parity}(\alpha)})$, for $i\in\{0,1\}$.

Proof

The proof is by induction and it supposes the soundness of both the (classical) Zielonka algorithm and the partial solver. Clearly, Algorithm 1 is correct in the basic cases $V=\emptyset$ (line 1) and $V\setminus Z=\emptyset$ (line 7).

Otherwise (see Figure 1), let $Z_{0},Z_{1}$ be the partial solutions computed by the partial solver (line 5). As $\overline{G}$ is a subgame by definition of a partial solver, a recursive call to Algorithm 1 can be executed with ${\overline{G}\setminus X}$ such that $X$ is the attractor computed in line 13 or 18. We know that:

the partial solutions computed by the partial solver are correct, 2. 2.

by induction hypothesis, the solutions computed recursively on $\overline{G}\setminus X$ are correct, 3. 3.

by Algorithm Zielonka, the solutions computed on $\overline{G}$ are thus correct, such that $X$ is part of the solution for some player $i_{0}$, 4. 4.

by Theorem 2.3, as $X$ is an attractor for player $i_{0}$, $\overline{V}\setminus X$ is a $i_{0}$-trap in $\overline{G}$.

We can thus define strategies $\sigma_{i}$, $i\in\{0,1\}$, in the whole game $G$ that are built (in the expected way) from the winning strategies of both players in the subgame $\overline{G}$ (by items 2 and 3) and their winning strategies with respect to $Z_{0},Z_{1}$ in $G$ (by item 1). These strategies are winning because:

• •

any player $i$ that can escape from $\overline{G}$ has no interest to escape because he will go to $Z_{1-i}$ by the hypothesis of Proposition 1, a part of $G$ where he is not winning (by item 1),

• •

only player $1-i_{0}$ can escape from $\overline{G}\setminus X$ to go to $X$ (by item 4), but he has no interest to escape since he is not winning in $X$ (by item 3). ∎

An extension of Zielonka’s algorithm to generalized parity games is introduced in [6]444This algorithm is referred to as “the classical algorithm” in [6].. This algorithm, that we call GenZielonka, has $O(|E|\cdot|V|^{2D})\binom{D}{d_{1},\ldots,d_{k}}$ time complexity where $D=\Sigma_{\ell=1}^{k}d_{\ell}$. While more complex, it has the same behavior with respect to the recursive call: an attractor $X$ is computed as part of the solution of one player and a recursive call is executed on the subgame $G\setminus X$. Therefore, as done in Algorithm 1, this algorithm can be combined with a partial solver for generalized parity games, as long as the latter satisfies the hypothesis of Proposition 1.

In the following sections, we present three partial solvers for parity games and their extension to generalized parity games. They all satisfy the assumptions of Proposition 1 because the partial solutions that they compute, if non empty, are composed of one or several attractors (see Theorem 2.3).

4 Algorithms BüchiSolver and GenBüchiSolver

In this section, we present simple partial solvers for parity games and generalized parity games. More elaborate and powerful partial solvers are presented in the next two sections. These first partial solvers are based on Propositions 1 and 2 that are direct consequences of the definition of parity games and generalized parity games. The first proposition states that for parity games, if player $i$ can ensure to visit infinitely often an $i$-priority without visiting infinitely often a greater $(1-i)$-priority, then he is winning for ${i}\mathsf{Parity}(\alpha)$.

Proposition 1

Let $(G,\mathsf{EvenParity}(\alpha))$ be a parity game and $p\in[d]$ be an $i$-priority. Let $U=\{v\in V\mid\alpha(v)=p\}$ and $U^{\prime}=\{v\in V\mid\alpha(v)$ is a $(1-i)$-priority and $\alpha(v)>p\}$. For all $v_{0}\in V$, if $v_{0}\in{\mathsf{Win}}({G},{i},{\mathsf{B\ddot{u}chi}(U)\cap\mathsf{CoB\ddot{u}chi}(U^{\prime})})$, then $v_{0}\in{\mathsf{Win}}({G},{i},{{i}\mathsf{Parity}(\alpha)})$. ∎

The second proposition states that for generalized parity games, (i) if player [math] can ensure to visit infinitely often a [math]-priority $p_{\ell}$ without visiting infinitely often a $1$-priority greater than $p_{\ell}$ on all dimensions $\ell$, then he is winning in the generalized parity game, and (ii) if player $1$ can ensure to visit infinitely often a $1$-priority $p_{\ell}$ without visiting infinitely often a [math]-priority greater than $p_{\ell}$ on some dimension $\ell$, then he is winning in the generalized parity game.

Proposition 2

Let $(G,\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k}))$ be a generalized parity game.

• •

Let $p=(p_{1},\ldots,p_{k})$, with $p_{\ell}\in[d_{\ell}]$, be a vector of [math]-priorities. For all $\ell$, let $U_{\ell}=\{v\in V\mid\alpha_{\ell}(v)=p_{\ell}\}$. Let $U^{\prime}=\{v\in V\mid\exists\ell,\,\alpha_{\ell}(v)$ is a $1$-priority and $\alpha_{\ell}(v)>p_{\ell}\}$. For all $v_{0}\in V$,

[TABLE]

• •

Let $\ell\in\{1,\ldots,k\}$ and $p_{\ell}\in[d_{\ell}]$ be a $1$-priority. Let $U=\{v\in V\mid\alpha_{\ell}(v)=p_{\ell}\}$ and $U^{\prime}=\{v\in V\mid\alpha_{\ell}(v)$ is a [math]-priority and $\alpha_{\ell}(v)>p_{\ell}\}$. For all $v_{0}\in V$,

[TABLE]

• ∎*

Partial Solver for Parity Games.

A partial solver for parity games can be easily derived from Proposition 1. Given a parity game $(G,\mathsf{EvenParity}(\alpha))$, the polynomial time algorithm BüchiSolver (see Algorithm 2) tries to find winning vertices for each player by applying this proposition as follows. Let us denote by $W_{p}$ the winning set computed by the algorithm for priority $p$ (line 5) and let us suppose (for simplicity) that the loop in line 1 treats the priorities from the highest one $d$ to the lowest one [math]. This algorithm thus computes $W_{d}$, $W_{d-1},\ldots$, until finding $W_{p}\neq\emptyset$. At this stage, the algorithm was able to find some winning vertices. It then repeats the process on the subgame $G\setminus W_{p}$ to find other winning vertices. At the end of the execution, it returns the partial solutions $\{Z_{0},Z_{1}\}$ that it was able to compute.

Notice that we could replace line 5 by

[TABLE]

since ${\mathsf{Attr}}_{i}({G},{W^{\prime}})\subseteq{\mathsf{Win}}({G},{i},{\mathsf{B\ddot{u}chi}(U)\cap\mathsf{CoB\ddot{u}chi}(U^{\prime})})$ (as the parity objective is prefix-independent, it is closed under attractor; and computing the attractor is necessary to get a subgame for the recursive call). This variant is investigated in [12, 13] under the name of Algorithm psolB.

Partial Solver for Generalized Parity Games.

Similarly, a partial solver for generalized parity games can be derived from Proposition 2. Instead of considering all $p\in[d]$ as done in line 1 of Algorithm BüchiSolver, we have here a more complex loop on all elements that are

• •

either a $1$-priority $p$ for some given dimension $\ell$ (case of player $1$),

• •

or a vector $(p_{1},\ldots,p_{k})$ with [math]-priorities $p_{\ell}$ (case of player [math]).

We suppose that we have a list $L$ of all possible such elements $(p,\ell)$ and $(p_{1},\ldots,p_{k})$. Given a generalized parity game, Algorithm GenBüchiSolver (see Algorithm 3) tries to find winning vertices for both players by applying Proposition 2. It returns the partial solutions $\{Z_{0},Z_{1}\}$ that it was able to compute. As in Algorithm BüchiSolver, objective $\mathsf{CoB\ddot{u}chi}(U^{\prime})$ can be replaced by $\mathsf{Safe}(U^{\prime})$ in lines 5 and 13 (with the addition of an attractor computation). This modification yields an algorithm in $O((\Pi_{\ell=1}^{k}\frac{d_{\ell}}{2})\cdot k\cdot|V|^{2}\cdot|E|)$ time by Theorem 2.2.

5 Algorithms GoodEpSolver and GenGoodEpSolver

In this section, we present a second polynomial time partial solver for parity games as proposed in [13]. We then explain how to extend it for partially solving generalized parity games. We finally explain how the latter solver can be transformed into a more efficient (in practice) antichain-based algorithm.

Partial solver for parity games.

In Section 4, given a parity game, the basic action of Algorithm BüchiSolver is to compute the set of winning vertices for player $i$ for the objective $\mathsf{B\ddot{u}chi}(U)\cap\mathsf{CoB\ddot{u}chi}(U^{\prime})$ that imposes to visit infinitely often a given $i$-priority $p$ (set $U$) without visiting infinitely often any greater $(1-i)$-priority (set $U^{\prime}$). In this section, this approach is extended to the set of all $i$-priorities instead of only one $i$-priority $p$.

To this end, we consider the extended game structure $G\times M$ with $M=[d]$ such that $m\in M$ records the maximum visited priority. More precisely, the set of vertices of $G\times M$ is equal to $V\times M$ where $V_{i}\times M$ is the set of vertices controlled by player $i$, and the set $E_{{M}}$ of its edges is composed of all pairs $((v,m),(v^{\prime},m^{\prime}))$ such that $(v,v^{\prime})\in E$ and $m^{\prime}=\max\{m,\alpha(v)\}$. Clearly, with this construction, in $G$, player $i$ can ensure to visit $v$ from $v_{0}$ such that the maximum visited priority ($v$ excluded) is an $i$-priority if and only if in $G\times M$, he can ensure to visit $(v,m)$ from $(v,\alpha(v_{0}))$ for some $i$-priority $m$.

We want to compute a set ${\mathsf{GoodEp}}_{i}({G},{\alpha})$ such that if $v_{0}\in{\mathsf{GoodEp}}_{i}({G},{\alpha})$, then player $i$ is winning from $v_{0}$ for ${i}\mathsf{Parity}(\alpha)$. We proceed by computing the following sequence $F^{(i)}=\bigcap_{j\geq 0}F_{j}$. Initially $F_{0}=V$ and for $j\geq 1$, $F_{j}$ is computed from $F_{j-1}$ as follows:

[TABLE]

Intuitively, if $v_{0}\in F_{j}$, then player $i$ has a strategy to ensure to visit some vertex $v\in F_{j-1}$ such that the maximum visited priority along the consistent history $hv$ from $v_{0}$ to $v$ (priority of $v$ excluded) is some $i$-priority. We say that $h$ is a good episode. Notice that $h$ is non empty since each $A_{j}$ is a positive attractor.

We define ${\mathsf{GoodEp}}_{i}({G},{\alpha})$ as the fixpoint $F^{(i)}$. Therefore from a vertex $v_{0}$ in this fixpoint, player $i$ can ensure a succession of good episodes in which the maximum visited priority is an $i$-priority. Thus he is winning from $v_{0}$ for ${i}\mathsf{Parity}(\alpha)$ as formalized in the next proposition. Notice that if $v_{0}$ belongs to the attractor for player $i$ of ${\mathsf{GoodEp}}_{i}({G},{\alpha})$, then $v_{0}$ still belongs to ${\mathsf{Win}}({G},{i},{{i}\mathsf{Parity}(\alpha)})$ as the latter objective is prefix-independent.

Proposition 1 ([13])

Let $(G,\mathsf{EvenParity}(\alpha))$ be a parity game. Then for all $v_{0}\in V$, if $v_{0}\in{\mathsf{Attr}}_{i}({G},{F^{(i)}})$, then $v_{0}\in{\mathsf{Win}}({G},{i},{{i}\mathsf{Parity}(\alpha)})$.

From Proposition 1, we derive the polynomial time algorithm called GoodEpSolver (see Algorithm 4). This algorithm is called psolC in [13].

Partial solver for generalized parity games.

The same approach can be applied to generalized parity games with some adaptations that depend on the player. Recall that the basic action of Algorithm GenBüchiSolver in Section 4 is (i) to test whether player [math] can ensure to visit infinitely often a [math]-priority $p_{\ell}$ without visiting infinitely often a $1$-priority greater than $p_{\ell}$ on all dimensions $\ell$, or (ii) to test whether player $1$ can ensure to visit infinitely often a $1$-priority $p_{\ell}$ without visiting infinitely often a [math]-priority greater than $p_{\ell}$ on some dimension $\ell$.

Therefore, for player $1$, in place of lines 3-5 of Algorithm 3 we can now apply the GoodEpSolver approach by computing $W={\mathsf{GoodEp}}_{1}({G},{\alpha_{\ell}})$.

For player [math], we have to deal with vectors of [math]-priorities. We thus consider the extended game structure $G\times M_{1}\times\ldots\times M_{k}$ such that for all $\ell$, $M_{\ell}$ is equal to $[d_{\ell}]$, and where $m_{\ell}\in M_{\ell}$ records the maximum visited priority in dimension $\ell$. Hence, the edges of this game structure have the form $((v,m_{1},\ldots,m_{k}),(v^{\prime},m^{\prime}_{1},\ldots,m^{\prime}_{k}))$ such that $(v,v^{\prime})\in E$ and $m^{\prime}_{\ell}=\max\{m_{\ell},\alpha_{\ell}(v)\}$ for all $\ell$. A good episode is now a history $h$ such that for all $\ell$, the maximum priority visited along $h$ in dimension $\ell$ is a [math]-priority. And the related set ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{\ell}})$ equal to $\bigcap_{j\geq 0}F_{j}$ is computed with Equations (4-6) modified as expected. We have the next counterpart of Proposition 1 with a similar proof.

Proposition 2

Let $(G,\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k}))$ be a generalized parity game. If $v_{0}\in{\mathsf{Attr}}_{0}({G},{F^{(i)}})$, then $v_{0}\in{\mathsf{Win}}({G},{0},{\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k})})$. ∎

For all the previous arguments, we derive Algorithm GenGoodEpSolver (see Algorithm 5). It tries to find a partial solution first for player $1$ (for some dimension $\ell$) and then for player $2$. By Theorem 2.2, its time complexity is in $O((\Pi_{\ell=1}^{k}d_{\ell})\cdot|V|^{2}\cdot|E|)$.

Partial solvers with antichains.

Algorithm GenGoodEpSolver has exponential time complexity due to the use of the extended structure $G\times M_{1}\times\ldots\times M_{k}$ associated to a generalized parity game, and in particular to the computation of ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}})$. We here show that the vertices of this extended game can be partially ordered in a way to obtain an antichain-based algorithm for the computation of ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}})$. The antichains allow compact representation and efficient manipulation of partially ordered sets [7].

Let us first recall the basic notions about antichains. Consider a partially ordered set $(S,\preceq)$ where $S$ is a finite set and $\preceq\,\subseteq S\times S$ is a partial order on $S$. Given $s,s^{\prime}\in S$, we write $s\sqcap s^{\prime}$ their greatest lower bound if it exists. A lower semilattice is a partially ordered set such that this greater lower bound always exists for all $s,s^{\prime}\in S$. Given two subsets $R,R^{\prime}\subseteq S$, we denote by $R\sqcap R^{\prime}$ the set $\{s\sqcap s^{\prime}\mid s\in R,s^{\prime}\in R^{\prime}\}$.

Given a lower semilattice $(S,\preceq)$, an antichain $A$ is a subset of $S$ composed of pairwise incomparable elements with respect to $\preceq$. Given a subset $R\subseteq S$, we denote $\lceil R\rceil$ the set of its maximal elements (which is thus an antichain). We say that $R$ is closed if whenever $s\in R$ and $s^{\prime}\preceq s$, then $s^{\prime}\in R$. If $A$ is an antichain, we denote by $\downarrow\!A$ the closed set that it represents, that is, $A=\lceil\downarrow\!A\rceil$. Hence when $R$ is closed, we have $R=\,\downarrow\!\lceil R\rceil$. The benefit of antichains is that they provide a compact representation of closed sets. Moreover some operations on those closed sets can be done at the level of their antichains as indicated in the next proposition.

Proposition 3 ([7])

Let $(S,\preceq)$ be a lower semilattice, and $R,R^{\prime}\subseteq S$ be two closed sets represented by their antichains $A=\lceil R\rceil,A^{\prime}=\lceil R^{\prime}\rceil$. Then

• •

for all $s\in S$, $s\in R$ if and only if there exists $s^{\prime}\in A$ such that $s\preceq s^{\prime}$,

• •

$R\cup R^{\prime}$* is closed, and $\lceil R\cup R^{\prime}\rceil=\lceil A\cup A^{\prime}\rceil$,*

• •

$R\cap R^{\prime}$* is closed, and $\lceil R\cap R^{\prime}\rceil=\lceil A\sqcap A^{\prime}\rceil$.*

For simplicity, we focus on the extended structure $G\times M$ associated to a parity game and begin to explain an antichain-based algorithm for the computation of set ${\mathsf{GoodEp}}_{0}({G},{\alpha})$ (this algorithm is inspired from [9]). We will explain later what are the needed adaptations to compute ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}})$ in generalized parity games. We equip $V\times M$ with the following partial order:

Definition 4

We define the strict partial order $\prec$ on $V\times M$ such that $(v^{\prime},m^{\prime})\prec(v,m)$ if and only if $v=v^{\prime}$ and:

either $m,m^{\prime}$ are even and $m^{\prime}>m$, 2. 2.

or $m,m^{\prime}$ are odd and $m^{\prime}<m$, 3. 3.

or $m$ is odd and $m^{\prime}$ is even.

We define $(v^{\prime},m^{\prime})\preceq(v,m)$ if either $(v^{\prime},m^{\prime})=(v,m)$ or $(v^{\prime},m^{\prime})\prec(v,m)$.

For instance, if $[d]=[4]$, then $(v,4)\prec(v,2)\prec(v,0)\prec(v,1)\prec(v,3)$. With this definition, two elements $(v,m),(v^{\prime},m^{\prime})$ are incomparable as soon as $v\neq v^{\prime}$. It follows that in Proposition 3, if $R\subseteq\{v\}\times M$ and $R^{\prime}\subseteq\{v^{\prime}\}\times M$ with $v\neq v^{\prime}$, then the union $A\cup A^{\prime}$ of their antichains is already an antichain, that is, $A\cup A^{\prime}=\lceil A\cup A^{\prime}\rceil$. Moreover, the operator $\sqcap$ useful in Proposition 3 is defined as indicated in the next lemma.

Lemma 5

Let $(v,m),(v,m^{\prime})\in V\times M$. Then $(v,m)\sqcap(v,m^{\prime})$ is equal to:

• •

$(v,\max\{m,m^{\prime}\})$* if $m,m^{\prime}$ are even,*

• •

$(v,\min\{m,m^{\prime}\})$* if $m,m^{\prime}$ are odd,*

• •

$(v,m)$* if $m$ is even and $m^{\prime}$ is odd,*

• •

$(v,m^{\prime})$* if $m$ is odd and $m^{\prime}$ is even.*

• ∎*

The computation of ${\mathsf{GoodEp}}_{0}({G},{\alpha})$ is based on Equations (4-6). Equation (5) involves the computation of positive attractors over $G\times M$ thanks to Equations (1-3). We are going to show that ${\mathsf{GoodEp}}_{0}({G},{\alpha})$ is a closed set as well as all the intermediate sets to compute it. It will follow that all the computations can be performed directly on the antichains that represent those sets.

We already know from Proposition 3 that the family of closed sets is stable under union and intersection and how the computations can be done at the level of their antichains. So we now focus on the basic operation ${\mathsf{Cpre}}_{0}({G\times M},{U})$ form some $U\subseteq V\times M$. We need to introduce the following functions $up$ and $down$. Given $(v,m)\in V\times M$, we define $up(m,\alpha(v))=\max\{m,\alpha(v)\}$. Recall that such an update from $m$ to $m^{\prime}=up(m,\alpha(v))$ is used in the edges $((v,m),(v^{\prime},m^{\prime}))$ of $G\times M$. Function $down$ is defined hereafter. It is the inverse reasoning of function $up$: given $(v^{\prime},m^{\prime})\in V\times M$ and $(v,v^{\prime})\in E$, the value $down(m^{\prime},\alpha(v))$ yields the maximal value $m$ such that $(v^{\prime},up(m,\alpha(v)))\preceq(v^{\prime},m^{\prime})$.

Definition 6

Given $(v^{\prime},m^{\prime})\in V\times M$ and $p=\alpha(v)$, we define $m=down(m^{\prime},p)$ as follows:

Case $p$ even:

• •

if $p<m^{\prime}$ then $m=m^{\prime}$,

• •

else $m=\max\{p-1,0\}$, 2. 2.

Case $p$ odd:

• •

if $p\leq m^{\prime}$ then $m=m^{\prime}$,

• •

else $m=p+1$ except if $p=d$ in which case $down(m^{\prime},p)$ is not defined.

The next proposition states that if the set $U\subseteq V\times M$ is closed, then the set ${\mathsf{Cpre}}_{0}({G\times M},{U})$ is also closed. It also indicates how to design an antichain-based algorithm for computing ${\mathsf{Cpre}}_{0}({G\times M},{U})$. For convenience, we recall Equation (1): ${\mathsf{Cpre}}_{0}({G\times M},{U})=C_{0}\cup C_{1}$ with

[TABLE]

Proposition 7

If $U\subseteq V\times M$ is a closed set, then ${\mathsf{Cpre}}_{0}({G\times M},{U})$ is closed. Let $A=\lceil U\rceil$ be the antichain representing $U$. Then $\lceil{\mathsf{Cpre}}_{0}({G\times M},{U})\rceil=\lceil B_{0}\cup B_{1}\rceil$ where $B_{0},B_{1}$ are the following antichains:

[TABLE]

Let us come back to the computation of ${\mathsf{GoodEp}}_{0}({G},{\alpha})$, which depends on Equations (4-6) and Equations (1-3) for the positive attractors of Equation (5). By the next lemma, all sets $T_{j}$ of Equation (4) are closed, and thus, by Propositions 3 and 7, we get an antichain-based algorithm for computing ${\mathsf{GoodEp}}_{0}({G},{\alpha})$ as announced.

Lemma 8

Each $T_{j}$ of Equation (4) is a closed set that is represented by the antichain $\lceil T_{j}\rceil=\{(v,0)\mid v\in F_{j}\}$. ∎

It remains to prove Proposition 3. We first prove the next properties of functions $up$ and $down$.

Lemma 9

For all $(v,m),(v,m_{1}),(v,m_{2})\in V\times M$ with $(v,v^{\prime})\in E$ and $p=\alpha(v)$,

if $(v,m_{1})\preceq(v,m_{2})$, then $(v^{\prime},up(m_{1},p))\preceq(v^{\prime},up(m_{2},p))$, 2. 2.

$(v,m)\preceq(v,down(up(m,p),p))$.

For all $(v,m^{\prime}),(v^{\prime},m^{\prime}_{1}),(v^{\prime},m^{\prime}_{2})\in V\times M$ with $(v,v^{\prime})\in E$ and $p=\alpha(v^{\prime})$, such that $down(m^{\prime},p)$, $down(m^{\prime}_{1},p)$, $down(m^{\prime}_{2},p)$ are all defined,

if $(v^{\prime},m^{\prime}_{1})\preceq(v^{\prime},m^{\prime}_{2})$, then $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$, 2. 4.

$(v^{\prime},up(down(m^{\prime},p),p))\preceq(v^{\prime},m^{\prime})$.

Proof

We begin with the proof of Item 1. If $(v,m_{1})=(v,m_{2})$, then clearly $(v^{\prime},up(m_{1},p))=(v^{\prime},up(m_{2},p))$. Hence we suppose that $(v,m_{1})\prec(v,m_{2})$.

Suppose that $m_{1}<m_{2}$. According to Definition 4, this happens when $m_{1},m_{2}$ are odd (Case 2. of Definition 4) or when $m_{1}$ is even and $m_{2}$ is odd (Case 3. of Definition 4), in summary when $m_{2}$ is odd. If $p<m_{1}$, then $up(m_{1},p)=m_{1}$, $up(m_{2},p)=m_{2}$, and thus $(v^{\prime},up(m_{1},p))\prec(v^{\prime},up(m_{2},p))$. If $m_{1}\leq p<m_{2}$, then $up(m_{1},p)=p$, $up(m_{2},p)=m_{2}$. It follows that if $p$ is even then $(v^{\prime},up(m_{1},p))\prec(v^{\prime},up(m_{2},p))$ by Case 3. of Definition 4, and if $p$ is odd then then $(v^{\prime},up(m_{1},p))\prec(v^{\prime},up(m_{2},p))$ by Case 2. of Definition 4. If $m_{2}\leq p$, then $up(m_{1},p)=up(m_{2},p)=p$ and thus $(v^{\prime},up(m_{1},p))\preceq(v^{\prime},up(m_{2},p))$. 2. 2.

Suppose that $m_{2}<m_{1}$. According to Definition 4, this happens when $m_{1},m_{2}$ are even (Case 1. of Definition 4) or when $m_{1}$ is even and $m_{2}$ is odd (Case 3. of Definition 4), in summary when $m_{1}$ is even. If $p<m_{2}$, then $up(m_{1},p)=m_{1}$, $up(m_{2},p)=m_{2}$, and thus $(v^{\prime},up(m_{1},p))\prec(v^{\prime},up(m_{2},p))$. If $m_{2}\leq p<m_{1}$, then $up(m_{2},p)=p$, $up(m_{1},p)=m_{1}$. It follows that if $p$ is even then $(v^{\prime},up(m_{1},p))\prec(v^{\prime},up(m_{2},p))$ by Case 1. of Definition 4, and if $p$ is odd then $(v^{\prime},up(m_{1},p))\prec(v^{\prime},up(m_{2},p))$ by Case 3. of Definition 4. If $m_{1}\leq p$, then $up(m_{2},p)=up(m_{1},p)=p$ and thus $(v^{\prime},up(m_{1},p))\preceq(v^{\prime},up(m_{2},p))$.

Let us proceed to the proof of Item 2.

Suppose that $p$ is even. If $p<m$, then $up(m,p)=m$ and thus $down(up(m,p),p)=m$ (Case 1. of Definition 6). It follows that $(v,m)\preceq(v,down(up(m,p),p)$. If $p\geq m$ with $p\neq 0$, then $up(m,p)=p$ and thus $down(up(m,p),p)=p-1$. If $m$ is even, then $(v,m)\preceq(v,down(up(m,p),p)$ ($p-1$ is odd, Case 3. of Definition 4); and if $m$ is odd, then $p-1\geq m$ (since $m,p$ have different parities) and $(v,m)\preceq(v,down(up(m,p),p)$ ($p-1$ is odd, Case 2. of Definition 4). If $p\geq m$ with $p=0$, then $m=0$, $up(m,p)=0$ and thus $down(up(m,p),p)=0$ (Case 1. of Definition 6). It follows that $(v,m)\preceq(v,down(up(m,p),p)$. 2. 2.

Suppose that $p$ is odd. If $p\leq m$, then $up(m,p)=m$ and thus $down(up(m,p),p)=m$ (Case 2. of Definition 6). It follows that $(v,m)\preceq(v,down(up(m,p),p)$. If $p>m$, then $up(m,p)=p$ and thus $down(up(m,p),p)=p$ (Case 2. of Definition 6). Hence $(v,m)\preceq(v,down(up(m,p),p)$ for both possible parities of $m$ (Cases 2 and 3 of Definition 4).

We now treat Item 3. By hypothesis, $down(m^{\prime}_{1},p)$ and $down(m^{\prime}_{2},p)$ are supposed to be defined. If $(v,m^{\prime}_{1})=(v,m^{\prime}_{2})$, then clearly $(v,down(m^{\prime}_{1},p))=(v,down(m^{\prime}_{2},p))$. Hence we suppose that $(v,m^{\prime}_{1})\prec(v,m^{\prime}_{2})$.

Suppose that $m^{\prime}_{1}<m^{\prime}_{2}$. According to Definition 4, this happens when $m^{\prime}_{1},m^{\prime}_{2}$ are odd (Case 2. of Definition 4) or when $m^{\prime}_{1}$ is even and $m^{\prime}_{2}$ is odd (Case 3. of Definition 4), in summary when $m^{\prime}_{2}$ is odd.

Suppose first that $p$ is even (Case 1. of Definition 6). If $p<m^{\prime}_{1}$, then $down(m^{\prime}_{1},p)=m^{\prime}_{1}$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$, and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$. If $m^{\prime}_{1}\leq p<m^{\prime}_{2}$ with $p\neq 0$, then $down(m^{\prime}_{1},p)=p-1$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$. It follows that $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$ ($p-1,m^{\prime}_{2}$ are odd, Case 2. of Definition 4). If $m^{\prime}_{1}\leq p<m^{\prime}_{2}$ with $p=0$, then $down(m^{\prime}_{1},p)=0$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$. It follows that $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$ (Case 3. of Definition 4). If $m^{\prime}_{2}\leq p$, then $down(m^{\prime}_{1},p)=down(m^{\prime}_{2},p)=p-1$ and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$.

Suppose now that $p$ is odd (Case 2. of Definition 6). If $p\leq m^{\prime}_{1}$, then $down(m^{\prime}_{1},p)=m^{\prime}_{1}$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$, and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$. If $m^{\prime}_{1}<p\leq m^{\prime}_{2}$, then $down(m^{\prime}_{1},p)=p+1$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$. It follows that $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$ ($p+1$ is even, $m^{\prime}_{2}$ is odd, Case 3. of Definition 4). If $m^{\prime}_{2}<p$, then $down(m^{\prime}_{1},p)=down(m^{\prime}_{2},p)=p+1$ and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$. 2. 2.

Suppose that $m^{\prime}_{2}<m^{\prime}_{1}$. According to Definition 4, this happens when $m^{\prime}_{1},m^{\prime}_{2}$ are even (Case 1. of Definition 4) or when $m^{\prime}_{1}$ is even and $m^{\prime}_{2}$ is odd (Case 3. of Definition 4), in summary when $m^{\prime}_{1}$ is even.

Suppose first that $p$ is even (Case 1. of Definition 6). If $p<m^{\prime}_{2}$, then $down(m^{\prime}_{1},p)=m^{\prime}_{1}$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$, and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$. If $m^{\prime}_{2}\leq p<m^{\prime}_{1}$ with $p\neq 0$, then $down(m^{\prime}_{2},p)=p-1$, $down(m^{\prime}_{1},p)=m^{\prime}_{1}$. It follows that $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$ ($p-1$ is odd, $m^{\prime}_{1}$ is even, Case 3. of Definition 4). If $m^{\prime}_{1}\leq p<m^{\prime}_{2}$ with $p=0$, then $down(m^{\prime}_{2},p)=0$, $down(m^{\prime}_{1},p)=m^{\prime}_{1}$. It follows that $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$ (Case 1. of Definition 4). If $m^{\prime}_{1}\leq p$, then $down(m^{\prime}_{2},p)=down(m^{\prime}_{1},p)=p-1$ and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$.

Suppose now that $p$ is odd (Case 2. of Definition 6). If $p\leq m^{\prime}_{2}$, then $down(m^{\prime}_{1},p)=m^{\prime}_{1}$, $down(m^{\prime}_{2},p)=m^{\prime}_{2}$, and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$. If $m^{\prime}_{2}<p\leq m^{\prime}_{1}$, then notice that $p+1\leq m^{\prime}_{1}$ as $p,m^{\prime}_{1}$ have opposite parities. Moreover $down(m^{\prime}_{2},p)=p+1$, $down(m^{\prime}_{1},p)=m^{\prime}_{1}$. It follows that $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$ ($p+1,m^{\prime}_{1}$ are even, Case 1. of Definition 4). If $m^{\prime}_{2}<p$, then $down(m^{\prime}_{2},p)=down(m^{\prime}_{1},p)=p+1$ and thus $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$.

It remains to consider the last item. By hypothesis, $down(m,p)$ is supposed to be defined.

Suppose that $p$ is even (Case 1. of Definition 6). If $p<m^{\prime}$, we have that $down(m^{\prime},p)=m^{\prime}$ and thus $up(down(m^{\prime},p),p)=m^{\prime}$. It follows that $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$. If $p\geq m^{\prime}$ with $p\neq 0$, we have that $down(m^{\prime},p)=p-1$ and thus $up(down(m^{\prime},p),p)=p$. It follows that if $m^{\prime}$ is even then $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$ by Case 1. of Definition 4; and if $m^{\prime}$ is odd then $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$ by Case 3. of Definition 4. If $p\geq m^{\prime}$ with $p=0$, then $m^{\prime}=0$, $down(m^{\prime},p)=0$ and thus $up(down(m,p),p)=0$. It follows that $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$. 2. 2.

Suppose that $p$ is odd (Case 2. of Definition 6). If $p\leq m^{\prime}$, then we have that $down(m^{\prime},p)=m^{\prime}$ and thus $up(down(m^{\prime},p),p)=m^{\prime}$. It follows that $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$. If $p>m^{\prime}$, then $down(m^{\prime},p)=p+1$ and thus $up(down(m^{\prime},p),p)=p+1$. It follows that if $m^{\prime}$ is even then $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$ by Case 1. of Definition 4; and if $m^{\prime}$ is odd then $(v^{\prime},up(down(m^{\prime},p),p)\preceq(v^{\prime},m^{\prime})$ by Case 3. of Definition 4.

∎

Proof (of Proposition 7)

We first prove that if $U$ is closed, then ${\mathsf{Cpre}}_{0}({G\times M},{U})$ is also closed. To this end we use the monotonicity of function $up$ (Item 1. of Lemma 9). Let $(v,m_{1}),(v,m_{2})$ be such that $(v,m_{2})\in{\mathsf{Cpre}}_{0}({G\times M},{U})$ and $(v,m_{1})\preceq(v,m_{2})$. We have to show that $(v,m_{1})\in{\mathsf{Cpre}}_{0}({G\times M},{U})$. We first suppose that $v\in V_{0}$. Hence, by Equation (7), there exists $((v,m_{2}),(v^{\prime},m^{\prime}_{2}))\in E_{{M}}$ with $(v^{\prime},m^{\prime}_{2})\in U$. Recall that $m^{\prime}_{2}=up(m_{2},\alpha(v))$. Let $m^{\prime}_{1}=up(m_{1},\alpha(v))$. As $(v,m_{1})\preceq(v,m_{2})$, by monotonicity of $up$, it follows that $(v^{\prime},m^{\prime}_{1})\preceq(v^{\prime},m^{\prime}_{2})$. Since $U$ is closed, we have $(v^{\prime},m^{\prime}_{1})\in U$, and thus $(v,m_{1})\in{\mathsf{Cpre}}_{0}({G\times M},{U})$. The proof is similar if $v\in V_{1}$.

Let us now prove that $\lceil{\mathsf{Cpre}}_{0}({G\times M},{U})\rceil=\lceil C_{0}\cup C_{1}\rceil=\lceil B_{0}\cup B_{1}\rceil$ or equivalently that $C_{0}=\,\downarrow\!B_{0}$ and $C_{1}=\,\downarrow\!B_{1}$. We only prove the first equality thanks to Lemma 9, the latter one being proved similarly.

Let $(v,m_{1})\in C_{0}$ with $p=\alpha(v)$ and let us show that $(v,m_{1})\in\,\downarrow\!B_{0}$. By Equation (7), there exists $((v,m_{1}),(v^{\prime},m^{\prime}_{1}))\in E_{{M}}$ with $(v^{\prime},m^{\prime}_{1})\in U$ and $m^{\prime}_{1}=up(m_{1},p)$. As $A=\lceil U\rceil$, there exists $(v^{\prime},m^{\prime}_{2})\in A$ such that $(v^{\prime},m^{\prime}_{1})\preceq(v^{\prime},m^{\prime}_{2})$. Let $(v,m_{2})=(v,down(m^{\prime}_{2},p))\in\,\downarrow\!B_{0}$. By Item 3. of Lemma 9, we have $(v,down(m^{\prime}_{1},p))\preceq(v,down(m^{\prime}_{2},p))$. Moreover, as $m^{\prime}_{1}=up(m_{1},p)$, by Item 2. of Lemma 9, we have $(v,m_{1})\preceq(v,down(m^{\prime}_{1},p))$. Therefore $(v,m_{1})\preceq(v,m_{2})$ showing that $(v,m_{1})\in\,\downarrow\!B_{0}$.

Let $(v,m_{1})\in\,\downarrow\!B_{0}$ with $p=\alpha(v)$ and let us show that $(v,m_{1})\in C_{0}$. As $(v,m_{1})\in\,\downarrow\!B_{0}$, there exists $(v,m_{2})\in B_{0}$ such that $(v,m_{1})\preceq(v,m_{2})$. As $(v,m_{2})\in B_{0}$, there exists $((v,m_{2}),(v^{\prime},m^{\prime}_{2}))\in E_{{M}}$ with $(v^{\prime},m^{\prime}_{2})\in A$ and $m_{2}=down(m^{\prime}_{2},p)$. By Item 1. of Lemma 9, we have $(v^{\prime},up(m_{1},p))\preceq(v^{\prime},up(m_{2},p))$. Let $(v^{\prime},m^{\prime}_{1})=(v^{\prime},up(m_{1},p))$. By Item 4. of Lemma 9, we have $(v^{\prime},up(m_{2},p))\preceq(v^{\prime},m^{\prime}_{2})$. Therefore $(v^{\prime},m^{\prime}_{1})\preceq(v^{\prime},m^{\prime}_{2})$. As $(v^{\prime},m^{\prime}_{2})\in A=\lceil U\rceil$, then $(v^{\prime},m^{\prime}_{1})\in U$ and thus $(v,m_{1})\in C_{0}$. ∎

Given a generalized parity game and its extended game $G\times M_{1}\times\ldots\times M_{k}$, we now explain what are the needed adaptations for computing ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}})$. The approach is similar and works dimension by dimension as we did before for parity games. First we define a partial order on $V\times M_{1}\times\ldots\times M_{k}$ such that the partial order of Definition 4 is used on each dimension. More precisely, we define the strict partial order $\prec$ on $V\times M_{1}\times\ldots\times M_{k}$ such that $(v^{\prime},m^{\prime}_{1},\ldots,m^{\prime}_{k})\prec(v,m_{1},\ldots,m_{k})$ if and only if $v=v^{\prime}$ and for all $\ell$:

either $m_{\ell},m^{\prime}_{\ell}$ are even and $m^{\prime}_{\ell}>m_{\ell}$, 2. 2.

or $m_{\ell},m^{\prime}_{\ell}$ are odd and $m^{\prime}_{\ell}<m_{\ell}$, 3. 3.

or $m_{\ell}$ is odd and $m^{\prime}_{\ell}$ is even.

For instance, if $[d_{1}]=[d_{2}]=[3]$, then for a fixed $v$ we have the lower semilattice of Figure 2.

Second, functions $up_{\ell}$ and $down_{\ell}$, with $\ell\in\{1,\dots,k\}$, are defined exactly as previous functions $up$ and $down$ (see Definition 6), for each dimension $\ell$ and with respect to priority function $\alpha_{\ell}$. Third, we adapt (as expected) Proposition 7 for the computation of ${\mathsf{Cpre}}_{0}({G\times M_{1}\times\ldots\times M_{k}},{U})$ for a closed set $U\subseteq V\times M_{1}\times\ldots\times M_{k}$. Finally, we obtain an antichain-based algorithm for ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}})$ as Lemma 8 remains true: each set $T_{j}$ is a closed set represented by the antichain $\lceil T_{j}\rceil=\{(v,0,\ldots,0)\mid v\in F_{j}\}$.

6 Algorithms LaySolver and GenLaySolver

In [12], the authors study another polynomial time partial solver for parity games, called psolQ, that has some similarities with the GoodEpSolver approach described in Section 5. It is a more complex partial solver that we present in this section. We then explain how to modify it to get a partial solver for generalized parity games. This partial solver (i) works on the initial game structure $G$ and not on the extended game structure $G\times M$, (ii) focuses on a subset $P$ of $i$-priorities and not on all $i$-priorities, and (iii) computes a set similar to ${\mathsf{GoodEp}}_{i}({G},{\alpha})$ such that the positive attractor of Equation (5) is replaced by a layered structure of attractors (one layer per priority $p\in P$).

Safe attractors.

As we do no longer work with the extended game $G\times M$, we have to adapt the notion positive attractor in a way to visit some $i$-priority while avoiding visiting any greatest $(1-i)$-priority. Let $G$ be a game structure and $U,U^{\prime}\subseteq V$ be two subsets of $V$. The positive safe attractor ${\mathsf{PSafeAttr}}_{i}({G},{U},{U^{\prime}})$ is the set of vertices from which player $i$ can ensure to visit $U$ in any positive number of steps while visiting no vertex of $U^{\prime}$. This can be computed with Equations (2-3) with the restriction that vertices in $U^{\prime}$ are not allowed.

Partial solver for parity games.

Let $(G,\mathsf{EvenParity}(\alpha))$ be a parity game. Let $q$ be some given $i$-priority and $P_{\geq q}\subseteq[d]$ be the set composed of all $i$-priorities $p\geq q$. Thus $P_{\geq q}=\{q,q+2,q+4,\ldots,d({i})\}$ such that $d({i})$ is equal to $d$ (resp. $d-1$) if $d$ (resp. $d-1$) is an $i$-priority. Let $U\subseteq\{v\in V\mid\alpha(v)\in P_{\geq q}\}$ be a subset of vertices with an $i$-priority at least $q$. For each $p\in P_{\geq q}$, let $U_{p}=U\cap\{v\in V\mid\alpha(v)\geq p\}$ be the set of vertices of $U$ with priority at least $p$. Hence $U_{d({i})}\subseteq U_{d({i})-2}\subseteq\ldots\subseteq U_{q+2}\subseteq U_{q}=U$. For each $p\in P_{\geq q}$, we also consider U^{\prime}_{p}=\{v\in V\mid\alpha(v)\mbox{ is a (1-i)-priority and }\alpha(v)>p\}, that is, the set of all vertices with $(1-i)$-priority greater than $p$. We compute the following layered structure of positive safe attractors: Initially $B_{d({i})+2}=\emptyset$ and for all $p\in P_{\geq q}$, $B_{p}$ is computed from $B_{p+2}$ as follows:

[TABLE]

We call layered attractor the set $B_{q}$ and we denote it by ${\mathsf{LayAttr}}_{i}({G},{\alpha},{P_{\geq q}},{U})$. Notice that $B_{d({i})}\subseteq B_{d({i})-2}\subseteq\ldots\subseteq U_{q+2}\subseteq B_{q}={\mathsf{LayAttr}}_{i}({G},{\alpha},{P_{\geq q}},{U})$.

For example, consider $d=9$ and the [math]-priority $q=4$. Hence $P_{\geq q}$ is equal to $\{4,6,d({0})=8\}$. Given some set $U\subseteq\{v\in V\mid\alpha(v)\in P_{\geq q}\}$, $U_{8}$ (resp. $U_{6}$, $U_{4}$) is the set of vertices of $U$ with priority $8$ (resp. priorities in $\{6,8\}$, in $\{4,6,8\}$), and $U^{\prime}_{8}$ (resp. $U^{\prime}_{6}$, $U^{\prime}_{4}$) is the set of vertices with priority $9$ (resp. priorities in $\{7,9\}$, in $\{5,7,9\}$). On Figure 3 is depicted the related layered attractor with three layers.

Let us give some intuition about this layered structure of attractors. From a vertex in $B_{q}\setminus B_{q+2}$ (lowest layer $q$), player $i$ can ensure to visit $U_{q}\cup B_{q+2}$ without visiting $U^{\prime}_{q}\setminus B_{q+2}$. In case of a visit to $U_{q}$, this is a good episode for himself (in the sense of Section 5) since the maximum visited priority along the current history consistent with his strategy is an $i$-priority ($\geq q$). In case of a visit to some $v\in B_{q+2}$, suppose that $v\in B_{p}\setminus B_{p+2}$ (layer $p$ with $p\geq q+2$). Then player $i$ can now ensure to visit $U_{p}\cup B_{p+2}$ without visiting $U^{\prime}_{p}\setminus B_{p+2}$. In case of a visit to $U_{p}$, this is again a good episode for player $i$, otherwise it is a visit to some vertex in a higher layer. If necessary this can be repeated until reaching the highest layer $d({i})$ where player $i$ can ensure to visit $U_{d({i})}$ without visiting $U^{\prime}_{d({i})}$ (since $B_{d({i})+2}$ is empty). Thus from all vertices of $B_{q}$, player $i$ can ensure a good episode for himself.

The new partial solver is the same as the GoodEpSolver solver of Section 5 except that in Equations (4-6), (i) the layered attractor ${\mathsf{LayAttr}}_{i}({G},{\alpha},{P_{\geq q}},{U})$ in the game $G$ replaces the attractor ${\mathsf{PAttr}}_{i}({G\times M},{T})$ in the extended game $G\times M$ of Equation (5), and (ii) the set $P_{\geq q}=\{q,q+2,q+4,\ldots,d({i})\}$ replaces the set of all $i$-priorities. More precisely, we compute the sequence $(F_{j})_{j\geq 0}$ such that $F_{0}=\{v\in V\mid\alpha(v)\in P_{\geq q}\}$ and for $j\geq 1$, $F_{j}$ is computed from $F_{j-1}$ as follows:

[TABLE]

We denote by ${\mathsf{LayEp}}_{i}({G},{\alpha},{P_{\geq q}})$ the fixpoint $\bigcap_{j\geq 0}F_{j}$. As in ${\mathsf{GoodEp}}_{i}({G},{\alpha})$, from any vertex $v_{0}$ in this fixpoint, player $i$ can ensure a succession of good episodes implying that he is winning from $v_{0}$ for ${i}\mathsf{Parity}(\alpha)$.

Proposition 1 ([12])

Let $(G,\mathsf{EvenParity}(\alpha))$ be a parity game and $P_{\geq q}\subseteq[d]$ be the set of all $i$-priorities $p\geq q$ for some given $i$-priority $q$. Let $F^{(i)}={\mathsf{LayEp}}_{i}({G},{\alpha},{P_{\geq q}})$. Then for all $v_{0}\in V$, if $v_{0}\in{\mathsf{Attr}}_{i}({G},{F^{(i)}})$, then $v_{0}\in{\mathsf{Win}}({G},{i},{{i}\mathsf{Parity}(\alpha)})$. ∎

We derive from this proposition a polynomial time algorithm similar to Algorithm 4 where ${\mathsf{LayEp}}_{i}({G},{\alpha},{P_{\geq q}})$ is used instead of ${\mathsf{GoodEp}}_{i}({G},{\alpha})$ and $\cal P$ is an input list composed of all possible sets $P_{\geq q}$, with $q\in[d]$. This algorithm considers different sets $P_{\geq q}$ until finding one composed of $i$-priorities and such that ${\mathsf{LayEp}}_{i}({G},{\alpha},{P_{\geq q}})$ is non empty and then makes a recursive call.

Partial solver for generalized parity games.

We want to adapt the LaySolver approach to generalized parity games. As for the GenBüchiSolver and GenGoodEpSolver approaches, we have to treat separately player [math] and player $1$.

For player $1$, recall that his objective is a disjunction of $\mathsf{OddParity}(\alpha_{\ell})$ over $\ell\in\{1,\ldots,k\}$. Therefore we can apply the LaySolver approach to each $\alpha_{\ell}$ as explained before for parity games, thus computing ${\mathsf{LayEp}}_{1}({G},{\alpha_{\ell}},{P_{\geq q}})$ for $P_{\geq q}$ depending on some $1$-priority $q\in[d_{\ell}]$.

For player [math], recall that his objective is a conjunction of $\mathsf{EvenParity}(\alpha_{\ell})$ over $\ell\in\{1,\ldots,k\}$. We are going to extend the LaySolver approach in this context, for player [math]. We fix a vector of [math]-priorities $q=(q_{{1}},\ldots,q_{{k}})$. Let $d({0})=(d_{{1}}(0),\ldots,d_{{k}}(0))$ be the vector of maximum [math]-priorities $d_{{\ell}}(0)\in[d_{\ell}]$ for all $\ell$. We denote by $P_{\geq q}$ the set $\{d({0}),d({0})-2,d({0})-4,\ldots,q\}$ such that if $p=(p_{1},\ldots,p_{k})$, then $p-2=(\max\{p_{1}-2,q_{1}\},\ldots,\max\{p_{k}-2,q_{k}\})$. Let us illustrate with an example. Consider a generalized parity game $d_{\ell}=9$ for all $\ell$ and $q=(4,\ldots,4)$. Then we get $P_{\geq q}=\{(8,\ldots,8),(6,\ldots,6),(4,\ldots,4)\}$.

Take a vector $p\in P_{\geq q}$ and a subset $U\subseteq V$ of vertices.555In this section, $p,q,d({0})$ are all vectors of priorities (and not a priority). In a first step, let us focus on how player [math] can ensure to visit $U$ such that along the history, for all $\ell$, a [math]-priority $\geq p_{\ell}$ is visited and no $1$-priority $>p_{\ell}$ is visited (in a way to extend Equation (9) temporarily without set $B_{p+2}$). Such a generalized reachability can be reduced to reachability by working with the game $G$ extended with memory ${\cal N}_{p}$ such that $N\in{\cal N}_{p}$ records the dimensions $\ell$ for which a vertex with [math]-priority $\geq p_{\ell}$ is already visited. More precisely, we consider the extended game structure $G_{p}=G\times{\cal N}_{p}$ with ${\cal N}_{p}=\{N\mid N\subseteq\{1,\ldots,k\}\}$. For each $v\in V$, we denote by N_{p}(v)=\{\ell\mid\alpha_{\ell}(v)\mbox{ is a 0-priority such that }\alpha_{\ell}(v)\geq p_{\ell}\}. The game structure $G_{p}$ has the set $V\times{\cal N}_{p}$ of vertices and the set $E_{p}$ of edges $((v,N),(v^{\prime},N^{\prime}))$ such that $(v,v^{\prime})\in E$ and $N^{\prime}=N\cup N_{p}(v^{\prime})$.666Notice that even if ${\cal N}_{p}$ does not depend on $p$, the edges of $G_{p}$ depend on $p$. Moreover, $V_{i}\times{\cal N}_{p}$ is the set of vertices controlled by player $i$, for $i\in\{0,1\}$. Finally to any initial vertex $v_{0}$ in $G$ corresponds the initial vertex $(v_{0},N_{p}(v_{0}))$ in the extended game $G_{p}$.

Define $T_{p}=\{(v,N)\mid v\in U,N=\{1,\ldots,k\}\}$ and $T^{\prime}_{p}=\{(v,N)\in V\times{\cal N}_{p}\mid\exists\ell,\,\alpha_{\ell}(v)$ is a $1$-priority $>p_{\ell}\}$777Notice that $T_{p}$ depends on $U$ while $T_{p}$ does not.. Clearly, in game $G$, player [math] can ensure to visit $U$ such that for all $\ell$, a [math]-priority $\geq p_{\ell}$ is visited and no $1$-priority $>p_{\ell}$ is visited from $v_{0}$ if and only if in the extended game $G_{p}$, he can ensure to visit $T_{p}$ while not visiting $T^{\prime}_{p}$ from $(v_{0},N_{p}(v_{0}))$. The latter condition is equivalent to $(v_{0},N_{p}(v_{0})\in{\mathsf{PSafeAttr}}_{0}({G_{p}},{T_{p}},{T^{\prime}_{p}})$. In this case player [math] can derive from $G_{p}$ to $G$, a winning strategy from $v_{0}$ (that has a finite memory equal to ${\cal N}_{p}$).

In a second step, let us explain how to generalize the concept of layered attractor, and in particular how to manage the set $B_{p+2}$ in Equation (9). For parity games we explained how player [math] has to adapt his attractor strategy when he shifts from layer $p$ to some higher layer $p^{\prime}>p$ due to the visit to some $v\in B_{p+2}$. Here when player [math] visits some vertex $(v,N)$ in layer $p$ for which he has to shift to layer $p^{\prime}$, he stops applying his winning strategy for layer $p$, and begins applying his winning strategy for layer $p^{\prime}$ from the initial vertex $(v,N_{p^{\prime}}(v))$ belonging to layer $p^{\prime}$. Hence Player [math] thus resets his memory from $(v,N)$ to $(v,N_{p^{\prime}}(v))$.

We are now ready to adapt Equation (9) to compute a layered attractor in the context of generalized parity games. Recall that $P_{\geq q}=\{d({0}),d({0})-2,\ldots,q\}$ for some given vector $q=(q_{{1}},\ldots,q_{{k}})$ of [math]-priorities and that $U$ is a subset of $V$. We compute the following layered structure of positive safe attractors: initially $C_{d({0})+2}=\emptyset$ and for all $p\in P_{\geq q}$, $C_{p}$ is computed from $C_{p+2}$ as follows:

[TABLE]

The layered attractor is here the set $\{v\in V\mid(v,N_{p}(v))\in B_{q}\}$; we denote it by ${\mathsf{LayAttr}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}},{P_{\geq q}},{U})$.

In a last step, it remains to explain how to use this adapted notion of layered attractor to obtain a partial solver for generalized parity games. We simply take the same equations (10-11) except that ${\mathsf{LayAttr}}_{0}({G},{\alpha},{P_{\geq q}},{F_{j}})$ must be replaced by ${\mathsf{LayAttr}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}},{P_{\geq q}},{F_{j}})$. We denote by ${\mathsf{LayEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}},{P_{\geq q}})$ the fixpoint $\bigcap_{j\geq 0}F_{j}$. From all the given arguments in the previous three steps follows the next proposition.

Proposition 2 ([12])

Let $(G,\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k}))$ be a generalized parity game. For some given vector $q=(q_{{1}},\ldots,q_{{k}})$ of [math]-priorities, let $P_{\geq q}=\{d({0}),d({0})-2,\ldots,q\}$ and let $F^{(0)}={\mathsf{LayEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}},{P_{\geq q}})$. Then for all $v_{0}\in V$, if $v_{0}\in{\mathsf{Attr}}_{0}({G},{F^{(0)}})$, then $v_{0}\in{\mathsf{Win}}({G},{0},{\mathsf{ConjEvenParity}(\alpha_{1},\ldots,\alpha_{k})})$. ∎

We derive from this proposition an algorithm (see Algorithm 7) similar to Algorithm 5 such that for each dimension $\ell$, ${\mathsf{GoodEp}}_{1}({G},{\alpha_{\ell}})$ is replaced by ${\mathsf{LayEp}}_{1}({G},{\alpha_{\ell}},{P_{\geq q}})$ with $P_{\geq q}$ depending on some $1$-priority $q\in[d_{\ell}]$ (player $1$) and ${\mathsf{GoodEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}})$ is replaced by ${\mathsf{LayEp}}_{0}({G},{\alpha_{1},\ldots,\alpha_{k}},{P_{\geq q}})$ with $P_{\geq q}$ depending on some vector $q$ of [math]-priorities (player [math]). However, as for Algorithm 6, this algorithm needs an input list $\cal P$ composed of:

• •

elements $(P_{\geq q},\ell)$ with $P_{\geq q}\subseteq[d_{\ell}]$ such that $q$ is a $1$-priority in $\{d({1}),d({1})-2,\ldots,1\}$,

• •

elements $P_{\geq q}\subseteq[d_{1}]\times\ldots\times[d_{k}]$ such that $q$ is a vector of [math]-priorities in $\{d({0}),d({0})-2,\ldots,0\}$.

By Theorem 2.2, this algorithm is in $O((\max_{\ell=1}^{k}\frac{d_{\ell}}{2})^{2}\cdot|V|^{2}\cdot|E|\cdot 2^{k})$ time complexity.

7 Empirical Evaluation

For parity games, the polynomial time partial solvers BüchiSolver888The variant with safety objectives., GoodEpSolver, and LaySolver are theoretically compared in [12, 13]. It is proved that the partial solutions computed by Algorithm BüchiSolver are included in the partial solutions computed by Algorithm LaySolver themselves included in the partial solutions computed by Algorithm GoodEpSolver. Examples of parity games are also given that distinguish the three partial solvers (strict inclusion of partial solutions), as well as an example that is not completely solved by the most powerful partial solver GoodEpSolver. This behavior also holds for the three partial solvers proposed here for generalized parity games. Furthermore, their time complexity is exponential in the number $k$ of priority functions whereas the classical algorithm for generalized parity games is exponential in both $k$ and all $d_{\ell}$ [6].

For both parity games and generalized parity games, we implemented the three partial solvers (with the antichain approach for Algorithm GenGoodEpSolver), Algorithm Zielonka (resp. GenZielonka) and its combination Ziel&PSolver (resp. GenZiel&PSolver) with each partial solver, and we executed all these algorithms on a large set of benchmarks.

Setting.

Our benchmarks were generated from TLSF specifications used for the Reactive Synthesis Competition (SYNTCOMP [14]) using a compositional translation as explained in the introduction.999The tool we implemented to realize this translation can be fetched from https://github.com/gaperez64/tlsf2gpg The source code for our prototype tool along with all the information about our benchmarks is publicly available at https://github.com/Skar0/generalizedparity. Our experiments have been carried out on a server with Mac OS X 10.13.4 (build 17E199). As hardware, the server had as CPU one 6-Core Intel Xeon; as processor speed, 3.33 GHz; as L2 Cache (per Core), 256 KB; as L3 Cache, 12 MB; as memory, 32 GB; and as processor interconnect speed, 6.4 GT/s. We implemented our algorithms in Python 2.7.

Experiments on parity games.

We considered 240 benchmarks for parity games. Those games have a mean size $|V|$ around 46K with a maximal size of 3157K, and a mean number $d$ of priorities of $4.1$ with a maximal number $d=15$. The statistics about the behaviors of the different algorithms are summarized in Table 1 (for all the 240 benchmarks) and Table 2 (for the 20 most difficult benchmarks for Algorithm Zielonka). Column $1$ indicates the name of the solver, Column $2$ counts the number of benchmarks completely solved (for the partial solvers, the second number is the number of incomplete solutions), Column $3$ counts the number of timeouts (fixed at 60000 ms), and Column $4$ counts how many times the solver was the fastest (excluding examples with timeout). In Table 1 (resp. 2), for the 233 (resp. 13) benchmarks without timeout for all the complete Algorithms Zielonka and Ziel&PSolver, Column $5$ indicates the mean execution time in milliseconds.

Experiments for generalized parity games.

We considered 152 benchmarks for generalized parity games. Those games have a mean size $|V|$ around 207K with a maximal size of 7009K. The mean number of priority functions is equal to $4.53$ with a maximum number of $17$. The statistics about the behaviors of the different algorithms are summarized in Table 3. The columns have the same meaning as before and the last column concerns the 87 benchmarks without timeout for all Algorithms GenZielonka and GenZiel&PSolver.

Observations.

Our experiments show that for parity games, Algorithm Zielonka is faster than partial solvers on average which was not observed on random graphs in [13]. For generalized parity games, they show that $4$ benchmarks that cannot be solved by Algorithm GenZielonka or by a partial solver alone, can be solved by the combination of GenZielonka with a partial solver. Our experiments also show that their combination with a partial solver improves the performances of Algorithms Zielonka and GenZielonka on a large portion of the benchmarks: 90 cases over 240 (38%) for parity games and 99 cases over 132 (75%) for generalized parity cases. They suggest that it is interesting to launch in parallel Algorithms GenZiel&GenBüchiSolver, GenZiel&GenGoodEpSolver, and GenZiel&GenLaySolver, as none appears to dominate the other ones. Nevertheless, the combination of GenZielonka with GenBüchiSolver is a good compromise.

8 Conclusion

In this paper, we have shown how to extend the three partial solvers for parity games proposed in [12, 13] to the case of generalized parity games (conjunction of parity conditions). For one of those partial solver, we also have provided an antichain-based variant to retain efficiency. In addition, we have shown how to combine those partial solvers with the classical recursive algorithms due to Zielonka [19] for parity games and its extension [6] for generalized parity games. For both parity games and generalized parity games, we have implemented the classical recursive algorithm, the three partial solvers and their combinations with the classical algorithm. All these algorithms have been tested on a large set of instances of parity games and generalized parity games, that were generated from meaningful LTL specifications proposed in the last LTL reactive synthesis competition [14]. For parity games, our experiments show that Zielonka’s algorithm is faster than partial solvers on average. This was not observed on random graphs in [13] where Algorithm BüchiSolver was faster. Equally interestingly, it appears that for generalized parity games, the combination of Algorithm GenZielonka with a partial solver allows to solve instances that cannot be solved by the classical recursive algorithm or a partial solver alone. Finally for both the parity games and the generalized parity games, our experiments indicate that the performances of the classical recursive algorithms are often improved when combined with partial solvers.