{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:43Z","timestamp":1760202643402,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642329395"},{"type":"electronic","value":"9783642329401"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32940-1_14","type":"book-chapter","created":{"date-parts":[[2012,9,1]],"date-time":"2012-09-01T20:47:02Z","timestamp":1346532422000},"page":"177-192","source":"Crossref","is-referenced-by-count":7,"title":["Quantified CTL: Expressiveness and Model Checking"],"prefix":"10.1007","author":[{"given":"Arnaud","family":"Da Costa","sequence":"first","affiliation":[]},{"given":"Fran\u00e7ois","family":"Laroussinie","sequence":"additional","affiliation":[]},{"given":"Nicolas","family":"Markey","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"5","key":"14_CR1","first-page":"672","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J.\u00a0ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"J.\u00a0ACM"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-540-92687-0_7","volume-title":"Logical Foundations of Computer Science","author":"T. Brihaye","year":"2008","unstructured":"Brihaye, T., Da Costa, A., Laroussinie, F., Markey, N.: ATL with Strategy Contexts and Bounded Memory. In: Artemov, S., Nerode, A. (eds.) LFCS 2009. LNCS, vol.\u00a05407, pp. 92\u2013106. Springer, Heidelberg (2008)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/3-540-48683-6_25","volume-title":"Computer Aided Verification","author":"G. Bruns","year":"1999","unstructured":"Bruns, G., Godefroid, P.: Model Checking Partial State Spaces with 3-Valued Temporal Logics. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 274\u2013287. Springer, Heidelberg (1999)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-540-74407-8_5","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Strategy Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 59\u201373. Springer, Heidelberg (2007)"},{"key":"14_CR5","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.M. Clarke","year":"1982","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 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic, a Language Theoretic Approach. Cambridge University Press (2011)","DOI":"10.1017\/CBO9780511977619"},{"key":"14_CR7","unstructured":"Da Costa, A., Laroussinie, F., Markey, N.: ATL with strategy contexts: Expressiveness and model checking. In: FSTTCS 2010. LIPIcs, vol.\u00a08, pp. 120\u2013132. LZI (2010)"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Da Costa, A., Laroussinie, F., Markey, N.: Quantified\u00a0CTL: expressiveness and model checking. Research Report LSV-12-02, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France (2012)","DOI":"10.1007\/978-3-642-32940-1_14"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Ebbinghaus, H.-D., Flum, J.: Finite Model Theory. Springer (1995)","DOI":"10.1007\/3-540-28788-4"},{"issue":"1","key":"14_CR10","first-page":"151","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: On\u00a0branching versus linear time temporal logic. J.\u00a0ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J.\u00a0ACM"},{"issue":"3","key":"14_CR11","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E.A. Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf.& Cont.\u00a061(3), 175\u2013201 (1984)","journal-title":"Inf.& Cont."},{"key":"14_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-45656-2_15","volume-title":"AI 2001: Advances in Artificial Intelligence","author":"T. French","year":"2001","unstructured":"French, T.: Decidability of Quantifed Propositional Branching Time Logics. In: Stumptner, M., Corbett, D.R., Brooks, M. (eds.) AI 2001. LNCS (LNAI), vol.\u00a02256, pp. 165\u2013176. Springer, Heidelberg (2001)"},{"issue":"2","key":"14_CR13","first-page":"421","volume":"42","author":"G. Gottlob","year":"1995","unstructured":"Gottlob, G.: NP trees and Carnap\u2019s modal logic. J.\u00a0ACM\u00a042(2), 421\u2013457 (1995)","journal-title":"J.\u00a0ACM"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: A complete proof systems for QPTL. In: LICS 1995, pp. 2\u201312. IEEE Comp. Soc. Press (1995)","DOI":"10.1109\/LICS.1995.523239"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/3-540-60045-0_60","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O.: Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 325\u2013338. Springer, Heidelberg (1995)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/3-540-44618-4_9","volume-title":"CONCUR 2000 - Concurrency Theory","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open Systems in Reactive Environments: Control and Synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 92\u2013107. Springer, Heidelberg (2000)"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: STOC 1998, pp. 224\u2013233. ACM Press (1998)","DOI":"10.1145\/276698.276748"},{"issue":"2","key":"14_CR18","first-page":"312","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model-checking. J.\u00a0ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J.\u00a0ACM"},{"key":"14_CR19","unstructured":"Mogavero, F., Murano, A., Vardi, M.Y.: Reasoning about strategies. In: FSTTCS 2010. LIPIcs, vol.\u00a08, pp. 133\u2013144. LZI (2010)"},{"issue":"1","key":"14_CR20","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0890-5401(03)00104-4","volume":"184","author":"F. Moller","year":"2003","unstructured":"Moller, F., Rabinovich, A.: Counting on CTL*: on\u00a0the expressive power of monadic path logic. Inf.& Comp.\u00a0184(1), 147\u2013159 (2003)","journal-title":"Inf.& Comp."},{"issue":"2-3","key":"14_CR21","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. TCS\u00a054(2-3), 267\u2013276 (1987)","journal-title":"TCS"},{"issue":"1-2","key":"14_CR22","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","volume":"141","author":"D.E. Muller","year":"1995","unstructured":"Muller, D.E., Schupp, P.E.: Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra. TCS\u00a0141(1-2), 69\u2013107 (1995)","journal-title":"TCS"},{"issue":"3","key":"14_CR23","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/S0020-0190(01)00260-5","volume":"82","author":"A.C. Patthak","year":"2002","unstructured":"Patthak, A.C., Bhattacharya, I., Dasgupta, A., Dasgupta, P., Chakrabarti, P.P.: Quantified computation tree logic. IPL\u00a082(3), 123\u2013129 (2002)","journal-title":"IPL"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-540-75596-8_19","volume-title":"Automated Technology for Verification and Analysis","author":"S. Pinchinat","year":"2007","unstructured":"Pinchinat, S.: A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 253\u2013267. Springer, Heidelberg (2007)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE Comp. Soc. Press (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"14_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"642","DOI":"10.1007\/978-3-540-45138-9_58","volume-title":"Mathematical Foundations of Computer Science 2003","author":"S. Riedweg","year":"2003","unstructured":"Riedweg, S., Pinchinat, S.: Quantified Mu-Calculus for Control Synthesis. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 642\u2013651. Springer, Heidelberg (2003)"},{"key":"14_CR28","unstructured":"Sistla, A.P.: Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, Cambridge, Massachussets, USA (1983)"},{"key":"14_CR29","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","volume":"49","author":"A.P. Sistla","year":"1987","unstructured":"Sistla, A.P., Vardi, M.Y., Wolper, P.: The complementation problem for B\u00fcchi automata with applications to temporal logics. TCS\u00a049, 217\u2013237 (1987)","journal-title":"TCS"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Languages, automata and logics. In: Handbook of Formal Languages, pp. 389\u2013455. Springer (1997)","DOI":"10.1007\/978-3-642-59126-6_7"},{"key":"14_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: The complexity of relational query languages. In: STOC 1982, pp. 137\u2013146. ACM Press (1982)","DOI":"10.1145\/800070.802186"},{"key":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"466","DOI":"10.1007\/978-3-642-23217-6_31","volume-title":"CONCUR 2011 \u2013 Concurrency Theory","author":"F. Wang","year":"2011","unstructured":"Wang, F., Huang, C.-H., Yu, F.: A Temporal Logic for the Interaction of Strategies. In: Katoen, J.-P., K\u00f6nig, B. (eds.) CONCUR 2011. LNCS, vol.\u00a06901, pp. 466\u2013481. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2012 \u2013 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32940-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T18:06:34Z","timestamp":1744049194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32940-1_14"}},"subtitle":["(Extended Abstract)"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329395","9783642329401"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32940-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}