1 Introduction

Parity games (PGs) [12, 24] are abstract games with a key role in automata theory and formal verification [7, 9, 18, 19, 23]. PGs are two-player turn-based games played on directed graphs whose nodes are labeled with priorities. Players take turns moving a token along the graph’s edges, starting from an initial node. A play induces an infinite path and Player  wins the play if the smallest priority visited infinitely often is even. Solving a PG amounts checking whether Player  can force such a winning play. Several algorithms to solve PGs have been proposed aiming to tighten the asymptotic complexity of the problem, as well as to work well in practice. Well known are Recursive () [24], small-progress measures () [14], and  [10, 18], the latter originated to deal with the emptiness of parity automata. Notably, all these algorithms are explicit, that is, they are formulated in terms of the underlying game graphs. Due to the exponential growth of finite-state systems, and, consequently, of the corresponding game graphs, the state-explosion problem limits the scalability of these algorithms in practice.

Symbolic algorithms are an efficient way to deal with extremely large graphs. They avoid explicit access to graphs by using a set of predefined operations that manipulate Binary Decision Diagrams (BDDs) [3] representing these graphs. This enables handling large graphs succinctly, and, in general, it makes symbolic algorithms scale better than explicit ones. For example, in hardware model checking symbolic algorithms enable going from millions of states to \(10^{20}\) states and more [4, 20]. In contrast, in the context of PG solvers, symbolic algorithms have been only marginally explored. In this direction we just mention a symbolic implementation of  [2, 16], which, however, has been done for different purposes and no benchmark comparison with the explicit version has been carried out. Other works close to this topic and worth mentioning are [5, 8], where a symbolic version of has been theoretically studied but not implemented.

In this work we provide the first broad investigation of the symbolic approach for solving PGs. We implement four symbolic algorithms and compare their performances to the corresponding explicit versions for different classes of PGs. Specifically, we implement in a new tool, called , the symbolic versions of , , and two variants of . The tool also allows to generate random games, as well as compare the performance of different symbolic algorithms.

The main result we obtain from our comparisons is that for random games, and even for constrained random games (see Sect. 4), explicit algorithms actually perform better than symbolic ones, most likely because BDDs do not offer any compression for random sets. The situation changes, however, for structured games, where symbolic algorithms sometimes outperform explicit algorithms. This is similar to what has been observed in the context of model checking [11]. We take this as an important development because it suggests a methodological weakness in this field of investigation, due to the excessive reliance on random benchmarks. We believe that, in evaluating algorithms for PG solving, it would be useful to have real benchmarks and not only random benchmarks, as the common practice has been. This would lead to a deeper understanding of the relative merits of PG solving algorithms, both explicit and symbolic.

2 Explicit and Symbolic Parity Games

Explicit Parity Games. A Parity Game (PG, for short) is a tuple , where and are two finite disjoint sets of nodes for Player  and Player , respectively, with , is the binary relation of moves, and is the priority function. By we denote the set of nodes to which the token can be moved, starting from q.

A play over is an infinite sequence of nodes that agree with , i.e., , for each . By we denote the priority sequence associated to , and by and , the sets of nodes and priorities that occur infinitely often in and , respectively. A play is winning for Player if is even. Player  (Player ) strategy is a function () that agrees with . Given a node , is the unique play starting in that agrees with both and . Player wins the game from if a strategy exists such that, for all strategies it holds that is winning for Player . Then is declared winning for Player . By we denote the set of winning nodes in for Player . Parity games enjoy determinacy, i.e., for every node q, either or  [12]. Also, if Player  has a winning strategy from a node q, then she has a memoryless one from q [24]. A strategy is memoryless if, for all prefixes of plays , it holds that iff last nodes of and coincide. Then, one can use defined as .

Symbolic Parity Games. We start with some notation. In the sequel we use symbols \(x_i\) for propositions (variables), \(l_i\) for literals, i.e., positive or negative variables, f for a generic Boolean formula, ||f|| for the set of interpretations that makes the formula f true, and \(\lambda (f) \subseteq V\) for the set of variables in f.

Definition 1

