{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:29Z","timestamp":1725558989553},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540253334"},{"type":"electronic","value":"9783540319801"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31980-1_31","type":"book-chapter","created":{"date-parts":[[2010,7,11]],"date-time":"2010-07-11T22:44:59Z","timestamp":1278888299000},"page":"477-492","source":"Crossref","is-referenced-by-count":20,"title":["A New Algorithm for Strategy Synthesis in LTL Games"],"prefix":"10.1007","author":[{"given":"Aidan","family":"Harding","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Ryan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre-Yves","family":"Schobbens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"5","key":"31_CR1","doi-asserted-by":"publisher","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. Journal of the ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"issue":"1","key":"31_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R. Alur","year":"2004","unstructured":"Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Transactions on Computational Logic\u00a05(1), 1\u201325 (2004)","journal-title":"ACM Transactions on Computational Logic"},{"key":"31_CR3","unstructured":"SMV 10-11-02p1 (November 2002), \n                    \n                      http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/smv\/"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-58179-0_72","volume-title":"Computer Aided Verification","author":"E. Clarke","year":"1994","unstructured":"Clarke, E., Grumberg, O., Hamaguchi, K.: Another look at LTL model checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 415\u2013427. Springer, Heidelberg (1994)"},{"key":"31_CR5","unstructured":"CuDD: Colorado university decision diagram package, release 2.30 (February 2001), \n                    \n                      http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"31_CR6","first-page":"995","volume-title":"chapter Temporal and Modal Logic","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Handbook of Theoretical Computer Science. In: chapter Temporal and Modal Logic, vol.\u00a0B, pp. 995\u20131072. Elsevier, Amsterdam (1990)"},{"key":"31_CR7","unstructured":"Emerson, E.A., Lei, C.: Efficient model checking in fragments of the propositional model mu-calculus. In: IEEE Symposium on Logic in Computer Science, pp. 267\u2013278 (June 1986)"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Logic, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500. Springer, Heidelberg (2002)"},{"issue":"3","key":"31_CR9","doi-asserted-by":"crossref","first-page":"399","DOI":"10.3233\/JCS-2003-11307","volume":"11","author":"S. Kremer","year":"2003","unstructured":"Kremer, S., Raskin, J.-F.: A game-based verification of non-repudiation and fair exchange protocols. Journal Of Computer Security\u00a011(3), 399\u2013429 (2003)","journal-title":"Journal Of Computer Security"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1996","unstructured":"Kupferman, O., Vardi, M.Y.: Module checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 75\u201386. Springer, Heidelberg (1996)"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"C. L\u00f6ding","year":"1999","unstructured":"L\u00f6ding, C.: Optimal bounds for the transformation of \u03c9-automata. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 97\u2013109. Springer, Heidelberg (1999)"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings Of 16th ACM Symposium On Principles Of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"31_CR13","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science, Rehovot, Israel (1992)"},{"key":"31_CR14","unstructured":"Safra, S.: Complexity of Automata on Infinite Objects. PhD thesis, The Weizmann Institute of Science, Rehovot, Israel (March 1989)"},{"key":"31_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/3-540-45653-8_3","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K. Schneider","year":"2001","unstructured":"Schneider, K.: Improving automata generation for linear temporal logic by considering the automaton hierarchy. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, p. 39. Springer, Heidelberg (2001)"},{"key":"31_CR16","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/3-540-36126-X_6","volume-title":"Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design","author":"F. Somenzi","year":"2002","unstructured":"Somenzi, F., Ravi, K., Bloem, R.: Analysis of symbolic scc hull algorithms. In: Proceedings of the 4th International Conference on Formal Methods in Computer-Aided Design, pp. 88\u2013105. Springer, Heidelberg (2002)"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/3-540-60385-9_16","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Tasiran","year":"1995","unstructured":"Tasiran, S., Hojati, R., Brayton, R.K.: Language containment using non-deterministic omega-automata. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol.\u00a0987, pp. 261\u2013277. Springer, Heidelberg (1995)"},{"key":"31_CR18","first-page":"133","volume-title":"chapter Automata on Infinite Objects","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Handbook of Theoretical Computer Science. In: chapter Automata on Infinite Objects, vol.\u00a0B, pp. 133\u2013192. Elsevier, Amsterdam (1990)"},{"key":"31_CR19","doi-asserted-by":"crossref","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Symposium on Theoretical Aspects of Computer Science, pp. 1\u201313 (1995)","DOI":"10.1007\/3-540-59042-0_57"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/3-540-45089-0_3","volume-title":"Implementation and Application of Automata","author":"N. Wallmeier","year":"2003","unstructured":"Wallmeier, N., H\u00fctten, P., Thomas, W.: Symbolic synthesis of finite-state controllers for request-response specifications. In: Ibarra, O.H., Dang, Z. (eds.) CIAA 2003. LNCS, vol.\u00a02759, pp. 11\u201322. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31980-1_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T03:44:37Z","timestamp":1620013477000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31980-1_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253334","9783540319801"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31980-1_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}