{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:11:51Z","timestamp":1760202711227,"version":"3.37.3"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2017,4,19]],"date-time":"2017-04-19T00:00:00Z","timestamp":1492560000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,4,19]],"date-time":"2017-04-19T00:00:00Z","timestamp":1492560000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP140103365"],"award-info":[{"award-number":["DP140103365"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2017,8]]},"DOI":"10.1007\/s10472-017-9546-x","type":"journal-article","created":{"date-parts":[[2017,4,19]],"date-time":"2017-04-19T11:13:58Z","timestamp":1492600438000},"page":"317-364","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["To be fair, use bundles"],"prefix":"10.1007","volume":"80","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4343-4119","authenticated-orcid":false,"given":"John","family":"McCabe-Dansted","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,4,19]]},"reference":[{"key":"9546_CR1","doi-asserted-by":"crossref","unstructured":"Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. In: POPL \u201981: Proceedings of the 8th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp 164\u2013176. ACM, New York, NY, USA (1981)","DOI":"10.1145\/567532.567551"},{"issue":"3","key":"9546_CR2","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/s10472-006-9018-1","volume":"46","author":"A Bolotov","year":"2006","unstructured":"Bolotov, A., Basukoski, A.: A clausal resolution method for branching-time logic ECTL+. Ann. Math. Artif. Intell. 46(3), 235\u2013263 (2006)","journal-title":"Ann. Math. Artif. Intell."},{"key":"9546_CR3","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"MC Browne","year":"1988","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115\u2013131 (1988)","journal-title":"Theor. Comput. Sci."},{"key":"9546_CR4","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L.: Sequential circuit verification using symbolic model checking. In: Design Automation Conference, 1990. Proceedings. 27th ACM\/IEEE, pp. 46\u201351. IEEE (1990)","DOI":"10.1145\/123186.123223"},{"key":"9546_CR5","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Vardi, M.Y., Wolper, P.: Reasoning about fair concurrent programs. In: Proceedings of the Eighteenth Annual ACM Symposium on Theory of Computing, pp. 283\u2013294. ACM (1986)","DOI":"10.1145\/12130.12159"},{"key":"9546_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. In: STOC, pp. 169\u2013180. ACM (1982)","DOI":"10.1145\/800070.802190"},{"issue":"1","key":"9546_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"EA Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985). doi:\n                    10.1016\/0022-0000(85)90001-7","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"9546_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"issue":"1","key":"9546_CR9","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"EA Emerson","year":"2000","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132\u2013158 (2000)","journal-title":"SIAM J. Comput."},{"issue":"3","key":"9546_CR10","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"EA Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program. 8(3), 275\u2013306 (1987)","journal-title":"Sci. Comput. Program."},{"key":"9546_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding Branching Time Logic: a Triple Exponential Decision Procedure for CTL*. In: E. M. Clarke and D. Kozen, editors, Logic of Programs, volume 164, pages 176\u2013192. Springer-Verlag (1983)","DOI":"10.1007\/3-540-12896-4_363"},{"key":"9546_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Sistla, A.P.: Deciding branching time logic. In: STOC \u201984: Proceedings of the 16th Annual ACM Symposium on Theory of Computing, pp 14\u201324. ACM Press, New York, NY, USA (1984)","DOI":"10.1145\/800057.808661"},{"key":"9546_CR13","doi-asserted-by":"crossref","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, vol. 6173, pp. 331\u2013345. Springer (2010)","DOI":"10.1007\/978-3-642-14203-1_28"},{"key":"9546_CR14","doi-asserted-by":"crossref","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: POPL \u201980: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp 163\u2013173. ACM, New York, NY, USA (1980)","DOI":"10.1145\/567446.567462"},{"key":"9546_CR15","doi-asserted-by":"crossref","unstructured":"Gor\u00e9, R., Thomson, J., Widmann, F.: An experimental comparison of theorem provers for CTL. In: Combi, C., Leucker, M., Wolter, F. (eds.) Proceedings of the 18th International Symposium on Temporal Representation and Reasoning, pp. 49\u201356. IEEE (2011)","DOI":"10.1109\/TIME.2011.16"},{"key":"9546_CR16","doi-asserted-by":"crossref","unstructured":"Johannsen, J., Lange, M.: CTL+ is complete for double exponential time. In: Automata, Languages and Programming, pp. 767\u2013775. Springer (2003)","DOI":"10.1007\/3-540-45061-0_60"},{"issue":"3","key":"9546_CR17","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0019-9958(82)91022-1","volume":"53","author":"DJ Lehmann","year":"1982","unstructured":"Lehmann, D.J., Shelah, S.: Reasoning with time and chance. Inf. Control. 53(3), 165\u2013198 (1982)","journal-title":"Inf. Control."},{"key":"9546_CR18","unstructured":"Marrero, W.: Using BDDs to decide CTL. In: TACAS\u201905, pp 222\u2013236. Springer, Berlin, Heidelberg (2005). See also third party implementation at \n                    http:\/\/rsise.anu.edu.au\/~rpg\/CTLProvers\/bddctl.tgz"},{"issue":"6","key":"9546_CR19","doi-asserted-by":"publisher","first-page":"1093","DOI":"10.1093\/logcom\/exq028","volume":"21","author":"A Masini","year":"2011","unstructured":"Masini, A., Vigan\u00f3, L., Volpe, M.: Labelled natural deduction for a bundled branching temporal logic. J. Log. Comput. 21(6), 1093\u20131163 (2011)","journal-title":"J. Log. Comput."},{"key":"9546_CR20","unstructured":"McCabe-Dansted, J.C.: A rooted tableau for BCTL*. In: The International Methods for Modalities Workshop, vol. 278, pp 145\u2013158. Amsterdam, The Netherlands (2011). Elsevier Science Publishers B. V. see also expanded version: \n                    http:\/\/staffhome.ecm.uwa.edu.au\/~00061811\/papers\/Rooted_BCTL_Tableau.pdf"},{"key":"9546_CR21","doi-asserted-by":"crossref","unstructured":"McCabe-Dansted, J.C.: A Tableau for the Combination of CTL and BCTL*. In: B. Moszkowski, M. Reynolds, and P. Terenziani, editors, Proceedings of the International Symposium on Temporal Representation and Reasoning, pages 29\u201336. IEEE Computer Society (2012)","DOI":"10.1109\/TIME.2012.17"},{"issue":"1","key":"9546_CR22","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*. J. Log. Comput. 17(1), 117\u2013132 (2007)","journal-title":"J. Log. Comput."},{"key":"9546_CR23","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s00165-010-0168-x","volume":"23","author":"M Reynolds","year":"2011","unstructured":"Reynolds, M.: A tableau-based decision procedure for CTL*. Journal of Formal Aspects of Computing 23, 1\u201341 (2011)","journal-title":"Journal of Formal Aspects of Computing"},{"key":"9546_CR24","doi-asserted-by":"crossref","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), pp 240\u2013251. ACM, New York, NY, USA (1985)","DOI":"10.1145\/22145.22173"},{"key":"9546_CR25","unstructured":"Wan, W., Bentahar, J., Yahyaoui, H., Ben Hamza, A.: Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications. Appl. Intell. 45(3), 747\u2013776 (2016)"},{"key":"9546_CR26","doi-asserted-by":"crossref","unstructured":"Wilke, T.: CTL+ is Exponentially More Succinct than CTL. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13\u201315, 1999, Proceedings, vol. 1738, pp. 110\u2013121. Springer (1999)","DOI":"10.1007\/3-540-46691-6_9"},{"issue":"1","key":"9546_CR27","first-page":"10","volume":"15","author":"L Zhang","year":"2014","unstructured":"Zhang, L., Hustadt, U., Dixon, C.: A resolution calculus for the branching-time temporal logic CTL. ACM Trans. Comput. Log. (TOCL) 15(1), 10 (2014)","journal-title":"ACM Trans. Comput. Log. (TOCL)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-017-9546-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-017-9546-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-017-9546-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,5,16]],"date-time":"2020-05-16T20:51:03Z","timestamp":1589662263000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-017-9546-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,4,19]]},"references-count":27,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2017,8]]}},"alternative-id":["9546"],"URL":"https:\/\/doi.org\/10.1007\/s10472-017-9546-x","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2017,4,19]]},"assertion":[{"value":"19 April 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}