{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,2]],"date-time":"2026-01-02T07:31:20Z","timestamp":1767339080335},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_62","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:42Z","timestamp":1330277802000},"page":"353-366","source":"Crossref","is-referenced-by-count":19,"title":["On the model checking problem for branching time logics and basic parallel processes"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Astrid","family":"Kiehn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"28_CR1","first-page":"109","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"J.A. Bergstra and J.W. Klop. Process algebra for synchronous communication. Information and Computation 60:109\u2013137, 1984.","journal-title":"Information and Computation"},{"key":"28_CR2","first-page":"123","volume":"630","author":"O. Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model checking for context-free processes. In Proceedings of CONCUR '92, LNCS 630:123\u2013137, 1992.","journal-title":"LNCS"},{"key":"28_CR3","first-page":"143","volume":"715","author":"S. Christensen","year":"1993","unstructured":"S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation Equivalence is Decidable for all Basic Parallel Processes. In Proceedings of CONCUR '93, LNCS 715:143\u2013157, 1993.","journal-title":"LNCS"},{"key":"28_CR4","first-page":"138","volume":"630","author":"S. Christensen","year":"1992","unstructured":"S. Christensen, H. H\u00fcttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-free Processes. In Proceedings of CONCUR '92, LNCS 630:138\u2013147, 1992.","journal-title":"LNCS"},{"key":"28_CR5","first-page":"52","volume":"131","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson. Design and Synthesis of synchronization skeletons using Branching Time Temporal Logic. In Proceedings of Workshop on Logics of Programs, LNCS 131:52\u201371, 1981.","journal-title":"LNCS"},{"key":"28_CR6","first-page":"995","volume":"B","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson. Temporal and Modal Logic. In Handbook of Theoretical Computer Science, Volume B, 995\u20131072, 1990.","journal-title":"Handbook of Theoretical Computer Science"},{"issue":"1","key":"28_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. \u201cSometimes\u201d and \u201cNot Never\u201d revisited: on Branching versus Linear Time Temporal Logic. Journal of the ACM 33(1):151\u2013178, 1986.","journal-title":"Journal of the ACM"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C. S. Jutla. Tree Automata, Mu-Calculus and Determinacy. In Proceedings of FOCS '91, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"28_CR9","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/BF01463946","volume":"28","author":"J. Engelfriet","year":"1991","unstructured":"J. Engelfriet. Branching processes of Petri nets. Acta Informatica 28:575\u2013591, 1991.","journal-title":"Acta Informatica"},{"key":"28_CR10","first-page":"115","volume":"787","author":"J. Esparza","year":"1994","unstructured":"J. Esparza. On the Decidability of the Model Checking Problem for Several \u03bccalculi and Petri Nets. In Proceedings of CAAP '94, LNCS 787:115\u2013129, 1994.","journal-title":"LNCS"},{"key":"28_CR11","unstructured":"J. Esparza. On the uniform word problem for commutative context-free grammars. Submitted for publication, 1994."},{"key":"28_CR12","first-page":"2","volume":"458","author":"R. Gorrieri","year":"1990","unstructured":"R. Gorrieri and U. Montanari. A Simple Calculus of Nets. In Proceedings of CONCUR '90, LNCS 458:2\u201330, 1990.","journal-title":"LNCS"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Y. Hirshfeld. Petri Nets and the Equivalence Problem. In Proceedings of CSL '93, 1994.","DOI":"10.1007\/BFb0049331"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"H. Hungar and B. Steffen. Local Model Checking for Context-Free Processes. In Proceedings of ICALP '93, LNCS 707, 1993.","DOI":"10.1007\/3-540-56939-1_105"},{"key":"28_CR15","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D. Muller","year":"1985","unstructured":"D. Muller and P. Schupp. The Theory of Ends, Pushdown Automata and Second Order Logic, Theoretical Computer Science 37: 51\u201375, 1985.","journal-title":"Theoretical Computer Science"},{"key":"28_CR16","unstructured":"M. Minsky: Computation. Finite and Infinite Machines. Prentice-Hall, 1967."},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"D. Peled, S. Katz, and A. Pnueli. Specifying and Proving Serializability in Temporal Logic. In Proceedings of LICS '91, 232\u2013245, 1991.","DOI":"10.1109\/LICS.1991.151648"},{"key":"28_CR18","first-page":"31","volume":"33","author":"W. Penczek","year":"1992","unstructured":"W. Penczek. Temporal Logics for Trace Systems: On Automated Verification. International Journal on Foundations of Computer Science 33:31\u201367, 1992.","journal-title":"International Journal on Foundations of Computer Science"},{"key":"28_CR19","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"M.O. Rabin. Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141:1\u201335, 1969.","journal-title":"Transactions of the American Mathematical Society"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"C. Stirling. Modal and Temporal Logics. In Handbook of Logic in Computer Science, Oxford University Press, 1991.","DOI":"10.1093\/oso\/9780198537618.003.0005"},{"key":"28_CR21","unstructured":"P.S. Thiagarajan. A Trace Based Extension of PTL. In Proceedings of LICS '94, 1994."},{"issue":"1","key":"28_CR22","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P. Wolper","year":"1983","unstructured":"P. Wolper. Temporal Logic can be more expressive. Information and Control 56(1,2):72\u201393, 1983.","journal-title":"Information and Control"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_62.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T16:39:08Z","timestamp":1713631148000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_62"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_62","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}