{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:09:33Z","timestamp":1725566973833},"publisher-location":"Berlin, Heidelberg","reference-count":84,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304951"},{"type":"electronic","value":"9783540324195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11590156_5","type":"book-chapter","created":{"date-parts":[[2005,12,5]],"date-time":"2005-12-05T15:43:16Z","timestamp":1133797396000},"page":"79-91","source":"Crossref","is-referenced-by-count":0,"title":["From Logic to Games"],"prefix":"10.1007","author":[{"given":"Igor","family":"Walukiewicz","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-27836-8_13","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2004","unstructured":"Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 122\u2013133. Springer, Heidelberg (2004)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30080-9_1","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"R. Alur","year":"2004","unstructured":"Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 1\u201324. Springer, Heidelberg (2004)"},{"key":"5_CR3","doi-asserted-by":"publisher","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\u2013Theoretical Informatics and Applications\u00a033, 329\u2013339 (1999)","journal-title":"RAIRO\u2013Theoretical Informatics and Applications"},{"key":"5_CR4","volume-title":"Studies in Logic","author":"A. Arnold","year":"2001","unstructured":"Arnold, A., Niwiski, D.: The Rudiments of the Mu-Calculus. In: Studies in Logic, vol.\u00a0146, North-Holand, Amsterdam (2001)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/3-540-36576-1_5","volume-title":"Foundations of Software Science and Computational Structures","author":"A. Arnold","year":"2003","unstructured":"Arnold, A., Santocanale, L.: Ambiguous classes in the games mu-calculus hierarchy. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 70\u201386. Springer, Heidelberg (2003)"},{"issue":"1","key":"5_CR6","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/S0304-3975(02)00442-5","volume":"303","author":"A. Arnold","year":"2003","unstructured":"Arnold, A., Vincent, A., Walukiewicz, I.: Games for synthesis of controllers with partial observation. Theoretical Computer Science\u00a0303(1), 7\u201334 (2003)","journal-title":"Theoretical Computer Science"},{"key":"5_CR7","unstructured":"Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Contrloller synthesis for timed automata. In: Proc. IFAC Symp. System Structure and Control, pp. 469\u2013474 (1998)"},{"key":"5_CR8","series-title":"Lecture Notes in Artificial Intelligence","first-page":"209","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Berwanger","year":"2004","unstructured":"Berwanger, D., Gr\u00e4del, E.: Entanglement - a measure for the complexity of directed graphs with applications to logic and games. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol.\u00a03452, pp. 209\u2013223. Springer, Heidelberg (2004)"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Applications to model checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1007\/11539452_36","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A. Bouajjani","year":"2005","unstructured":"Bouajjani, A., Mueller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 473\u2013487. Springer, Heidelberg (2005)"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-24597-1_8","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A. Bouquet","year":"2003","unstructured":"Bouquet, A., Serre, O., Walukiewicz, I.: Pushdown games with the unboundedness and regular conditions. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 88\u201399. Springer, Heidelberg (2003)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-30538-5_13","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"P. Bouyer","year":"2004","unstructured":"Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 148\u2013160. Springer, Heidelberg (2004)"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1007\/978-3-540-45069-6_18","volume-title":"Computer Aided Verification","author":"P. Bouyer","year":"2003","unstructured":"Bouyer, P., D\u2019Souza, D., Madhusudan, P., Petit, A.: Timed control with partial observability. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 180\u2013192. Springer, Heidelberg (2003)"},{"key":"5_CR14","first-page":"133","volume":"195","author":"J. Bradfield","year":"1997","unstructured":"Bradfield, J.: The modal mu-calculus alternation hierarchy is strict. Theoretical. Computer Science\u00a0195, 133\u2013153 (1997)","journal-title":"Computer Science"},{"key":"5_CR15","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1051\/ita:1999122","volume":"33","author":"J. Bradfield","year":"1999","unstructured":"Bradfield, J.: Fixpoint alternation: Arithmetic, transition systems, and the binary tree. RAIRO\u2013Theoretical Informatics and Applications\u00a033, 341\u2013356 (1999)","journal-title":"RAIRO\u2013Theoretical Informatics and Applications"},{"key":"5_CR16","first-page":"1","volume-title":"Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science","author":"J.R. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: On the decision method in restricted second-order arithmetic. In: Proc. Internat. Congr. on Logic, Methodology and Philosophy of Science, pp. 1\u201311. Stanford Univ. Press, Stanford (1960)"},{"key":"5_CR17","doi-asserted-by":"publisher","first-page":"1171","DOI":"10.2307\/2273681","volume":"48","author":"J.R. Buchi","year":"1983","unstructured":"Buchi, J.R.: State strategies for games in F\u03c3\u03b4 \u2229 G\u03b4\u03c3. Journal of Symbolic Logic\u00a048, 1171\u20131198 (1983)","journal-title":"Journal of Symbolic Logic"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Automata, Languages and Programming","author":"T. Cachat","year":"2002","unstructured":"Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., et al. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 704\u2013715. Springer, Heidelberg (2002)"},{"key":"5_CR19","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the 4th International Workshop on Verification of Infinite-State Systems","author":"T. Cachat","year":"2002","unstructured":"Cachat, T.: Uniform solution of parity games on prefix-recognizable graphs. In: Kucera, A., Mayr, R. (eds.) Proceedings of the 4th International Workshop on Verification of Infinite-State Systems. Electronic Notes in Theoretical Computer Science, vol.\u00a068, Elsevier Science Publishers, Amsterdam (2002)"},{"key":"5_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4070-7","volume-title":"Introduction to Discrete Event Systems","author":"C.G. Cassandras","year":"1999","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"5_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F. Cassez","year":"2005","unstructured":"Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 66\u201380. Springer, Heidelberg (2005)"},{"key":"5_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-45873-5_13","volume-title":"Hybrid Systems: Computation and Control","author":"F. Cassez","year":"2002","unstructured":"Cassez, F., Henzinger, T., Raskin, J.: A comparison of control problems for timed and hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol.\u00a02289, pp. 134\u2013148. Springer, Heidelberg (2002)"},{"issue":"1","key":"5_CR23","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"K. Chandra","year":"1981","unstructured":"Chandra, K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the Association of Computing Machinery\u00a028(1), 114\u2013133 (1981)","journal-title":"Journal of the Association of Computing Machinery"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/11539452_32","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"K. Chatterjee","year":"2005","unstructured":"Chatterjee, K.: Two-player nonzero-sum omega-regular games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 413\u2013427. Springer, Heidelberg (2005)"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E. Clarke","year":"1981","unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"5_CR26","unstructured":"Colcombet, T., Niwi\u0144ski, D.: On the positional determinacy of edge\u2013labeled games (2004) (submitted)"},{"key":"5_CR27","unstructured":"Courcelle, B., Weil, P.: The recognizability of sets of graphs is a robust property. Theoretical Computer Science (to appear), http:\/\/www.labri.fr\/Perso\/~weil\/publications\/"},{"key":"5_CR28","series-title":"Lecture Notes in Computer Science","first-page":"102","volume-title":"CONCUR 2003 - Concurrency Theory","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 102\u2013126. Springer, Heidelberg (2003)"},{"key":"5_CR29","series-title":"Lecture Notes in Computer Science","first-page":"142","volume-title":"CONCUR 2003 - Concurrency Theory","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 142\u2013156. Springer, Heidelberg (2003)"},{"key":"5_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/3-540-45841-7_51","volume-title":"STACS 2002","author":"S. Demri","year":"2002","unstructured":"Demri, S., Laroussinie, F., Schnoebelen, P.: A parametric analysis of the state exposion problem in model checking. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol.\u00a02285, pp. 620\u2013631. Springer, Heidelberg (2002)"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1007\/3-540-45841-7_47","volume-title":"STACS 2002","author":"D. D\u2019Souza","year":"2002","unstructured":"D\u2019Souza, D., Madhusudan, P.: Timed control synthesis for external specifications. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol.\u00a02285, pp. 571\u2013582. Springer, Heidelberg (2002)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Dziembowski, S., Jurdzinski, M., Walukiewicz, I.: How much memory is needed to win infinite games. In: LICS, pp. 99\u2013110 (1997)","DOI":"10.1109\/LICS.1997.614939"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. FOCS 1991, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Esparza, J., Podelski, A.: Efficient algorithms for pre star and post star on interprocedural parallel flow graphs. In: POPL 2000: Principles of Programming Languages (2000)","DOI":"10.1145\/325694.325697"},{"key":"5_CR35","doi-asserted-by":"crossref","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: LICS 2005 (2005)","DOI":"10.1109\/LICS.2005.53"},{"key":"5_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-540-30124-0_8","volume-title":"Computer Science Logic","author":"H. Gimbert","year":"2004","unstructured":"Gimbert, H.: Parity and explosion games on context-free graphs. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 56\u201370. Springer, Heidelberg (2004)"},{"key":"5_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1007\/978-3-540-28629-5_53","volume-title":"Mathematical Foundations of Computer Science 2004","author":"H. Gimbert","year":"2004","unstructured":"Gimbert, H., Zielonka, W.: When can you play positionally? In: Fiala, J., Koubek, V., Kratochv\u00edl, J. (eds.) MFCS 2004. LNCS, vol.\u00a03153, pp. 686\u2013697. Springer, Heidelberg (2004)"},{"key":"5_CR38","unstructured":"Mirkowska, G., Salwicki, A.: Algorithmic Logic. D.Reidel PWN (1987)"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Gr\u00e4del, E., Walukiewicz, I.: Positional determinacy of infnite games (2004) (submitted)","DOI":"10.1007\/978-3-540-24749-4_2"},{"key":"5_CR40","doi-asserted-by":"crossref","unstructured":"Gurevich, Y., Harrington, L.: Trees, automata and games. In: 14th ACM Symp. on Theory of Computations, pp. 60\u201365 (1982)","DOI":"10.1145\/800070.802177"},{"key":"5_CR41","doi-asserted-by":"crossref","unstructured":"Harel, D.: Dynamic logic. In: Handbook of Philosophical Logic vol.\u00a0II, pp. 497\u2013604. D.Reidel Publishing Company (1984)","DOI":"10.1007\/978-94-009-6259-0_10"},{"key":"5_CR42","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)"},{"key":"5_CR43","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012, 576\u2013585 (1969)","journal-title":"Communications of the ACM"},{"key":"5_CR44","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1287\/mnsc.12.5.359","volume":"12","author":"A. Hoffman","year":"1966","unstructured":"Hoffman, A., Karp, R.: On nonterminating stochastic games. Management Science\u00a012, 369\u2013370 (1966)","journal-title":"Management Science"},{"key":"5_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/11417170_5","volume-title":"Typed Lambda Calculi and Applications","author":"C.-H.L.O.K. Aehlig","year":"2005","unstructured":"Aehlig, C.-H.L.O.K., de Miranda, J.G.: The monadic second order theory of trees given by arbitrary level-two recursion schemes is decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 39\u201354. Springer, Heidelberg (2005)"},{"key":"5_CR46","unstructured":"Kamp, H.: Tense Logic and the Theory of Linear Order. PhD thesis, University of California (1968)"},{"key":"5_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1450","DOI":"10.1007\/11523468_117","volume-title":"Automata, Languages and Programming","author":"T. Knapik","year":"2005","unstructured":"Knapik, T., Niwinski, D., Urzyczyn, P., Walukiewicz, I.: Unsafe grammars and panic automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1450\u20131461. Springer, Heidelberg (2005)"},{"key":"5_CR48","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. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"5_CR49","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-2217-1","volume-title":"Modeling and control of logical discrete event systems","author":"R. Kumar","year":"1995","unstructured":"Kumar, R., Garg, V.K.: Modeling and control of logical discrete event systems. Kluwer Academic Pub., Dordrecht (1995)"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/10722167_7","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.: An automata-theoretic approach to reasoning about infinite-state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 36\u201352. Springer, Heidelberg (2000)"},{"key":"5_CR51","unstructured":"Kupferman, O., Vardi, M.: Synthesizing distributed systems. In: Proc. 16th IEEE Symp. on Logic in Computer Science (2001)"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Lamport, L.: sometime is sometimes not never \u2013 on the temporal logic of programs. In: POPL 1980, pp. 174\u2013185 (1980)","DOI":"10.1145\/567446.567463"},{"key":"5_CR53","unstructured":"Madhusudan, P.: Control and Synthesis of Open Reactive Systems. Ph.D thesis, University of Madras (2001)"},{"key":"5_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-45694-5_11","volume-title":"CONCUR 2002 - Concurrency Theory","author":"P. Madhusudan","year":"2002","unstructured":"Madhusudan, P., Thiagarajan, P.: A decidable class of asynchronous distributed controllers. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, p. 145. Springer, Heidelberg (2002)"},{"key":"5_CR55","first-page":"215","volume-title":"The Correctness Problem in Computer Scince","author":"Z. Manna","year":"1981","unstructured":"Manna, Z., Pnueli, A.: Verification of the concurrent programs: the temporal framework. In: Boyer, R., Moore, J. (eds.) The Correctness Problem in Computer Scince, pp. 215\u2013273. Academic Press, London (1981)"},{"key":"5_CR56","doi-asserted-by":"publisher","first-page":"363","DOI":"10.2307\/1971035","volume":"102","author":"D. Martin","year":"1975","unstructured":"Martin, D.: Borel determinacy. Ann. Math.\u00a0102, 363\u2013371 (1975)","journal-title":"Ann. Math."},{"issue":"4","key":"5_CR57","doi-asserted-by":"publisher","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D. Martin","year":"1998","unstructured":"Martin, D.: The determinacy of Blackwell games. The Journal of Symbolic Logic\u00a063(4), 1565\u20131581 (1998)","journal-title":"The Journal of Symbolic Logic"},{"key":"5_CR58","doi-asserted-by":"publisher","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 and Applied Logic\u00a065, 149\u2013184 (1993)","journal-title":"Ann. Pure and Applied Logic"},{"key":"5_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-540-24597-1_29","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"S. Mohalik","year":"2003","unstructured":"Mohalik, S., Walukiewicz, I.: Distributed games. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 338\u2013351. Springer, Heidelberg (2003)"},{"key":"5_CR60","series-title":"Lecture Notes in Computer Science","first-page":"157","volume-title":"Computation Theory","author":"W. Mostowski","year":"1984","unstructured":"Mostowski, W.: Regular expressions for infinite trees and a standard form of automata. In: Skowron, A. (ed.) SCT 1984. LNCS, vol.\u00a0208, pp. 157\u2013168. Springer, Heidelberg (1984)"},{"key":"5_CR61","unstructured":"Mostowski, W.: Games with forbidden positions. Technical Report 78, University of Gdansk (1991)"},{"key":"5_CR62","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D. Muller","year":"1985","unstructured":"Muller, D., Schupp, P.: The theory of ends, pushdown automata and secondorder logic. Theoretical Computer Science\u00a037, 51\u201375 (1985)","journal-title":"Theoretical Computer Science"},{"key":"5_CR63","first-page":"267","volume":"54","author":"D. Muller","year":"1987","unstructured":"Muller, D., Schupp, P.: Alternating automata on infinite trees. Theoretical. Computer Science\u00a054, 267\u2013276 (1987)","journal-title":"Computer Science"},{"key":"5_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/3-540-16761-7_96","volume-title":"Automata, Languages and Programming","author":"D. Niwi\u0144ski","year":"1986","unstructured":"Niwi\u0144ski, D.: On fixed-point clones. In: Kott, L. (ed.) ICALP 1986. LNCS, vol.\u00a0226, pp. 464\u2013473. Springer, Heidelberg (1986)"},{"key":"5_CR65","series-title":"Lecture Notes in Computer Science","volume-title":"STACS 98","author":"D. Niwi\u0144ski","year":"1998","unstructured":"Niwi\u0144ski, D., Walukiewicz, I.: Relating hierarchies of word and tree automata. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol.\u00a01373, Springer, Heidelberg (1998)"},{"issue":"1","key":"5_CR66","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1016\/S0304-3975(02)00452-8","volume":"303","author":"D. Niwi\u0144ski","year":"2003","unstructured":"Niwi\u0144ski, D., Walukiewicz, I.: A gap property of deterministic tree languages. Theoretical Computer Science\u00a0303(1), 215\u2013231 (2003)","journal-title":"Theoretical Computer Science"},{"key":"5_CR67","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.entcs.2004.05.015","volume":"123","author":"D. Niwi\u0144ski","year":"2005","unstructured":"Niwi\u0144ski, D., Walukiewicz, I.: Deciding nondeterministic hierarchy of deterministic tree automata. Electr. Notes Theor. Comput. Sci.\u00a0123, 195\u2013208 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"5_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-540-45069-6_7","volume-title":"Computer Aided Verification","author":"J. Obdrzalek","year":"2003","unstructured":"Obdrzalek, J.: Fast mu-calculus model checking when tree-width is bounded. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 80\u201392. Springer, Heidelberg (2003)"},{"key":"5_CR69","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. ACM POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"5_CR70","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc.\u00a0141, 1\u201335 (1969)","journal-title":"Trans. Amer. Math. Soc."},{"key":"#cr-split#-5_CR71.1","doi-asserted-by":"crossref","unstructured":"Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research and Development, 114\u2013125 (1959);","DOI":"10.1147\/rd.32.0114"},{"key":"#cr-split#-5_CR71.2","unstructured":"Reprinted in Sequential machines (editor E. F. Moore), Addison-Wesley, Reading, Massachusetts, pp. 63-91 (1964)"},{"issue":"2","key":"5_CR72","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"P.J.G. Ramadge","year":"1989","unstructured":"Ramadge, P.J.G., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE\u00a077(2), 81\u201398 (1989)","journal-title":"Proceedings of the IEEE"},{"issue":"11","key":"5_CR73","doi-asserted-by":"publisher","first-page":"1692","DOI":"10.1109\/9.173140","volume":"37","author":"K. Rudie","year":"1992","unstructured":"Rudie, K., Wonham, W.: Think globally, act locally: Decentralized supervisory control. IEEE Trans. on Automat. Control\u00a037(11), 1692\u20131708 (1992)","journal-title":"IEEE Trans. on Automat. Control"},{"key":"5_CR74","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/S0020-0190(02)00445-3","volume":"85","author":"O. Serre","year":"2003","unstructured":"Serre, O.: Note on winning positions on pushdown games with \u03c9-regular conditions. Information Processing Letters\u00a085, 285\u2013291 (2003)","journal-title":"Information Processing Letters"},{"key":"5_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1150","DOI":"10.1007\/978-3-540-27836-8_95","volume-title":"Automata, Languages and Programming","author":"O. Serre","year":"2004","unstructured":"Serre, O.: Games with winning conditions of high Borel complexity. In: D\u00edaz, J., et al. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 1150\u20131162. Springer, Heidelberg (2004)"},{"key":"5_CR76","series-title":"Texts in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3550-5","volume-title":"Modal and Temporal Properties of Processes","author":"C. Stirling","year":"2001","unstructured":"Stirling, C.: Modal and Temporal Properties of Processes. Texts in Computer Science. Springer, Heidelberg (2001)"},{"key":"5_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"465","DOI":"10.1007\/3-540-13345-3_43","volume-title":"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.) ICALP 1984. LNCS, vol.\u00a0172, pp. 465\u2013472. Springer, Heidelberg (1984)"},{"key":"5_CR78","doi-asserted-by":"publisher","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. Information and Computation\u00a081, 249\u2013264 (1989)","journal-title":"Information and Computation"},{"key":"5_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/3-540-44577-3_18","volume-title":"Informatics","author":"W. Thomas","year":"2001","unstructured":"Thomas, W.: Logic for computer science: The engineering challenge. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol.\u00a02000, pp. 257\u2013267. Springer, Heidelberg (2001)"},{"key":"5_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-45022-X_56","volume-title":"Automata, Languages and Programming","author":"T. Urba\u0144ski","year":"2000","unstructured":"Urba\u0144ski, T.: On deciding if deterministic Rabin language is in B\u00fcchi class. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 663\u2013674. Springer, Heidelberg (2000)"},{"key":"5_CR81","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. In: Sixteenth ACM Symposium on the Theoretical Computer Science (1984)","DOI":"10.1145\/800057.808711"},{"key":"5_CR82","first-page":"473","volume":"13","author":"K. Wagner","year":"1977","unstructured":"Wagner, K.: Eine topologische Charakterisierung einiger Klassen regul\u00e4rer Folgenmengen. J. Inf. Process. Cybern. EIK\u00a013, 473\u2013487 (1977)","journal-title":"J. Inf. Process. Cybern. EIK"},{"issue":"2","key":"5_CR83","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I. Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model checking. Information and Computation\u00a0164(2), 234\u2013263 (2001)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11590156_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:49:19Z","timestamp":1619506159000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11590156_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304951","9783540324195"],"references-count":84,"URL":"https:\/\/doi.org\/10.1007\/11590156_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}