{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:33:37Z","timestamp":1742963617480,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_11","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"228-251","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Survey on\u00a0Satisfiability Checking for\u00a0the\u00a0$$\\mu $$-Calculus Through Tree Automata"],"prefix":"10.1007","author":[{"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Theory of Computing, STOC 2017, pp. 252\u2013263. ACM (2017)","DOI":"10.1145\/3055399.3055409"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: An O(n$${}^{{2}}$$) time algorithm for alternating b\u00fcchi games. In: SODA, pp. 1386\u20131399. SIAM (2012)","DOI":"10.1137\/1.9781611973099.109"},{"key":"11_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-17127-8_1","volume-title":"Foundations of Software Science and Computation Structures","author":"T Colcombet","year":"2019","unstructured":"Colcombet, T., Fijalkow, N.: Universal graphs and good for games automata: new tools for infinite duration games. In: Boja\u0144czyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 1\u201326. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17127-8_1"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Czerwinski, W., Daviaud, L., Fijalkow, N., Jurdzinski, M., Lazic, R., Parys, P.: Universal trees grow inside separating automata: Quasi-polynomial lower bounds for parity games. In: SODA, pp. 2333\u20132349. SIAM (2019)","DOI":"10.1137\/1.9781611975482.142"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"EA Emerson","year":"1999","unstructured":"Emerson, E.A., Jutla, C.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132\u2013158 (1999)","journal-title":"SIAM J. Comput."},{"key":"11_CR6","unstructured":"Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: LICS, pp. 267\u2013278. IEEE Computer Society (1986)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-662-54577-5_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Esparza","year":"2017","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Raskin, J.-F., Sickert, S.: From LTL and limit-deterministic B\u00fcchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 426\u2013442. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25"},{"key":"11_CR8","doi-asserted-by":"publisher","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 $$\\mu $$-calculus. J. Appl. Non-Class. Log. 23, 353\u2013371 (2013)","journal-title":"J. Appl. Non-Class. Log."},{"key":"11_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-9(4:5)2013","volume":"9","author":"O Friedmann","year":"2013","unstructured":"Friedmann, O., Latte, M., Lange, M.: Satisfiability games for branching-time logics. Log. Methods Comput. Sci. 9, 1\u201336 (2013)","journal-title":"Log. Methods Comput. Sci."},{"key":"11_CR10","unstructured":"Hausmann, D.: Satisfiability checking for the coalgebraic $$\\mu $$-calculus. Ph.D. thesis, University of Erlangen-Nuremberg, Germany (2018). https:\/\/opus4.kobv.de\/opus4-fau\/frontdoor\/index\/index\/docId\/9932"},{"key":"11_CR11","unstructured":"Hausmann, D., Piterman, N.: A survey on satisfiability checking for the $$\\mu $$-calculus through tree automata. CoRR abs\/2207.00517 (2022). https:\/\/arxiv.org\/abs\/2207.00517"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-319-89963-3_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Hausmann","year":"2018","unstructured":"Hausmann, D., Schr\u00f6der, L., Deifel, H.-P.: Permutation games for the weakly aconjunctive $$\\mu $$-calculus. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 361\u2013378. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_21"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/11874683_26","volume-title":"Computer Science Logic","author":"TA Henzinger","year":"2006","unstructured":"Henzinger, T.A., Piterman, N.: Solving games without determinization. In: \u00c9sik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 395\u2013410. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11874683_26"},{"key":"11_CR14","unstructured":"Jurdzinski, M., Morvan, R.: A universal attractor decomposition algorithm for parity games. CoRR abs\/2001.04333 (2020). https:\/\/arxiv.org\/abs\/2001.04333"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/3-540-45315-6_18","volume-title":"Foundations of Software Science and Computation Structures","author":"V King","year":"2001","unstructured":"King, V., Kupferman, O., Vardi, M.Y.: On the complexity of parity word automata. In: Honsell, F., Miculan, M. (eds.) FoSSaCS 2001. LNCS, vol. 2030, pp. 276\u2013286. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45315-6_18"},{"key":"11_CR16","doi-asserted-by":"publisher","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. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR17","unstructured":"Kupke, C., Marti, J., Venema, Y.: Succinct graph representations of $$\\mu $$-calculus formulas. In: Computer Science Logic, CSL 2022. LIPIcs, vol. 216, pp. 29:1\u201329:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Lange, M., Stirling, C.: Focus games for satisfiability and completeness of temporal logic. In: Logic in Computer Science, LICS 2001, pp. 357\u2013365. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932511"},{"key":"11_CR19","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on $$\\omega $$-words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR20","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, pp. 422\u2013427. IEEE Computer Society (1988)","DOI":"10.1109\/LICS.1988.5139"},{"key":"11_CR21","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"DE Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theor. Comput. Sci. 54, 267\u2013276 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N Piterman","year":"2007","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Meth. Comput. Sci. 3, 1\u201321 (2007)","journal-title":"Log. Meth. Comput. Sci."},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega-automata. In: Foundations of Computer Science, FOCS 1988, pp. 319\u2013327. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/978-3-642-00596-1_13","volume-title":"Foundations of Software Science and Computational Structures","author":"S Schewe","year":"2009","unstructured":"Schewe, S.: Tighter bounds for the determinisation of B\u00fcchi automata. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 167\u2013181. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00596-1_13"},{"key":"11_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"486","DOI":"10.1007\/978-3-662-44522-8_41","volume-title":"Mathematical Foundations of Computer Science 2014","author":"S Schewe","year":"2014","unstructured":"Schewe, S., Varghese, T.: Determinising parity automata. In: Csuhaj-Varj\u00fa, E., Dietzfelbinger, M., \u00c9sik, Z. (eds.) MFCS 2014. LNCS, vol. 8634, pp. 486\u2013498. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44522-8_41"},{"issue":"3","key":"11_CR26","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"RS Streett","year":"1989","unstructured":"Streett, R.S., Emerson, E.A.: An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput. 81(3), 249\u2013264 (1989)","journal-title":"Inf. Comput."},{"key":"11_CR27","doi-asserted-by":"publisher","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. Belgian Math. Soc. Simon Stevin 8, 359\u2013391 (2001)","journal-title":"Bull. Belgian Math. Soc. Simon Stevin"}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:54:36Z","timestamp":1728615276000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}