{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:26:21Z","timestamp":1740108381033,"version":"3.37.3"},"reference-count":56,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,8,4]],"date-time":"2017-08-04T00:00:00Z","timestamp":1501804800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Open University of The Netherlands"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,8]]},"DOI":"10.1007\/s00236-017-0301-x","type":"journal-article","created":{"date-parts":[[2017,8,4]],"date-time":"2017-08-04T06:27:59Z","timestamp":1501828079000},"page":"401-444","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Parity game reductions"],"prefix":"10.1007","volume":"55","author":[{"given":"Sjoerd","family":"Cranen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5772-9527","authenticated-orcid":false,"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3049-7962","authenticated-orcid":false,"given":"Tim A. C.","family":"Willemse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,8,4]]},"reference":[{"issue":"1","key":"301_CR1","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1016\/S0304-3975(02)00442-5","volume":"303","author":"A Arnold","year":"2003","unstructured":"Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theor. Comput. Sci. 303(1), 7\u201334 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"301_CR2","series-title":"Volume 2 of Texts in Logic and Games","first-page":"29","volume-title":"Logic and Automata","author":"A Arnold","year":"2008","unstructured":"Arnold, A., Walukiewicz, I.: Nondeterministic controllers of nondeterministic processes. Logic and Automata. Volume 2 of Texts in Logic and Games, pp. 29\u201352. Amsterdam University Press, Amsterdam (2008)"},{"issue":"3","key":"301_CR3","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/0020-0190(96)00034-8","volume":"58","author":"T Basten","year":"1996","unstructured":"Basten, T.: Branching bisimilarity is an equivalence indeed!. Inf. Proc. Let. 58(3), 141\u2013147 (1996)","journal-title":"Inf. Proc. Let."},{"key":"301_CR4","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-009-6259-0_4","volume-title":"Handbook of Philosophical Logic volume\u00a0II,","author":"J Benthem van","year":"1984","unstructured":"van Benthem, J.: Correspondence theory. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic volume\u00a0II, pp. 167\u2013248. Springer, Dordrecht (1984)"},{"key":"301_CR5","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund, H., Sandberg, S., Vorobyov, S.G.: A discrete subexponential algorithm for parity games. In: Proceedings STACS\u201903 volume 2607 of LNCS, pp. 663\u2013674. Springer (2003)","DOI":"10.1007\/3-540-36494-3_58"},{"issue":"3","key":"301_CR6","doi-asserted-by":"crossref","first-page":"347","DOI":"10.1016\/j.tcs.2005.07.041","volume":"349","author":"H Bj\u00f6rklund","year":"2005","unstructured":"Bj\u00f6rklund, H., Vorobyov, S.G.: Combinatorial structure and randomized subexponential algorithms for infinite games. Theor. Comput. Sci. 349(3), 347\u2013360 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"301_CR7","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. TCS 59, 115\u2013131 (1988)","journal-title":"TCS"},{"key":"301_CR8","unstructured":"Bulychev, P.E., Konnov, I.V., Zakharov, V.A.: Computing (bi)simulation relations preserving CTL*-X for ordinary and fair kripke structures. Institute for System Programming, Russian Academy of Sciences, Mathematical Methods and Algorithms, 12 (2007)"},{"issue":"2","key":"301_CR9","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/635499.635502","volume":"4","author":"D Bustan","year":"2003","unstructured":"Bustan, D., Grumberg, O.: Simulation-based minimization. ACM Trans. Comput. Log. 4(2), 181\u2013206 (2003)","journal-title":"ACM Trans. Comput. Log."},{"key":"301_CR10","doi-asserted-by":"crossref","unstructured":"Clemente, L.: B\u00fcchi automata can have smaller quotients. In: ICALP\u201911, volume 6756 of Lecture Notes in Computer Science, pp. 258\u2013270. Springer (2011)","DOI":"10.1007\/978-3-642-22012-8_20"},{"key":"301_CR11","unstructured":"Cranen, S.: Getting the point: obtaining and understanding fixpoints in model checking. PhD thesis, Eindhoven University of Technology. Eindhoven (2015)"},{"issue":"4","key":"301_CR12","doi-asserted-by":"crossref","first-page":"29:1","DOI":"10.1145\/2740964","volume":"16","author":"S Cranen","year":"2015","unstructured":"Cranen, S., Gazda, M., Wesselink, J.W., Willemse, T.A.C.: Abstraction in fixpoint logic. ACM Trans. Comput. Logic 16(4), 29:1\u201329:39 (2015)","journal-title":"ACM Trans. Comput. Logic"},{"key":"301_CR13","doi-asserted-by":"crossref","unstructured":"Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: Stuttering mostly speeds up solving parity games. In: Proceedings of NFM\u201911 volume 6617 of LNCS, pp. 207\u2013221. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_16"},{"key":"301_CR14","doi-asserted-by":"crossref","unstructured":"Cranen, S., Keiren, J.J.A., Willemse., T.A.C.: A cure for stuttering parity games. In: Proceedings of ICTAC\u201912, volume 7521 of LNCS, pp. 198\u2013212. Springer (2012)","DOI":"10.1007\/978-3-642-32943-2_16"},{"key":"301_CR15","unstructured":"Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: Parity game reductions (2016), arXiv:1603.06422"},{"key":"301_CR16","doi-asserted-by":"publisher","unstructured":"de Frutos Escrig, D., Keiren, J.J.A., Willemse, T.A.C.: Branching bisimulation games. In: Proceedings of FORTE\u201916, (2016). doi: 10.1007\/978-3-319-39570-8_10","DOI":"10.1007\/978-3-319-39570-8_10"},{"key":"301_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of FOCS\u201991. IEEE Computer Society, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"301_CR18","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S., Sistla, A.P.: On model checking for the $${\\rm \\mu }$$ \u03bc -calculus and its fragments. Theor. Comput. Sci. 258(1\u20132), 491\u2013522 (2001)","DOI":"10.1016\/S0304-3975(00)00034-7"},{"key":"301_CR19","unstructured":"Etessami, K., Wilke, Th., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for b\u00fcchi automata. SIAM J. Comput. 34(5), 1159\u20131175 (2005)"},{"key":"301_CR20","doi-asserted-by":"crossref","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Proceedings of ATVA\u201909, volume 5799 of LNCS. Springer, pp. 182\u2013196 (2009)","DOI":"10.1007\/978-3-642-04761-9_15"},{"issue":"4","key":"301_CR21","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1080\/11663081.2013.861181","volume":"23","author":"O Friedmann","year":"2013","unstructured":"Friedmann, O., Lange, M.: Deciding the unguarded modal $${\\rm \\mu }$$ \u03bc -calculus. J. Appl. Non-Class. Log. 23(4), 353\u2013371 (2013)","journal-title":"J. Appl. Non-Class. Log."},{"key":"301_CR22","unstructured":"Fritz, C.: Simulation-Based Simplification of omega-Automata. PhD thesis, Christian-Albrechts-Universit\u00e4t zu Kiel, (2005)"},{"key":"301_CR23","doi-asserted-by":"crossref","unstructured":"Fritz, C., Wilke. T., Simulation relations for alternating parity automata and parity games. In: Proceedings of DLT\u201906, volume 4036 of LNCS, pp. 59\u201370. Springer (2006)","DOI":"10.1007\/11779148_7"},{"key":"301_CR24","doi-asserted-by":"crossref","unstructured":"Fritz, C., Wilke, Th.: State space reductions for alternating b\u00fcchi automata. In: Proceedings of FSTTCS\u201902, volume 2556 of LNCS, pp. 157\u2013168. Springer (2002)","DOI":"10.1007\/3-540-36206-1_15"},{"key":"301_CR25","doi-asserted-by":"crossref","unstructured":"Gazda, M.W., Willemse, T.A.C.: Consistent consequence for boolean equation systems. In: Proceedings of SOFSEM\u201912, volume 7147 of LNCS, pp. 277\u2013288. Springer (2012)","DOI":"10.1007\/978-3-642-27660-6_23"},{"key":"301_CR26","doi-asserted-by":"crossref","unstructured":"Gazda, M.W., Willemse, T.A.C.: On parity game preorders and the logic of matching plays. In: Proceedings of SOFSEM\u201916, volume 9587 of LNCS, pp. 277\u2013289. Springer (2016)","DOI":"10.1007\/978-3-662-49192-8_23"},{"key":"301_CR27","doi-asserted-by":"crossref","unstructured":"Glabbeek, van R.J.: The linear time\u2014branching time spectrum. In: Proceedings of CONCUR \u201990, volume 458 of LNCS, pp. 278\u2013297. Springer (1990)","DOI":"10.1007\/BFb0039066"},{"key":"301_CR28","doi-asserted-by":"crossref","unstructured":"Glabbeek, van R.J.: The linear time\u2014branching time spectrum II. In: Proceedings of CONCUR\u201993, volume 715 of LNCS, pages 66\u201381. Springer (1993)","DOI":"10.1007\/3-540-57208-2_6"},{"key":"301_CR29","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T., (eds) Automata Logics, and Infinite Games, volume 2500 of LNCS. Springer (2002)","DOI":"10.1007\/3-540-36387-4"},{"key":"301_CR30","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Vaandrager, F.W.: An efficient algorithm for branching bisimulation and stuttering equivalence. In: Proceedings of ICALP\u201990, volume 443 of LNCS, pp. 626\u2013638. Springer (1990)","DOI":"10.1007\/BFb0032063"},{"key":"301_CR31","doi-asserted-by":"publisher","unstructured":"Groote, J.F., Jansen, D.N., Keiren, J.J.A., Wijs, A.: An O(mlogn) algorithm for computing stuttering equivalence and branching bisimulation. ACM Trans. Comput. Log. 18(2), 13:1\u20133:34 (2017). doi: 10.1145\/3060140","DOI":"10.1145\/3060140"},{"key":"301_CR32","doi-asserted-by":"crossref","unstructured":"Huth, M., Kuo, J.H.-P., Piterman, N.: Fatal attractors in parity games. In: Proceedings of FOSSACS\u201913, volume 7794 of LNCS, pp. 34\u201349. Springer (2013)","DOI":"10.1007\/978-3-642-37075-5_3"},{"key":"301_CR33","doi-asserted-by":"crossref","unstructured":"Huth, M., Kuo, J.H.-P., Piterman, N., Static analysis of parity games: alternating reachability under parity. In: Semantics, Logics, and Calculi, volume 9560 of LNCS, pp. 159\u2013177. Springer (2016)","DOI":"10.1007\/978-3-319-27810-0_8"},{"key":"301_CR34","unstructured":"Janin, D.: A contribution to formal methods: games, logic and automata, December (2005). Habilitation thesis"},{"issue":"3","key":"301_CR35","doi-asserted-by":"crossref","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 $$\\cap $$ \u2229 co-UP. Inf. Proc. Let. 68(3), 119\u2013124 (1998)","journal-title":"Inf. Proc. Let."},{"key":"301_CR36","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Proceedings of STACS\u201900, volume 1770 of LNCS, pp. 290\u2013301. Springer (2000)","DOI":"10.1007\/3-540-46541-3_24"},{"key":"301_CR37","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., Paterson, M., Zwick, U.: A Deterministic Subexponential Algorithm for Solving Parity Games. In: Proceedings of SODA\u201906, pp. 117\u2013123. ACM\/SIAM (2006)","DOI":"10.1145\/1109557.1109571"},{"key":"301_CR38","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Kemna, T., Zapreev, I.S., Jansen, D.N.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Proceedings of TACAS\u201907 volume 4424 of LNCS, pp. 76\u201392. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_9"},{"key":"301_CR39","unstructured":"Keiren, J.J.A.: Advanced Reduction Techniques for Model Checking. PhD thesis, Eindhoven University of Technology, (2013)"},{"key":"301_CR40","doi-asserted-by":"crossref","unstructured":"Keiren, J.J.A.: Benchmarks for parity games. In: Proceedings of FSEN\u201915, volume 9392 of LNCS, pp. 126\u2013142. Springer (2015)","DOI":"10.1007\/978-3-319-24644-4_9"},{"key":"301_CR41","doi-asserted-by":"crossref","unstructured":"Keiren, J.J.A., Wesselink, J.W., Willemse, T.A.C.: Liveness analysis for parameterised Boolean equation systems. In: Proceedings of ATVA\u201914 volume 8837 of LNCS, pp. 219\u2013234. Springer (2014)","DOI":"10.1007\/978-3-319-11936-6_16"},{"key":"301_CR42","doi-asserted-by":"crossref","unstructured":"Keiren, J.J.A., Willemse, T.A.C.: Bisimulation Minimisations for Boolean Equation Systems. In: Proceedings of HVC\u201909, volume 6405 of LNCS. Springer (2011)","DOI":"10.1007\/978-3-642-19237-1_12"},{"key":"301_CR43","doi-asserted-by":"crossref","unstructured":"Mayr, R., Clemente, L.: Advanced automata minimization. In: POPL\u201913, pp. 63\u201374. ACM (2013)","DOI":"10.1145\/2429069.2429079"},{"issue":"2","key":"301_CR44","doi-asserted-by":"crossref","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. Ann. Pure Appl. Log. 65(2), 149\u2013184 (1993)","journal-title":"Ann. Pure Appl. Log."},{"key":"301_CR45","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Proceedings of FSTTCS\u201997, volume 1346 of LNCS, pp. 284\u2013296. Springer (1997)","DOI":"10.1007\/BFb0058037"},{"key":"301_CR46","doi-asserted-by":"crossref","unstructured":"Orzan, S., Wesselink, J.W., Willemse, T.A.C.: Static analysis techniques for parameterised Boolean equation systems. In: Proceedings of TACAS\u201909, volume 5505 of LNCS, pp. 230\u2013245. Springer (2009)","DOI":"10.1007\/978-3-642-00768-2_22"},{"issue":"11\u201313","key":"301_CR47","doi-asserted-by":"crossref","first-page":"1338","DOI":"10.1016\/j.tcs.2009.11.001","volume":"411","author":"S Orzan","year":"2010","unstructured":"Orzan, S., Willemse, T.A.C.: Invariants for parameterised boolean equation systems. Theor. Comput. Sci. 411(11\u201313), 1338\u20131371 (2010)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"301_CR48","first-page":"324","volume":"8","author":"V Petersson","year":"2001","unstructured":"Petersson, V., Vorobyov, S.G.: A randomized subexponential algorithm for parity games. Nordic J. Comput. 8(3), 324\u2013345 (2001)","journal-title":"Nordic J. Comput."},{"key":"301_CR49","doi-asserted-by":"crossref","unstructured":"Schewe, S.: Solving parity games in big steps. In: Proceedings of FSTTCS\u201907, volume 4855 of LNCS, pp. 449\u2013460. Springer (2007)","DOI":"10.1007\/978-3-540-77050-3_37"},{"key":"301_CR50","doi-asserted-by":"crossref","unstructured":"Stevens, P., Stirling, C.: Practical model checking using games. In: Proceedings of TACAS\u201998, volume 1384 of LNCS, pp. 85\u2013101. Springer (1998)","DOI":"10.1007\/BFb0054166"},{"issue":"1","key":"301_CR51","doi-asserted-by":"crossref","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. Log. J. IGPL 7(1), 103\u2013124 (1999)","journal-title":"Log. J. IGPL"},{"key":"301_CR52","doi-asserted-by":"crossref","unstructured":"Thomas, W.: On the Ehrenfeucht-Fra\u00efss\u00e9 game in theoretical computer science. In: Proceedings of TAPSOFT\u201993, volume 668 of LNCS, pp. 559\u2013568. Springer (1993)","DOI":"10.1007\/3-540-56610-4_89"},{"key":"301_CR53","doi-asserted-by":"crossref","unstructured":"V\u00f6ge, J., Jurdzi\u0144ski, M.: A discrete strategy improvement algorithm for solving parity games. In: Proceedings of CAV\u201900, volume 1855 of LNCS, pp. 202\u2013215. Springer (2000)","DOI":"10.1007\/10722167_18"},{"key":"301_CR54","doi-asserted-by":"crossref","unstructured":"Willemse, T.A.C., Consistent correlations for parameterised Boolean equation systems with applications in correctness proofs for manipulations. In: Proceedings of CONCUR\u201910, volume 6269 of LNCS, pp. 584\u2013598. Springer (2010)","DOI":"10.1007\/978-3-642-15375-4_40"},{"key":"301_CR55","doi-asserted-by":"crossref","unstructured":"Yin, Q., Fu, Y., He, C., Huang, M.,Tao, X.: Branching bisimilarity checking for PRS. In :Proceedings of ICALP\u201914, volume 8573 of LNCS, pp. 363\u2013374. Springer (2014)","DOI":"10.1007\/978-3-662-43951-7_31"},{"issue":"1\u20132","key":"301_CR56","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-017-0301-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0301-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-017-0301-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,1]],"date-time":"2019-10-01T21:16:29Z","timestamp":1569964589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-017-0301-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,8,4]]},"references-count":56,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,8]]}},"alternative-id":["301"],"URL":"https:\/\/doi.org\/10.1007\/s00236-017-0301-x","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2017,8,4]]}}}