{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:50:38Z","timestamp":1780116638562,"version":"3.54.0"},"publisher-location":"Cham","reference-count":125,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"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-10575-8_26","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"871-919","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":34,"title":["The mu-calculus and Model Checking"],"prefix":"10.1007","author":[{"given":"Julian","family":"Bradfield","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"issue":"2","key":"26_CR1","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1016\/j.jcss.2003.07.009","volume":"68","author":"L. Alfaro de","year":"2004","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374\u2013397 (2004)","journal-title":"J. Comput. Syst. Sci."},{"key":"26_CR2","first-page":"100","volume-title":"Int. Symp. on Foundations of Computer Science","author":"R. Alur","year":"1997","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. In: Int. Symp. on Foundations of Computer Science, pp.\u00a0100\u2013109. IEEE, Piscataway (1997)"},{"issue":"1","key":"26_CR3","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H. Andersen","year":"1994","unstructured":"Andersen, H.: Model checking boolean graphs. Theor. Comput. Sci. 126(1), 3\u201330 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR4","first-page":"398","volume-title":"Ann. Symp. on Logic in Computer Science","author":"H.R. Andersen","year":"1995","unstructured":"Andersen, H.R.: Partial model checking. In: Ann. Symp. on Logic in Computer Science, pp.\u00a0398\u2013407. IEEE, Piscataway (1995)"},{"key":"26_CR5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1023\/A:1004275029985","volume":"27","author":"H. Andr\u00e9ka","year":"1998","unstructured":"Andr\u00e9ka, H., van Benthem, J., Nem\u00e9ti, I.: Modal logics and bounded fragments of predicate logic. J. Philos. Log. 27, 217\u2013274 (1998)","journal-title":"J. Philos. Log."},{"key":"26_CR6","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1051\/ita:1999121","volume":"33","author":"A. Arnold","year":"1999","unstructured":"Arnold, A.: The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO Theor. Inform. Appl. 33, 329\u2013339 (1999)","journal-title":"RAIRO Theor. Inform. Appl."},{"key":"26_CR7","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(88)90029-4","volume":"29","author":"A. Arnold","year":"1988","unstructured":"Arnold, A., Crubille, P.: A linear time algorithm to solve fixpoint equations on transition systems. Inf. Process. Lett. 29, 57\u201366 (1988)","journal-title":"Inf. Process. Lett."},{"key":"26_CR8","volume-title":"Rudiments of \u03bc$\\mu$-Calculus","author":"A. Arnold","year":"2001","unstructured":"Arnold, A., Niwi\u0144ski, D.: Rudiments of \u03bc$\\mu$-Calculus. Elsevier, Amsterdam (2001)"},{"key":"26_CR9","first-page":"29","volume-title":"Logic and Automata, Texts in Logic and Games","author":"A. Arnold","year":"2007","unstructured":"Arnold, A., Walukiewicz, I.: Nondeterministic controllers of nondeterministic processes. In: Flum, J., Gr\u00e4del, E., Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games, vol.\u00a02, pp.\u00a029\u201352. Amsterdam University Press, Amsterdam (2007)"},{"key":"26_CR10","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/BFb0048939","volume-title":"Programming Languages and Their Definition\u2014Hans Bekic (1936\u20131982)","author":"H. Bekic","year":"1984","unstructured":"Bekic, H.: Definable operation in general algebras, and the theory of automata and flowcharts. In: Jones, C.B. (ed.) Programming Languages and Their Definition\u2014Hans Bekic (1936\u20131982). LNCS, vol.\u00a0177, pp.\u00a030\u201355. Springer, Heidelberg (1984)"},{"issue":"1","key":"26_CR11","first-page":"4:1","volume":"11","author":"M. Benedikt","year":"2009","unstructured":"Benedikt, M., Segoufin, L.: Regular tree languages definable in FO and in FOmod. Trans. Comput. Log. 11(1), 4:1\u20134:32 (2009)","journal-title":"Trans. Comput. Log."},{"issue":"2","key":"26_CR12","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1027358927272","volume":"75","author":"D. Berwanger","year":"2003","unstructured":"Berwanger, D.: Game logic is strong enough for parity games. Stud. Log. 75(2), 205\u2013219 (2003)","journal-title":"Stud. Log."},{"key":"26_CR13","doi-asserted-by":"crossref","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. Theor. Comput. Sci. 463, 2\u201325 (2012)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"26_CR14","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/s00224-006-1317-8","volume":"40","author":"D. Berwanger","year":"2007","unstructured":"Berwanger, D., Gr\u00e4del, E., Lenzi, G.: The variable hierarchy of the mu-calculus is strict. Theory Comput. Syst. 40(4), 437\u2013466 (2007)","journal-title":"Theory Comput. Syst."},{"issue":"23","key":"26_CR15","doi-asserted-by":"crossref","first-page":"928","DOI":"10.1016\/j.ipl.2012.08.021","volume":"112","author":"D. Berwanger","year":"2012","unstructured":"Berwanger, D., Serre, O.: Parity games on undirected graphs. Inf. Process. Lett. 112(23), 928\u2013932 (2012)","journal-title":"Inf. Process. Lett."},{"key":"26_CR16","first-page":"304","volume-title":"Ann. Symp. on Logic in Computer Science","author":"G. Bhat","year":"1996","unstructured":"Bhat, G., Cleaveland, R.: Efficient model checking via the equational \u03bc$\\mu$-calculus. In: Clarke, E.M. (ed.) Ann. Symp. on Logic in Computer Science, pp.\u00a0304\u2013312. IEEE, Piscataway (1996)"},{"issue":"2","key":"26_CR17","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/j.dam.2006.04.029","volume":"155","author":"H. Bj\u00f6rklund","year":"2007","unstructured":"Bj\u00f6rklund, H., Vorobyov, S.G.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Appl. Math. 155(2), 210\u2013229 (2007)","journal-title":"Discrete Appl. Math."},{"key":"26_CR18","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"R. Blackburn","year":"2001","unstructured":"Blackburn, R., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001)"},{"key":"26_CR19","volume-title":"Handbook of Model Checking","author":"R. Bloem","year":"2018","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"26_CR20","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1093\/logcom\/exh037","volume":"13","author":"A. Blumensath","year":"2005","unstructured":"Blumensath, A., Kreutzer, S.: An extension to Muchnik\u2019s theorem. J. Log. Comput. 13, 59\u201374 (2005)","journal-title":"J. Log. Comput."},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M., Segoufin, L., Straubing, H.: Piecewise testable tree languages. Log. Methods Comput. Sci. 8(3) (2012)","DOI":"10.2168\/LMCS-8(3:26)2012"},{"key":"26_CR22","first-page":"19","volume":"3","author":"M. Bojanczyk","year":"2012","unstructured":"Bojanczyk, M., Straubing, H., Walukiewicz, I.: Wreath products of forest algebras, with applications to tree logics. Log. Methods Comput. Sci. 3, 19 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"2\u20133","key":"26_CR23","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/j.tcs.2006.01.018","volume":"358","author":"M. Bojanczyk","year":"2006","unstructured":"Bojanczyk, M., Walukiewicz, I.: Characterizing EF and EX tree logics. Theor. Comput. Sci. 358(2\u20133), 255\u2013272 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR24","first-page":"107","volume-title":"Logic and Automata, Texts in Logic and Games","author":"M. Bojanczyk","year":"2007","unstructured":"Bojanczyk, M., Walukiewicz, I.: Forest algebras. In: Flum, J., Gr\u00e4del, E., Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games, vol.\u00a02, pp.\u00a0107\u2013132. Amsterdam University Press, Amsterdam (2007)"},{"key":"26_CR25","first-page":"11","volume":"3","author":"P.A. Bonatti","year":"2008","unstructured":"Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched mu-calculi. Log. Methods Comput. Sci. 3, 11 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"26_CR26","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/s10849-010-9127-4","volume":"20","author":"P. Bouyer","year":"2011","unstructured":"Bouyer, P., Cassez, F., Laroussinie, F.: Timed modal logics for real-time systems: specification, verification and control. J. Log. Lang. Inf. 20, 169\u2013203 (2011)","journal-title":"J. Log. Lang. Inf."},{"key":"26_CR27","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0304-3975(97)00217-X","volume":"195","author":"J. Bradfield","year":"1997","unstructured":"Bradfield, J.: The modal mu-calculus alternation hierarchy is strict. Theor. Comput. Sci. 195, 133\u2013153 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR28","first-page":"721","volume-title":"The Handbook of Modal Logic","author":"J. Bradfield","year":"2006","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) The Handbook of Modal Logic, pp.\u00a0721\u2013756. Elsevier, Amsterdam (2006)"},{"key":"26_CR29","first-page":"120","volume-title":"Ann. Symp. on Logic in Computer Science","author":"C. Broadbent","year":"2010","unstructured":"Broadbent, C., Carayol, A., Ong, L., Serre, O.: Recursion schemes and logical reflection. In: Ann. Symp. on Logic in Computer Science, pp.\u00a0120\u2013129. IEEE, Piscataway (2010)"},{"key":"26_CR30","series-title":"LNCS","first-page":"112","volume-title":"Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science","author":"A. Carayol","year":"2003","unstructured":"Carayol, A., W\u00f6hrle, S.: The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a02914, pp.\u00a0112\u2013124. Springer, Heidelberg (2003)"},{"key":"26_CR31","volume-title":"Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, M.: An O(n2)${O}(n^{2})$ time algorithm for alternating B\u00fcchi games. In: Indyk, P. (ed.) Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA). SIAM, Philadelphia (2012)"},{"key":"26_CR32","first-page":"3","volume-title":"Summaries of the Summer Institute of Symbolic Logic","author":"A. Church","year":"1957","unstructured":"Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol.\u00a0I, pp.\u00a03\u201350. Cornell University, Ithaca (1957)"},{"key":"26_CR33","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Steffen, B.: A linear model checking algorithm for the alternation-free modal \u03bc$\\mu$-caluclus. Form. Methods Syst. Des. 2, 121\u2013147 (1993)","journal-title":"Form. Methods Syst. Des."},{"key":"26_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/978-3-642-02930-1_13","volume-title":"International Colloquium on Automata, Languages and Programming","author":"T. Colcombet","year":"2009","unstructured":"Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled B\u00fcchi automata. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) International Colloquium on Automata, Languages and Programming. LNCS, vol.\u00a05556, pp.\u00a0151\u2013162. Springer, Heidelberg (2009)"},{"issue":"2","key":"26_CR35","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0890-5401(92)90048-K","volume":"96","author":"A. Condon","year":"1992","unstructured":"Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203\u2013224 (1992)","journal-title":"Inf. Comput."},{"issue":"1","key":"26_CR36","doi-asserted-by":"crossref","first-page":"310","DOI":"10.2307\/2586539","volume":"65","author":"G. D\u2019Agostino","year":"2000","unstructured":"D\u2019Agostino, G., Hollenberg, M.: Logical questions concerning the mu-calculus: interpolation, Lyndon and \u0141o\u015b-Tarski. J. Symb. Log. 65(1), 310\u2013332 (2000)","journal-title":"J. Symb. Log."},{"issue":"3","key":"26_CR37","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1093\/logcom\/exs028","volume":"23","author":"G. D\u2019Agostino","year":"2013","unstructured":"D\u2019Agostino, G., Lenzi, G.: On modal mu-calculus over reflexive symmetric graphs. J. Log. Comput. 23(3), 445\u2013455 (2013)","journal-title":"J. Log. Comput."},{"issue":"1","key":"26_CR38","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL\u2217 and ECTL\u2217 as fragments of the modal \u03bc$\\mu $-calculus. Theor. Comput. Sci. 126(1), 77\u201396 (1994)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"26_CR39","doi-asserted-by":"crossref","first-page":"282","DOI":"10.1145\/976706.976710","volume":"5","author":"A. Dawar","year":"2004","unstructured":"Dawar, A., Gr\u00e4del, E., Kreutzer, S.: Inflationary fixed points in modal logic. Trans. Comput. Log. 5(2), 282\u2013315 (2004)","journal-title":"Trans. Comput. Log."},{"key":"26_CR40","volume-title":"Finite Model Theory","author":"H.D. Ebbinghaus","year":"1999","unstructured":"Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1999)"},{"key":"26_CR41","volume-title":"Mathematical Logic","author":"H.D. Ebbinghaus","year":"1984","unstructured":"Ebbinghaus, H.D., Flum, J., Thomas, W.: Mathematical Logic. Springer, New York (1984)"},{"issue":"1\u20132","key":"26_CR42","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1016\/S0304-3975(00)00034-7","volume":"258","author":"E. Emerson","year":"2001","unstructured":"Emerson, E., Jutla, C., Sistla, A.: On model-checking for the mu-calculus and its fragments. Theor. Comput. Sci. 258(1\u20132), 491\u2013522 (2001)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR43","first-page":"995","volume-title":"Handbook of Theoretical Computer Science, vol.\u00a0B","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp.\u00a0995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"26_CR44","first-page":"328","volume-title":"Int. Symp. on Foundations of Computer Science","author":"E.A. Emerson","year":"1988","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: Int. Symp. on Foundations of Computer Science, pp.\u00a0328\u2013337. IEEE, Piscataway (1988)"},{"key":"26_CR45","first-page":"368","volume-title":"Int. Symp. on Foundations of Computer Science","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Int. Symp. on Foundations of Computer Science, pp.\u00a0368\u2013377. IEEE, Piscataway (1991)"},{"issue":"1","key":"26_CR46","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"E.A. Emerson","year":"1999","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132\u2013158 (1999)","journal-title":"SIAM J. Comput."},{"key":"26_CR47","first-page":"267","volume-title":"Ann. Symp. on Logic in Computer Science","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Lei, C.: Efficient model checking in fragments of propositional mu-calculus. In: Ann. Symp. on Logic in Computer Science, pp.\u00a0267\u2013278. IEEE, Piscataway (1986)"},{"key":"26_CR48","doi-asserted-by":"crossref","first-page":"696","DOI":"10.1007\/s00224-009-9201-y","volume":"47","author":"D. Fischer","year":"2010","unstructured":"Fischer, D., Gr\u00e4del, E., Kaiser, L.: Model checking games for the quantitative mu-calculus. Theory Comput. Syst. 47, 696\u2013719 (2010)","journal-title":"Theory Comput. Syst."},{"key":"26_CR49","first-page":"286","volume-title":"Annual Symp. on the Theory of Computing","author":"M. Fisher","year":"1977","unstructured":"Fisher, M., Ladner, R.: Propositional modal logic of programs. In: Hopcroft, J.E., Friedman, E.P., Harrison, M.A. (eds.) Annual Symp. on the Theory of Computing, pp.\u00a0286\u2013294. ACM, New York (1977)"},{"key":"26_CR50","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. Fisher","year":"1979","unstructured":"Fisher, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"26_CR51","first-page":"23","volume":"3","author":"O. Friedmann","year":"2011","unstructured":"Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. Log. Methods Comput. Sci. 3, 23 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"26_CR52","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1137\/1.9781611973082.19","volume-title":"Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"O. Friedmann","year":"2011","unstructured":"Friedmann, O., Hansen, T.D., Zwick, U.: A subexponential lower bound for the random facet algorithm for parity games. In: Randall, D. (ed.) Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.\u00a0202\u2013216. SIAM, Philadelphia (2011)"},{"key":"26_CR53","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-642-22119-4_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX)","author":"O. Friedmann","year":"2011","unstructured":"Friedmann, O., Lange, M.: The modal mu-calculus caught off guard. In: Br\u00fcnnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). LNCS, vol.\u00a06793, pp.\u00a0149\u2013163. Springer, Heidelberg (2011)"},{"key":"26_CR54","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a053\u201365. Springer, Heidelberg (2001)"},{"key":"26_CR55","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"850","DOI":"10.1007\/978-3-540-73420-8_73","volume-title":"International Colloquium on Automata, Languages and Programming","author":"H. Gimbert","year":"2007","unstructured":"Gimbert, H., Zielonka, W.: Perfect information stochastic priority games. In: Arge, L., Cachin, C., Jurdzinski, T., Tarlecki, A. (eds.) International Colloquium on Automata, Languages and Programming. LNCS, vol.\u00a04596, pp.\u00a0850\u2013861. Springer, Heidelberg (2007)"},{"issue":"1","key":"26_CR56","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1016\/S0304-3975(01)00151-7","volume":"288","author":"E. Gr\u00e4del","year":"2002","unstructured":"Gr\u00e4del, E.: Guarded fixed point logics and the monadic theory of countable trees. Theor. Comput. Sci. 288(1), 129\u2013152 (2002)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"26_CR57","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1145\/507382.507388","volume":"3","author":"E. Gr\u00e4del","year":"2002","unstructured":"Gr\u00e4del, E., Hirsch, C., Otto, M.: Back and forth between guarded and modal logics. Trans. Comput. Log. 3(3), 418\u2013463 (2002)","journal-title":"Trans. Comput. Log."},{"key":"26_CR58","volume-title":"Finite Model Theory and Its Applications","author":"E. Gr\u00e4del","year":"2007","unstructured":"Gr\u00e4del, E., Kolaitis, P., Libkin, L., Marx, M., Spencer, J., Vardi, M., Venema, Y., Weinstein, S.: Finite Model Theory and Its Applications. Springer, Heidelberg (2007)"},{"key":"26_CR59","volume-title":"Automata, Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games, vol.\u00a02500. Springer, Heidelberg (2002)"},{"key":"26_CR60","first-page":"45","volume-title":"Ann. Symp. on Logic in Computer Science","author":"E. Gr\u00e4del","year":"1999","unstructured":"Gr\u00e4del, E., Walukiewicz, I.: Guarded fixed point logic. In: Ann. Symp. on Logic in Computer Science, pp.\u00a045\u201355. IEEE, Piscataway (1999)"},{"key":"26_CR61","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/978-94-009-6259-0_10","volume-title":"Handbook of Philosophical Logic, Vol. II","author":"D. Harel","year":"1984","unstructured":"Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Vol. II, pp.\u00a0497\u2013604. Reidel, Dordrecht (1984)"},{"key":"26_CR62","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"issue":"2","key":"26_CR63","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193\u2013244 (1994)","journal-title":"Inf. Comput."},{"key":"26_CR64","first-page":"225","volume-title":"International Colloquium on Automata, Languages and Programming","author":"P. Hitchcock","year":"1973","unstructured":"Hitchcock, P., Park, D.: Induction rules and termination proofs. In: Nivat, M. (ed.) International Colloquium on Automata, Languages and Programming, pp.\u00a0225\u2013251 (1973)"},{"key":"26_CR65","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1287\/mnsc.12.5.359","volume":"12","author":"A. Hoffman","year":"1966","unstructured":"Hoffman, A., Karp, R.: On nonterminating stochastic games. Manag. Sci. 12, 359\u2013370 (1966)","journal-title":"Manag. Sci."},{"key":"26_CR66","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0539-5","volume-title":"Descriptive Complexity","author":"N. Immerman","year":"1999","unstructured":"Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)"},{"issue":"3\u20134","key":"26_CR67","doi-asserted-by":"crossref","first-page":"247","DOI":"10.3233\/FUN-2004-613-404","volume":"61","author":"D. Janin","year":"2004","unstructured":"Janin, D., Lenzi, G.: On the relationship between monadic and weak monadic second order logic on arbitrary trees, with applications to the mu-calculus. Fundam. Inform. 61(3\u20134), 247\u2013265 (2004)","journal-title":"Fundam. Inform."},{"key":"26_CR68","series-title":"LNCS","first-page":"552","volume-title":"International Symposium on Mathematical Foundations of Computer Science","author":"D. Janin","year":"1995","unstructured":"Janin, D., Walukiewicz, I.: Automata for the mu-calculus and related results. In: Wiedermann, J., H\u00e1jek, P. (eds.) International Symposium on Mathematical Foundations of Computer Science. LNCS, vol.\u00a0969, pp.\u00a0552\u2013562. Springer, Heidelberg (1995)"},{"key":"26_CR69","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/3-540-61604-7_60","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"D. Janin","year":"1996","unstructured":"Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In: Montanari, U., Sassone, V. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a01119, pp.\u00a0263\u2013277. Springer, Heidelberg (1996)"},{"issue":"3","key":"26_CR70","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\u2229co-UP. Inf. Process. Lett. 68(3), 119\u2013124 (1998)","journal-title":"Inf. Process. Lett."},{"key":"26_CR71","series-title":"LNCS","first-page":"290","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"M. Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a01770, pp.\u00a0290\u2013301. Springer, Heidelberg (2000)"},{"issue":"4","key":"26_CR72","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."},{"key":"26_CR73","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/3-540-45931-6_15","volume-title":"Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS)","author":"T. Knapik","year":"2002","unstructured":"Knapik, T., Niwinski, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol.\u00a02303, pp.\u00a0205\u2013222. Springer, Heidelberg (2002)"},{"key":"26_CR74","first-page":"416","volume-title":"Ann. ACM Symp. on Principles of Programming Languages","author":"N. Kobayashi","year":"2009","unstructured":"Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Shao, Z., Pierce, B.C. (eds.) Ann. ACM Symp. on Principles of Programming Languages, pp.\u00a0416\u2013428. ACM, New York (2009)"},{"key":"26_CR75","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. Theor. Comput. Sci. 27, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR76","volume-title":"Handbook of Model Checking","author":"O. Kupferman","year":"2018","unstructured":"Kupferman, O.: Automata theory and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"26_CR77","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07003-1","volume-title":"Elements of Finite Model Theory","author":"L. Libkin","year":"2004","unstructured":"Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)"},{"key":"26_CR78","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-58179-0_66","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"D.E. Long","year":"1994","unstructured":"Long, D.E., Browne, A., Clarke, E.M., Jha, S., Marrero, W.R.: An improved algorithm for the evaluation of fixpoint expressions. In: Dill, D.L. (ed.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0818, pp.\u00a0338\u2013350. Springer, Heidelberg (1994)"},{"issue":"6","key":"26_CR79","first-page":"109","volume":"32","author":"L.L. Maksimova","year":"1991","unstructured":"Maksimova, L.L.: Absence of interpolation and of Beth\u2019s property in temporal logics with \u201cthe next\u201d operation. Sib. Math. J. 32(6), 109\u2013113 (1991)","journal-title":"Sib. Math. J."},{"key":"26_CR80","doi-asserted-by":"crossref","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"D. Martin","year":"1975","unstructured":"Martin, D.: Borel determinacy. Ann. Math. 102, 363\u2013371 (1975)","journal-title":"Ann. Math."},{"key":"26_CR81","doi-asserted-by":"crossref","unstructured":"McIver, A., Morgan, C.: Results on the quantitative \u03bc$\\mu$-calculus qM\u03bc$\\mu$. Trans. Comput. Log. 8(1) (2007)","DOI":"10.1145\/1182613.1182616"},{"key":"26_CR82","volume-title":"Handbook of Model Checking","author":"K.L. McMillan","year":"2018","unstructured":"McMillan, K.L.: Interpolation and model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"26_CR83","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, 149\u2013184 (1993)","journal-title":"Ann. Pure Appl. Log."},{"key":"26_CR84","unstructured":"Mio, M.: Game semantics for probabilistic mu-calculi. Ph.D. thesis, University of Edinburgh (2012)"},{"key":"26_CR85","volume-title":"Elementary Induction on Abstract Structures","author":"Y. Moschovakis","year":"1974","unstructured":"Moschovakis, Y.: Elementary Induction on Abstract Structures. North-Holland, Amsterdam (1974)"},{"key":"26_CR86","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/S0168-0072(98)00042-6","volume":"96","author":"L.S. Moss","year":"1999","unstructured":"Moss, L.S.: Coalgebraic logic. Ann. Pure Appl. Log. 96, 277\u2013317 (1999). Erratum published Ann. Pure Appl. Log. 99, 241\u2013259 (1999)","journal-title":"Ann. Pure Appl. Log."},{"key":"26_CR87","series-title":"LNCS","first-page":"157","volume-title":"Fifth Symposium on Computation Theory","author":"A.W. Mostowski","year":"1984","unstructured":"Mostowski, A.W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) Fifth Symposium on Computation Theory. LNCS, vol.\u00a0208, pp.\u00a0157\u2013168. Springer, Heidelberg (1984)"},{"key":"26_CR88","unstructured":"Mostowski, A.W.: Games with forbidden positions. Tech. Rep. 78, University of Gdansk (1991)"},{"key":"26_CR89","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D. Muller","year":"1987","unstructured":"Muller, D., Schupp, P.: Alternating automata on infinite trees. Theor. Comput. Sci. 54, 267\u2013276 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR90","first-page":"402","volume-title":"Ann. Symp. on Logic in Computer Science","author":"D. Niwi\u0144ski","year":"1988","unstructured":"Niwi\u0144ski, D.: Fixed points vs. infinite generation. In: Ann. Symp. on Logic in Computer Science, pp.\u00a0402\u2013409. IEEE, Piscataway (1988)"},{"key":"26_CR91","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"54","DOI":"10.1007\/978-3-540-74915-8_8","volume-title":"Intl. Workshop Computer Science Logic (CSL)","author":"J. Obdrz\u00e1lek","year":"2007","unstructured":"Obdrz\u00e1lek, J.: Clique-width and parity games. In: Duparc, J., Henzinger, T.A. (eds.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol.\u00a04646, pp.\u00a054\u201368. Springer, Heidelberg (2007)"},{"key":"26_CR92","first-page":"81","volume-title":"Ann. Symp. on Logic in Computer Science","author":"C.H.L. Ong","year":"2006","unstructured":"Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Ann. Symp. on Logic in Computer Science, pp.\u00a081\u201390. IEEE, Piscataway (2006)"},{"key":"26_CR93","first-page":"111","volume":"24","author":"R. Parikh","year":"1985","unstructured":"Parikh, R.: The logic of games and its applications. Ann. Discrete Math. 24, 111\u2013140 (1985)","journal-title":"Ann. Discrete Math."},{"key":"26_CR94","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D. Park","year":"1976","unstructured":"Park, D.: Finiteness is \u03bc$\\mu$-ineffable. Theor. Comput. Sci. 3, 173\u2013181 (1976)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"26_CR95","doi-asserted-by":"crossref","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. Methods Comput. Sci. 3(3), 1\u201321 (2007)","journal-title":"Log. Methods Comput. Sci."},{"key":"26_CR96","doi-asserted-by":"crossref","unstructured":"Place, T., Segoufin, L.: A decidable characterization of locally testable tree languages. Log. Methods Comput. Sci. 7(4) (2011)","DOI":"10.2168\/LMCS-7(4:3)2011"},{"key":"26_CR97","first-page":"421","volume-title":"Int. Symp. on Foundations of Computer Science","author":"V. Pratt","year":"1981","unstructured":"Pratt, V.: A decidable \u03bc$\\mu$-calculus: preliminary report. In: Int. Symp. on Foundations of Computer Science, pp.\u00a0421\u2013427. IEEE, Piscataway (1981)"},{"key":"26_CR98","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1\u201323 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"26_CR99","first-page":"1","volume-title":"Mathematical Logic and Foundations of Set Theory","author":"M.O. Rabin","year":"1970","unstructured":"Rabin, M.O.: Weakly definable relations and special automata. In: Mathematical Logic and Foundations of Set Theory, pp.\u00a01\u201323 (1970)"},{"key":"26_CR100","volume-title":"Int. Symp. on Foundations of Computer Science","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9$\\omega$-automata. In: Int. Symp. on Foundations of Computer Science. IEEE, Piscataway (1988)"},{"key":"26_CR101","first-page":"227","volume":"18","author":"A. Salwicki","year":"1970","unstructured":"Salwicki, A.: Formalized algorithmic languages. Bull. Acad. Pol. Sci., S\u00e9r. Sci. Math. Astron. Phys. 18, 227\u2013232 (1970)","journal-title":"Bull. Acad. Pol. Sci., S\u00e9r. Sci. Math. Astron. Phys."},{"key":"26_CR102","series-title":"LNCS","first-page":"449","volume-title":"Intl. Conf. on 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.) Intl. Conf. on Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a0485, pp.\u00a0449\u2013460. Springer, Heidelberg (2007)"},{"key":"26_CR103","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/978-3-540-87531-4_27","volume-title":"Intl. Workshop Computer Science Logic (CSL)","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.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol.\u00a05213, pp.\u00a0369\u2013384. Springer, Heidelberg (2008)"},{"key":"26_CR104","series-title":"Leibniz International Proceedings in Informatics","first-page":"661","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"S. Schewe","year":"2009","unstructured":"Schewe, S.: B\u00fcchi complementation made tight. In: Albers, S., Marion, J. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics, vol.\u00a03, pp.\u00a0661\u2013672. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, Dagstuhl (2009)"},{"key":"26_CR105","unstructured":"Scott, D., de Bakker, J.: A theory of programs. (1969). Unpublished notes, IBM, Vienna (1969)"},{"key":"26_CR106","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1137\/0219027","volume":"19","author":"H. Seidl","year":"1990","unstructured":"Seidl, H.: Deciding equivalence of finite tree automata. SIAM J. Comput. 19, 424\u2013437 (1990)","journal-title":"SIAM J. Comput."},{"issue":"6","key":"26_CR107","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0020-0190(96)00130-5","volume":"59","author":"H. Seidl","year":"1996","unstructured":"Seidl, H.: Fast and simple nested fixpoints. Inf. Process. Lett. 59(6), 303\u2013308 (1996)","journal-title":"Inf. Process. Lett."},{"key":"26_CR108","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1007\/3-540-48168-0_34","volume-title":"Intl. Workshop Computer Science Logic (CSL)","author":"H. Seidl","year":"1999","unstructured":"Seidl, H., Neumann, A.: On guarding nested fixpoints. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol.\u00a01683, pp.\u00a0484\u2013498. Springer, Heidelberg (1999)"},{"key":"26_CR109","series-title":"LNCS","first-page":"162","volume-title":"International Symposium on Mathematical Foundations of Computer Science","author":"A. Semenov","year":"1984","unstructured":"Semenov, A.: Decidability of monadic theories. In: Chytil, M., Koubek, V. (eds.) International Symposium on Mathematical Foundations of Computer Science. LNCS, vol.\u00a0176, pp.\u00a0162\u2013175. Springer, Heidelberg (1984)"},{"key":"26_CR110","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54, 121\u2013141 (1982)","journal-title":"Inf. Control"},{"key":"26_CR111","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-13345-3_43","volume-title":"International Colloquium on Automata, Languages and Programming","author":"R.S. Streett","year":"1984","unstructured":"Streett, R.S., Emerson, E.A.: The propositional mu-calculus is elementary. In: Paredaens, J. (ed.) International Colloquium on Automata, Languages and Programming. LNCS, vol.\u00a0172, pp.\u00a0465\u2013472. Springer, Heidelberg (1984)"},{"key":"26_CR112","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0890-5401(89)90031-X","volume":"81","author":"R.S. Streett","year":"1989","unstructured":"Streett, R.S., Emerson, E.A.: An automata theoretic procedure for the propositional mu-calculus. Inf. Comput. 81, 249\u2013264 (1989)","journal-title":"Inf. Comput."},{"key":"26_CR113","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of Formal Languages, vol. III","author":"W. Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. III, pp.\u00a0389\u2013455. Springer, Heidelberg (1997)"},{"key":"26_CR114","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/3-540-45657-0_5","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"W. Thomas","year":"2002","unstructured":"Thomas, W.: Infinite games and verification. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02404, pp.\u00a058\u201364. Springer, Heidelberg (2002)"},{"key":"26_CR115","series-title":"LNCS","first-page":"113","volume-title":"International Symposium on Mathematical Foundations of Computer Science","author":"W. Thomas","year":"2003","unstructured":"Thomas, W.: Constructing infinite graphs with a decidable MSO-theory. In: Rovan, B., Vojt\u00e1s, P. (eds.) International Symposium on Mathematical Foundations of Computer Science. LNCS, vol.\u00a02747, pp.\u00a0113\u2013124. Springer, Heidelberg (2003)"},{"key":"26_CR116","doi-asserted-by":"crossref","first-page":"635","DOI":"10.1007\/978-3-540-78127-1_35","volume-title":"Pillars of Computer Science, Lecture Notes in Computer Science","author":"W. Thomas","year":"2008","unstructured":"Thomas, W.: Church\u2019s problem and a tour through automata theory. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science, Lecture Notes in Computer Science, vol.\u00a04800, pp.\u00a0635\u2013655. Springer, Heidelberg (2008)"},{"key":"26_CR117","volume-title":"Modal Logic and Classical Logic","author":"J. Benthem van","year":"1983","unstructured":"van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis, Napoli (1983)"},{"key":"26_CR118","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"International Colloquium on Automata, Languages and Programming","author":"M. Vardi","year":"1998","unstructured":"Vardi, M.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) International Colloquium on Automata, Languages and Programming. LNCS, vol.\u00a01443, pp.\u00a0628\u2013641. Springer, Heidelberg (1998)"},{"key":"26_CR119","series-title":"LNCS","first-page":"12","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y.: The B\u00fcchi complementation saga. In: Thomas, W., Weil, P. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol.\u00a04393, pp.\u00a012\u201322. Springer, Heidelberg (2007)"},{"key":"26_CR120","first-page":"629","volume-title":"Logic and Automata, Texts in Logic and Games","author":"M.Y. Vardi","year":"2007","unstructured":"Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Flum, J., Gr\u00e4del, E., Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games, vol.\u00a02, pp.\u00a0629\u2013736. Amsterdam University Press, Amsterdam (2007)"},{"issue":"4","key":"26_CR121","doi-asserted-by":"crossref","first-page":"637","DOI":"10.1016\/j.ic.2005.06.003","volume":"204","author":"Y. Venema","year":"2006","unstructured":"Venema, Y.: Automata and fixed point logic: a coalgebraic perspective. Inf. Comput. 204(4), 637\u2013678 (2006)","journal-title":"Inf. Comput."},{"key":"26_CR122","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/10722167_18","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"J. V\u00f6ge","year":"2000","unstructured":"V\u00f6ge, J., Jurdzi\u0144ski, M.: A discrete strategy improvement algorithm for solving parity games (extended abstract). In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0202\u2013215. Springer, Heidelberg (2000)"},{"key":"26_CR123","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1999.2836","volume":"157","author":"I. Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Completeness of Kozen\u2019s axiomatisation of the propositional \u03bc$\\mu$-calculus. Inf. Comput. 157, 142\u2013182 (2000)","journal-title":"Inf. Comput."},{"issue":"1\u20132","key":"26_CR124","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1016\/S0304-3975(01)00185-2","volume":"257","author":"I. Walukiewicz","year":"2002","unstructured":"Walukiewicz, I.: Monadic second order logic on tree-like structures. Theor. Comput. Sci. 257(1\u20132), 311\u2013346 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"26_CR125","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, 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:26:04Z","timestamp":1751646364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":125,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_26","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}