{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:08Z","timestamp":1761611288850},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2011,11,1]],"date-time":"2011-11-01T00:00:00Z","timestamp":1320105600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2011,11]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We present a sound, complete and implementable tableau method for deciding satisfiability of formulas in the propositional version of computation tree logic CTL*. This is the first such tableau. CTL* is an exceptionally important temporal logic with applications from hardware design to agent reasoning, but there is no easily automated reasoning approach to CTL*. The tableau here is a traditional tree-shaped or top-down style tableau, and affords the possibility of reasonably quick decisions on the satisfiability of medium-sized formulas and construction of small models for them. A straightforward subroutine is given for determining when looping allows successful branch termination, but much needed further development is left as future work. In particular, a more general repetition prevention mechanism is needed to speed up the task of tableau construction.<\/jats:p>","DOI":"10.1007\/s00165-011-0193-4","type":"journal-article","created":{"date-parts":[[2011,8,9]],"date-time":"2011-08-09T00:11:44Z","timestamp":1312848704000},"page":"739-779","source":"Crossref","is-referenced-by-count":8,"title":["A tableau-based decision procedure for CTL*"],"prefix":"10.1145","volume":"23","author":[{"given":"Mark","family":"Reynolds","sequence":"first","affiliation":[{"name":"CSSE, The University of Western Australia (UWA), M002, Stirling Highway, 6009, Crawley, WA, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Bhat G Cleaveland R Grumberg O (1995) Efficient on-the-fly model checking for ctl. In: LICS 1995. IEEE Computer Society Press pp 388\u2013397"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Bolotov A Dixon C Fisher M (1999) Clausal resolution for ctl. In: MFCS\u201999 pp 137\u2013148","DOI":"10.1007\/3-540-48340-3_13"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Bernholtz O Grumberg O (1994) Buy one get one free !!! In: Gabbay D Ohlbach H (eds) Temporal logic. Proceedings of ICTL \u201994 LNAI vol 827. Springer Berlin pp 210\u2013224","DOI":"10.1007\/BFb0013990"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Clarke E Emerson E (1981) Synthesis of synchronization skeletons for branching time temporal logic. In: Proceedings of IBM workshop on logic of programs Yorktown heights NY. Springer Berlin pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4999"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Emerson E Jutla C (1988) Complexity of tree automata and modal logics of programs. In: Proceedings of 29th IEEE foundations of computer science. IEEE","DOI":"10.1109\/SFCS.1988.21949"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90082-8"},{"key":"e_1_2_1_2_10_2","volume-title":"Handbook of theoretical computer science, vol B","author":"Emerson EA","year":"1990"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_3"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80047-9"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Fitting M (1983) Proof methods for modal and intuitionistic logics. Reidel","DOI":"10.1007\/978-94-017-2794-5"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Friedmann O Latte M Lange M (2010) A decision procedure for ctl* based on tableaux and automata. In: IJCAR\u201910 pp 331\u2013345","DOI":"10.1007\/978-3-642-14203-1_28"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-1754-0_6"},{"key":"e_1_2_1_2_16_2","unstructured":"Gough G (1989) Decision procedures for temporal logics. Technical report UMCS-89-10-1. Department of Computer Science University of Manchester"},{"key":"e_1_2_1_2_17_2","volume-title":"An introduction to modal logic","author":"Hughes G","year":"1968"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Hodkinson I Reynolds M (2007) Temporal logic. In: Handbook of modal logic. Elsevier pp 655\u2013720","DOI":"10.1016\/S1570-2464(07)80014-0"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Heuerding A Seyfried M Zimmermann H (1996) Efficient loop-check for backward proof search in some non-classical propositional logics. In: Miglioli P Moscato U Mundici D Ornaghi M (eds) TABLEAUX. Lecture notes in computer science vol 1071. Springer Berlin pp 210\u2013225","DOI":"10.1007\/3-540-61208-4_14"},{"key":"e_1_2_1_2_20_2","unstructured":"Lange M (2002) Games for modal and temporal logics. PhD thesis University of Edinburgh"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Luo X Su K Sattar A Chen Q Lv G (2005) Bounded model checking knowledge and branching time in synchronous multi-agent systems. In: AAMAS \u201905: Proceedings of the fourth international joint conference on autonomous agents and multiagent systems. ACM New York pp 1129\u20131130","DOI":"10.1145\/1082473.1082657"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Kesten Y (2002) A deductive proof system for CTL*. In: Brim L Jancar P Kret\u00ednsk\u00fd M Kucera A (eds) CONCUR. Lecture notes in computer science vol 2421. Springer Berlin pp 24\u201340","DOI":"10.1007\/3-540-45694-5_2"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of the eighteenth symposium on foundations of computer science Providence RI pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Pnueli A Rosner R (1989) On the synthesis of a reactive module. In: Proceedings of the sixteenth symposium of principles of programming languages. ACM pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Reynolds M Dixon C (2005) Theorem-proving for discrete temporal logic. In: Fisher M Gabbay D and Vila L (eds) Handbook of temporal reasoning in artificial intelligence. Elsevier pp 279\u2013314","DOI":"10.1016\/S1574-6526(05)80011-2"},{"key":"e_1_2_1_2_26_2","unstructured":"Reynolds M (2000) More past glories. In: Fifteenth annual IEEE symposium on logic in computer science (LICS\u20192000) Santa Barbara California USA June 26\u201328 2000. IEEE pp 229\u2013240"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.2307\/2695091"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/j.ic.2005.03.005","article-title":"An axiomatization of PCTL*","volume":"201","author":"Reynolds M","year":"2005","journal-title":"Inf Comput"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exl033"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Reynolds M (2009) A tableau for CTL*. In: Cavalcanti A Dams D (eds) FM 2009: Proceedings of formal methods second world congress Eindhoven The Netherlands November 2009. Lecture notes in computer science vol 5850. Springer pp 403\u2013418","DOI":"10.1007\/978-3-642-05089-3_26"},{"key":"#cr-split#-e_1_2_1_2_31_2.1","doi-asserted-by":"crossref","unstructured":"Schwendimann S (1998) A new one-pass tableau calculus for PLTL. In: de Swart HCM","DOI":"10.1007\/3-540-69778-0_28"},{"key":"#cr-split#-e_1_2_1_2_31_2.2","unstructured":"(ed) Proceedings of international conference TABLEAUX 1998 Oisterwijk LNAI 1397. Springer pp 277-291"},{"key":"e_1_2_1_2_32_2","unstructured":"Sprenger C (2000) Deductive local model checking. PhD thesis Swiss Federal Institute of Technology Lausanne Switzerland"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Stirling C (1992) Modal and temporal logics. In: Abramsky S Gabbay D Maibaum T (eds) Handbook of logic in computer science vol 2. Oxford University Press pp 477\u2013563","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Vardi M Stockmeyer L (1985) Improved upper and lower bounds for modal logics of programs. In: Proceedings of 17th ACM symposium on theory of computing. ACM pp 240\u2013251","DOI":"10.1145\/22145.22173"},{"key":"e_1_2_1_2_35_2","first-page":"110","article-title":"The tableau method for temporal logic: an overview","volume":"28","author":"Wolper P","year":"1985","journal-title":"Logique et Analyse"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0193-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0193-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0193-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,9]],"date-time":"2024-04-09T19:55:17Z","timestamp":1712692517000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0193-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11]]},"references-count":36,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2011,11]]}},"alternative-id":["10.1007\/s00165-011-0193-4"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0193-4","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11]]}}}