Given a PG , the corresponding symbolic PG (SPG, for short) is the tuple defined as follows:

  • \(\mathcal {X} = \{x_1,\ldots , x_n\}\), with , is the set of propositions used to encode nodes in , i.e., to each we associate a Boolean formula \(f_v = l_{v,1} \wedge ... \wedge l_{v,n}\) where \(l_{v,i}\) is either \(x_i\) or \(\overline{x_i}\). We also associate to v the interpretation \(\mathcal {X}_v \in 2^{\mathcal {X}}\), i.e., the subset of variables appearing positively in \(f_v\).

  • \(\mathcal {X}_M = \{x'_1, ..., x'_n\}\), with , is the set of propositions used to encode the successor nodes such that \(\mathcal {X} \cap \mathcal {X}_M = \emptyset \). We extend to \(\mathcal {X}_M\) the definitions of \(f_v\) and \(X_v\) as used in the previous item.

  • , for \(i \in \{0,1\} \), is a Boolean formula such that .

  • is a Boolean formula over the propositions \( \mathcal {X} \cup \mathcal {X}_M\) such that .

  • is the symbolic representation of the priority function ; formally, it is a function associating to each interpretation \(X_v\) a natural number.

Fig. 1.
figure 1

A parity game

Full size image

Example. Consider the PG depicted in Fig. 1. It has (circles) and (squares); is given by arrows; and , for \(1 \le i \le 3\). The correlating SPG is as follows: \(\mathcal {X}= \{x_1,x_2\}\) and \(\mathcal {X}_M= \{y_1,y_2\}\) are the set of propositions; and are Boolean formulas representing and , respectively; is the Boolean formula for ; finally, the function , given by , for \(1 \le i \le 3\). represents the priority function .

To solve an SPG we compute the Boolean formulas over \(\mathcal {X}\) that is satisfied by those interpretations that correspond to winning nodes for Player 0.

For technical reasons, we also need the definition of symbolic sub-games.

Definition 2

Let be a PG and . By we denote the PG restricted to nodes .

Let \(f_U\) be a Boolean formula such that \(||f_U||=U\) and be the corresponding SPG of the PG . By we denote the SPG of , where:

  • , for \(i\in \{0,1\}\), is the Boolean formula for nodes ;

  • , where \(||f_U' ||=U \) and \(\lambda (f_U') = \mathcal {X}_M\), is the Boolean formula representing moves restricted to ;

  • is the symbolic representation of that associates to the interpretations \(X_v\) satisfying the Boolean formula a natural number.

3 Solving Parity Games: Explicit vs Symbolic Algorithms

3.1 Explicit Algorithms

Small Progress Measures Algorithm () [13]. The core idea of is a ranking function that assigns to each node a vector of counters (namely a progress measure) collecting the number n of times Player 1 can force a play to visit an odd priority until a lower priority is seen. If this value is sufficiently large, then the node is declared winning for Player 1. computes the progress measure by updating the values of a node according to those associated to its successors, i.e., by computing a least fixed-point for all nodes with respect to the ranking function.

