@inproceedings(DBLP:conf/mochart/BakeraEKR08, author = {Marco Bakera and Stefan Edelkamp and Peter Kissmann and Clemens~D. Renner}, year = {2008}, title = {Solving {$\mathrm{\mu}$}-Calculus Parity Games by Symbolic Planning}, booktitle = {MoChArt}, series = {Lecture Notes in Computer Science}, volume = {5348}, publisher = {Springer}, pages = {15--33}, doi = {10.1007/978-3-540-92221-6}, ) @article(DBLP:journals/fmsd/BenerecettiDM18, author = {Massimo Benerecetti and Daniele Dell'Erba and Fabio Mogavero}, year = {2018}, title = {Solving parity games via priority promotion}, journal = {Formal Methods Syst. Des.}, volume = {52}, number = {2}, pages = {193--226}, doi = {10.1016/0304-3975(95)00188-3}, ) @book(boole1854investigation, author = {George Boole}, year = {1854}, title = {An investigation of the laws of thought: on which are founded the mathematical theories of logic and probabilities}, volume = {2}, publisher = {Walton and Maberly}, ) @inproceedings(DBLP:journals/corr/BruseFL14, author = {Florian Bruse and Michael Falk and Martin Lange}, year = {2014}, title = {The Fixpoint-Iteration Algorithm for Parity Games}, booktitle = {GandALF}, series = {{EPTCS}}, volume = {161}, pages = {116--130}, doi = {10.4204/EPTCS.161.12}, ) @article(DBLP:journals/csur/Bryant92, author = {Randal~E. Bryant}, year = {1992}, title = {Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams}, journal = {{ACM} Comput. Surv.}, volume = {24}, number = {3}, pages = {293--318}, doi = {10.1145/42282.46161}, ) @article(DBLP:journals/iandc/BurchCMDH92, author = {Jerry~R. Burch and Edmund~M. Clarke and Kenneth~L. McMillan and David~L. Dill and L.~J. Hwang}, year = {1992}, title = {Symbolic Model Checking: 10{\^{}}20 States and Beyond}, journal = {Inf. Comput.}, volume = {98}, number = {2}, pages = {142--170}, doi = {10.1016/0890-5401(92)90017-A}, ) @inproceedings(DBLP:conf/stoc/CaludeJKL017, author = {Cristian~S. Calude and Sanjay Jain and Bakhadyr Khoussainov and Wei Li and Frank Stephan}, year = {2017}, title = {Deciding parity games in quasipolynomial time}, booktitle = {{STOC}}, publisher = {{ACM}}, pages = {252--263}, doi = {10.1145/3055399.3055409}, ) @inproceedings(DBLP:conf/lpar/ChatterjeeDHS18, author = {Krishnendu Chatterjee and Wolfgang Dvor{\'{a}}k and Monika Henzinger and Alexander Svozil}, year = {2018}, title = {Quasipolynomial Set-Based Symbolic Algorithms for Parity Games}, booktitle = {{LPAR}}, series = {EPiC Series in Computing}, volume = {57}, publisher = {EasyChair}, pages = {233--253}, doi = {10.29007/5z5k}, ) @inproceedings(DBLP:conf/soda/CzerwinskiDFJLP19, author = {Wojciech Czerwinski and Laure Daviaud and Nathana{\"{e}}l Fijalkow and Marcin Jurdzinski and Ranko Lazic and Pawel Parys}, year = {2019}, title = {Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games}, booktitle = {{SODA}}, publisher = {{SIAM}}, pages = {2333--2349}, doi = {10.1137/1.9781611975482.142}, ) @inproceedings(DBLP:conf/cav/Dijk18, author = {Tom van Dijk}, year = {2018}, title = {Attracting Tangles to Solve Parity Games}, booktitle = {{CAV} {(2)}}, series = {Lecture Notes in Computer Science}, volume = {10982}, publisher = {Springer}, pages = {198--215}, doi = {10.1007/978-3-319-96142-2\_14}, ) @inproceedings(DBLP:conf/tacas/Dijk18, author = {Tom van Dijk}, year = {2018}, title = {Oink: An Implementation and Evaluation of Modern Parity Game Solvers}, booktitle = {{TACAS} {(1)}}, series = {Lecture Notes in Computer Science}, volume = {10805}, publisher = {Springer}, pages = {291--308}, doi = {10.1016/S0304-3975(98)00009-7}, ) @article(DBLP:journals/sttt/DijkP17, author = {Tom van Dijk and Jaco van~de Pol}, year = {2017}, title = {Sylvan: multi-core framework for decision diagrams}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {19}, number = {6}, pages = {675--696}, doi = {10.1007/s10009-016-0433-2}, ) @inproceedings(DBLP:journals/corr/abs-1909-07659, author = {Tom van Dijk and Bob Rubbens}, year = {2019}, title = {Simple Fixpoint Iteration To Solve Parity Games}, booktitle = {GandALF}, series = {{EPTCS}}, volume = {305}, pages = {123--139}, doi = {10.4204/EPTCS.305.9}, ) @book(DBLP:books/daglib/0029044, author = {Rolf Drechsler and Bernd Becker}, year = {1998}, title = {Binary Decision Diagrams - Theory and Implementation}, publisher = {Springer}, doi = {10.1007/978-1-4757-2892-7}, ) @article(DBLP:journals/sttt/DrechslerS01, author = {Rolf Drechsler and Detlef Sieling}, year = {2001}, title = {Binary decision diagrams in theory and practice}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {3}, number = {2}, pages = {112--136}, doi = {10.1007/s100090100056}, ) @inproceedings(DBLP:conf/focs/EmersonJ91, author = {E.~Allen Emerson and Charanjit~S. Jutla}, year = {1991}, title = {Tree Automata, Mu-Calculus and Determinacy (Extended Abstract)}, booktitle = {{FOCS}}, publisher = {{IEEE} Computer Society}, pages = {368--377}, doi = {10.1109/SFCS.1991.185392}, ) @article(DBLP:journals/sttt/FearnleyJKSSW19, author = {John Fearnley and Sanjay Jain and Bart de~Keijzer and Sven Schewe and Frank Stephan and Dominik Wojtczak}, year = {2019}, title = {An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {21}, number = {3}, pages = {325--349}, doi = {10.1016/S0304-3975(98)00009-7}, ) @article(pgsolver, author = {Oliver Friedmann and Martin Lange}, year = {2009}, title = {The PGSolver collection of parity game solvers}, journal = {University of Munich}, pages = {4--6}, ) @inproceedings(DBLP:journals/corr/abs-1711-11439, author = {Swen Jacobs and Nicolas Basset and Roderick Bloem and Romain Brenguier and Maximilien Colange and Peter Faymonville and Bernd Finkbeiner and Ayrat Khalimov and Felix Klein and Thibaud Michaud and Guillermo~A. P{\'{e}}rez and Jean{-}Fran{\c{c}}ois Raskin and Ocan Sankur and Leander Tentrup}, year = {2017}, title = {The 4th Reactive Synthesis Competition {(SYNTCOMP} 2017): Benchmarks, Participants {\&} Results}, booktitle = {SYNT@CAV}, series = {{EPTCS}}, volume = {260}, pages = {116--143}, doi = {10.4204/EPTCS.260.10}, ) @article(DBLP:journals/ipl/Jurdzinski98, author = {Marcin Jurdzinski}, year = {1998}, title = {Deciding the Winner in Parity Games is in {UP} {\textbackslash}cap co-Up}, journal = {Inf. Process. Lett.}, volume = {68}, number = {3}, pages = {119--124}, doi = {10.1016/S0020-0190(98)00150-1}, ) @inproceedings(DBLP:conf/stacs/Jurdzinski00, author = {Marcin Jurdzinski}, year = {2000}, title = {Small Progress Measures for Solving Parity Games}, booktitle = {{STACS}}, series = {Lecture Notes in Computer Science}, volume = {1770}, publisher = {Springer}, pages = {290--301}, doi = {10.1007/3-540-46541-3\_24}, ) @inproceedings(DBLP:conf/tacas/KantLMPBD15, author = {Gijs Kant and Alfons Laarman and Jeroen Meijer and Jaco van~de Pol and Stefan Blom and Tom van Dijk}, year = {2015}, title = {LTSmin: High-Performance Language-Independent Model Checking}, booktitle = {{TACAS}}, series = {Lecture Notes in Computer Science}, volume = {9035}, publisher = {Springer}, pages = {692--707}, doi = {10.1016/S0304-3975(98)00009-7}, ) @inproceedings(kant_parity_bdd, author = {Gijs Kant and Jaco van~de Pol}, year = {2014}, title = {Generating and Solving Symbolic Parity Games}, booktitle = {{GRAPHITE}}, series = {{EPTCS}}, volume = {159}, pages = {2--14}, doi = {10.4204/EPTCS.159.2}, ) @inproceedings(apt, author = {Orna Kupferman and Moshe~Y. Vardi}, year = {1998}, title = {Weak Alternating Automata and Tree Automata Emptiness}, booktitle = {{STOC}}, publisher = {{ACM}}, pages = {224--233}, doi = {10.1145/276698.276748}, ) @inproceedings(DBLP:conf/vmcai/LapauwBD20, author = {Ruben Lapauw and Maurice Bruynooghe and Marc Denecker}, year = {2020}, title = {Improving Parity Game Solvers with Justifications}, booktitle = {{VMCAI}}, series = {Lecture Notes in Computer Science}, volume = {11990}, publisher = {Springer}, pages = {449--470}, doi = {10.1016/S0304-3975(98)00009-7}, ) @inproceedings(DBLP:conf/cav/MeyerSL18, author = {Philipp~J. Meyer and Salomon Sickert and Michael Luttenberger}, year = {2018}, title = {Strix: Explicit Reactive Synthesis Strikes Back!}, booktitle = {{CAV} {(1)}}, series = {Lecture Notes in Computer Science}, volume = {10981}, publisher = {Springer}, pages = {578--586}, doi = {10.1007/978-3-319-96145-3\_31}, ) @inproceedings(DBLP:conf/mfcs/Parys19, author = {Pawel Parys}, year = {2019}, title = {Parity Games: Zielonka's Algorithm in Quasi-Polynomial Time}, booktitle = {{MFCS}}, series = {LIPIcs}, volume = {138}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, pages = {10:1--10:13}, doi = {10.4230/LIPIcs.MFCS.2019.10}, ) @article(DBLP:journals/corr/abs-1912-05793, author = {Guillermo~A. P{\'{e}}rez}, year = {2019}, title = {The Extended {HOA} Format for Synthesis}, journal = {CoRR}, volume = {abs/1912.05793}, ) @inproceedings(willemse, author = {Lisette Sanchez and Wieger Wesselink and Tim A.~C. Willemse}, year = {2018}, title = {A Comparison of BDD-Based Parity Game Solvers}, booktitle = {GandALF}, series = {{EPTCS}}, volume = {277}, pages = {103--117}, doi = {10.4204/EPTCS.277.8}, ) @article(shannon1938symbolic, author = {Claude~E Shannon}, year = {1938}, title = {A symbolic analysis of relay and switching circuits}, journal = {Electrical Engineering}, volume = {57}, number = {12}, pages = {713--723}, doi = {10.1109/EE.1938.6431064}, ) @article(DBLP:journals/sttt/Somenzi01, author = {Fabio Somenzi}, year = {2001}, title = {Efficient manipulation of decision diagrams}, journal = {Int. J. Softw. Tools Technol. Transf.}, volume = {3}, number = {2}, pages = {171--181}, doi = {10.1007/s100090100042}, ) @inproceedings(stasio_bdd_parity, author = {Antonio~Di Stasio and Aniello Murano and Moshe~Y. Vardi}, year = {2018}, title = {Solving Parity Games: Explicit vs Symbolic}, booktitle = {{CIAA}}, series = {Lecture Notes in Computer Science}, volume = {10977}, publisher = {Springer}, pages = {159--172}, doi = {10.1016/S0304-3975(98)00009-7}, ) @inproceedings(DBLP:conf/cav/VogeJ00, author = {Jens V{\"{o}}ge and Marcin Jurdzinski}, year = {2000}, title = {A Discrete Strategy Improvement Algorithm for Solving Parity Games}, booktitle = {{CAV}}, series = {Lecture Notes in Computer Science}, volume = {1855}, publisher = {Springer}, pages = {202--215}, doi = {10.1016/0304-3975(95)00188-3}, ) @article(mu_calculus, author = {Igor Walukiewicz}, year = {2002}, title = {Monadic second-order logic on tree-like structures}, journal = {Theor. Comput. Sci.}, volume = {275}, number = {1-2}, pages = {311--346}, doi = {10.1016/S0304-3975(01)00185-2}, ) @article(DBLP:journals/tcs/Zielonka98, author = {Wieslaw Zielonka}, year = {1998}, title = {Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees}, journal = {Theor. Comput. Sci.}, volume = {200}, number = {1-2}, pages = {135--183}, doi = {10.1016/S0304-3975(98)00009-7}, )