In this paper, we review a broad investigation of the symbolic approach for solving Parity Games. Specifically, we implement in a tool, called SymPGSolver, four symbolic algorithms to solve Parity Games and compare their performances to the corresponding explicit versions for diferent classes of games. By means of benchmarks, we show that for random games, even for constrained random games, explicit algorithms actually perform better than symbolic algorithms. The situation changes, however, for structured games, where symbolic algorithms seem to have the advantage. This suggests that when evaluating algorithms for parity-game solving, it would be useful to have real benchmarks and not only random benchmarks, as the common practice has been.
over a singleton alphabet, and the system is correct with respect to the specification if this
automaton is nonempty [
The problem of deciding if Player 0 has a winning strategy (i.e., can induce a winning play)
in a given parity game is known to be in UPTime ∩ CoUPTime [14]; whether a polynomial time
solution exists is a long-standing open question [
Symbolic algorithms are an eficient 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) [20] 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 1020 states and more [21, 22]. 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 RE [23, 24], which, however, has been done for diferent purposes and no benchmark comparison with the explicit version has been carried out. Other works close to this topic and worth mentioning are [25, 26], where a symbolic version of SPM has been theoretically studied but not implemented.
In [27, 28] a first broad investigation of the symbolic approach for solving PGs is provided. We implement four symbolic algorithms and compare their performances to the corresponding explicit versions for diferent classes of PGs [ 29]. Specifically, we implement in a new tool, called SymPGSolver1, the symbolic versions of RE, APT, and two variants of SPM. The tool also allows to generate random games, as well as compare the performance of diferent symbolic algorithms.
Our analysis started from constrained random games [30]. The results show that on these games the explicit approach is better than the symbolic one, exhibiting a diferent behavior than the one showed in [30]. 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 1The tool is available for download from https://github.com/antoniodistasio/sympgsolver practical model-checking problems.
Ladder Games. In a ladder game, every node in P has priority . In addition, each node ∈ P has two successors: one in P0 and one in P1, 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 specifies the number of node pairs. Formally, a ladder game of index is = (P0, P1, Mv , p) where P0 = {0, 2, . . . , 2 − 2}, P1 = {1, 3, . . . , 2 − 1}, Mv = {(, )| ≡ 2 + for ∈ {1, 2}}, and p() = 2. Tables 1 and 2 reports the benchmarks.
1,000 10,000 100,000 1,000,000 10,000,000
SRE
SAPT
SSP
Benchmarks indicate that SRE and SAPT outperform their explicit versions, showing an excellent runtime execution even on fairly large instances. Indeed, while RE needs 6.31 seconds for games with index = 10 , SRE takes just 0.00015 seconds. Tests also show that SSP and SSP2 have yet the worst performance.
Clique Games. Clique games are fully connected games without self-loops, where P0 (resp., P1) contains the nodes with an even index (resp., odd) and each node ∈ P has as priority the index of . An important feature of the clique games is the high number of cycles, which may pose dificulties for certain algorithms. Formally, a clique game of index is = (P0, P1, Mv , p) where P0 = {0, 2, . . . , − 2}, P1 = {1, 3, . . . , − 1}, Mv = {(, )| ̸= }, and p() = . Benchmarks on clique games are reported in Tables 3 and 4.
The main result we obtain from our comparisons is that for random games, and even for constrained random games, explicit algorithms actually perform better than symbolic ones, most likely because BDDs do not ofer 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 [31].
Finally, we evaluate the symbolic and explicit approaches on some practical model checking problems as in [32]. 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.
As we can see, by comparing Tables 5, 6, and 7, the experiments indicate more nuanced relationship between the symbolic and explicit approaches. Indeed, they show a diferent behavior depending on the protocol and the property we are checking. Overall, we note that SSP SRE outperforms the other symbolic algorithms in all protocols, although the advantage over RE is discontinued. Specifically, SRE is the best performing in checking absence of deadlock in all three protocols, but for IORD1 in the SWP protocol with = 2, or for IORW in the OP protocol, RE exhibits a significant advantage. Diferently, SAPT and SSP2 show better performances on a smaller number of properties. Moreover, the results highlights that SSP exhibits the worst performances in all protocols and properties.
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. Acknowledgments We thank our co-authors on the publications mentioned in this communication: Aniello Murano and Moshe Y. Vardi. This work is partially supported by the ERC Advanced Grant WhiteMech (No. 834228), by the EU ICT-48 2020 project TAILOR (No. 952215), and by the PRIN project RIPER (No. 20203FFYLK). [9] O.Kupferman, M.Vardi, P.Wolper, Module Checking., Information and Computation. 164 (2001) 322–344. [10] W. Thomas, Facets of Synthesis: Revisiting Church’s Problem, in: Foundations of Software Science and Computational Structures, 12th International Conference, FOSSACS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009., LNCS 5504, 2009, pp. 1–14. [11] B. Aminof, O. Kupferman, A. Murano, Improved Model Checking of Hierarchical Systems,
Inf. Comput. 210 (2012) 68–86. [12] F. Mogavero, A. Murano, L. Sorrentino, On Promptness in Parity Games, in: Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013., LNCS 8312, 2013, pp. 601–618. [13] D. Kozen, Results on the Propositional -Calculus, Theoretical Computer Science 27 (1983) 333–354. [14] M. Jurdzinski, Deciding the Winner in Parity Games is in UP ∩ co-Up, Inf. Process. Lett.
68 (1998) 119–124. [15] W. Zielonka, Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees, Theor. Comput. Sci. 200 (1998) 135–183. [16] M. Jurdzinski,Small Progress Measures for Solving Parity Games, in: STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, LNCS 1770, 2000, pp. 290–301. [17] A. Di Stasio, A. Murano, G. Perelli, M. Y. Vardi, Solving parity games using an automatabased algorithm, in: Implementation and Application of Automata - 21st International Conference, CIAA 2016, Seoul, South Korea, July 19-22, 2016., 2016, pp. 64–76. [18] C. S. Calude, S. Jain, B. Khoussainov, W. Li, F. Stephan, Deciding parity games in quasipolynomial time, in: STOC 2017, 2017, pp. 252–263. [19] M. Jurdzinski, M. Paterson, U. Zwick, A deterministic subexponential algorithm for solving parity games, in: Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2006, Miami, Florida, USA, January 22-26, 2006, ACM Press, 2006, pp. 117–123. [20] R. E. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Trans.
Comput. (1986) 677–691. [21] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang, Symbolic model checking: 10ˆ20 states and beyond, in: Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS ’90), Philadelphia, Pennsylvania, USA, June 4-7, 1990, 1990, pp. 428–439. [22] K. L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993. [23] G. Kant, J. van de Pol, Generating and solving symbolic parity games, in: Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering, GRAPHITE 2014, Grenoble, France, 5th April 2014, 2014, pp. 2–14. [24] M. Bakera, S. Edelkamp, P. Kissmann, C. D. Renner, Solving -calculus parity games by symbolic planning, in: Model Checking and Artificial Intelligence, 5th International Workshop, MoChArt 2008, Patras, Greece, July 21, 2008., 2008, pp. 15–33. [25] D. Bustan, O. Kupferman, M. Y. Vardi, A measured collapse of the modal -calculus alternation hierarchy, in: STACS 2004, 21st Annual Symposium on Theoretical Aspects of Computer Science, Montpellier, France, March 25-27, 2004, Proceedings, 2004, pp. 522–533. [26] K. Chatterjee, W. Dvorák, M. Henzinger, V. Loitzenbauer, Improved set-based symbolic algorithms for parity games, in: 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, August 20-24, 2017, Stockholm, Sweden, 2017, pp. 18:1–18:21. [27] A. Di Stasio, A. Murano, M. Y. Vardi, Solving parity games: Explicit vs symbolic, in: Implementation and Application of Automata - 23rd International Conference, CIAA 2018, Charlottetown, PE, Canada, July 30 - August 2, 2018, Proceedings, 2018, pp. 159–172. [28] A. D. Stasio, Reasoning about LTL Synthesis over finite and infinite games, Ph.D. thesis,
University of Naples Federico II, Italy, 2018. [29] T. van Dijk, Oink: An implementation and evaluation of modern parity game solvers, in: Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, LNCS 10805, Springer, 2018, pp. 291–308. [30] D. Tabakov, Evaluation of Explicit and Symbolic Automata-Theoretic Algorithm, Master’s thesis, Rice University, 2005. [31] C. Eisner, D. A. Peled, Comparing symbolic and explicit model checking of a software system, in: Model Checking of Software, 9th International SPIN Workshop, Grenoble, France, April 11-13, 2002, Proceedings, 2002, pp. 230–239. [32] J. A. Keiren, Benchmarks for parity games, in: FSEN 2015, 2015, pp. 127–142.