We fix some notation. Let be a PG with maximal priority c and \(d \in \mathbb {N}^c\) be a c-tuple of non-negative integers. By < we denote the usual lexicographic ordering over \(\mathbb {N}^c\). For each odd number i, by \(n_i\) we denote the number of nodes in with priority i. For i even, we set \(n_i=0\). The progress measure domain is defined as \(M_G^{\top }=M_G \cup \{\top \}\) with \(M_G =(M_0 \times \ldots \times M_{c-1})\) and \(M_i = [n_i]\). The element \(\top \) is the biggest value such that \(m < \top \) for all \(m \in M_G\). For \(d=(d_0,\ldots ,d_{c-1})\) and \(l<c\), we set \(\langle d \rangle _l=(d_0,\ldots ,d_l,0,\ldots ,0)\), i.e., all \(d_{i>l}\) in d are set to 0. By we denote the smallest tuple \(d' \in M_G^{\top }\) such that \(d<d'\). This notion easily extends to tuples in \(\mathbb {N}^l\) by defining with \(l>0\) to be the smallest tuple \(d' \in M_G^{\top }\) such that \(d<_l d'\) iff \(\langle d \rangle _l < \langle d' \rangle _l\). In particular, for \(d=\top \) we have . Otherwise, if l is even and \(\min \{y \in M_G^{\top } | y >_l d\}\) if l is odd. To conclude we introduce a ranking function that associates to each node either a c-tuple in \(M_G\) or the value \(\top \), and a function Lift that defines the increment of a node v based on its priority and the values of its neighbors. The formal definition of Lift follows.

Lift is monotone and the progress measures over v is the least fixed point of \(Lift(\cdot , v)\). The solution algorithm starts by setting 0 to every node. Then, it applies the lift as long as for some node v. Next lemma relates the solution of a PG with the least fixed point calculation of .

Lemma 1

([13]). If \(\varrho \) is a progress measures function then the set of nodes v with \(\varrho (v) < \top \) is the set of winning nodes for Player 0.

The Algorithm () [10]. was first introduced by Kupferman and Vardi in [18] to solve parity games via emptiness checking of parity automata. It makes use of two special sets of nodes, and , called Visiting and Avoiding, respectively. Intuitively, a node is visiting for a player at the stage in which it is clear that, by reaching that node, he can surely induce a winning play. The reasoning is symmetric for the avoiding set. The algorithm, in turns, tries to partition all nodes of the game into these two sets. Some formal details follow.

Given a PG , an Extended Parity Game, (EPG, for short) is a tuple where , , , , and are as in PG. Moreover, the sets are two disjoint sets of Visiting and Avoiding nodes, respectively. For EPGs we make use of the same notion of play as given for PG. A play in is winning for Player , while a play in is winning for Player . A play that never hits either or is declared winning for Player iff it satisfies the parity condition, i.e., is even, otherwise it is winning for Player .

To solve an EPG, makes use of two functions: and . For , is the set of nodes from which Player i can force, in one step, a move to . The function denotes the nodes from which Player i has a strategy that avoids , and either forces a visit to or satisfies the parity condition \(\alpha \). Note that in \(\alpha \) is given as a finite sequence of sets, where , i.e., the set of nodes with priority j. Formally, is defined as follows. If \(\alpha = \varepsilon \), then . Otherwise, if , for some set , then , where \(\mu \) is the least fixed-point operator.

Recursive Zielonka Algorithm () [24]. Introduced by Zielonka, makes use of a divide and conquer technique. The core subroutine of is the attractor. Intuitively, given a set of nodes U the attractor of U for a Player i represents those nodes that i can force the play toward. At each step, the algorithm removes all nodes with the highest priority p, together with all nodes Player \(i = p \ mod \ 2\) can attract to them, and recursively computes the winning sets \((W_0 , W_1 )\) for Player 0 and Player 1, respectively, on the remaining subgame. If Player i wins the subgame, then he also wins the whole starting game. Otherwise if Player i does not win the subgame, i.e., \(W_{1-i}\) is non empty, the algorithm computes the attractor for Player \(1-i\) of \(W_{1-i}\) and recursively solves the subgame.

3.2 Symbolic Algorithms

We now describe symbolic versions of the explicit algorithms listed in Sect. 3.1.

SPG Implementation. An SPG can be implemented using Binary Decision Diagrams (BDDs) and Algebraic Decision Diagrams (ADDs) [1] to represent and manipulate the associated Boolean functions introduced along with its definition. ADDs were introduced to extend BDDs by allowing values from any arbitrary finite domain to be associated with the terminal nodes of the diagram, i.e., an ADD can be seen as a BDD whose leaves may take on values belonging to a set of constants different from 0 and 1. Given an SPG with maximal priority c, we use BDDs to represent the Boolean formulas , and , and an ADD for the function . Moreover, we decompose the function into a sequence of BDDs \(\mathcal {B}=\langle B_0,\ldots , B_{c-1} \rangle \) where each \(B_i\) encodes the nodes with priority i, to easily manage the selection of a set of nodes with a specific priority. In the sequel, by BDD (resp., ADD) f, we denote the BDD (resp., ADD) representing the function f.

Symbolic () [5]. This is the first symbolic implementation of we are aware of, and which we describe with some minor corrections compared to the one in [5]. is encoded by using ADDs and the algorithm computes the progress measure as the least fixed point \(f_G\) of on a ranking function here given by the function , with \(D= M_G \cup \{\infty , -\infty \}\). The algorithm takes as input an SPG and returns an ADD representing the least fixed point \(f_G\) such that the set of winning nodes for Player 0 is \(\{v | f_G(v) < \infty \}\), and the set of winning nodes for Player 1 is \(\{v | f_G(v) = \infty \}\). See Algorithm 1.

figure a

The algorithm calls the procedure (resp., ), which given an ADD , the BDD , and \(1 \le j \le k\), returns an ADD that assigns to every node (resp., ,), with , the value (resp., ).

(resp., ) aims at constructing an ADD that represents the ranking function (resp., ). To do this, given an ADD and the BDD , it is generated an ADD such that if and \(f(v')=d\). Then, the ADD \(f_{suc}\) is given in input to the procedure , described in Algorithm 2, that constructs the ADD for \(f_{min}\). The procedure is defined similarly. Let n be an ADD node, we refer to the left and right successors of n as n.l and n.r, respectively, and refer to the variable that n represents as n.v.

figure b

The procedure calls the procedure , reported in Algorithm 3, that gets in input the pointer to the roots \(n_1\) and \(n_2\) of two ADDs representing the functions \(f_1\) and \(f_2\), both from some set to D, and merges them to an ADD in which every \(u \in U\) is mapped into \(\min (f_1(u),f_2(u))\).

figure c

Set-Based Symbolic () [8]. This is a symbolic implementation of that has been introduced very recently. It allows to use only basic set operations like \(\cup \), \(\cap \), \(\setminus \), \(\subseteq \), and one-step predecessor operations for its description. Unlike the implementation described previously, the ranking function is implicitly encoded by using sets of nodes. This allows representing the Lift operator just by BDDs.

To encode the ranking function the algorithm defines for each rank \(r \in M_G^{\top }\) the set \(S_r\) containing the nodes with rank r or higher. Formally, given the ranking function , the corresponding sets are defined as \(S_r=\{ v | \varrho (v) \ge r\}\). Conversely, given the family of sets \(\{S_r\}_r\), the corresponding ranking function, say \(\varrho _{\{S_r\}_r}\), is given by \(\varrho _{\{S_r\}_r}(v)=\max \{r \in M_G^{\top } | v \in S_r\}\). This formulation encodes the ranking function with sets but uses exponential in c many sets.

Space is reduced to a linear number of sets by encoding the value of each coordinate of the rank r, separately. In detail, for each odd priority i, the algorithm defines the sets \(C^i_{0},\ldots , C^i_{n_i} \). Each set \(C^i_{x}\) with \(x\in \{0,\ldots ,n_i\}\) contains the nodes that have x as i-th coordinate of their rank. Therefore, the algorithm has to construct the set \(S_r\) whenever it needs it.

Let the one-step controllable predecessor operator. The algorithm starts initializing the sets \(S_r\) for \(r>0\) to empty, and \(S_0\) with the set of all nodes . The rank r initially is set to the second lowest rank . Then, at each iteration the set \(S_r\) is updated for the current value of r by using the Lift encoded by the \(Cpre_i\) operator. After the update of \(S_r\), it is checked if \( S_r' \supseteq S_r\) for all \(r' < r\), i.e., if the property of the anti-monotonicity is preserved. Anti-monotonicity together with the definition of the sets \(S_r'\) allows to decide whether the rank of a node v can be increased to r by only considering one set \(S_r'\). If the anti-monotonicity is preserved, then for \(r < \top \) the value of r is increased to the next highest rank and for \(r=\top \) the algorithm terminates. Otherwise the nodes newly added to \(S_r\) are also added to all sets with \(r' < r\) that do not already contain them; the variable r is then updated to the lowest \(r'\) for which a new node is added to \(S_r'\) in this iteration. Due to lack of space, we omit the algorithm (see [8] for more details).

Symbolic Versions of () and (). and can be easily rephrased symbolically by using BDDs to represent the operations they make use of set basic operations like union, intersection, complement, and inclusion; the controllable predecessor operators used to implement the function in , and the attractor in ; the symbolic construction of a subgame used in and implemented following the definition of symbolic subgame reported previously.

4 Experimental Evaluations: Methodology and Results

We now analyze the performance of the introduced symbolic approach to solve PGs and compare with the explicit one. We have implemented the symbolic algorithms described in Sect. 3.2 in a fresh tool, called (Symbolic Parity Games Solver). Footnote 1 is implemented in C++ and uses the CUDDFootnote 2 package as the underlying BDD and ADD library. The platform provides a collection of tools to randomly generate and solve SPGs, as well as compare the performance of different symbolic algorithms.

We have also compared them with Oink, a platform recently developed in C++ by van Dijk [22], which collects the large majority of explicit PGs algorithms introduced in the literature [6, 14, 15, 24].

4.1 Experimental Results

In this section we report on some experimental results on evaluating the performance for the explicit algorithms , , and , as well as their corresponding symbolic versions , and . All tests have been run on an Intel Core i7 @2.40 GHz, with 16 GB of RAM running macOS 10.12. We have used different classes of parity games: random games with linear structures, ladder games, clique games as well as games corresponding to practical model checking problems. Random games are generated by , while for ladder and clique games we use Oink. We have taken 100 different instances for each class of games and used the average time execution. In all tests, we use \(\mathtt{abort}_{T}\) to denote an aborted execution due to time-out (greater than 200 s). On the class of ladder games and in model checking problems the benchmarks have been executed using the variable ordering given by the heuristic WINDOW2 module available in the CUDD package.

Random Games with Linear Structure. Tabakov and Vardi showed that in the context of automata-theoretic problems, explicit algorithms generally dominate symbolic algorithms, as BDDs do not offer any compression for random sets [21]. We found that the same holds for parity-game solving (we omit details due to lack of space). In [21] it was observed that, in case of random games with linear structures, the symbolic algorithms are the best performing ones. Hence, we have investigated the same class here as well, but with a different outcome.

A random game with linear structure is built by restricting the transition relation as follows: a node \(v_i\) can make a transition to node \(v_j\), where , if and only if \(|i-j| \le d\), where d is named as the distance parameter.

Table 1. Runtime executions of the symbolic algorithms
Full size table

Table 1 collects the running time of the symbolic algorithms on random games with linear structures having priorities 2, 3, and 5, and distance \(d= 25\). The results show that performs better than the others in solving games with \( n \le 10,000\) nodes and 2 priorities, while is the best performing in all other cases. Also, they show that and have the worst performances in all instances, with overcoming of more than 200 s on games with 3, 000 nodes. In Table 2 we collect the execution time of the explicit algorithms on the same set of games. The results highlight that the explicit algorithms are faster than the symbolic ones in all instances.

Table 2. Runtime executions of the explicit algorithms
Full size table

Ladder Games. In a ladder game, every node in has priority i. In addition, each node has two successors: one in and one in , which form a node pair. Every pair is connected to the next pair forming a ladder of pairs. Finally, the last pair is connected to the top. The parameter m specifies the number of node pairs. Formally, a ladder game of index m is where for \( i \in \{1,2\} \}\), and . Tables 3 and 4 report the benchmarks.

Table 3. Runtime executions of the symbolic algorithms on ladder games.
Full size table
Table 4. Runtime executions of the explicit algorithms on ladder games.
Full size table

Benchmarks indicate that and outperform their explicit versions, showing an excellent runtime execution even on fairly large instances. Indeed, while needs 6.31 s for games with index \(m=10M\), takes just 0.00015 s. Tests also show that and have yet the worst performance (Table 3).

Clique Games. Clique games are fully connected games without self-loops, where (resp., ) contains the nodes with an even index (resp., odd) and each node has as priority the index of v. An important feature of the clique games is the high number of cycles, which may pose difficulties for certain algorithms. Formally, a clique game of index n is where , and . Benchmarks on clique games are reported in Tables 5 and 6.

Table 5. Runtime executions of the symbolic algorithms on clique games
Full size table
Table 6. Runtime executions of the explicit algorithms on clique games
Full size table

Benchmarks show that is the best one among the symbolic algorithms in all instances, and outperform the explicit ones (as in ladder games), and the symbolic versions of do not show good results even on small games.

Finally, we evaluate the symbolic and explicit approaches on some practical model checking problems as in [17]. Specifically, we use models coming from: the Sliding Window Protocol (SWP) with window size (WS) of 2 and 4 (WS represents the boundary of the total number of packets to be acknowledged by the receiver), the Onebit Protocol (OP), and the Lifting Truck (Lift). The properties we check on these models concern: absence of deadlock (ND), a message of a certain type (d1) is received infinitely often (IORD1), if there are infinitely many read steps then there are infinitely many write steps (IORW), liveness, and safety. Note that, in all benchmarks, data size (DS) denotes the number of messages.

Table 7. SWP (Sliding Window Protocol)
Full size table
Table 8. OP (Onebit Protocol)
Full size table
Table 9. Lift (Lifting Truck)
Full size table

As we can see, by comparing Tables 7, 8, and 9, the experiments indicate more nuanced relationship between the symbolic and explicit approaches. Indeed, they show a different behavior depending on the protocol and the property we are checking. Overall, we note that outperforms the other symbolic algorithms in all protocols, although the advantage over is discontinued. Specifically, is the best performing in checking absence of deadlock in all three protocols, but for IORD1 in the SWP protocol with \(WS=2\), or for IORW in the OP protocol, exhibits a significant advantage. Differently, and show better performances on a smaller number of properties. Moreover, the results highlights that exhibits the worst performances in all protocols and properties.

5 Concluding Remarks

In this paper we have compared for the first time the performances of different symbolic and explicit versions of classic algorithms to solve parity games. To this aim we have implemented in a fresh tool, which we have called , the symbolic versions of Recursive [24], [10, 18], and the small-progress-measures algorithms presented in [5, 8].

Our analysis started from constrained random games [21]. The results show that on these games the explicit approach is better than the symbolic one, exhibiting a different behavior than the one showed in [21]. To gain a fuller understanding of the performances of the symbolic and the explicit algorithms, we have further tested the two approaches on structured games. Precisely, we have considered ladder games, clique games, as well as game models coming from practical model-checking problems. We have showed several cases in which the symbolic algorithms have the advantage over the explicit ones.

Our empirical study let us to conclude that on comparing explicit and symbolic algorithms for solving parity games, it would be useful to have real scenarios and not only random games, as the common practice has been.