{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:08:59Z","timestamp":1760202539308,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540429609"},{"type":"electronic","value":"9783540456568"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45656-2_15","type":"book-chapter","created":{"date-parts":[[2007,7,2]],"date-time":"2007-07-02T15:46:10Z","timestamp":1183391170000},"page":"165-176","source":"Crossref","is-referenced-by-count":12,"title":["Decidability of Quantifed Propositional Branching Time Logics"],"prefix":"10.1007","author":[{"given":"Tim","family":"French","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,2,14]]},"reference":[{"issue":"2","key":"15_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theorectical Computer Science, 82(2):253\u2013284, May 1991.","journal-title":"Theorectical Computer Science"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"E. Clarke and E. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Proc. IBM Workshop on Logic of Programs, Yorktown Heights, NY, pages 52\u201371. Springer, Berlin, 1981.","DOI":"10.1007\/BFb0025774"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"E. Emerson. Alternative semantics for temporal logics. TCS, 26, 1983.","DOI":"10.1016\/0304-3975(83)90082-8"},{"key":"15_CR4","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E. Emerson","year":"1984","unstructured":"E. Emerson and A. Sistla. Deciding full branching time logic. Information and Control, 61:175\u2013201, 1984.","journal-title":"Information and Control"},{"key":"15_CR5","unstructured":"T. French. The theory of branching time logics with quantified propositions. PhD thesis, Murdoch University, In preparation."},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"668","DOI":"10.2307\/2274321","volume":"50","author":"Y. Gurevich","year":"1985","unstructured":"Y. Gurevich and S. Shelah. The decision problem for branching time logic. J. of Symbolic Logic, 50:668\u2013681, 1985.","journal-title":"J. of Symbolic Logic"},{"issue":"1","key":"15_CR7","first-page":"224","volume":"33","author":"D. Harel","year":"1986","unstructured":"D. Harel. Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness. J. A.C.M., 33(1):224\u2013248, 1986.","journal-title":"J. A.C.M."},{"key":"15_CR8","unstructured":"R. van der Meyden K. Engelhardt and Y. Moses. Knowledge and the logic of local propositions. In Conf. on Theoretical Aspects of Rationality and Knowledge, 1998."},{"key":"15_CR9","doi-asserted-by":"crossref","unstructured":"Yonit Kesten and Amir Pnueli. A complete proof systems for qptl. In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 2\u201312, 1995.","DOI":"10.1109\/LICS.1995.523239"},{"key":"15_CR10","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0168-0072(94)90086-8","volume":"69","author":"N. Klarlund","year":"1994","unstructured":"N. Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Annals of Pure and Applied Logic, 69:243\u2013268, 1994.","journal-title":"Annals of Pure and Applied Logic"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"O. Kupferman. Augmenting branching temporal logics with existential quantification over atomic propositions. In Computer Aided Verification, Proc. 7th Int. Conference, pages 325\u2013338, Liege, 1995. Springer-Verlag.","DOI":"10.1007\/3-540-60045-0_60"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"O. Kupferman and O. Grumberg. Branching time temporal logic and amorphous tree automata. In Proceedings of the Fourth Conference on Concurrency Theory, pages 262\u2013277, Hildesheim, 1993. Springer-Verlag.","DOI":"10.1007\/3-540-57208-2_19"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"O. Kupferman and A. Pnueli. Once and for all. In Proceedings of the Tenth IEEE Symposium on Logic in Computer Science, San Diego, 1995.","DOI":"10.1109\/LICS.1995.523241"},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"92","DOI":"10.1007\/3-540-10235-3","volume-title":"A calculus of communicating systems","author":"R. Milner","year":"1980","unstructured":"R. Milner. A calculus of communicating systems. Lecture Notes in Computer Science, 92, 1980."},{"issue":"2","key":"15_CR15","doi-asserted-by":"publisher","first-page":"529","DOI":"10.2307\/2275545","volume":"62","author":"P. Kremer","year":"1997","unstructured":"P. Kremer. On the complexity of propositional quantification in intuitionistic logic. J. of Symbolic Logic, 62(2):529\u2013544, 1997.","journal-title":"J. of Symbolic Logic"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In Proceedings of the Eighteenth Symposium on Foundations of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1995086","volume":"141","author":"M. Rabin","year":"1969","unstructured":"M. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. AMS, 141:1\u201335, 1969.","journal-title":"Trans. AMS"},{"key":"15_CR18","unstructured":"A. P. Sistla. Theoretical Issues in the Design and Verification of Distributed Systems. PhD thesis, Harvard University, 1983."},{"key":"15_CR19","unstructured":"Albert Visser. Bisimulations, model descriptions and propositional quantifiers. Manuscript, see http:\/\/www.citeseer.nj.nec.com\/visser96bisimulation.html ."}],"container-title":["Lecture Notes in Computer Science","AI 2001: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45656-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T02:50:53Z","timestamp":1737168653000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45656-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540429609","9783540456568"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-45656-2_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}