{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T12:40:09Z","timestamp":1751719209609,"version":"3.41.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319948119"},{"type":"electronic","value":"9783319948126"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-94812-6_14","type":"book-chapter","created":{"date-parts":[[2018,6,28]],"date-time":"2018-06-28T22:12:26Z","timestamp":1530223946000},"page":"159-172","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Solving Parity Games: Explicit vs Symbolic"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Di Stasio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aniello","family":"Murano","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,6,29]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"R Iris Bahar","year":"1997","unstructured":"Iris Bahar, R., Frohm, E.A., Gaona, C.M., Hachtel, G.D., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Formal Methods Syst. Des. 10, 171\u2013206 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-00431-5_2","volume-title":"Model Checking and Artificial Intelligence","author":"M Bakera","year":"2009","unstructured":"Bakera, M., Edelkamp, S., Kissmann, P., Renner, C.D.: Solving $$\\mu $$-calculus parity games by symbolic planning. In: Peled, D.A., Wooldridge, M.J. (eds.) MoChArt 2008. LNCS (LNAI), vol. 5348, pp. 15\u201333. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00431-5_2"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. In: LICS 1990, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"522","DOI":"10.1007\/978-3-540-24749-4_46","volume-title":"STACS 2004","author":"D Bustan","year":"2004","unstructured":"Bustan, D., Kupferman, O., Vardi, M.Y.: A measured collapse of the modal $$\\mu $$-calculus alternation hierarchy. In: Diekert, V., Habib, M. (eds.) STACS 2004. LNCS, vol. 2996, pp. 522\u2013533. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24749-4_46"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC 2017, pp. 252\u2013263 (2017)","DOI":"10.1145\/3055399.3055409"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Cerm\u00e1k, P., Lomuscio, A., Murano, A.: Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In: AAAI 2015, pp. 2038\u20132044 (2015)","DOI":"10.1609\/aaai.v29i1.9444"},{"key":"14_CR8","unstructured":"Chatterjee, K., Dvor\u00e1k, W., Henzinger, M., Loitzenbauer, V.: Improved set-based symbolic algorithms for parity games. In: CSL 2017, pp. 18:1\u201318:21 (2017)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-319-40946-7_6","volume-title":"Implementation and Application of Automata","author":"A Di Stasio","year":"2016","unstructured":"Di Stasio, A., Murano, A., Perelli, G., Vardi, M.Y.: Solving parity games using an automata-based algorithm. In: Han, Y.-S., Salomaa, K. (eds.) CIAA 2016. LNCS, vol. 9705, pp. 64\u201376. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40946-7_6"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-46017-9_18","volume-title":"Model Checking Software","author":"C Eisner","year":"2002","unstructured":"Eisner, C., Peled, D.: Comparing symbolic and explicit model checking of a software system. In: Bo\u0161na\u010dki, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 230\u2013239. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46017-9_18"},{"key":"14_CR12","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"},{"issue":"3","key":"14_CR13","doi-asserted-by":"publisher","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":"14_CR14","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. 1770, pp. 290\u2013301. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46541-3_24"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M., Lazic, R.: Succinct progress measures for solving parity games. In: LICS 2017, pp. 1\u20139 (2017)","DOI":"10.1109\/LICS.2017.8005092"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"2","DOI":"10.4204\/EPTCS.159.2","volume":"159","author":"Gijs Kant","year":"2014","unstructured":"Kant, G., van de Pol, J.: Generating and solving symbolic parity games. In: GRAPHITE 2014, pp. 2\u201314 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-319-24644-4_9","volume-title":"Fundamentals of Software Engineering","author":"JJA Keiren","year":"2015","unstructured":"Keiren, J.J.A.: Benchmarks for parity games. In: Dastani, M., Sirjani, M. (eds.) FSEN 2015. LNCS, vol. 9392, pp. 127\u2013142. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24644-4_9"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: STOC 1998, pp. 224\u2013233 (1998)","DOI":"10.1145\/276698.276748"},{"issue":"2","key":"14_CR19","doi-asserted-by":"publisher","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":"14_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"KL McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Norwell (1993)"},{"key":"14_CR21","unstructured":"Tabakov, D.: Evaluation of explicit and symbolic automata-theoretic algorithm. Master\u2019s thesis, Rice University (2005)"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-89960-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T van Dijk","year":"2018","unstructured":"van Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 291\u2013308. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16"},{"issue":"2","key":"14_CR23","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":"14_CR24","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. 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":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94812-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,5]],"date-time":"2025-07-05T12:05:50Z","timestamp":1751717150000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-94812-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948119","9783319948126"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94812-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"29 June 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CIAA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Implementation and Application of Automata","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Charlottetown, PE","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 August 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"wia2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.smcs.upei.ca\/ciaa2018","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}