{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:48Z","timestamp":1776316848539,"version":"3.50.1"},"publisher-location":"Cham","reference-count":181,"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_27","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T08:05:28Z","timestamp":1526630728000},"page":"921-962","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":59,"title":["Graph Games and Reactive Synthesis"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Krishnendu","family":"Chatterjee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"27_CR1","series-title":"LNCS","first-page":"1","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0372, pp.\u00a01\u201317. Springer, Heidelberg (1989)"},{"key":"27_CR2","series-title":"LNCS","first-page":"144","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","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.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a02761, pp.\u00a0144\u2013158. Springer, Heidelberg (2003)"},{"key":"27_CR3","first-page":"109","volume-title":"Intl. Symp. on Foundations of Software Engineering (FSE)","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Tjoa, A.M., Gruhn, V. (eds.) Intl. Symp. on Foundations of Software Engineering (FSE), pp.\u00a0109\u2013120. ACM, New York (2001)"},{"key":"27_CR4","series-title":"LNCS","first-page":"148","volume-title":"Intl. Conf. on Embedded Software (EMSOFT)","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) Intl. Conf. on Embedded Software (EMSOFT). LNCS, vol.\u00a02211, pp.\u00a0148\u2013165. Springer, Heidelberg (2001)"},{"issue":"3","key":"27_CR5","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/j.tcs.2007.07.008","volume":"386","author":"L. Alfaro de","year":"2007","unstructured":"de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. Theor. Comput. Sci. 386(3), 188\u2013217 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR6","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1007\/10722167_17","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Henzinger, T.A., Mang, F.: Detecting errors before reaching them. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0186\u2013201. Springer, Heidelberg (2000)"},{"key":"27_CR7","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/380752.380871","volume-title":"Annual ACM Symposium on Theory of Computing (STOC)","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Majumdar, R.: Quantitative solution of omega-regular games. In: Vitter, J.S., Spirakis, P.G., Yannakakis, M. (eds.) Annual ACM Symposium on Theory of Computing (STOC), pp.\u00a0675\u2013683. ACM, New York (2001)"},{"key":"27_CR8","first-page":"1","volume-title":"Dependable Software Systems Engineering","author":"R. Alur","year":"2015","unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, pp.\u00a01\u201325. IOS Press, Amsterdam (2015)"},{"key":"27_CR9","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"27_CR10","first-page":"291","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"R. Alur","year":"2001","unstructured":"Alur, R., Torre, S.L.: Deterministic generators and games for LTL fragments. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0291\u2013302. IEEE, Piscataway (2001)"},{"key":"27_CR11","unstructured":"Antoniotti, M.: Synthesis and verification of discrete controllers for robotics and manufacturing devices with temporal logic and the Control-D system. Ph.D. thesis, New York University (1995)"},{"key":"27_CR12","first-page":"493","volume-title":"IFIP Intl. Conf. on Theoretical Computer Science","author":"C. Baier","year":"2004","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: IFIP Intl. Conf. on Theoretical Computer Science, pp.\u00a0493\u2013506 (2004)"},{"key":"27_CR13","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1145\/320613.320614","volume":"5","author":"C. Beeri","year":"1980","unstructured":"Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. Database Syst. 5, 241\u2013259 (1980)","journal-title":"ACM Trans. Database Syst."},{"key":"27_CR14","first-page":"319","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"N. Bertrand","year":"2009","unstructured":"Bertrand, N., Genest, B., Gimbert, H.: Qualitative determinacy and decidability of stochastic games with signals. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0319\u2013328. IEEE, Piscataway (2009)"},{"key":"27_CR15","series-title":"LNCS","first-page":"663","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science (STACS)","author":"H. Bj\u00f6rklund","year":"2003","unstructured":"Bj\u00f6rklund, H., Sandberg, S., Vorobyov, S.: A discrete subexponential algorithms for parity games. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a02607, pp.\u00a0663\u2013674. Springer, Heidelberg (2003)"},{"key":"27_CR16","series-title":"LNCS","first-page":"673","volume-title":"Intl. Symp. on Mathematical Foundations of Computer Science (MFCS)","author":"H. Bjorklund","year":"2004","unstructured":"Bjorklund, H., Sandberg, S., Vorobyov, S.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol.\u00a03153, pp.\u00a0673\u2013685. Springer, Heidelberg (2004)"},{"key":"27_CR17","series-title":"LNCS","volume-title":"Intl. Conf. on Formal Approaches to Software Testing (FATES)","author":"A. Blass","year":"2005","unstructured":"Blass, A., Gurevich, Y., Nachmanson, L., Veanes, M.: Play to test. In: Intl. Conf. on Formal Approaches to Software Testing (FATES). LNCS, vol.\u00a03997. Springer, Heidelberg (2005)"},{"key":"27_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/978-3-642-14295-6_36","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Bloem","year":"2010","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Jobstmann, B.: Robustness in the presence of liveness. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a0410\u2013424. Springer, Heidelberg (2010)"},{"key":"27_CR19","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05643, pp.\u00a0140\u2013156. Springer, Heidelberg (2009)"},{"key":"27_CR20","first-page":"85","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"R. Bloem","year":"2009","unstructured":"Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a085\u201392. IEEE, Piscataway (2009)"},{"issue":"5\u20136","key":"27_CR21","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/s10009-013-0287-9","volume":"15","author":"R. Bod\u00edk","year":"2013","unstructured":"Bod\u00edk, R., Jobstmann, B.: Algorithmic program synthesis: introduction. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 397\u2013411 (2013)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"27_CR22","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"Intl. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS)","author":"P. Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Intl. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS). LNCS, vol.\u00a05215, pp.\u00a033\u201347. Springer, Heidelberg (2008)"},{"key":"27_CR23","volume-title":"Handbook of Model Checking","author":"P. Bouyer","year":"2018","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Ouaknine, J., Worrell, J., Verification of real-time systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"27_CR24","volume-title":"Handbook of Model Checking","author":"J. Bradfield","year":"2018","unstructured":"Bradfield, J., Walukiewicz, I.: The mu-calculus. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"27_CR25","first-page":"33","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"T. Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: Symp. on Logic in Computer Science (LICS), pp.\u00a033\u201342. IEEE, Piscataway (2011)"},{"key":"27_CR26","first-page":"331","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"T. Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0331\u2013340. IEEE, Piscataway (2013)"},{"key":"27_CR27","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-31424-7_8","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"T. Br\u00e1zdil","year":"2012","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Kucera, A., Novotn\u00fd, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a023\u201338. Springer, Heidelberg (2012)"},{"issue":"2","key":"27_CR28","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/s10703-010-0105-x","volume":"38","author":"L. Brim","year":"2011","unstructured":"Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.F.: Faster algorithms for mean-payoff games. Form. Methods Syst. Des. 38(2), 97\u2013118 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"27_CR29","volume-title":"Handbook of Model Checking","author":"R.E. Bryant","year":"2018","unstructured":"Bryant, R.E.: Binary decision diagrams: an algorithmic basis for symbolic model checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"27_CR30","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1090\/S0002-9947-1969-0280205-0","volume":"138","author":"J.R. B\u00fcchi","year":"1969","unstructured":"B\u00fcchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. Am. Math. Soc. 138, 295\u2013311 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"27_CR31","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-68612-7","volume-title":"Introduction to Discrete Event Systems","author":"C.G. Cassandras","year":"2008","unstructured":"Cassandras, C.G., Lafortune, S.: Introduction to Discrete Event Systems, 2nd edn. Springer, Heidelberg (2008)","edition":"2"},{"key":"27_CR32","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"P. Cern\u00fd","year":"2011","unstructured":"Cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06806, pp.\u00a0243\u2013259. Springer, Heidelberg (2011)"},{"key":"27_CR33","series-title":"LNCS","first-page":"117","volume-title":"Intl. Conf. on Embedded Software (EMSOFT)","author":"A. Chakrabarti","year":"2003","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Intl. Conf. on Embedded Software (EMSOFT). LNCS, vol.\u00a02855, pp.\u00a0117\u2013133. Springer, Heidelberg (2003)"},{"key":"27_CR34","unstructured":"Chatterjee, K.: Stochastic \u03c9$\\omega$-regular games. Ph.D. thesis, UC Berkeley (2007)"},{"key":"27_CR35","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1016\/j.ic.2011.11.004","volume":"211","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K.: The complexity of stochastic M\u00fcller games. Inf. Comput. 211, 29\u201348 (2012)","journal-title":"Inf. Comput."},{"key":"27_CR36","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"878","DOI":"10.1007\/11523468_71","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"K. Chatterjee","year":"2005","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of stochastic Rabin and Streett games. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a03580, pp.\u00a0878\u2013890. Springer, Heidelberg (2005)"},{"key":"27_CR37","first-page":"678","volume-title":"ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.A.: The complexity of quantitative concurrent parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.\u00a0678\u2013687. ACM\/SIAM, New York\/Philadelphia (2006)"},{"key":"27_CR38","first-page":"291","volume-title":"Intl. Conf. on Quantitative Evaluation of Systems (QEST)","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Strategy improvement in concurrent reachability games. In: Intl. Conf. on Quantitative Evaluation of Systems (QEST), pp.\u00a0291\u2013300. IEEE, Piscataway (2006)"},{"issue":"4","key":"27_CR39","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1145\/1970398.1970404","volume":"12","author":"K. Chatterjee","year":"2011","unstructured":"Chatterjee, K., de Alfaro, L., Henzinger, T.A.: Qualitative concurrent parity games. ACM Trans. Comput. Log. 12(4), 28 (2011)","journal-title":"ACM Trans. Comput. Log."},{"key":"27_CR40","series-title":"LIPIcs","volume-title":"Annual Conf. on Computer Science Logic (CSL)","author":"K. Chatterjee","year":"2013","unstructured":"Chatterjee, K., Chmelik, M., Tracol, M.: What is decidable about partially observable Markov decision processes with omega-regular objectives. In: Annual Conf. on Computer Science Logic (CSL). LIPIcs, vol.\u00a023 (2013)"},{"key":"27_CR41","series-title":"LNCS","first-page":"1","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L.: The complexity of partial-observation parity games. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol.\u00a06397, pp.\u00a01\u201314. Springer, Heidelberg (2010)"},{"key":"27_CR42","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/j.tcs.2012.07.038","volume":"458","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49\u201360 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR43","first-page":"175","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Doyen, L.: Partial-observation stochastic games: how to win when belief fails. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0175\u2013184. IEEE, Piscataway (2012)"},{"key":"27_CR44","series-title":"LNCS","first-page":"246","volume-title":"Intl. Symp. on Mathematical Foundations of Computer Science (MFCS)","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Gimbert, H., Henzinger, T.A.: Randomness for free. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol.\u00a06281, pp.\u00a0246\u2013257. Springer, Heidelberg (2010)"},{"key":"27_CR45","series-title":"LIPIcs","first-page":"505","volume-title":"Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T., Raskin, J.F.: Generalized mean-payoff and energy games. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LIPIcs, vol.\u00a08, pp.\u00a0505\u2013516. Schloss Dagstuhl\u2014LZI, Dagstuhl (2010)"},{"key":"27_CR46","series-title":"LNCS","first-page":"258","volume-title":"Intl. Symp. on Mathematical Foundations of Computer Science (MFCS)","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Qualitative analysis of partially-observable Markov decision processes. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol.\u00a06281, pp.\u00a0258\u2013269. Springer, Heidelberg (2010)"},{"issue":"2","key":"27_CR47","doi-asserted-by":"crossref","first-page":"268","DOI":"10.1007\/s10703-012-0164-2","volume":"43","author":"K. Chatterjee","year":"2013","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: A survey of partial-observation stochastic parity games. Form. Methods Syst. Des. 43(2), 268\u2013284 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"27_CR48","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/11874683_19","volume-title":"Annual Conf. on Computer Science Logic (CSL)","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.: Algorithms for omega-regular games with imperfect information. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol.\u00a04207, pp.\u00a0287\u2013302. Springer, Heidelberg (2006)"},{"key":"27_CR49","series-title":"LNCS","volume-title":"Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS)","author":"K. Chatterjee","year":"2014","unstructured":"Chatterjee, K., Doyen, L., Nain, S., Vardi, M.Y.: The complexity of partial-observation stochastic parity games with finite-memory strategies. In: Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol.\u00a08412. Springer, Heidelberg (2014)"},{"key":"27_CR50","series-title":"LNCS","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"K. Chatterjee","year":"2013","unstructured":"Chatterjee, K., Forejt, V., Wojtczak, D.: Multi-objective discounted reward verification in graphs and MDPs. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol.\u00a08312. Springer, Heidelberg (2013)"},{"key":"27_CR51","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"K. Chatterjee","year":"2015","unstructured":"Chatterjee, K., Goyal, P., Ibsen-Jensen, R., Pavlogiannis, A.: Faster algorithms for algebraic path properties in recursive state machines with constant treewidth. In: Symp. on Principles of Programming Languages (POPL). ACM, New York (2015)"},{"key":"27_CR52","doi-asserted-by":"crossref","first-page":"1386","DOI":"10.1137\/1.9781611973099.109","volume-title":"ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, M.: An O(n2$^{\\mbox{2}}$) time algorithm for alternating B\u00fcchi games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.\u00a01386\u20131399 (2012)"},{"issue":"3","key":"27_CR53","doi-asserted-by":"crossref","first-page":"15:1","DOI":"10.1145\/2597631","volume":"61","author":"K. Chatterjee","year":"2014","unstructured":"Chatterjee, K., Henzinger, M.: Efficient and dynamic algorithms for alternating B\u00fcchi games and maximal end-component decomposition. J. ACM 61(3), 15:1\u201315:40 (2014)","journal-title":"J. ACM"},{"key":"27_CR54","series-title":"LNCS","first-page":"1","volume-title":"Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"K. Chatterjee","year":"2005","unstructured":"Chatterjee, K., Henzinger, T.A.: Semiperfect-information games. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol.\u00a03821, pp.\u00a01\u201318. Springer, Heidelberg (2005)"},{"key":"27_CR55","series-title":"LNCS","first-page":"261","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A.: Assume-guarantee synthesis. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a04424, pp.\u00a0261\u2013275. Springer, Heidelberg (2007)"},{"issue":"2","key":"27_CR56","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1016\/j.jcss.2011.05.002","volume":"78","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Henzinger, T.A.: A survey of stochastic omega-regular games. J. Comput. Syst. Sci. 78(2), 394\u2013413 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"27_CR57","series-title":"CONCUR","first-page":"147","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: Intl. Conf. on Concurrency Theory (CONCUR). CONCUR, vol.\u00a02008, pp.\u00a0147\u2013161. Springer, Heidelberg (2008)"},{"key":"27_CR58","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"380","DOI":"10.1007\/978-3-642-14295-6_34","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a0380\u2013395. Springer, Heidelberg (2010)"},{"key":"27_CR59","first-page":"160","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"K. Chatterjee","year":"2004","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzi\u0144ski, M.: Games with secure equilibria. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0160\u2013169. IEEE, Piscataway (2004)"},{"key":"27_CR60","first-page":"178","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"K. Chatterjee","year":"2005","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0178\u2013187 (2005)"},{"key":"27_CR61","volume-title":"Workshop on Games in Design and Verification (GDV)","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Algorithms for B\u00fcchi games. In: Workshop on Games in Design and Verification (GDV) (2006)"},{"key":"27_CR62","series-title":"LNCS","first-page":"153","volume-title":"Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS)","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol.\u00a04423, pp.\u00a0153\u2013167. Springer, Heidelberg (2007)"},{"issue":"6","key":"27_CR63","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1016\/j.ic.2009.07.004","volume":"208","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy logic. Inf. Comput. 208(6), 677\u2013693 (2010)","journal-title":"Inf. Comput."},{"key":"27_CR64","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"100","DOI":"10.1007\/978-3-540-45220-1_11","volume-title":"Annual Conf. on Computer Science Logic (CSL)","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.A.: Simple stochastic parity games. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol.\u00a02803, pp.\u00a0100\u2013113. Springer, Heidelberg (2003)"},{"key":"27_CR65","first-page":"121","volume-title":"ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"K. Chatterjee","year":"2004","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.A.: Quantitative stochastic parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.\u00a0121\u2013130. SIAM, Philadelphia (2004)"},{"key":"27_CR66","series-title":"LNCS","first-page":"325","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science (STACS)","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a03884, pp.\u00a0325\u2013336. Springer, Heidelberg (2006)"},{"issue":"2","key":"27_CR67","doi-asserted-by":"crossref","first-page":"219","DOI":"10.1007\/s00182-007-0110-5","volume":"37","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Stochastic limit-average games are in EXPTIME. Int. J. Game Theory 37(2), 219\u2013234 (2008)","journal-title":"Int. J. Game Theory"},{"key":"27_CR68","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"K. Chatterjee","year":"2015","unstructured":"Chatterjee, K., Pavlogiannis, A., Velner, Y.: Quantitative interprocedural analysis. In: Symp. on Principles of Programming Languages (POPL). ACM, New York (2015)"},{"key":"27_CR69","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-642-27940-9_11","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Raman, V.: Synthesizing protocols for digital contract signing. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a07148, pp.\u00a0152\u2013168. Springer, Heidelberg (2012)"},{"issue":"4","key":"27_CR70","doi-asserted-by":"crossref","first-page":"825","DOI":"10.1007\/s00165-013-0283-6","volume":"26","author":"K. Chatterjee","year":"2014","unstructured":"Chatterjee, K., Raman, V.: Assume-guarantee synthesis for digital contract signing. Form. Asp. Comput. 26(4), 825\u2013859 (2014)","journal-title":"Form. Asp. Comput."},{"key":"27_CR71","series-title":"LNCS","first-page":"115","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Randour, M., Raskin, J.F.: Strategy synthesis for multi-dimensional quantitative objectives. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a07454, pp.\u00a0115\u2013131. Springer, Heidelberg (2012)"},{"key":"27_CR72","first-page":"195","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"K. Chatterjee","year":"2012","unstructured":"Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0195\u2013204. IEEE, Piscataway (2012)"},{"key":"27_CR73","series-title":"LNCS","first-page":"500","volume-title":"Intl. Conf. on Concurrency Theory (CONCUR)","author":"K. Chatterjee","year":"2013","unstructured":"Chatterjee, K., Velner, Y.: Hyperplane separation technique for multidimensional mean-payoff games. In: Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol.\u00a08052, pp.\u00a0500\u2013515. Springer, Heidelberg (2013)"},{"key":"27_CR74","series-title":"LNCS","first-page":"266","volume-title":"Intl. Symp. on Mathematical Foundations of Computer Science (MFCS)","author":"T. Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M.Z., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol.\u00a08087, pp.\u00a0266\u2013277. Springer, Heidelberg (2013)"},{"key":"27_CR75","first-page":"23","volume-title":"Proceedings of the International Congress of Mathematicians","author":"A. Church","year":"1962","unstructured":"Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians, pp.\u00a023\u201335. Institut Mittag-Leffler, Djursholm (1962)"},{"key":"27_CR76","series-title":"LNCS","first-page":"52","volume-title":"Logic of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs. LNCS, vol.\u00a0131, pp.\u00a052\u201371. Springer, Heidelberg (1981)"},{"issue":"2","key":"27_CR77","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."},{"key":"27_CR78","series-title":"DIMACS Series in Discrete Mathematics and Theoretical Computer Science","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1090\/dimacs\/013\/04","volume-title":"Advances in Computational Complexity Theory","author":"A. Condon","year":"1993","unstructured":"Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol.\u00a013, pp.\u00a051\u201373. AMS, Providence (1993)"},{"key":"27_CR79","doi-asserted-by":"crossref","unstructured":"Dill, D.L.: Trace theory for automatic hierarchical verification of speed-independent circuits. Ph.D. thesis, ACM Distinguished Dissertation Series. MIT Press (1989)","DOI":"10.7551\/mitpress\/6874.001.0001"},{"key":"27_CR80","first-page":"99","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"S. Dziembowski","year":"1997","unstructured":"Dziembowski, S., Jurdzi\u0144ski, M., Walukiewicz, I.: How much memory is needed to win infinite games? In: Symp. on Logic in Computer Science (LICS), pp.\u00a099\u2013110. IEEE, Piscataway (1997)"},{"key":"27_CR81","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-642-31424-7_9","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"R. Ehlers","year":"2012","unstructured":"Ehlers, R.: ACTL \u2229 LTL synthesis. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a07358, pp.\u00a039\u201354. Springer, Heidelberg (2012)"},{"issue":"2","key":"27_CR82","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/s10703-011-0137-x","volume":"40","author":"R. Ehlers","year":"2012","unstructured":"Ehlers, R.: Symbolic bounded synthesis. Form. Methods Syst. Des. 40(2), 232\u2013262 (2012)","journal-title":"Form. Methods Syst. Des."},{"issue":"2","key":"27_CR83","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/BF01768705","volume":"8","author":"A. Ehrenfeucht","year":"1979","unstructured":"Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. J. Game Theory 8(2), 109\u2013113 (1979)","journal-title":"Int. J. Game Theory"},{"issue":"3","key":"27_CR84","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982)","journal-title":"Sci. Comput. Program."},{"key":"27_CR85","first-page":"328","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"E.A. Emerson","year":"1988","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0328\u2013337. IEEE, Piscataway (1988)"},{"key":"27_CR86","first-page":"368","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0368\u2013377. IEEE, Piscataway (1991)"},{"key":"27_CR87","doi-asserted-by":"crossref","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:8)2008"},{"issue":"5","key":"27_CR88","doi-asserted-by":"crossref","first-page":"1159","DOI":"10.1137\/S0097539703420675","volume":"34","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Wilke, T., Schuller, R.A.: Fair simulation relations, parity games, and state space reduction for B\u00fcchi automata. SIAM J. Comput. 34(5), 1159\u20131175 (2005)","journal-title":"SIAM J. Comput."},{"key":"27_CR89","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"891","DOI":"10.1007\/11523468_72","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"K. Etessami","year":"2005","unstructured":"Etessami, K., Yannakakis, M.: Recursive Markov decision processes and recursive stochastic games. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a03580, pp.\u00a0891\u2013903. Springer, Heidelberg (2005)"},{"key":"27_CR90","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/11787006_28","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"K. Etessami","year":"2006","unstructured":"Etessami, K., Yannakakis, M.: Recursive concurrent stochastic games. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a04052, pp.\u00a0324\u2013335. Springer, Heidelberg (2006)"},{"issue":"6","key":"27_CR91","doi-asserted-by":"crossref","first-page":"2531","DOI":"10.1137\/080720826","volume":"39","author":"K. Etessami","year":"2010","unstructured":"Etessami, K., Yannakakis, M.: On the complexity of Nash equilibria and other fixed points. SIAM J. Comput. 39(6), 2531\u20132597 (2010)","journal-title":"SIAM J. Comput."},{"key":"27_CR92","volume-title":"Competitive Markov Decision Processes","author":"J. Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Heidelberg (1997)"},{"key":"27_CR93","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.F.: An antichain algorithm for LTL realizability. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a05643, pp.\u00a0263\u2013277. Springer, Heidelberg (2009)"},{"key":"27_CR94","first-page":"321","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"B. Finkbeiner","year":"2005","unstructured":"Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0321\u2013330. IEEE, Piscataway (2005)"},{"key":"27_CR95","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/978-3-642-15205-4_25","volume-title":"Annual Conf. on Computer Science Logic (CSL)","author":"B. Finkbeiner","year":"2010","unstructured":"Finkbeiner, B., Schewe, S.: Coordination logic. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol.\u00a06247, pp.\u00a0305\u2013319. Springer, Heidelberg (2010)"},{"key":"27_CR96","series-title":"LNCS","first-page":"112","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06065, pp.\u00a0112\u2013127. Springer, Heidelberg (2011)"},{"key":"27_CR97","first-page":"145","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"O. Friedmann","year":"2009","unstructured":"Friedmann, O.: An exponential lower bound for the parity game strategy improvement algorithm as we know it. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0145\u2013156. IEEE, Piscataway (2009)"},{"key":"27_CR98","unstructured":"Friedmann, O.: Exponential lower bounds for solving infinitary payoff games and linear programs. Ph.D. thesis, University of Munich (2011)"},{"key":"27_CR99","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: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a02102, pp.\u00a053\u201365. Springer, Heidelberg (2001)"},{"issue":"2","key":"27_CR100","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/s10703-009-0084-y","volume":"35","author":"A. Girault","year":"2009","unstructured":"Girault, A., Rutten, \u00c9.: Automating the addition of fault tolerance with discrete controller synthesis. Form. Methods Syst. Des. 35(2), 190\u2013225 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"27_CR101","first-page":"60","volume-title":"Annual ACM Symposium on Theory of Computing (STOC)","author":"Y. Gurevich","year":"1982","unstructured":"Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Annual ACM Symposium on Theory of Computing (STOC), pp.\u00a060\u201365. ACM, New York (1982)"},{"key":"27_CR102","first-page":"205","volume-title":"Annual ACM Symposium on Theory of Computing (STOC)","author":"K.A. Hansen","year":"2011","unstructured":"Hansen, K.A., Kouck\u00fd, M., Lauritzen, N., Miltersen, P.B., Tsigaridas, E.P.: Exact algorithms for solving stochastic games: extended abstract. In: Annual ACM Symposium on Theory of Computing (STOC), pp.\u00a0205\u2013214 (2011)"},{"key":"27_CR103","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"644","DOI":"10.1007\/3-540-45465-9_55","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Krishnan, S., Kupferman, O., Mang, F.: Synthesis of uninitialized systems. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a02380, pp.\u00a0644\u2013656. Springer, Heidelberg (2002)"},{"key":"27_CR104","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1006\/inco.2001.3085","volume":"173","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Inf. Comput. 173, 64\u201381 (2002)","journal-title":"Inf. Comput."},{"key":"27_CR105","volume-title":"Workshop on Games in Design and Verification (GDV)","author":"F. Horn","year":"2005","unstructured":"Horn, F.: Streett games on finite graphs. In: Workshop on Games in Design and Verification (GDV) (2005)"},{"key":"27_CR106","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1016\/0022-0000(81)90039-8","volume":"22","author":"N. Immerman","year":"1981","unstructured":"Immerman, N.: Number of quantifiers is better than number of tape cells. J. Comput. Syst. Sci. 22, 384\u2013406 (1981)","journal-title":"J. Comput. Syst. Sci."},{"key":"27_CR107","series-title":"LNCS","first-page":"362","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Jacobs","year":"2012","unstructured":"Jacobs, S., Bloem, R.: Parameterized synthesis. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a07214, pp.\u00a0362\u2013376. Springer, Heidelberg (2012)"},{"key":"27_CR108","first-page":"117","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"B. Jobstmann","year":"2006","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a0117\u2013124. IEEE, Piscataway (2006)"},{"issue":"2","key":"27_CR109","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/j.jcss.2011.05.005","volume":"78","author":"B. Jobstmann","year":"2012","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441\u2013460 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"3","key":"27_CR110","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 \u2229 co-UP. Inf. Process. Lett. 68(3), 119\u2013124 (1998)","journal-title":"Inf. Process. Lett."},{"key":"27_CR111","series-title":"LNCS","first-page":"290","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science (STACS)","author":"M. Jurdzi\u0144ski","year":"2000","unstructured":"Jurdzi\u0144ski, M.: Small progress measures for solving parity games. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a01770, pp.\u00a0290\u2013301. Springer, Heidelberg (2000)"},{"key":"27_CR112","first-page":"117","volume-title":"ACM-SIAM Symposium on Discrete Algorithms (SODA)","author":"M. Jurdzi\u0144ski","year":"2006","unstructured":"Jurdzi\u0144ski, M., Paterson, M., Zwick, U.: A deterministic subexponential algorithm for solving parity games. In: ACM-SIAM Symposium on Discrete Algorithms (SODA), pp.\u00a0117\u2013123. ACM\/SIAM, New York\/Philadelphia (2006)"},{"key":"27_CR113","series-title":"LNCS","first-page":"117","volume-title":"Intl. Haifa Verification Conference (HVC)","author":"G. Katz","year":"2009","unstructured":"Katz, G., Peled, D.: Synthesizing solutions to the leader election problem using model checking and genetic programming. In: Intl. Haifa Verification Conference (HVC). LNCS, vol.\u00a06405, pp.\u00a0117\u2013132. Springer, Heidelberg (2009)"},{"key":"27_CR114","first-page":"50","volume-title":"Intl. Workshop on Approaches and Applications of Inductive Programming (AAIP)","author":"E. Kitzelmann","year":"2009","unstructured":"Kitzelmann, E.: Inductive programming: a survey of program synthesis techniques. In: Intl. Workshop on Approaches and Applications of Inductive Programming (AAIP), pp.\u00a050\u201373 (2009)"},{"key":"27_CR115","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/978-3-642-27940-9_19","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"U. Klein","year":"2012","unstructured":"Klein, U., Piterman, N., Pnueli, A.: Effective synthesis of asynchronous systems from GR(1) specifications. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a07148, pp.\u00a0283\u2013298. Springer, Heidelberg (2012)"},{"key":"27_CR116","first-page":"316","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"V. Kuncak","year":"2010","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0316\u2013329. ACM, New York (2010)"},{"key":"27_CR117","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a031\u201344. Springer, Heidelberg (2006)"},{"key":"27_CR118","first-page":"91","volume-title":"2nd International Conference on Temporal Logic","author":"O. Kupferman","year":"1997","unstructured":"Kupferman, O., Vardi, M.: Synthesis with incomplete information. In: 2nd International Conference on Temporal Logic, Manchester, pp.\u00a091\u2013106 (1997)"},{"key":"27_CR119","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1145\/276698.276748","volume-title":"Annual ACM Symposium on Theory of Computing (STOC)","author":"O. Kupferman","year":"1998","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata and tree automata emptiness. In: Annual ACM Symposium on Theory of Computing (STOC), pp.\u00a0224\u2013233. ACM, New York (1998)"},{"key":"27_CR120","first-page":"531","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"O. Kupferman","year":"2005","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0531\u2013542. IEEE, Piscataway (2005)"},{"key":"27_CR121","unstructured":"Madusudan, P.: Control and synthesis of open reactive systems. Ph.D. thesis, Theoretical Computer Science Group, Institute of Mathematical Sciences, University of Madras (2001)"},{"key":"27_CR122","first-page":"643","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"M. Maidl","year":"2000","unstructured":"Maidl, M.: The common fragment of CTL and LTL. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0643\u2013652. IEEE, Piscataway (2000)"},{"key":"27_CR123","series-title":"LNCS","first-page":"229","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science (STACS)","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a0900, pp.\u00a0229\u2013242. Springer, Heidelberg (1995)"},{"key":"27_CR124","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1992)"},{"key":"27_CR125","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems. Springer, Heidelberg (1995)"},{"issue":"1","key":"27_CR126","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1145\/357233.357237","volume":"6","author":"Z. Manna","year":"1984","unstructured":"Manna, Z., Wolper, P.: Synthesis of communicating processes from temporal logic specifications. Trans. Program. Lang. Syst. 6(1), 68\u201393 (1984)","journal-title":"Trans. Program. Lang. Syst."},{"issue":"4","key":"27_CR127","doi-asserted-by":"crossref","first-page":"1565","DOI":"10.2307\/2586667","volume":"63","author":"D. Martin","year":"1998","unstructured":"Martin, D.: The determinacy of Blackwell games. J. Symb. Log. 63(4), 1565\u20131581 (1998)","journal-title":"J. Symb. Log."},{"key":"27_CR128","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":"27_CR129","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S. Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR130","doi-asserted-by":"crossref","first-page":"263","DOI":"10.2991\/978-94-91216-95-4","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"F. Mogavero","year":"2013","unstructured":"Mogavero, F., Murano, A., Sauro, L.: On the boundary of behavioral strategies. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0263\u2013272 (2013)"},{"key":"27_CR131","series-title":"LIPIcs","first-page":"133","volume-title":"Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"F. Mogavero","year":"2010","unstructured":"Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LIPIcs, vol.\u00a08, pp.\u00a0133\u2013144 (2010)"},{"key":"27_CR132","unstructured":"Morgenstern, A.: Symbolic controller synthesis for LTL specifications. Ph.D. thesis, TU Kaiserslautern (2010)"},{"key":"27_CR133","series-title":"LNCS","first-page":"157","volume-title":"Symposium on Computation Theory","author":"A. Mostowski","year":"1984","unstructured":"Mostowski, A.: Regular expressions for infinite trees and a standard form of automata. In: Symposium on Computation Theory. LNCS, vol.\u00a0208, pp.\u00a0157\u2013168. Springer, Heidelberg (1984)"},{"key":"27_CR134","series-title":"LNCS","first-page":"100","volume-title":"Automata on Infinite Words","author":"D.E. Muller","year":"1984","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite objects, determinacy and Rabin\u2019s theorem. In: Automata on Infinite Words. LNCS, vol.\u00a0192, pp.\u00a0100\u2013107. Springer, Heidelberg (1984)"},{"key":"27_CR135","first-page":"341","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"S. Nain","year":"2013","unstructured":"Nain, S., Vardi, M.Y.: Solving partial-information stochastic parity games. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0341\u2013348. IEEE, Piscataway (2013)"},{"key":"27_CR136","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1287\/moor.12.3.441","volume":"12","author":"C.H. Papadimitriou","year":"1987","unstructured":"Papadimitriou, C.H., Tsitsiklis, J.N.: The complexity of Markov decision processes. Math. Oper. Res. 12, 441\u2013450 (1987)","journal-title":"Math. Oper. Res."},{"key":"27_CR137","first-page":"255","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"N. Piterman","year":"2006","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0255\u2013264. IEEE, Seattle (2006)"},{"key":"27_CR138","first-page":"275","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"N. Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A.: Faster solution of Rabin and Streett games. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0275\u2013284. IEEE, Piscataway (2006)"},{"key":"27_CR139","volume-title":"Handbook of Model Checking","author":"N. Piterman","year":"2018","unstructured":"Piterman, N., Pnueli, A.: Temporal logic and fair discrete systems. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)"},{"key":"27_CR140","series-title":"LNCS","first-page":"364","volume-title":"Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI)","author":"N. Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u00b4ar, Y.: Synthesis of reactive(1) designs. In: Intl. Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI). LNCS, vol.\u00a03855, pp.\u00a0364\u2013380. Springer, Heidelberg (2006)"},{"key":"27_CR141","first-page":"46","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a046\u201357. IEEE, Piscataway (1977)"},{"key":"27_CR142","first-page":"179","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0179\u2013190. ACM, New York (1989)"},{"key":"27_CR143","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Intl. Colloquium on Automata, Languages and Programming (ICALP)","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Intl. Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a0372, pp.\u00a0652\u2013671. Springer, Heidelberg (1989)"},{"key":"27_CR144","first-page":"746","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"A. Pnueli","year":"1990","unstructured":"Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0746\u2013757. IEEE, Piscataway (1990)"},{"key":"27_CR145","series-title":"LNCS","first-page":"592","volume-title":"Intl. Symp. on Mathematical Foundations of Computer Science (MFCS)","author":"B. Puchala","year":"2010","unstructured":"Puchala, B.: Asynchronous omega-regular games with partial information. In: Intl. Symp. on Mathematical Foundations of Computer Science (MFCS). LNCS, vol.\u00a06281, pp.\u00a0592\u2013603. Springer, Heidelberg (2010)"},{"key":"27_CR146","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\u201335 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"27_CR147","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1137\/0325013","volume":"25","author":"P.J. Ramadge","year":"1987","unstructured":"Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete event processes. SIAM J. Control Optim. 25, 206\u2013230 (1987)","journal-title":"SIAM J. Control Optim."},{"key":"27_CR148","doi-asserted-by":"crossref","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. Proc. IEEE 77, 81\u201398 (1989)","journal-title":"Proc. IEEE"},{"key":"27_CR149","first-page":"288","volume-title":"Annual ACM Symposium on Theory of Computing (STOC)","author":"J.H. Reif","year":"1979","unstructured":"Reif, J.H.: Universal games of incomplete information. In: Annual ACM Symposium on Theory of Computing (STOC), pp.\u00a0288\u2013308. ACM, New York (1979)"},{"key":"27_CR150","unstructured":"Rosner, R.: Modular synthesis of reactive systems. Ph.D. thesis, Weizmann Institute of Science (1992)"},{"key":"27_CR151","first-page":"319","volume-title":"Annual Symp. on Foundations of Computer Science (FOCS)","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9$\\omega$-automata. In: Annual Symp. on Foundations of Computer Science (FOCS), pp.\u00a0319\u2013327. IEEE, Piscataway (1988)"},{"key":"27_CR152","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/11901914_20","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"S. Schewe","year":"2006","unstructured":"Schewe, S.: Synthesis for probabilistic environments. In: Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a04218, pp.\u00a0245\u2013259. Springer, Heidelberg (2006)"},{"key":"27_CR153","series-title":"LNCS","first-page":"449","volume-title":"Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS)","author":"S. Schewe","year":"2007","unstructured":"Schewe, S.: Solving parity games in big steps. In: Annual Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS). LNCS, vol.\u00a04855, pp.\u00a0449\u2013460. Springer, Heidelberg (2007)"},{"key":"27_CR154","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/978-3-540-87531-4_27","volume-title":"Annual Conf. on Computer Science Logic (CSL)","author":"S. Schewe","year":"2008","unstructured":"Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: Annual Conf. on Computer Science Logic (CSL). LNCS, vol.\u00a05213, pp.\u00a0369\u2013384. Springer, Heidelberg (2008)"},{"key":"27_CR155","series-title":"LNCS","first-page":"127","volume-title":"Intl. Sym. on Logic-Based Program Synthesis and Transformation, 16th International (LOPSTR)","author":"S. Schewe","year":"2006","unstructured":"Schewe, S., Finkbeiner, B.: Synthesis of asynchronous systems. In: Intl. Sym. on Logic-Based Program Synthesis and Transformation, 16th International (LOPSTR). LNCS, vol.\u00a04407, pp.\u00a0127\u2013142. Springer, Heidelberg (2006)"},{"key":"27_CR156","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Intl. Symp. Automated Technology for Verification and Analysis (ATVA)","author":"S. Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Intl. Symp. Automated Technology for Verification and Analysis (ATVA). LNCS, vol.\u00a04762, pp.\u00a0474\u2013488. Springer, Heidelberg (2007)"},{"key":"27_CR157","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Intl. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). LNCS, vol.\u00a02250, pp.\u00a039\u201354. Springer, Heidelberg (2001)"},{"key":"27_CR158","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"126","DOI":"10.1007\/978-3-540-39724-3_12","volume-title":"Correct Hardware Design and Verification Methods (CHARME)","author":"R. Sebastiani","year":"2003","unstructured":"Sebastiani, R., Tonetta, S.: \u201cMore deterministic\u201d vs. \u201csmaller\u201d B\u00fcchi automata for efficient LTL model checking. In: Correct Hardware Design and Verification Methods (CHARME). LNCS, vol.\u00a02860, pp.\u00a0126\u2013140. Springer, Heidelberg (2003)"},{"key":"27_CR159","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.1073\/pnas.39.10.1953","volume":"39","author":"L. Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. USA 39, 1095\u20131100 (1953)","journal-title":"Proc. Natl. Acad. Sci. USA"},{"key":"27_CR160","first-page":"77","volume-title":"Formal Methods in Computer Aided Design (FMCAD)","author":"S. Sohail","year":"2009","unstructured":"Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for LTL games. In: Formal Methods in Computer Aided Design (FMCAD), pp.\u00a077\u201384. IEEE, Piscataway (2009)"},{"key":"27_CR161","first-page":"136","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"A. Solar-Lezama","year":"2008","unstructured":"Solar-Lezama, A., Jones, C.G., Bod\u00edk, R.: Sketching concurrent data structures. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0136\u2013148. ACM, New York (2008)"},{"key":"27_CR162","first-page":"281","volume-title":"Conf. on Programming Language Design and Implementation (PLDI)","author":"A. Solar-Lezama","year":"2005","unstructured":"Solar-Lezama, A., Rabbah, R.M., Bod\u00edk, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: Conf. on Programming Language Design and Implementation (PLDI), pp.\u00a0281\u2013294. ACM, New York (2005)"},{"key":"27_CR163","first-page":"404","volume-title":"Architectural Support for Programming Languages and Operating Systems (ASPLOS)","author":"A. Solar-Lezama","year":"2006","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Architectural Support for Programming Languages and Operating Systems (ASPLOS), pp.\u00a0404\u2013415. ACM, New York (2006)"},{"key":"27_CR164","unstructured":"Somenzi, F.: Colorado University Decision Diagram Package (1998). http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"27_CR165","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient B\u00fcchi automata from LTL formulae. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0248\u2013263. Springer, Heidelberg (2000)"},{"key":"27_CR166","unstructured":"Stockmeyer, L.: The complexity of decision problems in automata theory and logic. Ph.D. thesis, Massachusetts Institute of Technology (1974)"},{"key":"27_CR167","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp.\u00a0133\u2013191. Elsevier, Amsterdam (1990)"},{"key":"27_CR168","series-title":"LNCS","first-page":"1","volume-title":"Annual Symposium on Theoretical Aspects of Computer Science (STACS)","author":"W. Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Annual Symposium on Theoretical Aspects of Computer Science (STACS). LNCS, vol.\u00a0900, pp.\u00a01\u201313. Springer, Heidelberg (1995)"},{"key":"27_CR169","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/978-3-642-59126-6_7","volume-title":"Handbook of Formal Languages","author":"W. Thomas","year":"1997","unstructured":"Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, vol.\u00a03, pp.\u00a0389\u2013455. Springer, Heidelberg (1997). Beyond Words, Chap.\u00a07"},{"key":"27_CR170","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/3-540-60045-0_56","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: An automata-theoretic approach to fair realizability and synthesis. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a0939, pp.\u00a0267\u2013278. Springer, Heidelberg (1995)"},{"issue":"1","key":"27_CR171","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"27_CR172","series-title":"LNCS","first-page":"139","volume-title":"Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M.T. Vechev","year":"2009","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Inferring synchronization under limited observability. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a05505, pp.\u00a0139\u2013154. Springer, Heidelberg (2009)"},{"key":"27_CR173","first-page":"327","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"M.T. Vechev","year":"2010","unstructured":"Vechev, M.T., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0327\u2013338. ACM, New York (2010)"},{"key":"27_CR174","series-title":"LNCS","first-page":"275","volume-title":"Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS)","author":"Y. Velner","year":"2011","unstructured":"Velner, Y., Rabinovich, A.: Church synthesis problem for noisy input. In: Intl. Conf. on Foundations of Software Science and Computational Structures (FoSSaCS). LNCS, vol.\u00a06604, pp.\u00a0275\u2013289. Springer, Heidelberg (2011)"},{"key":"27_CR175","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. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01855, pp.\u00a0202\u2013215. Springer, Heidelberg (2000)"},{"key":"27_CR176","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Intl. Conf. on Computer-Aided Verification (CAV)","author":"I. Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Pushdown processes: games and model checking. In: Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol.\u00a01102, pp.\u00a062\u201374. Springer, Heidelberg (1996)"},{"issue":"2","key":"27_CR177","doi-asserted-by":"crossref","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. Inf. Comput. 164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."},{"key":"27_CR178","first-page":"356","volume-title":"Symp. on Logic in Computer Science (LICS)","author":"I. Walukiewicz","year":"2004","unstructured":"Walukiewicz, I.: A landscape with games in the background. In: Symp. on Logic in Computer Science (LICS), pp.\u00a0356\u2013366. IEEE, Piscataway (2004)"},{"key":"27_CR179","first-page":"252","volume-title":"Symp. on Principles of Programming Languages (POPL)","author":"Y. Wang","year":"2009","unstructured":"Wang, Y., Lafortune, S., Kelly, T., Kudlur, M., Mahlke, S.A.: The theory of deadlock avoidance via discrete control. In: Symp. on Principles of Programming Languages (POPL), pp.\u00a0252\u2013263. ACM, New York (2009)"},{"issue":"1\u20132","key":"27_CR180","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(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."},{"key":"27_CR181","doi-asserted-by":"crossref","first-page":"343","DOI":"10.1016\/0304-3975(95)00188-3","volume":"158","author":"U. Zwick","year":"1996","unstructured":"Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158, 343\u2013359 (1996)","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_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,2]],"date-time":"2023-09-02T18:19:19Z","timestamp":1693678759000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":181,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_27","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}