{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T05:45:57Z","timestamp":1725860757958},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319409450"},{"type":"electronic","value":"9783319409467"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-40946-7_6","type":"book-chapter","created":{"date-parts":[[2016,7,5]],"date-time":"2016-07-05T11:52:20Z","timestamp":1467719540000},"page":"64-76","source":"Crossref","is-referenced-by-count":7,"title":["Solving Parity Games Using an Automata-Based Algorithm"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Di Stasio","sequence":"first","affiliation":[]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[]},{"given":"Giuseppe","family":"Perelli","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,7,6]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1016\/j.ic.2011.10.008","volume":"210","author":"B Aminof","year":"2012","unstructured":"Aminof, B., Kupferman, O., Murano, A.: Improved model checking of hierarchical systems. Inf. Comput. 210, 68\u201386 (2012)","journal-title":"Inf. Comput."},{"key":"6_CR2","first-page":"115","volume":"225","author":"A Antonik","year":"2009","unstructured":"Antonik, A., Charlton, N., Huth, M.: Polynomial-time under-approximation of winning regions in parity games. ENTCS 225, 115\u2013139 (2009)","journal-title":"ENTCS"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1007\/978-3-540-70918-3_17","volume-title":"STACS 2007","author":"D Berwanger","year":"2007","unstructured":"Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 188\u2013199. Springer, Heidelberg (2007)"},{"key":"6_CR4","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Generalized mean-payoff and energy games. In: FSTTCS 2010. LIPIcs, vol. 8, pp. 505\u2013516 (2010)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: An $$O(n^2)$$ time algorithm for alternating B\u00fcchi games. In: SODA 2012, pp. 1386\u20131399 (2012)","DOI":"10.1137\/1.9781611973099.109"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS 2005, pp. 178\u2013187 (2005)","DOI":"10.1109\/LICS.2005.26"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Jurdzinski, M., Henzinger, T.A.: Quantitative stochastic parity games. In: SODA 2004, pp. 121\u2013130 (2004)","DOI":"10.21236\/ADA603293"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) LP 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"6_CR9","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking (2002)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/978-3-540-73368-3_13","volume-title":"Computer Aided Verification","author":"L Alfaro de","year":"2007","unstructured":"de Alfaro, L., Faella, M.: An accelerated algorithm for 3-color parity games with an application to timed games. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 108\u2013120. Springer, Heidelberg (2007)"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.: Tree automata, $$\\mu $$ -calculus and determinacy. In: FOCS 1991, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"6_CR12","unstructured":"Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. University of Munich (2009)"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5799, pp. 182\u2013196. Springer, Heidelberg (2009)"},{"issue":"2","key":"6_CR14","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1016\/j.jcss.2011.05.004","volume":"78","author":"K Heljanko","year":"2012","unstructured":"Heljanko, K., Kein\u00e4nen, M., Lange, M., Niemel\u00e4, I.: Solving parity games by a reduction to SAT. J. Comput. Syst. Sci. 78(2), 430\u2013440 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"6_CR15","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M Jurdzinski","year":"1998","unstructured":"Jurdzinski, M.: Deciding the winner in parity games is in UP $$\\cap $$ co-Up. Inf. Process. Lett. 68(3), 119\u2013124 (1998)","journal-title":"Inf. Process. Lett."},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 1770, p. 290. Springer, Heidelberg (2000)"},{"issue":"4","key":"6_CR17","doi-asserted-by":"crossref","first-page":"1519","DOI":"10.1137\/070686652","volume":"38","author":"M Jurdzinski","year":"2008","unstructured":"Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519\u20131532 (2008)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"6_CR18","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional $$\\mu $$ -calculus. TCS 27(3), 333\u2013354 (1983)","journal-title":"TCS"},{"issue":"2","key":"6_CR19","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1006\/inco.2000.2893","volume":"164","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M., Wolper, P.: Module checking. Inf. Comput. 164(2), 322\u2013344 (2001)","journal-title":"Inf. Comput."},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: STOC, pp. 224\u2013233 (1998)","DOI":"10.1145\/276698.276748"},{"issue":"2","key":"6_CR21","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"601","DOI":"10.1007\/978-3-642-45221-5_40","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"F Mogavero","year":"2013","unstructured":"Mogavero, F., Murano, A., Sorrentino, L.: On promptness in parity games. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 601\u2013618. Springer, Heidelberg (2013)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: LICS 1988, pp. 422\u2013427 (1988)","DOI":"10.1109\/LICS.1988.5139"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 4855, pp. 449\u2013460. Springer, Heidelberg (2007)"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. 5213, pp. 369\u2013384. Springer, Heidelberg (2008)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-642-00596-1_1","volume-title":"Foundations of Software Science and Computational Structures","author":"W Thomas","year":"2009","unstructured":"Thomas, W.: Facets of synthesis: revisiting church\u2019s problem. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 1\u201314. Springer, Heidelberg (2009)"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/10722167_18","volume-title":"Computer Aided Verification","author":"J V\u00f6ge","year":"2000","unstructured":"V\u00f6ge, J., Jurdzi\u0144ski, M.: A discrete strategy improvement algorithm for solving parity games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202\u2013215. Springer, Heidelberg (2000)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Computer Aided Verification","author":"I Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62\u201374. Springer, Heidelberg (1996)"},{"issue":"2","key":"6_CR30","doi-asserted-by":"crossref","first-page":"359","DOI":"10.36045\/bbms\/1102714178","volume":"8","author":"T Wilke","year":"2001","unstructured":"Wilke, T.: Alternating tree automata, parity games, and modal $$\\mu $$ -calculus. Bull. Belg. Math. Soc. Simon Stevin 8(2), 359 (2001)","journal-title":"Bull. Belg. Math. Soc. Simon Stevin"},{"issue":"1\u20132","key":"6_CR31","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":["Lecture Notes in Computer Science","Implementation and Application of Automata"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40946-7_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,23]],"date-time":"2020-09-23T12:21:26Z","timestamp":1600863686000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40946-7_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319409450","9783319409467"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40946-7_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}