Oink: An Implementation and Evaluation of Modern Parity Game Solvers

Parity games are turn-based games played on a finite graph. Two players Odd and Even play an infinite game by moving a token along the edges of the graph. Each vertex is labeled with a natural number priority and the winner of the game is determined by the parity of the highest priority that is encountered infinitely often. Player Odd wins if this parity is odd; otherwise, player Even wins.

Parity games are interesting both for their practical applications and for complexity theoretic reasons. Their study has been motivated by their relation to many problems in formal verification and synthesis that can be reduced to the problem of solving parity games, as parity games capture the expressive power of nested least and greatest fixpoint operators [17]. In particular, deciding the winner of a parity game is polynomial-time equivalent to checking non-emptiness of non-deterministic parity tree automata [33], and to the explicit model-checking problem of the modal \(\mu \)-calculus [14, 15, 23, 32].

Parity games are interesting in complexity theory, as the problem of determining the winner of a parity game is known to lie in \(\text {UP}\cap \text {co-UP}\) [26], as well as in \(\text {NP}\,\cap \,\text {co-NP}\) [15]. This problem is therefore unlikely to be NP-complete and it is widely believed that a polynomial solution may exist. Despite much effort, no such algorithm has yet been found.

In past publications new and improved algorithms are often tested against the implementation of Zielonka’s algorithm in the PGSolver tool [19]. However, various recent publications [1, 34, 40] suggest that much better performance can be obtained. We combine a number of improvements from the literature [34, 40, 41] and propose additional optimizations. We show that our implementation of Zielonka’s algorithm outperforms PGSolver by several orders of magnitude.

We describe Oink in Sect. 3 and provide accessible descriptions of the implemented state-of-the-art algorithms in Sects. 4–7. We implement the strategy improvement algorithm (Sect. 4), both the small progress measures and the recently proposed quasi-polynomial progress measures algorithms (Sect. 5), the well-known Zielonka algorithm (Sect. 6) as well as a number of related algorithms from the priority promotion family (Sect. 7). We also propose an alternative multi-core implementation of strategy improvement.

Parity games are two-player turn-based infinite-duration games over a finite directed graph \(G=(V,E)\), where every vertex belongs to exactly one of two players called player Even and player Odd, and where every vertex is assigned a natural number called the priority. Starting from some initial vertex, a play of both players is an infinite path in G where the owner of each vertex determines the next move. The winner of such an infinite play is determined by the parity of the highest priority that occurs infinitely often along the play.

More formally, a parity game is a tuple where is a set of vertices partitioned into the sets controlled by player Even and controlled by player Odd, and \(E\subseteq V\times V\) is a total relation describing all possible moves, i.e., every vertex has at least one successor. We also write E(u) for all successors of u and \(u\rightarrow v\) for \(v\in E(u)\). The function assigns to each vertex a priority, where d is the highest priority in the game.

We write \(\textsf {pr}(v)\) for the priority of a vertex v and \(\textsf {pr}(V)\) for the highest priority of a set of vertices V and for the highest priority in the game . Furthermore, we write \(\textsf {pr}^{-1}(i)\) for all vertices with the priority i. A path \(\pi =v_0 v_1 \dots \) is a sequence of vertices consistent with E, i.e., \(v_i \rightarrow v_{i+1}\) for all successive vertices. A play is an infinite path. We write \(\textsf {pr}(\pi )\) for the highest priority in \(\pi \) is \(\pi \) is finite, or the highest priority that occurs infinitely often if \(\pi \) is infinite. Player Even wins a play \(\pi \) if \(\textsf {pr}(\pi )\) is even; player Odd wins if \(\textsf {pr}(\pi )\) is odd.

A strategy \(\sigma :V\rightarrow V\) is a partial function that assigns to each vertex in its domain a single successor in E, i.e., \(\sigma \subseteq E\). We typically refer to a strategy of player \(\alpha \) to restrict \(\sigma \) to all vertices controlled by player \(\alpha \). A player wins a vertex if they have a strategy such that all plays consistent with this strategy are winning for the player. A fundamental result for parity games is that they are memoryless determined [13], i.e., each vertex is winning for exactly one player, and both players have a strategy for each of their winning vertices.

