{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T23:05:10Z","timestamp":1773097510874,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540433668","type":"print"},{"value":"9783540459316","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45931-6_26","type":"book-chapter","created":{"date-parts":[[2007,6,9]],"date-time":"2007-06-09T04:53:52Z","timestamp":1181364832000},"page":"372-386","source":"Crossref","is-referenced-by-count":12,"title":["Verifying Temporal Properties Using Explicit Approximants: Completeness for Context-free Processes"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Sch\u00f6pp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Simpson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,15]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1145\/200836.200876","volume":"42","author":"B. Bloom","year":"1995","unstructured":"B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can\u2019t be traced. J. Assoc. Comput. Mach., 42:232\u2013268, 1995.","journal-title":"J. Assoc. Comput. Mach."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification over infinite states. In Handbook of Process Algebra, pages 545\u2013623. Elsevier, 2001.","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"issue":"1\u20132","key":"26_CR3","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0304-3975(99)00034-1","volume":"221","author":"O. Burkart","year":"1999","unstructured":"O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. Theoretical Computer Science, 221(1\u20132):251\u2013270, 1999.","journal-title":"Theoretical Computer Science"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"M. Dam. Compositional proof systems for model checking infinite state processes. In International Conference on Concurrency Theory, pages 12\u201326, 1995.","DOI":"10.1007\/3-540-60218-6_2"},{"issue":"2","key":"26_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1006\/inco.1997.2680","volume":"140","author":"M. Dam","year":"1998","unstructured":"M. Dam. Proving properties of dynamic process networks. Information and Computation, 140(2):95\u2013114, 1998.","journal-title":"Information and Computation"},{"key":"26_CR6","unstructured":"M. Dam. Proof systems for \u03c0-calculus logics. In R. de Queiroz, editor, Logic for Concurrency and Synchronisation. OUP, 2001."},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"M. Dam, L. Fredlund, and D. Gurov. Toward parametric verification of open distributed systems. In A. Pnueli H. Langmaack and W.-P. de Roever, editors, Compositionality: the Significant Difference. Springer, 1998.","DOI":"10.1007\/3-540-49213-5_7"},{"key":"26_CR8","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of PSI\u201999","author":"M. Dam","year":"1999","unstructured":"M. Dam and D. Gurov. Compositional verification of CCS processes. In Proceedings of PSI\u201999. Springer LNCS 1755, 1999."},{"key":"26_CR9","unstructured":"M. Dam and D. Gurov. \u03bc-calculus with explicit points and approximations. Journal of Logic and Computation, to appear, 2001. Abstract in Proceedings of FICS 2000."},{"key":"26_CR10","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of FOSSACS\u201999","author":"J. Esparza","year":"1999","unstructured":"J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data flow analysis. In Proceedings of FOSSACS\u201999. Springer LNCS 1578, 1999."},{"key":"26_CR11","unstructured":"L. Fredlund. A framework for reasoning about Erlang code. PhD Thesis, Swedish Institute of Computer Science, 2001."},{"key":"26_CR12","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach., 32:137\u2013161, 1985.","journal-title":"J. Assoc. Comput. Mach."},{"issue":"3","key":"26_CR13","first-page":"364","volume":"1","author":"H. Hungar","year":"1994","unstructured":"H. Hungar and B. Steffen. Local model checking for context-free processes. Nordic Journal of Computing, 1(3):364\u2013385, Fall 1994.","journal-title":"Nordic Journal of Computing"},{"key":"26_CR14","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":"26_CR15","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D. E. Muller","year":"1985","unstructured":"D. E. Muller and P. E. Schupp. The theory of ends, pushdown automata, and secondorder logic. Theoretical Computer Science, 37:51\u201375, 1985.","journal-title":"Theoretical Computer Science"},{"key":"26_CR16","unstructured":"U. Sch\u00f6pp. Formal verification of processes. MSc Dissertation, University of Edinburgh, 2001. Available as http:\/\/www.dcs.ed.ac.uk\/home\/us\/th.ps.gz ."},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"A. K. Simpson. Compositionality via cut-elimination: Hennessy-Milner logic for an arbitrary GSOS. In Logic in Computer Science, pages 420\u2013430, 1995.","DOI":"10.1109\/LICS.1995.523276"},{"key":"26_CR18","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/0304-3975(87)90012-0","volume":"49","author":"C. P. Stirling","year":"1987","unstructured":"C. P. Stirling. Modal logics for communicating systems. Theoretical Computer Science, 49:311\u2013347, 1987.","journal-title":"Theoretical Computer Science"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"C. P. Stirling. Modal and temporal properties of processes. Texts in Computer Science. Springer, 2001.","DOI":"10.1007\/978-1-4757-3550-5"},{"issue":"2","key":"26_CR20","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I. Walukiewicz","year":"2001","unstructured":"I. Walukiewicz. Pushdown processes: games and model-checking. Information and Computation, 164(2):234\u2013263, January 2001.","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45931-6_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T04:20:23Z","timestamp":1737087623000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45931-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433668","9783540459316"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45931-6_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}