{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:09:30Z","timestamp":1725566970589},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304951"},{"type":"electronic","value":"9783540324195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11590156_31","type":"book-chapter","created":{"date-parts":[[2005,12,5]],"date-time":"2005-12-05T15:43:16Z","timestamp":1133797396000},"page":"384-395","source":"Crossref","is-referenced-by-count":1,"title":["Towards a CTL* Tableau"],"prefix":"10.1007","author":[{"given":"Mark","family":"Reynolds","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"publisher","first-page":"566","DOI":"10.2307\/2273296","volume":"44","author":"J.P. Burgess","year":"1979","unstructured":"Burgess, J.P.: Logic and time. J. Symbolic Logic\u00a044, 566\u2013582 (1979)","journal-title":"J. Symbolic Logic"},{"key":"31_CR2","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BF00370320","volume":"39","author":"J.P. Burgess","year":"1980","unstructured":"Burgess, J.P.: Decidability for Branching Time. Studia Logica\u00a039, 203\u2013218 (1980)","journal-title":"Studia Logica"},{"key":"31_CR3","first-page":"52","volume-title":"Proc. IBM Workshop on Logic of Programs","author":"E. Clarke","year":"1981","unstructured":"Clarke, E., Emerson, E.: Synthesis of synchronization skeletons for branching time temporal logic. In: Proc. IBM Workshop on Logic of Programs, Yorktown Heights, NY, pp. 52\u201371. Springer, Berlin (1981)"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E., Emerson, E., Sistla, A.: Automatic verification of finite state concurrent system using temporal logic specifications: a practical approach. In: Proc. 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 117\u2013126 (1983)","DOI":"10.1145\/567067.567080"},{"key":"31_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":"31_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":"31_CR7","volume-title":"Proceedings of 29th IEEE Foundations of Computer Science","author":"E. Emerson","year":"1988","unstructured":"Emerson, E., Jutla, C.: Complexity of tree automata and modal logics of programs. In: Proceedings of 29th IEEE Foundations of Computer Science, IEEE, Los Alamitos (1988)"},{"key":"31_CR8","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":"31_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0304-3975(83)90082-8","volume":"26","author":"E. Emerson","year":"1983","unstructured":"Emerson, E.: Alternative semantics for temporal logics. Theoretical Computer Science\u00a026, 121\u2013130 (1983)","journal-title":"Theoretical Computer Science"},{"key":"31_CR10","volume-title":"Handbook of Theoretical Computer Science","author":"E. Emerson","year":"1990","unstructured":"Emerson, E.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, Elsevier, Amsterdam (1990)"},{"key":"31_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, Boston (1983)"},{"key":"31_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., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"31_CR13","unstructured":"Gough, G.: Decision procedures for temporal logics. Technical Report UMCS-89- 10-1, Department of Computer Science, University of Manchester (1989)"},{"key":"31_CR14","series-title":"Logic in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1109\/LICS.2002.1029847","volume-title":"LICS 2002, Proceedings of 17th Annual IEEE Symp.","author":"I. Hodkinson","year":"2002","unstructured":"Hodkinson, I., Wolter, F., Zakharyaschev, M.: Decidable and undecidable fragments of first-order branching temporal logics. In: LICS 2002, Proceedings of 17th Annual IEEE Symp. Logic in Computer Science, pp. 393\u2013402. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"31_CR15","volume-title":"An Introduction to Modal Logic","author":"G. Hughes","year":"1968","unstructured":"Hughes, G., Cresswell, M.: An Introduction to Modal Logic. Methuen, London (1968)"},{"key":"31_CR16","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":"31_CR17","first-page":"46","volume-title":"Proceedings of 18th Symp. on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th Symp. on Foundations of Computer Science, pp. 46\u201357. Providence, RI (1977)"},{"key":"31_CR18","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)"},{"issue":"3","key":"31_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":"31_CR20","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/j.ic.2005.03.005","volume":"201","author":"M. Reynolds","year":"2005","unstructured":"Reynolds, M.: An axiomatization of PCTL*. Information and Computation\u00a0201, 72\u2013119 (2005)","journal-title":"Information and Computation"},{"key":"31_CR21","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":"31_CR22","unstructured":"Sprenger, C.: Deductive Local Model Checking. PhD thesis, Swiss Federal Institute of Technology, Lausanne, Switzerland (2000)"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"Stirling, C.: Modal and temporal logics. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, pp. 477\u2013563. OUP (1992)","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"31_CR24","first-page":"240","volume-title":"17th ACM Symp. on Theory of Computing, Proceedings","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 Theory of Computing, Proceedings, pp. 240\u2013251. ACM Press, New York (1985)"},{"key":"31_CR25","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","FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11590156_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,1]],"date-time":"2024-02-01T10:43:55Z","timestamp":1706784235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11590156_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304951","9783540324195"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11590156_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}