Algorithms for solving parity games frequently employ (variations of) attractor computation. Given a set of vertices A, the attractor of A for a player \(\alpha \) represents those vertices that \(\alpha \) can force the play toward. We write to attract vertices in to A as player \(\alpha \), i.e.,Informally, we compute the \(\alpha \)-attractor of A by iteratively adding vertices to A of \(\alpha \) that have a successor in A and of \({\overline{\alpha }}\) that have no successors outside A.

We study modern parity game algorithms using our research tool named Oink. Oink is written in C++ and is publicly available under a permissive license via https://​www.​github.​com/​trolando/​oink. Oink is easy to extend, as new solvers subclass the Solver class and only require a few extra lines in solvers.cpp.

Apart from implementing the full solvers described below, Oink also implements several preprocessors similar to other parity game solvers. We base our choices mainly on the practical considerations and observations by Friedmann and Lange [19] and by Verver [41]. We always reorder the vertices by priority and renumber the priorities from 0 to eliminate gaps (not the same as compression). The former is beneficial for the attractor-based algorithms in Sects. 6 and 7. The latter may reduce the amount of memory required for the measures-based algorithms in Sects. 4 and 5.

The following preprocessors are optional. Oink can perform priority inflation and priority compression, as described in [19]. We implement self-loop solving and winner-controlled winning cycle detection, as proposed in [41]. Winner-controlled winning cycle detection is a prerequisite for the strategy improvement algorithm of Sect. 4 but is optional for the other algorithms. We trivially solve games with only a single parity. Finally, we also implement SCC decomposition, which repeatedly solves a bottom SCC of the game until the full game is solved.

The correctness of an algorithm does not imply that implementations are correct. Although a formal proof of the implementations would be preferred, we also implement a fast solution verifier and verify all obtained solutions.

Strategy improvement is a technique where each player iteratively improves their strategies until they are optimal. Strategy improvement algorithms were first explored for parity games by Jurdziński and Vöge [42] and have been subsequently improved in [7, 16, 20, 35, 38]. Recently, parallel implementations have been studied for the GPU [17, 24, 36]. Fearnley [17] also implements their parallel algorithm for multi-core CPUs. Our treatment in this section is mostly based on [17, 35].

In the strategy improvement algorithm, player Even has a strategy \(\sigma \) and player Odd has a strategy \(\tau \) for all their vertices. They improve their strategies until a fixed point is reached, at which point the game is solved. Instead of choosing a successor, player Even may also end the play. In the specific algorithm here, player Even delays selecting a strategy for a vertex until there is a favorable continuation. As \(\sigma \) and \(\tau \) cover all vertices, they induce a fixed path from each vertex. This path is either infinite (a play) or ends at a vertex of player Even. The strategy is evaluated by computing a valuation for each vertex based on the current paths. Strategies are improved by choosing the most favorable successor.

The valuation used in e.g. [17, 35] assigns to (infinite) plays the value \(\top \) and to (finite) paths a function L(p) that records for each priority p how often it occurs in the path. To determine the best move for each player, a total order \(\sqsubset \) compares valuations as follows. For non-\(\top \) valuations \(L_1\) and \(L_2\), \(L_1 \sqsubset L_2\) iff there exists a highest priority z that is different in \(L_1\) and \(L_2\), i.e., \(z = \max \,\{\, z \mid L_1(z) \ne L_2(z) \,\}\), and either \(L_1(z)<L_2(z)\) if z is even, or \(L_1(z)>L_2(z)\) if z is odd. Furthermore, \(L\sqsubset \top \) for any \(L\ne \top \). If \(L_1 \sqsubset L_2\), then \(L_2\) is more favorable for player Even and \(L_1\) is more favorable for player Odd.

Intuitively, player Even likes plays where higher even priorities occur more often. Furthermore, player Even will end the play unless the highest priority in the continuation is even. Thus infinite paths are won by player Even and the valuation \(\top \) represents this. Player Even will always play to \(\top \) and player Odd will always try to avoid \(\top \). This assumes that no winner-controlled winning cycles exist where player Odd wins, which can be guaranteed using a preprocessing step that removes these cycles.

