{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:36Z","timestamp":1760202576161},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705826"},{"type":"electronic","value":"9783540705833"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-70583-3_31","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"373-385","source":"Crossref","is-referenced-by-count":23,"title":["ATL* Satisfiability Is 2EXPTIME-Complete"],"prefix":"10.1007","author":[{"given":"Sven","family":"Schewe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","unstructured":"Wolper, P.: Synthesis of Communicating Processes from Temporal-Logic Specifications. PhD thesis, Stanford University (1982)"},{"key":"31_CR2","first-page":"52","volume-title":"Proc. IBM Workshop on Logics 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: Proc. IBM Workshop on Logics of Programs, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"31_CR3","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, 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"key":"31_CR4","first-page":"995","volume-title":"Temporal and modal logic","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic, pp. 995\u20131072. MIT Press, Cambridge (1990)"},{"key":"31_CR5","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. Transactions On Programming Languages and Systems\u00a08, 244\u2013263 (1986)","journal-title":"Transactions On Programming Languages and Systems"},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM\u00a047, 312\u2013360 (2000)","journal-title":"Journal of the ACM"},{"key":"31_CR7","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1093\/logcom\/exl009","volume":"16","author":"D. Walther","year":"2006","unstructured":"Walther, D., Lutz, C., Wolter, F., Wooldridge, M.: Atl satisfiability is indeed exptime-complete. Journal of Logic and Computation\u00a016, 765\u2013787 (2006)","journal-title":"Journal of Logic and Computation"},{"key":"31_CR8","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, 399\u2013430 (2003)","journal-title":"Journal of Computer Security"},{"key":"31_CR9","first-page":"591","volume-title":"Proc. CSL","author":"S. Schewe","year":"2006","unstructured":"Schewe, S., Finkbeiner, B.: Satisfiability and finite model property for the alternating-time \u03bc-calculus. In: Proc. CSL, pp. 591\u2013605. Springer, Heidelberg (2006)"},{"key":"31_CR10","unstructured":"Even, S., Yacobi, Y.: Relations among public key signature systems. Technical Report 175, Technion, Haifa, Israel (1980)"},{"key":"31_CR11","first-page":"279","volume-title":"Proc. LICS","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for omega-regular objectives. In: Proc. LICS, pp. 279\u2013290. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"31_CR12","first-page":"208","volume-title":"Proc. LICS","author":"G. Drimmelen van","year":"2003","unstructured":"van Drimmelen, G.: Satisfiability in alternating-time temporal logic. In: Proc. LICS, pp. 208\u2013217. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"Wilke, T.: Alternating tree automata, parity games, and modal \u03bc-calculus. Bull. Soc. Math. Belg.\u00a08 (2001)","DOI":"10.36045\/bbms\/1102714178"},{"key":"31_CR14","doi-asserted-by":"publisher","first-page":"245","DOI":"10.2307\/421091","volume":"5","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Church\u2019s problem revisited. The bulletin of Symbolic Logic\u00a05, 245\u2013263 (1999)","journal-title":"The bulletin of Symbolic Logic"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Wilke","year":"1999","unstructured":"Wilke, T.: CTL\u2009+\u2009 is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 110\u2013121. Springer, Heidelberg (1999)"},{"key":"31_CR16","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Safraless decision procedures. In: Proc. 46th IEEE Symp. on Foundations of Computer Science, Pittsburgh, pp. 531\u2013540 (2005)","DOI":"10.1109\/SFCS.2005.66"},{"key":"31_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"key":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"S. Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 474\u2013488. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70583-3_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T05:07:59Z","timestamp":1605762479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70583-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540705826","9783540705833"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70583-3_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}