{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:41:44Z","timestamp":1761597704927},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540583295"},{"type":"electronic","value":"9783540486541"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/978-3-540-48654-1_9","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T09:34:34Z","timestamp":1462872874000},"page":"98-113","source":"Crossref","is-referenced-by-count":16,"title":["Pushdown Processes: Parallel Composition and Model Checking"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Burkart","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","volume-title":"and J.W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. Technical Report CS-R8632","author":"JCM Baeten","year":"1987","unstructured":"J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. Technical Report CS-R8632, CWI, September 1987."},{"key":"9_CR2","volume-title":"University of Edinburgh","author":"JC Bradfield","year":"1991","unstructured":"J.C. Bradfield. Verifying Temporal Properties of Systems with Applications to Petri Nets. PhD thesis, University of Edinburgh, 1991."},{"key":"9_CR3","volume-title":"Technical Report ECS-LFCS-90-115, LFCS, Edinburgh","author":"JC Bradfield","year":"1991","unstructured":"J.C. Bradfield and C. Stirling. Local Model Checking for Infinite State Spaces. Technical Report ECS-LFCS-90\u2013115, LFCS, Edinburgh, Jun 1991."},{"key":"9_CR4","volume-title":"Concur 92, Lncs 630, pages 123-137. Springer","author":"O Burkart","year":"1992","unstructured":"O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In CONCUR \u201882, LNCS\n                630, pages 123\u2013137. Springer, 1992."},{"key":"9_CR5","volume-title":"Universit\u00e4t Passau","author":"O Burkart","year":"1994","unstructured":"O. Burkart and B. Steffen. Composition, Decomposition and Model Checking of Pushdown Processes. Technical Report MIP-9402, Universit\u00e4t Passau, 1994."},{"issue":"2","key":"9_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications. ACM Transactions on Programming Languages and Systems, 8 (2): 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR7","volume-title":"CONCUR 92, LNCS 630, pages 138-147. Springer","author":"S Christensen","year":"1992","unstructured":"S. Christensen, H. H\u00fcttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes. In CONCUR \u201882, LNCS\n                630, pages 138\u2013147. Springer, 1992."},{"key":"9_CR8","first-page":"410","volume-title":"CAV \u201882, LNCS 663","author":"R Cleaveland","year":"1992","unstructured":"R. Cleaveland, M. Klein, and B. Steffen. Faster Model Checking for the Modal Mu-Calculus. In CAV \u201882, LNCS\n                663, pages 410\u2013422, 1992."},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-Based Model Checking in the Propositional Mu-Calculus. Acta Informatica, 27: 725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"9_CR10","volume-title":"Graph-Theoretic Concepts in Computer Science, LNCS 484, pages 311-337. Springer","author":"D Caucal","year":"1990","unstructured":"D. Caucal and R. Monfort. On the Transition Graphs of Automata and Grammars. In Graph-Theoretic Concepts in Computer Science, LNCS\n                484, pages 311\u2013337. Springer, 1990."},{"key":"9_CR11","volume-title":"Icalp 91, Lncs 510, pages 127-138. Springer","author":"R Cleaveland","year":"1991","unstructured":"R. Cleaveland and B. Steffen. Computing Behavioural Relations, Logically. In ICALP \u201881, LNCS\n                510, pages 127\u2013138. Springer, 1991."},{"key":"9_CR12","volume-title":"Cav 91, Lncs 575, pages 48-58. Springer","author":"R Cleaveland","year":"1992","unstructured":"R. Cleaveland and B. Steffen. A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus. In CAV \u201881, LNCS\n                575, pages 48\u201358. Springer, 1992."},{"key":"9_CR13","volume-title":"Proc. 1th Annual Syrup. on Logic in Computer Science, pages 267-278. IEEE Computer Society Press","author":"EA Emerson","year":"1986","unstructured":"E.A. Emerson and C.-L. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus. In Proc. 1th Annual Syrup. on Logic in Computer Science, pages 267\u2013278. IEEE Computer Society Press, 1986."},{"key":"9_CR14","unstructured":"H. H\u00fcttel. Decidability, Behavioural Equivalences and Infinite Transition Graphs. PhD thesis, University of Edinburgh, Dec 1991. CST-86\u201391."},{"key":"9_CR15","volume-title":"Prentice\u2014Hall","author":"CAR Hoare","year":"1988","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice\u2014Hall, 1988."},{"key":"9_CR16","first-page":"593","volume-title":"Icalp \u201883, Lncs 700","author":"H Hungar","year":"1993","unstructured":"H. Hungar and B. Steffen. Local Model-Checking for Context-Free Processes. In ICALP \u201883, LNCS\n                700, pages 593\u2013605, 1993."},{"key":"9_CR17","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"D. Kozen. Results on the Propositional \u03bc-Calculus. Theoretical Computer Science, 27: 333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"9_CR18","volume-title":"Caap 88, LNCS 299, pages 215-230. Springer","author":"KG Larsen","year":"1988","unstructured":"K.G. Larsen. Proof Systems for Hennessy\u2014Milner Logic with Recursion. In CAAP \u201888, LNCS\u2019\n                299, pages 215\u2013230. Springer, 1988."},{"key":"9_CR19","volume-title":"Prentice\u2014Hall","author":"R Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice\u2014Hall, 1989."},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"DE Muller","year":"1985","unstructured":"D.E. Muller and P.E. Schupp. The Theory of Ends, Pushdown Automata, and Second-Order Logic. Theoretical Computer Science, 37: 51\u201375, 1985.","journal-title":"Theoretical Computer Science"},{"key":"9_CR21","unstructured":"S. Purushothaman Iyer. A Note on Model Checking Context-Free Processes. In NA PAW \u201883, 1993. To appear in LNCS."},{"key":"9_CR22","volume-title":"TAPSOFT 89, LNCS 351, pages 369-383. Springer","author":"C Stirling","year":"1989","unstructured":"C. Stirling and D. Walker. Local Model Checking in the Modal Mu-Calculus. In TAPSOFT \u201889, LNCS\n                351, pages 369\u2013383. Springer, 1989."},{"key":"9_CR23","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"A. Tarski. A Lattice-Theoretical Fixpoint Theorem and its Applications. Pacific Journal of Mathematics, 5: 285\u2013309, 1955.","journal-title":"Pacific Journal of Mathematics"},{"key":"9_CR24","volume-title":"ICALP 89, LNCS 372, pages 761-772. Springer","author":"G Winskel","year":"1989","unstructured":"G. Winskel. A Note on Model Checking the Modal Mu-Calculus. In ICALP \u201889, LNCS\n                372, pages 761\u2013772. Springer, 1989."}],"container-title":["Lecture Notes in Computer Science","CONCUR '94: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-48654-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T14:50:11Z","timestamp":1558795811000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-48654-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540583295","9783540486541"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-48654-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}