{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:08:01Z","timestamp":1725829681365},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_3","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"22-37","source":"Crossref","is-referenced-by-count":1,"title":["A Tableau for Bundled Strategies"],"prefix":"10.1007","author":[{"given":"John","family":"McCabe-Dansted","sequence":"first","affiliation":[]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"issue":"5","key":"3_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 (JACM)\u00a049(5), 672\u2013713 (2002)","journal-title":"Journal of the ACM (JACM)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1007\/978-3-319-08587-6_21","volume-title":"Automated Reasoning","author":"S. Cerrito","year":"2014","unstructured":"Cerrito, S., David, A., Goranko, V.: Optimal tableaux-based decision procedure for testing satisfiability in the alternating-time temporal logic ATL+. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol.\u00a08562, pp. 277\u2013291. Springer, Heidelberg (2014)"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"David, A.: Deciding ATL* satisfiability by tableaux. Technical report, Laboratoire IBISC \u2013 Universit\u00e9 d\u2019\u00c9vry Val-d\u2019Essonne (2015), https:\/\/www.ibisc.univ-evry.fr\/~adavid\/fichiers\/cade15_tableaux_atl_star_long.pdf (retrieved)","DOI":"10.1007\/978-3-319-21401-6_14"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"McCabe-Dansted, J.C., Reynolds, M.: EXPTIME fairness with bundled CTL. In: Cesta, A., Combi, C., Laroussinie, F. (eds.) Proceedings of the International Symposium on Temporal Representation and Reasoning, TIME 2014, pp. 164\u2013173 (2014), http:\/\/www.csse.uwa.edu.au\/~john\/papers\/ExpFair.pdf","DOI":"10.1109\/TIME.2014.22"},{"issue":"1","key":"3_CR5","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1093\/logcom\/exl033","volume":"17","author":"M. Reynolds","year":"2007","unstructured":"Reynolds, M.: A tableau for Bundled CTL*. Journal of Logic and Computation\u00a017(1), 117\u2013132 (2007)","journal-title":"Journal of Logic and Computation"},{"issue":"6","key":"3_CR6","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1007\/s00165-011-0193-4","volume":"23","author":"M. Reynolds","year":"2011","unstructured":"Reynolds, M.: A tableau-based decision procedure for CTL*. Formal Aspects of Computing\u00a023(6), 739\u2013779 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-540-70583-3_31","volume-title":"Automata, Languages and Programming","author":"S. Schewe","year":"2008","unstructured":"Schewe, S.: ATL* satisfiability is 2EXPTIME-complete. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L.A., Halld\u00f3rsson, M.M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol.\u00a05126, pp. 373\u2013385. Springer, Heidelberg (2008)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-642-14203-1_28","volume-title":"Automated Reasoning","author":"O. Friedmann","year":"2010","unstructured":"Friedmann, O., Latte, M., Lange, M.: A decision procedure for CTL* based on tableaux and automata. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 331\u2013345. Springer, Heidelberg (2010)"},{"issue":"4","key":"3_CR9","doi-asserted-by":"publisher","first-page":"679","DOI":"10.1093\/logcom\/12.4.679","volume":"12","author":"M. Reynolds","year":"2002","unstructured":"Reynolds, M.: Axioms for branching time. Journal of Logic and Computation\u00a012(4), 679\u2013697 (2002)","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"3_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1093\/logcom\/14.1.3","volume":"14","author":"S. Bauer","year":"2004","unstructured":"Bauer, S., Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: On non-local propositional and weak monodic quantified CTL*. Journal of Logic and Computation\u00a014(1), 3\u201322 (2004)","journal-title":"Journal of Logic and Computation"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"McCabe-Dansted, J.C., Reynolds, M.: Verification of rewrite rules for computation tree logics. In: Cesta, A., Combi, C., Laroussinie, F. (eds.) Proceedings of the International Symposium on Temporal Representation and Reasoning, TIME 2014, pp. 142\u2013151. IEEE Computer Society (2014), http:\/\/www.csse.uwa.edu.au\/~john\/papers\/Rewrite-Long.pdf","DOI":"10.1109\/TIME.2014.25"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"McCabe-Dansted, J.C., Reynolds, M.: A tableau for bundled strategies (expanded version) (2015) http:\/\/www.csse.uwa.edu.au\/~john\/papers\/BATL-Long.pdf","DOI":"10.1007\/978-3-319-24312-2_3"},{"key":"3_CR13","unstructured":"McCabe-Dansted, J.C.: Improved BCTL* tableau applet (2011) http:\/\/www.csse.uwa.edu.au\/~john\/BCTL2\/"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"McCabe-Dansted, J.C.: A rooted tableau for BCTL*. In: The International Methods for Modalities Workshop, vol. 278, pp. 145\u2013158. Elsevier Science Publishers B. V., Amsterdam, November 2011, http:\/\/www.csse.uwa.edu.au\/~john\/papers\/Rooted_BCTL_Tableau.pdf","DOI":"10.1016\/j.entcs.2011.10.012"},{"issue":"1","key":"3_CR15","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"E.A. Emerson","year":"2000","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM Journal on Computing\u00a029(1), 132\u2013158 (2000)","journal-title":"SIAM Journal on Computing"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-12896-4_363","volume-title":"Logics of Programs","author":"E.A. Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding branching time logic: A triple exponential decision procedure for CTL*. In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol.\u00a0164, pp. 176\u2013192. Springer, Heidelberg (1984)"},{"key":"3_CR17","first-page":"14","volume-title":"STOC 1984: Proceedings of the 16th Annual ACM Symposium on Theory of Computing","author":"E.A. Emerson","year":"1984","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC 1984: Proceedings of the 16th Annual ACM Symposium on Theory of Computing, pp. 14\u201324. ACM Press, New York (1984)"},{"key":"3_CR18","first-page":"240","volume-title":"Proceedings of the 17th Annual ACM Symposium on Theory of Computing, STOC 1985","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y., Stockmeyer, L.J.: Improved upper and lower bounds for modal logics of programs. In: Proceedings of the 17th Annual ACM Symposium on Theory of Computing, STOC 1985, pp. 240\u2013251. ACM, New York (1985)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,21]],"date-time":"2022-05-21T16:23:07Z","timestamp":1653150187000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}