For every strategy \(\sigma \) of player Even, a so-called best response \(\tau \) of player Odd minimizes the valuation of each position. Player Even always plays against this best response. In each iteration, after player Odd computes their best response, player Even computes all switchable edges based on the current valuation L and the current strategy \(\sigma \). An edge (u, v) is switchable if \(L_v \sqsupset L_{\sigma (u)}\). Not all switchable edges need to be selected for the improved strategy, but as argued in [17], the greedy all-switches rule that simply selects the best edge (maximal in \(\sqsubset \)) for every position performs well in practice.

There are different methods to compute the best response of player Odd. We refer again to [17] for a more in-depth discussion. Player Odd can compute their best response by repeatedly switching all Odd-switchable edges, i.e., edges (u, v) s.t. \(L_v \sqsubset L_{\tau (u)}\) and \(L_v\) is minimal in \(\sqsubset \) of all successors of u.

The players thus improve their strategies as in Algorithm 1, where \(\text {All}_\text {Odd}\) and \(\text {All}_\text {Even}\) compute all switchable edges as described above. The initial strategy for player Even is to always end the play. Player Odd computes their best response, starting from a random \(\tau \) initially. Player Even then improves their strategy once. They improve their strategies until a fixed point is reached. Then all vertices with valuation \(\top \) are won by player Even with strategy \(\sigma \) and all other vertices are won by player Odd with strategy \(\tau \) [17]. We extend the algorithm given in [17] at line 8 by marking vertices with valuation \(\top \) after player Odd computes their best response as “won”. We no longer need to consider them for \(\text {All}_\text {Odd}\) and \(\text {All}_\text {Even}\) as player Odd was unable to break the infinite play and thus they are won by Even.

The valuations can be computed in different ways. Fearnley implements a parallel algorithm that uses list ranking in two steps. The first step computes an Euler tour of the game restricted to chosen strategies \(\sigma \) and \(\tau \) resulting in a list. The second step uses a three-step parallel reduction algorithm to sum all values of the list. The list is divided into sublists which are each summed independently in the first sweep, all subresults are then propagated in the second sweep and then the final values are computed in the third sweep. See further [17].

We propose an alternative parallel algorithm to compute the valuation. We start from each Even vertex where the path ends and perform updates along a recursive backwards search, processing predecessors in parallel using task parallelism. Any vertex that is not visited has valuation \(\top \). See Algorithm 2. This algorithm is implemented in Oink using the high-performance work-stealing framework Lace [12]. When updating the valuations in L, we first sweep twice over all vertices to initialize L for each vertex to \(\top \) and to add all vertices to \(\texttt {into}(v)\) that have their strategy to v. We also implement computing switchable edges in parallel via a straight-forward binary reduction using Lace.

Empirical Evaluation. We compare the performance of Oink with the sequential and parallel solvers (1 or 8 threads) by Fearnley [17] and the “optstratimprov” solver in PGSolver. We disable optional preprocessing in all solvers. We only consider games without winner-controlled winning cycles, which are 289 model checking, 182 equivalence checking and 279 random games, in total 750 games.

See Table 1. We observe that PGSolver is vastly outperformed by Oink and the sequential solver of Fearnley. PGSolver timed out for 160 games, whereas psi and parsi-seq only timed out for 1 and 5 models, respectively. We observe similar parallel speedup for the parallel solvers, although Fearnley’s solver has more overhead from sequential to parallel with 1 thread. This might be due to the extra work to produce the Euler tour and to perform list ranking. The speedup we obtain with Oink is not very impressive, but the vast majority of the games are solved within 1 s already. Furthermore, psi and parsi-seq are fairly close in performance. This is not a surprise, as their implementations are similar; the main difference is that Fearnley uses a forward search and we use a backward search. Hence, Oink is faster, but not by a large margin. Finally, we remark that Fearnley reports excellent results for list ranking on GPUs, whereas our algorithm is designed for a multi-core architecture.

