The mu-calculus and model checking. (English) Zbl 1392.68236
Clarke, Edmund M. (ed.) et al., Handbook of model checking. Cham: Springer (ISBN 978-3-319-10574-1/hbk; 978-3-319-10575-8/ebook). 871-919 (2018).
Summary: This chapter presents that part of the theory of the \(\mu\)-calculus that is relevant to the model-checking problem as broadly understood. The \(\mu\)-calculus is one of the most important logics in model checking. It is a logic with an exceptional balance between expressiveness and algorithmic properties.
For the entire collection see [Zbl 1390.68001].
For the entire collection see [Zbl 1390.68001].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 03B45 | Modal logic (including the logic of norms) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Software:
LTL2BAReferences:
| [1] | 1. de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. J. Comput. Syst. Sci. 68(2), 374-397 (2004) · Zbl 1093.91001 |
| [2] | 2. Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. In: Int. Symp. on Foundations of Computer Science, pp. 100-109. IEEE, Piscataway (1997) · Zbl 1326.68181 |
| [3] | 3. Andersen, H.: Model checking boolean graphs. Theor. Comput. Sci. 126(1), 3-30 (1994) · Zbl 0798.03017 |
| [4] | 4. Andersen, H.R.: Partial model checking. In: Ann. Symp. on Logic in Computer Science, pp. 398-407. IEEE, Piscataway (1995) |
| [5] | 5. Andréka, H., van Benthem, J., Neméti, I.: Modal logics and bounded fragments of predicate logic. J. Philos. Log. 27, 217-274 (1998) · Zbl 0919.03013 |
| [6] | 6. Arnold, A.: The mu-calculus alternation-depth hierarchy is strict on binary trees. RAIRO Theor. Inform. Appl. 33, 329-339 (1999) · Zbl 0945.68118 |
| [7] | 7. Arnold, A., Crubille, P.: A linear time algorithm to solve fixpoint equations on transition systems. Inf. Process. Lett. 29, 57-66 (1988) · Zbl 0663.68075 |
| [8] | 8. Arnold, A., Niwiński, D.: Rudiments of |
| [9] | 9. Arnold, A., Walukiewicz, I.: Nondeterministic controllers of nondeterministic processes. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games, vol. 2, pp. 29-52. Amsterdam University Press, Amsterdam (2007) · Zbl 1215.93082 |
| [10] | 10. Bekic, H.: Definable operation in general algebras, and the theory of automata and flowcharts. In: Jones, C.B. (ed.) Programming Languages and Their Definition—Hans Bekic (1936-1982). LNCS, vol. 177, pp. 30-55. Springer, Heidelberg (1984) |
| [11] | 11. Benedikt, M., Segoufin, L.: Regular tree languages definable in FO and in FO_{\(mod\)}. Trans. Comput. Log. 11(1), 4:1-4:32 (2009) · Zbl 1351.68134 |
| [12] | 12. Berwanger, D.: Game logic is strong enough for parity games. Stud. Log. 75(2), 205-219 (2003) · Zbl 1046.03017 |
| [13] | 13. Berwanger, D., Grädel, E., Kaiser, L., Rabinovich, R.: Entanglement and the complexity of directed graphs. Theor. Comput. Sci. 463, 2-25 (2012) · Zbl 1256.05086 |
| [14] | 14. Berwanger, D., Grädel, E., Lenzi, G.: The variable hierarchy of the mu-calculus is strict. Theory Comput. Syst. 40(4), 437-466 (2007) · Zbl 1121.68072 |
| [15] | 15. Berwanger, D., Serre, O.: Parity games on undirected graphs. Inf. Process. Lett. 112(23), 928-932 (2012) · Zbl 1248.68234 |
| [16] | 16. Bhat, G., Cleaveland, R.: Efficient model checking via the equational · Zbl 0991.68043 |
| [17] | 17. Björklund, H., Vorobyov, S.G.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. Discrete Appl. Math. 155(2), 210-229 (2007) · Zbl 1176.68087 |
| [18] | 18. Blackburn, R., de Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2001) · Zbl 0988.03006 |
| [19] | 19. 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) · Zbl 1392.68233 |
| [20] | 20. Blumensath, A., Kreutzer, S.: An extension to Muchnik’s theorem. J. Log. Comput. 13, 59-74 (2005) · Zbl 1067.03016 |
| [21] | 21. Bojanczyk, M., Segoufin, L., Straubing, H.: Piecewise testable tree languages. Log. Methods Comput. Sci. 8(3) (2012) · Zbl 1261.03126 |
| [22] | 22. Bojanczyk, M., Straubing, H., Walukiewicz, I.: Wreath products of forest algebras, with applications to tree logics. Log. Methods Comput. Sci. 3, 19 (2012) · Zbl 1258.03044 |
| [23] | 23. Bojanczyk, M., Walukiewicz, I.: Characterizing EF and EX tree logics. Theor. Comput. Sci. 358(2-3), 255-272 (2006) · Zbl 1097.03013 |
| [24] | 24. Bojanczyk, M., Walukiewicz, I.: Forest algebras. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games, vol. 2, pp. 107-132. Amsterdam University Press, Amsterdam (2007) · Zbl 1217.68123 |
| [25] | 25. Bonatti, P.A., Lutz, C., Murano, A., Vardi, M.Y.: The complexity of enriched mu-calculi. Log. Methods Comput. Sci. 3, 11 (2008) · Zbl 1151.03016 |
| [26] | 26. Bouyer, P., Cassez, F., Laroussinie, F.: Timed modal logics for real-time systems: specification, verification and control. J. Log. Lang. Inf. 20, 169-203 (2011) · Zbl 1216.68158 |
| [27] | 27. Bradfield, J.: The modal mu-calculus alternation hierarchy is strict. Theor. Comput. Sci. 195, 133-153 (1997) · Zbl 0915.03017 |
| [28] | 28. Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) The Handbook of Modal Logic, pp. 721-756. Elsevier, Amsterdam (2006) |
| [29] | 29. Broadbent, C., Carayol, A., Ong, L., Serre, O.: Recursion schemes and logical reflection. In: Ann. Symp. on Logic in Computer Science, pp. 120-129. IEEE, Piscataway (2010) |
| [30] | 30. Carayol, A., Wöhrle, 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. 2914, pp. 112-124. Springer, Heidelberg (2003) · Zbl 1205.03022 |
| [31] | 31. Chatterjee, K., Henzinger, M.: An |
| [32] | 32. Church, A.: Applications of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol. I, pp. 3-50. Cornell University, Ithaca (1957) · Zbl 0206.47902 |
| [33] | 33. Cleaveland, R., Steffen, B.: A linear model checking algorithm for the alternation-free modal · Zbl 0772.68038 |
| [34] | 34. Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled Büchi automata. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) International Colloquium on Automata, Languages and Programming. LNCS, vol. 5556, pp. 151-162. Springer, Heidelberg (2009) · Zbl 1248.68292 |
| [35] | 35. Condon, A.: The complexity of stochastic games. Inf. Comput. 96(2), 203-224 (1992) · Zbl 0756.90103 |
| [36] | 36. D’Agostino, G., Hollenberg, M.: Logical questions concerning the mu-calculus: interpolation, Lyndon and Łoś-Tarski. J. Symb. Log. 65(1), 310-332 (2000) · Zbl 0982.03011 |
| [37] | 37. D’Agostino, G., Lenzi, G.: On modal mu-calculus over reflexive symmetric graphs. J. Log. Comput. 23(3), 445-455 (2013) · Zbl 1276.03019 |
| [38] | 38. Dam, M.: CTL\^{}{∗} and ECTL\^{}{∗} as fragments of the modal · Zbl 0798.03018 |
| [39] | 39. Dawar, A., Grädel, E., Kreutzer, S.: Inflationary fixed points in modal logic. Trans. Comput. Log. 5(2), 282-315 (2004) · Zbl 1407.03031 |
| [40] | 40. Ebbinghaus, H.D., Flum, J.: Finite Model Theory. Springer, Heidelberg (1999) · Zbl 0932.03032 |
| [41] | 41. Ebbinghaus, H.D., Flum, J., Thomas, W.: Mathematical Logic. Springer, New York (1984) · Zbl 0556.03001 |
| [42] | 42. Emerson, E., Jutla, C., Sistla, A.: On model-checking for the mu-calculus and its fragments. Theor. Comput. Sci. 258(1-2), 491-522 (2001) · Zbl 0973.68120 |
| [43] | 43. Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995-1072. Elsevier, Amsterdam (1990) · Zbl 0900.03030 |
| [44] | 44. Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: Int. Symp. on Foundations of Computer Science, pp. 328-337. IEEE, Piscataway (1988) |
| [45] | 45. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Int. Symp. on Foundations of Computer Science, pp. 368-377. IEEE, Piscataway (1991) |
| [46] | 46. Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132-158 (1999) · Zbl 0937.68074 |
| [47] | 47. Emerson, E.A., Lei, C.: Efficient model checking in fragments of propositional mu-calculus. In: Ann. Symp. on Logic in Computer Science, pp. 267-278. IEEE, Piscataway (1986) |
| [48] | 48. Fischer, D., Grädel, E., Kaiser, L.: Model checking games for the quantitative mu-calculus. Theory Comput. Syst. 47, 696-719 (2010) · Zbl 1205.68243 |
| [49] | 49. 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. 286-294. ACM, New York (1977) |
| [50] | 50. Fisher, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 194-211 (1979) · Zbl 0408.03014 |
| [51] | 51. Friedmann, O.: An exponential lower bound for the latest deterministic strategy iteration algorithms. Log. Methods Comput. Sci. 3, 23 (2011) · Zbl 1237.68087 |
| [52] | 52. 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. 202-216. SIAM, Philadelphia (2011) · Zbl 1377.68091 |
| [53] | 53. Friedmann, O., Lange, M.: The modal mu-calculus caught off guard. In: Brünnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX). LNCS, vol. 6793, pp. 149-163. Springer, Heidelberg (2011) · Zbl 1333.03007 |
| [54] | 54. Gastin, P., Oddoux, D.: Fast LTL to Büchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2102, pp. 53-65. Springer, Heidelberg (2001) · Zbl 0991.68044 |
| [55] | 55. 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. 4596, pp. 850-861. Springer, Heidelberg (2007) · Zbl 1171.91315 |
| [56] | 56. Grädel, E.: Guarded fixed point logics and the monadic theory of countable trees. Theor. Comput. Sci. 288(1), 129-152 (2002) · Zbl 1061.03022 |
| [57] | 57. Grädel, E., Hirsch, C., Otto, M.: Back and forth between guarded and modal logics. Trans. Comput. Log. 3(3), 418-463 (2002) · Zbl 1365.03019 |
| [58] | 58. Grädel, E., Kolaitis, P., Libkin, L., Marx, M., Spencer, J., Vardi, M., Venema, Y., Weinstein, S.: Finite Model Theory and Its Applications. Springer, Heidelberg (2007) · Zbl 1133.03001 |
| [59] | 59. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games, vol. 2500. Springer, Heidelberg (2002) · Zbl 1011.00037 |
| [60] | 60. Grädel, E., Walukiewicz, I.: Guarded fixed point logic. In: Ann. Symp. on Logic in Computer Science, pp. 45-55. IEEE, Piscataway (1999) |
| [61] | 61. Harel, D.: Dynamic logic. In: Gabbay, D., Guenther, F. (eds.) Handbook of Philosophical Logic, Vol. II, pp. 497-604. Reidel, Dordrecht (1984) · Zbl 0875.03076 |
| [62] | 62. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000) · Zbl 0976.68108 |
| [63] | 63. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193-244 (1994) · Zbl 0806.68080 |
| [64] | 64. Hitchcock, P., Park, D.: Induction rules and termination proofs. In: Nivat, M. (ed.) International Colloquium on Automata, Languages and Programming, pp. 225-251 (1973) · Zbl 0387.68011 |
| [65] | 65. Hoffman, A., Karp, R.: On nonterminating stochastic games. Manag. Sci. 12, 359-370 (1966) · Zbl 0136.14303 |
| [66] | 66. Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999) · Zbl 0918.68031 |
| [67] | 67. 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-4), 247-265 (2004) · Zbl 1097.03010 |
| [68] | 68. Janin, D., Walukiewicz, I.: Automata for the mu-calculus and related results. In: Wiedermann, J., Hájek, P. (eds.) International Symposium on Mathematical Foundations of Computer Science. LNCS, vol. 969, pp. 552-562. Springer, Heidelberg (1995) · Zbl 1193.68163 |
| [69] | 69. 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. 1119, pp. 263-277. Springer, Heidelberg (1996) · Zbl 1514.68171 |
| [70] | 70. Jurdziński, M.: Deciding the winner in parity games is in UP∩co-UP. Inf. Process. Lett. 68(3), 119-124 (1998) · Zbl 1338.68109 |
| [71] | 71. Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 1770, pp. 290-301. Springer, Heidelberg (2000) · Zbl 0962.68111 |
| [72] | 72. Jurdzinski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. SIAM J. Comput. 38(4), 1519-1532 (2008) · Zbl 1173.91326 |
| [73] | 73. 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. 2303, pp. 205-222. Springer, Heidelberg (2002) · Zbl 1077.03508 |
| [74] | 74. 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. 416-428. ACM, New York (2009) · Zbl 1315.68099 |
| [75] | 75. Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333-354 (1983) · Zbl 0553.03007 |
| [76] | 76. 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) · Zbl 1392.68255 |
| [77] | 77. Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004) · Zbl 1060.03002 |
| [78] | 78. 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. 818, pp. 338-350. Springer, Heidelberg (1994) · Zbl 0901.68118 |
| [79] | 79. Maksimova, L.L.: Absence of interpolation and of Beth’s property in temporal logics with “the next” operation. Sib. Math. J. 32(6), 109-113 (1991) · Zbl 0751.03008 |
| [80] | 80. Martin, D.: Borel determinacy. Ann. Math. 102, 363-371 (1975) · Zbl 0336.02049 |
| [81] | 81. McIver, A., Morgan, C.: Results on the quantitative |
| [82] | 82. 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) · Zbl 1392.68260 |
| [83] | 83. McNaughton, R.: Infinite games played on finite graphs. Ann. Pure Appl. Log. 65, 149-184 (1993) · Zbl 0798.90151 |
| [84] | 84. Mio, M.: Game semantics for probabilistic mu-calculi. Ph.D. thesis, University of Edinburgh (2012) · Zbl 1238.68082 |
| [85] | 85. Moschovakis, Y.: Elementary Induction on Abstract Structures. North-Holland, Amsterdam (1974) · Zbl 0307.02003 |
| [86] | 86. Moss, L.S.: Coalgebraic logic. Ann. Pure Appl. Log. 96, 277-317 (1999). Erratum published Ann. Pure Appl. Log. 99, 241-259 (1999) · Zbl 0969.03026 |
| [87] | 87. 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. 208, pp. 157-168. Springer, Heidelberg (1984) · Zbl 0612.68046 |
| [88] | 88. Mostowski, A.W.: Games with forbidden positions. Tech. Rep. 78, University of Gdansk (1991) |
| [89] | 89. Muller, D., Schupp, P.: Alternating automata on infinite trees. Theor. Comput. Sci. 54, 267-276 (1987) · Zbl 0636.68108 |
| [90] | 90. Niwiński, D.: Fixed points vs. infinite generation. In: Ann. Symp. on Logic in Computer Science, pp. 402-409. IEEE, Piscataway (1988) |
| [91] | 91. Obdrzálek, J.: Clique-width and parity games. In: Duparc, J., Henzinger, T.A. (eds.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol. 4646, pp. 54-68. Springer, Heidelberg (2007) · Zbl 1179.68090 |
| [92] | 92. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Ann. Symp. on Logic in Computer Science, pp. 81-90. IEEE, Piscataway (2006) |
| [93] | 93. Parikh, R.: The logic of games and its applications. Ann. Discrete Math. 24, 111-140 (1985) · Zbl 0552.90110 |
| [94] | 94. Park, D.: Finiteness is · Zbl 0353.02027 |
| [95] | 95. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3), 1-21 (2007) · Zbl 1125.68067 |
| [96] | 96. Place, T., Segoufin, L.: A decidable characterization of locally testable tree languages. Log. Methods Comput. Sci. 7(4) (2011) · Zbl 1237.68119 |
| [97] | 97. Pratt, V.: A decidable |
| [98] | 98. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Am. Math. Soc. 141, 1-23 (1969) · Zbl 0221.02031 |
| [99] | 99. Rabin, M.O.: Weakly definable relations and special automata. In: Mathematical Logic and Foundations of Set Theory, pp. 1-23 (1970) · Zbl 0214.02208 |
| [100] | 100. Safra, S.: On the complexity of · Zbl 1273.91298 |
| [101] | 101. Salwicki, A.: Formalized algorithmic languages. Bull. Acad. Pol. Sci., Sér. Sci. Math. Astron. Phys. 18, 227-232 (1970) · Zbl 0198.02801 |
| [102] | 102. 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. 485, pp. 449-460. Springer, Heidelberg (2007) · Zbl 1135.68480 |
| [103] | 103. 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. 5213, pp. 369-384. Springer, Heidelberg (2008) · Zbl 1156.68478 |
| [104] | 104. Schewe, S.: Büchi complementation made tight. In: Albers, S., Marion, J. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics, vol. 3, pp. 661-672. Schloss Dagstuhl—Leibniz-Zentrum fuer Informatik, Dagstuhl (2009) · Zbl 1236.68176 |
| [105] | 105. Scott, D., de Bakker, J.: A theory of programs. (1969). Unpublished notes, IBM, Vienna (1969) |
| [106] | 106. Seidl, H.: Deciding equivalence of finite tree automata. SIAM J. Comput. 19, 424-437 (1990) · Zbl 0699.68075 |
| [107] | 107. Seidl, H.: Fast and simple nested fixpoints. Inf. Process. Lett. 59(6), 303-308 (1996) · Zbl 0900.68458 |
| [108] | 108. Seidl, H., Neumann, A.: On guarding nested fixpoints. In: Flum, J., Rodríguez-Artalejo, M. (eds.) Intl. Workshop Computer Science Logic (CSL). LNCS, vol. 1683, pp. 484-498. Springer, Heidelberg (1999) · Zbl 0944.03023 |
| [109] | 109. Semenov, A.: Decidability of monadic theories. In: Chytil, M., Koubek, V. (eds.) International Symposium on Mathematical Foundations of Computer Science. LNCS, vol. 176, pp. 162-175. Springer, Heidelberg (1984) · Zbl 0553.03005 |
| [110] | 110. Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54, 121-141 (1982) · Zbl 0515.68062 |
| [111] | 111. 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. 172, pp. 465-472. Springer, Heidelberg (1984) · Zbl 0556.68005 |
| [112] | 112. Streett, R.S., Emerson, E.A.: An automata theoretic procedure for the propositional mu-calculus. Inf. Comput. 81, 249-264 (1989) · Zbl 0671.03023 |
| [113] | 113. Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol. III, pp. 389-455. Springer, Heidelberg (1997) |
| [114] | 114. Thomas, W.: Infinite games and verification. In: Brinksma, E., Larsen, K.G. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 2404, pp. 58-64. Springer, Heidelberg (2002) · Zbl 1010.68504 |
| [115] | 115. Thomas, W.: Constructing infinite graphs with a decidable MSO-theory. In: Rovan, B., Vojtás, P. (eds.) International Symposium on Mathematical Foundations of Computer Science. LNCS, vol. 2747, pp. 113-124. Springer, Heidelberg (2003) · Zbl 1124.03314 |
| [116] | 116. Thomas, W.: Church’s 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. 4800, pp. 635-655. Springer, Heidelberg (2008) · Zbl 1133.68367 |
| [117] | 117. van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis, Napoli (1983) · Zbl 0639.03014 |
| [118] | 118. 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. 1443, pp. 628-641. Springer, Heidelberg (1998) · Zbl 0909.03019 |
| [119] | 119. Vardi, M.Y.: The Büchi complementation saga. In: Thomas, W., Weil, P. (eds.) Annual Symposium on Theoretical Aspects of Computer Science. LNCS, vol. 4393, pp. 12-22. Springer, Heidelberg (2007) · Zbl 1186.03062 |
| [120] | 120. Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata, Texts in Logic and Games, vol. 2, pp. 629-736. Amsterdam University Press, Amsterdam (2007) · Zbl 1234.03026 |
| [121] | 121. Venema, Y.: Automata and fixed point logic: a coalgebraic perspective. Inf. Comput. 204(4), 637-678 (2006) · Zbl 1110.68066 |
| [122] | 122. Vöge, J., Jurdziński, 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. 1855, pp. 202-215. Springer, Heidelberg (2000) · Zbl 0974.68527 |
| [123] | 123. Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional · Zbl 1046.68628 |
| [124] | 124. Walukiewicz, I.: Monadic second order logic on tree-like structures. Theor. Comput. Sci. 257(1-2), 311-346 (2002) · Zbl 1026.68087 |
| [125] | 125. Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci. 200, 135-183 (1998) · Zbl 0915.68120 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
