{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:51:29Z","timestamp":1764402689491,"version":"3.41.0"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319246437"},{"type":"electronic","value":"9783319246444"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24644-4_9","type":"book-chapter","created":{"date-parts":[[2015,9,24]],"date-time":"2015-09-24T05:34:39Z","timestamp":1443072879000},"page":"127-142","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Benchmarks for Parity Games"],"prefix":"10.1007","author":[{"given":"Jeroen J. A.","family":"Keiren","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"issue":"5","key":"9_CR1","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1016\/j.jctb.2006.12.006","volume":"97","author":"I. Adler","year":"2007","unstructured":"Adler, I.: Directed tree-width examples. Journal of Combinatorial Theory, Series B\u00a097(5), 718\u2013725 (2007)","journal-title":"Journal of Combinatorial Theory, Series B"},{"key":"9_CR2","unstructured":"Albert, M.H., Grossman, J.P., Nowakowski, R.J., Wolfe, D.: An introduction to clobber. Integers\u00a05(2) (2005)"},{"issue":"2","key":"9_CR3","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1137\/0608024","volume":"8","author":"S. Arnborg","year":"1987","unstructured":"Arnborg, S., Corneil, D.G., Proskurowski, A.: Complexity of finding embeddings in a k-tree. SIAM Journal on Algebraic Discrete Methods\u00a08(2), 277\u2013284 (1987)","journal-title":"SIAM Journal on Algebraic Discrete Methods"},{"issue":"5","key":"9_CR4","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1145\/362946.362970","volume":"12","author":"K.A. Bartlett","year":"1969","unstructured":"Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM\u00a012(5), 260\u2013261 (1969)","journal-title":"Communications of the ACM"},{"key":"9_CR5","unstructured":"Beck, A., Bleicher, M.N., Crowe, D.W.: Excursions into Mathematics: The Millennium Edition. CRC Press (2000)"},{"key":"9_CR6","unstructured":"Beffara, E., Vorobyov, S.G.: Adapting Gurvich-Karzanov-Khachiyan\u2019s algorithm for parity games. Technical report, Uppsala University, Sweden, Uppsala (2001)"},{"issue":"4","key":"9_CR7","doi-asserted-by":"publisher","first-page":"900","DOI":"10.1016\/j.jctb.2012.04.004","volume":"102","author":"D. Berwanger","year":"2012","unstructured":"Berwanger, D., Dawar, A., Hunter, P.W., Kreutzer, S., Obdr\u017e\u00e1lek, J.: The DAG-width of directed graphs. Journal of Combinatorial Theory, Series B\u00a0102(4), 900\u2013923 (2012)","journal-title":"Journal of Combinatorial Theory, Series B"},{"issue":"6","key":"9_CR8","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s00224-004-1147-5","volume":"37","author":"D. Berwanger","year":"2004","unstructured":"Berwanger, D., Gr\u00e4del, E.: Fixed-point logics and solitaire games. Theory of Computing Systems\u00a037(6), 675\u2013694 (2004)","journal-title":"Theory of Computing Systems"},{"key":"9_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-32275-7_15","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Berwanger","year":"2005","unstructured":"Berwanger, D., Gr\u00e4del, E.: Entanglement \u2013 A measure for the complexity of directed graphs with applications to logic and games. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 209\u2013223. Springer, Heidelberg (2005)"},{"key":"9_CR10","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2012.07.010","volume":"463","author":"D. Berwanger","year":"2012","unstructured":"Berwanger, D., Gr\u00e4del, E., Kaiser, L., Rabinovich, R.: Entanglement and the complexity of directed graphs. Theoretical Computer Science\u00a0463, 2\u201325 (2012)","journal-title":"Theoretical Computer Science"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/BFb0029946","volume-title":"Mathematical Foundations of Computer Science 1997","author":"H.L. Bodlaender","year":"1997","unstructured":"Bodlaender, H.L.: Treewidth: Algorithmic techniques and results. In: Privara, I., Ru\u017ei\u010dka, P. (eds.) MFCS 1997. LNCS, vol.\u00a01295, pp. 19\u201336. Springer, Heidelberg (1997)"},{"issue":"3","key":"9_CR12","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/j.ic.2009.03.008","volume":"208","author":"H.L. Bodlaender","year":"2010","unstructured":"Bodlaender, H.L., Koster, A.M.C.A.: Treewidth computations I. upper bounds. Information and Computation\u00a0208(3), 259\u2013275 (2010)","journal-title":"Information and Computation"},{"issue":"7","key":"9_CR13","doi-asserted-by":"publisher","first-page":"1103","DOI":"10.1016\/j.ic.2011.04.003","volume":"209","author":"H.L. Bodlaender","year":"2011","unstructured":"Bodlaender, H.L., Koster, A.M.C.A.: Treewidth computations II. lower bounds. Information and Computation\u00a0209(7), 1103\u20131119 (2011)","journal-title":"Information and Computation"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Bradfield, J.C., Stirling, C.: Modal logics and mu-calculi: an introduction. In: Handbook of Process Algebra, pp. 293\u2013330. Elsevier (2000)","DOI":"10.1016\/B978-044482830-9\/50022-9"},{"issue":"5","key":"9_CR15","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1109\/TCOM.1974.1092259","volume":"22","author":"V. Cerf","year":"1974","unstructured":"Cerf, V., Kahn, R.E.: A protocol for packet network intercommunication. IEEE Transactions on Communications\u00a022(5), 637\u2013648 (1974)","journal-title":"IEEE Transactions on Communications"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/978-3-642-14295-6_57","volume-title":"Computer Aided Verification","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Radhakrishna, A.: GIST: A solver for probabilistic games. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 665\u2013669. Springer, Heidelberg (2010)"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-540-74407-8_9","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"T. Chen","year":"2007","unstructured":"Chen, T., Ploeger, S.C.W., van de Pol, J.C., Willemse, T.A.C.: Equivalence checking for infinite systems using parameterized Boolean equation systems. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 120\u2013135. Springer, Heidelberg (2007)"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/3-540-56496-9_32","volume-title":"Computer Aided Verification","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Klein, M., Steffen, B.: Faster model checking for the modal mu-calculus. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 410\u2013422. Springer, Heidelberg (1993)"},{"issue":"1-3","key":"9_CR19","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/S0166-218X(99)00184-5","volume":"101","author":"B. Courcelle","year":"2000","unstructured":"Courcelle, B., Olariu, S.: Upper bounds to the clique width of graphs. Discrete Applied Mathematics\u00a0101(1-3), 77\u2013114 (2000)","journal-title":"Discrete Applied Mathematics"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/978-3-642-36742-7_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Cranen","year":"2013","unstructured":"Cranen, S., Groote, J.F., Keiren, J.J.A., Stappers, F.P.M., de Vink, E.P., Wesselink, J.W., Willemse, T.A.C.: An overview of the mCRL2 toolset and its recent advances. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 199\u2013213. Springer, Heidelberg (2013)"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-20398-5_16","volume-title":"NASA Formal Methods","author":"S. Cranen","year":"2011","unstructured":"Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: Stuttering mostly speeds up solving parity games. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 207\u2013221. Springer, Heidelberg (2011)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-642-32943-2_16","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"S. Cranen","year":"2012","unstructured":"Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: A cure for stuttering parity games. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol.\u00a07521, pp. 198\u2013212. Springer, Heidelberg (2012)"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-319-15317-9_9","volume-title":"Formal Aspects of Component Software","author":"A. Di Stasio","year":"2015","unstructured":"Di Stasio, A., Murano, A., Prignano, V., Sorrentino, L.: Solving parity games in Scala. In: Lanese, I., Madelaine, E. (eds.) FACS 2014. LNCS, vol.\u00a08997, pp. 145\u2013161. Springer, Heidelberg (2015)"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: SFCS 1991: Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, pp. 368\u2013377. IEEE Computer Society (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"9_CR25","unstructured":"Emerson, E.A., Lei, C.L.L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proceedings of LICS 1986, pp. 267\u2013278. IEEE Computer Society (1986)"},{"key":"9_CR26","doi-asserted-by":"crossref","unstructured":"Friedmann, O.: A super-polynomial lower bound for the parity game strategy improvement algorithm as we know it. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science, vol.\u00a07, pp. 145\u2013156 (2009)","DOI":"10.1109\/LICS.2009.27"},{"issue":"03","key":"9_CR27","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1142\/S0129054110007246","volume":"21","author":"O. Friedmann","year":"2010","unstructured":"Friedmann, O.: The Stevens-Stirling-algorithm for solving parity games locally requires exponential time. International Journal of Foundations of Computer Science\u00a021(03), 277\u2013287 (2010)","journal-title":"International Journal of Foundations of Computer Science"},{"key":"9_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(3:23)2011","volume":"7","author":"O. Friedmann","year":"2011","unstructured":"Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. Logical Methods in Computer Science\u00a07, 1\u201342 (2011)","journal-title":"Logical Methods in Computer Science"},{"issue":"4","key":"9_CR29","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1051\/ita\/2011124","volume":"45","author":"O. Friedmann","year":"2011","unstructured":"Friedmann, O.: Recursive algorithm for parity games requires exponential time. RAIRO - Theoretical Informatics and Applications\u00a045(4), 449\u2013457 (2011)","journal-title":"RAIRO - Theoretical Informatics and Applications"},{"key":"9_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-04761-9_15","volume-title":"Automated Technology for Verification and Analysis","author":"O. Friedmann","year":"2009","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 182\u2013196. Springer, Heidelberg (2009)"},{"key":"9_CR31","unstructured":"Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. Technical report, Institut f\u00fcr Informatik, Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Germany (2010)"},{"key":"9_CR32","doi-asserted-by":"crossref","unstructured":"Friedmann, O., Lange, M.: A solver for modal fixpoint logics. In: Electronic Notes in Theoretical Computer Science, vol.\u00a0262, pp. 99\u2013111. Elsevier (2010)","DOI":"10.1016\/j.entcs.2010.04.008"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-14203-1_28","volume-title":"Automated Reasoning","author":"O. Friedmann","year":"2010","unstructured":"Friedmann, O., Latte, M., Lange, M.: A decision procedure for CTL* based on tableaux and automata. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 331\u2013345. Springer, Heidelberg (2010)"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1038\/scientificamerican0374-102","volume":"230","author":"M. Gardner","year":"1974","unstructured":"Gardner, M.: Mathematical games: Cram, crosscram and quadraphage: New games having elusive winning strategies. Scientific American\u00a0230, 106\u2013108 (1974)","journal-title":"Scientific American"},{"key":"9_CR35","doi-asserted-by":"crossref","unstructured":"Gazda, M.W., Willemse, T.A.C.: Zielonka\u2019s recursive algorithm: dull, weak and solitaire games and tighter bounds. In: Proceedings GandALF 2013. EPTCS, vol.\u00a0119, pp. 7\u201320 (2013)","DOI":"10.4204\/EPTCS.119.4"},{"key":"9_CR36","unstructured":"Gogate, V., Dechter, R.: A complete anytime algorithm for treewidth. In: Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence, UAI 2004, pp. 201\u2013208. AUAI Press (2004)"},{"issue":"1-2","key":"9_CR37","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/S1567-8326(02)00038-3","volume":"55","author":"J.F. Groote","year":"2003","unstructured":"Groote, J.F., Pang, J., Wouters, A.G.G.: Analysis of a distributed system for lifting trucks. The Journal of Logic and Algebraic Programming\u00a055(1-2), 21\u201356 (2003)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"9_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1007\/BFb0014338","volume-title":"Algebraic Methodology and Software Technology","author":"J.F. Groote","year":"1996","unstructured":"Groote, J.F., van de Pol, J.: A bounded retransmission protocol for large data packets. In: Nivat, M., Wirsing, M. (eds.) AMAST 1996. LNCS, vol.\u00a01101, pp. 536\u2013550. Springer, Heidelberg (1996)"},{"key":"9_CR39","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/S0020-0190(98)00158-6","volume":"68","author":"W.H. Hesselink","year":"1998","unstructured":"Hesselink, W.H.: Invariants for the construction of a handshake register. Information Processing Letters\u00a068, 173\u2013177 (1998)","journal-title":"Information Processing Letters"},{"issue":"3","key":"9_CR40","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1016\/j.tcs.2008.02.038","volume":"399","author":"P.W. Hunter","year":"2008","unstructured":"Hunter, P.W., Kreutzer, S.: Digraph measures: Kelly decompositions, games, and orderings. Theoretical Computer Science\u00a0399(3), 206\u2013219 (2008)","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"9_CR41","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1006\/jctb.2000.2031","volume":"82","author":"T. Johnson","year":"2001","unstructured":"Johnson, T., Robertson, N., Seymour, P.D., Thomas, R.: Directed tree-width. Journal of Combinatorial Theory, Series B\u00a082(1), 138\u2013154 (2001)","journal-title":"Journal of Combinatorial Theory, Series B"},{"issue":"3","key":"9_CR42","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M. Jurdzi\u0144ski","year":"1998","unstructured":"Jurdzi\u0144ski, M.: Deciding the winner in parity games is in UP \u2229 co-UP. Information Processing Letters\u00a068(3), 119\u2013124 (1998)","journal-title":"Information Processing Letters"},{"key":"9_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/3-540-46541-3_24","volume-title":"STACS 2000","author":"M. Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol.\u00a01770, pp. 290\u2013301. Springer, Heidelberg (2000)"},{"key":"9_CR44","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: Proceedings of the Seventeenth Annual ACM-SIAM Symposium on Discrete Algorithm, SODA 2006, pp. 117\u2013123 (2006)","DOI":"10.1145\/1109557.1109571"},{"key":"9_CR45","unstructured":"Keiren, J.J.A.: Advanced Reduction Techniques for Model Checking. PhD thesis, Eindhoven University of Technology (2013)"},{"key":"9_CR46","unstructured":"Keiren, J.J.A.: Benchmarks for parity games. CoRR, abs\/1407.3121 (2014)"},{"key":"9_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-642-19237-1_12","volume-title":"Hardware and Software: Verification and Testing","author":"J.J.A. Keiren","year":"2011","unstructured":"Keiren, J.J.A., Willemse, T.A.C.: Bisimulation minimisations for Boolean equation systems. In: Namjoshi, K., Zeller, A., Ziv, A. (eds.) HVC 2009. LNCS, vol.\u00a06405, pp. 102\u2013116. Springer, Heidelberg (2011)"},{"key":"9_CR48","doi-asserted-by":"crossref","unstructured":"Koymans, C.P.J., Mulder, J.C.: A modular approach to protocol verification using process algebra. In: Applications of Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol.\u00a017, pp. 261\u2013306 (1990)","DOI":"10.1017\/CBO9780511608841.012"},{"key":"9_CR49","unstructured":"Lange, M.: Solving parity games by a reduction to SAT. In: Proc. of the Workshop on Games in Design and Verification, GDV 2005 (2005)"},{"key":"9_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/3-540-56496-9_4","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1993","unstructured":"Larsen, K.G.: Efficient local correctness checking. In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol.\u00a0663, pp. 30\u201343. Springer, Heidelberg (1993)"},{"key":"9_CR51","unstructured":"Luttik, S.P.: Description and formal specification of the link layer of P1394. In: Workshop on Applied Formal Methods in System Design, pp. 43\u201356 (1997)"},{"key":"9_CR52","unstructured":"Maarup, T.: Hex - everything you always wanted to know about hex but were afraid to ask. Master\u2019s thesis (2005)"},{"key":"9_CR53","unstructured":"Mader, A.: Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (1997)"},{"key":"9_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/3-540-36577-X_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R.: A generic on-the-fly solver for alternation-free Boolean equation systems. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 81\u201396. Springer, Heidelberg (2003)"},{"issue":"2","key":"9_CR55","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0168-0072(93)90036-D","volume":"65","author":"R. McNaughton","year":"1993","unstructured":"McNaughton, R.: Infinite games played on finite graphs. Annals of Pure and Applied Logic\u00a065(2), 149\u2013184 (1993)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2-3","key":"9_CR56","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1016\/0012-365X(83)90160-7","volume":"43","author":"R. Nowakowski","year":"1983","unstructured":"Nowakowski, R., Winkler, P.: Vertex-to-vertex pursuit in a graph. Discrete Mathematics\u00a043(2-3), 235\u2013239 (1983)","journal-title":"Discrete Mathematics"},{"key":"9_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-540-45069-6_7","volume-title":"Computer Aided Verification","author":"J. Obdr\u017e\u00e1lek","year":"2003","unstructured":"Obdr\u017e\u00e1lek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 80\u201392. Springer, Heidelberg (2003)"},{"key":"9_CR58","unstructured":"Obdr\u017e\u00e1lek, J.: Algorithmic Analysis of Parity Games. PhD thesis, Laboritory for Foundations of Computer Science, School of Informatics, University of Edinburgh (2006)"},{"issue":"1","key":"9_CR59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlap.2006.08.007","volume":"71","author":"J. Pang","year":"2007","unstructured":"Pang, J., Fokkink, W.J., Hofman, R., Veldema, R.: Model checking a cache coherence protocol of a Java DSM implementation. The Journal of Logic and Algebraic Programming\u00a071(1), 1\u201343 (2007)","journal-title":"The Journal of Logic and Algebraic Programming"},{"key":"9_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-24732-6_2","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2004","unstructured":"Pel\u00e1nek, R.: Typical structural properties of state spaces. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol.\u00a02989, pp. 5\u201322. Springer, Heidelberg (2004)"},{"key":"9_CR61","unstructured":"Pel\u00e1nek, R.: Web portal for benchmarking explicit model checkers. Technical Report FIMU-RS-2006-03, Faculty of Informatics Masaryk University Brno (2006)"},{"key":"9_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-73370-6_17","volume-title":"Model Checking Software","author":"R. Pel\u00e1nek","year":"2007","unstructured":"Pel\u00e1nek, R.: BEEM: benchmarks for explicit model checkers. In: Bo\u0161na\u010dki, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol.\u00a04595, pp. 263\u2013267. Springer, Heidelberg (2007)"},{"key":"9_CR63","unstructured":"Quilliot, A.: Jeux et pointes fixes sur les graphes. PhD thesis, Universit\u00e9 de Paris VI (1978)"},{"issue":"3","key":"9_CR64","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/0196-6774(86)90023-4","volume":"7","author":"N. Robertson","year":"1986","unstructured":"Robertson, N., Seymour, P.D.: Graph minors. II. algorithmic aspects of tree-width. Journal of Algorithms\u00a07(3), 309\u2013322 (1986)","journal-title":"Journal of Algorithms"},{"key":"9_CR65","unstructured":"Rose, B.: Othello: A Minute to Learn... A Lifetime to Master (2005)"},{"key":"9_CR66","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, pp. 319\u2013327. IEEE (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"9_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/978-3-540-77050-3_37","volume-title":"FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science","author":"S. Schewe","year":"2007","unstructured":"Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 449\u2013460. Springer, Heidelberg (2007)"},{"key":"9_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-540-87531-4_27","volume-title":"Computer Science Logic","author":"S. Schewe","year":"2008","unstructured":"Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 369\u2013384. Springer, Heidelberg (2008)"},{"key":"9_CR69","unstructured":"Schewe, S.: Synthesis of Distributed Systems. Phd thesis, Universit\u00e4t des Saarlandes (2008)"},{"key":"9_CR70","unstructured":"Siek, J.G., Lee, L.Q., Lumsdaine, A.: The Boost Graph Library: User Guide and Reference Manual. Addison-Wesley (2002)"},{"issue":"1","key":"9_CR71","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/s100090050018","volume":"2","author":"M. Sighireanu","year":"1998","unstructured":"Sighireanu, M., Mateescu, R.: Verification of the link layer protocol of the IEEE-1394 serial bus (FireWire): An experiment with e-Lotos. STTT\u00a02(1), 68\u201388 (1998)","journal-title":"STTT"},{"key":"9_CR72","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0054166","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Stevens","year":"1998","unstructured":"Stevens, P., Stirling, C.: Practical model checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 85\u2013101. Springer, Heidelberg (1998)"},{"issue":"1","key":"9_CR73","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1093\/jigpal\/7.1.103","volume":"7","author":"C. Stirling","year":"1999","unstructured":"Stirling, C.: Bisimulation, modal logic and model checking games. Logic Journal of IGPL\u00a07(1), 103\u2013124 (1999)","journal-title":"Logic Journal of IGPL"},{"key":"9_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-78800-3_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y.K. Tsay","year":"2008","unstructured":"Tsay, Y.K., Chen, Y.F., Tsai, M.H., Chan, W.C., Luo, C.J.: GOAL extended: Towards a research tool for omega automata and temporal logic. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 346\u2013350. Springer, Heidelberg (2008)"},{"issue":"2","key":"9_CR75","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.entcs.2008.11.011","volume":"220","author":"J.C. Pol van de","year":"2008","unstructured":"van de Pol, J.C., Weber, M.: A multi-core solver for parity games. Electronic Notes in Theoretical Computer Science\u00a0220(2), 19\u201334 (2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"7","key":"9_CR76","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/568014.379578","volume":"36","author":"R. Veldema","year":"2001","unstructured":"Veldema, R., Hofman, R.F.H., Bhoedjang, R.A.F., Jacobs, C.J.H., Bal, H.E.: Source-level global optimizations for fine-grain distributed shared memory systems. ACM SIGPLAN Notices\u00a036(7), 83\u201392 (2001)","journal-title":"ACM SIGPLAN Notices"},{"key":"9_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/3-540-58201-0_77","volume-title":"Automata, Languages, and Programming","author":"B. Vergauwen","year":"1994","unstructured":"Vergauwen, B., Lewi, J.: Efficient local correctness checking for single and alternating Boolean equation systems. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol.\u00a0820, pp. 304\u2013315. Springer, Heidelberg (1994)"},{"issue":"1-2","key":"9_CR78","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science\u00a0200(1-2), 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24644-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T19:53:24Z","timestamp":1748634804000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24644-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319246437","9783319246444"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24644-4_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"12 November 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}