Progress measures is a technique that assigns to each vertex a monotonically increasing measure. The measure of each vertex is lifted based on the measures of its successors. By lifting vertices, players Even and Odd essentially play the game backwards. The measure represents a statistic of the most optimal play so far from the vertex, without storing the plays explicitly.

While progress measures have been used elsewhere, they were introduced for parity games by Jurdziński [27]. Several improvements to the original algorithm are due to Verver [41] and Gazda and Willemse [22]. A number of parallel implementations have been proposed for the Playstation 3 [6], for multi-core architectures [25, 37] and for GPUs [8, 24]. Furthermore, Chatterjee et al. proposed an implementation using BDDs [10]. Different types of progress measures were introduced after the recent breakthrough of a quasi-polynomial time algorithm due to Calude et al. [9], which resulted in the progress measures algorithms by Jurdziński et al. [28] and by Fearnley et al. [18]. This section studies small progress measures [27] and quasi-polynomial progress measures [18].

The algorithm by Zielonka [43] is a recursive solver that despite its relatively bad theoretical complexity is known to outperform other algorithms in practice [19]. Furthermore, tight bounds are known for various classes of games [21].

Zielonka’s recursive algorithm is based on attractor computation. At each step, given current subgame , the algorithm removes the attractor , i.e., all vertices attracted to the current highest vertices of priority for player \(\alpha =p \bmod 2\), and recursively computes the winning regions of the remaining subgame . If the opponent \({\overline{\alpha }}\) can attract vertices in A to \(W_{\overline{\alpha }}\), then \({\overline{\alpha }}\) wins and the solution for the remainder is computed recursively. Otherwise, \(\alpha \) wins A and no further recursion is necessary. The strategies for both players are trivially obtained during attractor computation and by assigning to winning p-vertices in A any strategy to vertices in \(W_\alpha \cup A\).

Zielonka’s original algorithm has been extended and improved over the years. In his thesis, Verver [41] improves the partitioning of the game after computing A by extending A with the attractors of the next highest vertices if they are of the same parity. The original algorithm always recomputes the solution of if \(W_{\overline{\alpha }}\) is nonempty, even if no vertices are attracted to \(W_{\overline{\alpha }}\). Liu et al. propose that this is not necessary [34]. See Algorithm 3 for the recursive algorithm with these modifications. Other extensions that we do not consider here are the subexponential algorithm [29] and the big steps algorithm [39] that have been reported to perform slower than ordinary Zielonka [19]. Also, variations using BDDs have been proposed [2, 30].

Although the implementation of the recursive algorithm in PGsolver [19] is typically used for comparisons in the literature, improved implementations have been proposed by Verver [41], Di Stasio et al. [40], Liu et al. [34], and Arcucci et al. [1]. Verver suggests to record the number of remaining “escaping” edges for each vertex during attractor computation, to reduce the complexity of attractor computation at the cost of an extra integer per vertex. Di Stasio et al. avoid creating copies of the game for recursive operations by recording which vertices are removed in a special array. Recently, Arcucci et al. extended the implementation in [40] with a multi-core implementation of attractor computation [1].

The implementation in Oink is based upon the ideas described above. Furthermore, we improve the implementation using the following techniques.

In the interest of space, we cannot describe the multi-core attractor in-depth. This implementation is fairly straightforward. We implement the attractor recursively where the work-stealing framework runs the recursive operations in parallel. Like typical lock-free algorithms, we rely on the compare-and-swap operation to implement safe communication between threads. The attractor uses this operation when manipulating the number of escaping edges and to “claim” a vertex by setting its value in the region array from \(\bot \) to r.

Empirical Evaluation. We compare our implementation of Zielonka’s recursive algorithm with and without the optimizations of Algorithm 3 to PGSolver, to Verver’s implementation pbespgsolve [11, 41] and to SPGSolver [1, 40]. Unfortunately, the Java version of SPGSolver (all three variations) suffers from severe performance degradation for unknown reasons. They also provide a C++ implementation in their online repository, which we used instead. The multi-core version of the SPGSolver tool relies on async tasks provided by C++11. Similar to the previous sections, we disable the optional preprocessors that solve single parity games, remove self-loops and solve winner-controlled winning cycles.

