{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:32Z","timestamp":1761611252203},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_26","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"403-418","source":"Crossref","is-referenced-by-count":10,"title":["A Tableau for CTL*"],"prefix":"10.1007","author":[{"given":"Mark","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","first-page":"388","volume-title":"LICS 1995","author":"G. Bhat","year":"1995","unstructured":"Bhat, G., Cleaveland, R., Grumberg, O.: Efficient On-the-Fly Model Checking for CTL*. In: LICS 1995, pp. 388\u2013397. IEEE Computer Society Press, Los Alamitos (1995)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","first-page":"52","volume-title":"Logic of Programs","author":"E. Clarke","year":"1981","unstructured":"Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: Engeler, E. (ed.) Logic of Programs 1979. LNCS, vol.\u00a0125, pp. 52\u201371. Springer, Heidelberg (1981)"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Emerson, E.: Alternative semantics for temporal logic. Th. C. Sci.\u00a026, 121\u2013130 (1983)","DOI":"10.1016\/0304-3975(83)90082-8"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60915-6_3","volume-title":"Logics for Concurrency","author":"E. Emerson","year":"1996","unstructured":"Emerson, E.: Automated temporal reasoning for reactive systems. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 41\u2013101. Springer, Heidelberg (1996)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Emerson, E., Clarke, E.C.: Using branching time temporal logic to synthesise synchronisation skeletons. Sci. of Computer Programming\u00a02 (1982)","DOI":"10.1016\/0167-6423(83)90017-5"},{"issue":"1","key":"26_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E. Emerson","year":"1985","unstructured":"Emerson, E., Halpern, J.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comp. and Sys. Sci.\u00a030(1), 1\u201324 (1985)","journal-title":"J. Comp. and Sys. Sci."},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E., Halpern, J.: \u2018Sometimes\u2019 and \u2018not never\u2019 revisited: on branching versus linear time. J. ACM\u00a033 (1986)","DOI":"10.1145\/4904.4999"},{"key":"26_CR8","volume-title":"29th IEEE Foundations of Computer Science, Proceedings","author":"E. Emerson","year":"1988","unstructured":"Emerson, E., Jutla, C.: Complexity of tree automata and modal logics of programs. In: 29th IEEE Foundations of Computer Science, Proceedings. IEEE, Los Alamitos (1988)"},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E. Emerson","year":"1984","unstructured":"Emerson, E., Sistla, A.: Deciding full branching time logic. Information and Control\u00a061, 175\u2013201 (1984)","journal-title":"Information and Control"},{"key":"26_CR10","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B. Elsevier, Amsterdam (1990)"},{"key":"26_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof methods for modal and intuitionistic logics","author":"M. Fitting","year":"1983","unstructured":"Fitting, M.: Proof methods for modal and intuitionistic logics. Reidel, Dordrecht (1983)"},{"key":"26_CR12","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods","author":"R. Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., et al. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer, Dordrecht (1999)"},{"key":"26_CR13","volume-title":"An Intro. to Modal Logic","author":"G. Hughes","year":"1968","unstructured":"Hughes, G., Cresswell, M.: An Intro. to Modal Logic. Methuen, London (1968)"},{"key":"26_CR14","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM\u00a047, 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th Symposium on Foundations of Computer Science, Providence, RI, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"26_CR16","first-page":"179","volume-title":"Proc. 16th Symposium of Principles of Programming Languages","author":"A. Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th Symposium of Principles of Programming Languages, pp. 179\u2013190. ACM, New York (1989)"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45694-5_2","volume-title":"CONCUR 2002 - Concurrency Theory","author":"A. Pnueli","year":"2002","unstructured":"Pnueli, A., Kesten, Y.: A deductive proof system for CTL*. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"26_CR18","unstructured":"Rao, A.S., Georgeff, M.P.: Modelling rational agents within a BDI-Architecture. In: Fikes, R., Sandewall, E. (eds.) Proceedings of the Second International Conference on Principles of Knowledge Representation and Reasoning, KR 1991, Cambridge, MA, pp. 473\u2013484 (1991)"},{"issue":"3","key":"26_CR19","doi-asserted-by":"publisher","first-page":"1011","DOI":"10.2307\/2695091","volume":"66","author":"M. Reynolds","year":"2001","unstructured":"Reynolds, M.: An axiomatization of full computation tree logic. J. Symbolic Logic\u00a066(3), 1011\u20131057 (2001)","journal-title":"J. Symbolic Logic"},{"key":"26_CR20","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. Logic and Comp.\u00a017, 117\u2013132 (2007)","journal-title":"J. Logic and Comp."},{"key":"26_CR21","unstructured":"Reynolds, M.: A tableau for CTL*, long version. Tech. report, UWA (January 2009), http:\/\/www.csse.uwa.edu.au\/~mark\/research\/Online\/StarTab.html"},{"key":"26_CR22","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/S1574-6526(05)80011-2","volume-title":"Handbook of Temporal Reasoning in Artificial Intelligence","author":"M. Reynolds","year":"2005","unstructured":"Reynolds, M., Dixon, C.: Theorem-proving for discrete temporal logic. In: Fisher, M., Gabbay, D., Vila, L. (eds.) Handbook of Temporal Reasoning in Artificial Intelligence, pp. 279\u2013314. Elsevier, Amsterdam (2005)"},{"key":"26_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/3-540-69778-0_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Schwendimann","year":"1998","unstructured":"Schwendimann, S.: A new one-pass tableau calculus for PLTL. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 277\u2013291. Springer, Heidelberg (1998)"},{"key":"26_CR24","unstructured":"Sprenger, C.: Deductive Local Model Checking. PhD thesis, Swiss Federal Institute of Technology, Lausanne, Switzerland (2000)"},{"key":"26_CR25","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Modal and temporal logics. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) H\u2019book of Logic in Comp. Sci., OUP, vol.\u00a02, pp. 477\u2013563 (1992)","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"26_CR26","first-page":"240","volume-title":"17th ACM Symp. on Th. of Comp.","author":"M. Vardi","year":"1985","unstructured":"Vardi, M., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: 17th ACM Symp. on Th. of Comp., pp. 240\u2013251. ACM, New York (1985)"},{"key":"26_CR27","first-page":"110","volume":"28","author":"P. Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Logique et Analyse\u00a028, 110\u2013111 (1985)","journal-title":"Logique et Analyse"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,17]],"date-time":"2024-03-17T12:32:31Z","timestamp":1710678751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}