See Table 3. The results show that the implementation in Oink outperforms PGSolver by several orders of magnitude on all benchmark types. PGSolver timed out for 83 of all 949 games. The solvers spg-seq and pbeszlk are faster than Oink on the model checking and equivalence checking games, but are significantly outperformed on random games. We also observe severe performance degradation for spg-mc on random games. It appears that our parallel implementation of Zielonka’s algorithm also does not scale well. Finally, there seems to be no significant difference between the optimized and unoptimized versions of Zielonka’s algorithm, except for random games.

In recent work, a new family of algorithms has been proposed based on priority promotion [5]. Priority promotion starts with a similar decomposition of the game as Zielonka’s recursive algorithm. Priority promotion is based on the insight that a recursive decomposition based on attractor computation leads to regions with a specific property related to the highest priority in the region, called its measure p. This property is that all plays that stay in the region are won by the player who wins the highest priority p, denoted by player \(\alpha \). The other player \({\overline{\alpha }}\) has three options. They either lose the game by staying in the region, or they can leave the region by playing to an \(\alpha \)-region of higher measure, or they can leave the region to a lower region of either player via a vertex with priority p. The goal of \(\alpha \) is to find “closed” \(\alpha \)-regions, where \({\overline{\alpha }}\) cannot escape to lower regions. The result is a region where player \({\overline{\alpha }}\) either loses, or leaves the region to a higher \(\alpha \)-region which may or may not be closed. The measure of the closed \(\alpha \)-region is then “promoted” to the measure of the lowest higher region to which \({\overline{\alpha }}\) can escape and the attractor-based decomposition is recomputed for all lower regions. The promoted region may now attract from regions with a measure between its original measure and its promoted measure, thus requiring recomputing the decomposition. When player \({\overline{\alpha }}\) cannot escape from an \(\alpha \)-region to a higher \(\alpha \)-region, player \(\alpha \) is the winner of all vertices in the region.

Priority promotion was proposed in [5] and improved in [3, 4]. The original PP algorithm [5] forgets all progress (“resets”) in lower regions after promotion. The PP+ algorithm [3] only resets lower regions of player \({\overline{\alpha }}\). The RR algorithm [4] only resets some lower regions of player \({\overline{\alpha }}\). The DP algorithm [3] uses a heuristic to delay certain promotions to avoid resets. We implement all four algorithms and also combine the DP algorithm, which is based on PP+, with the RR algorithm.

See Table 4. Overall, we see that the simplest solver pp performs just as good as the more complex solvers. The motivation for the variations is based on crafted families that require an exponential number of promotions. The pp solver may be most vulnerable to these crafted families, but on practical games and random games there is no significant difference.

See Table 5 for a comparison of the five main sequential algorithms in Oink, including the preprocessing that removes winner-controlled winning cycles, self-loops and solves single parity games. The results show that the zlk and the pp solvers have similar performance and outperform the other solvers. See also Fig. 1 for a cactus plot of these five solvers.

Priority promotion is a powerful and attractive idea, as promoting closed \(\alpha \)-regions is similar to cap-and-carryover in small progress measures. Attractor computation finds such regions directly whereas value iteration algorithms may require many iterations. We confirm the observations in [5] that the algorithm has a good performance but it is not faster than Zielonka’s algorithm.

In this work, we studied modern parity game algorithms using a new tool named Oink. Oink is publicly available via https://​www.​github.​com/​trolando/​oink. We implemented a number of modern algorithms and provided a comprehensive description of these algorithms, introducing cap-and-carryover to understand small progress measures. We proposed improvements to strategy improvement and to Zielonka’s algorithm. We presented an empirical evaluation of Oink, comparing its performance with state-of-the-art solvers, especially the popular PGSolver tool. The results demonstrate that Oink is competitive with other implementations and in fact outperforms PGSolver for all algorithms, especially Zielonka’s recursive algorithm. This result is particularly interesting considering that many publications compare the performance of novel ideas to Zielonka’s algorithm in PGSolver.