{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:04:49Z","timestamp":1725663889374},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_52","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:01Z","timestamp":1330269901000},"page":"169-181","source":"Crossref","is-referenced-by-count":2,"title":["Model checking of macro processes"],"prefix":"10.1007","author":[{"given":"Hardi","family":"Hungar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-55253-7_1","volume":"582","author":"H. Andersen","year":"1992","unstructured":"Andersen, H., Model checking on boolean graphs. ESOP '92, LNCS 582 (1992), 1\u201319.","journal-title":"ESOP '92, LNCS"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Bergstra, J.A., and Klop, J.W., Process theory based on bisimulation semantics. LNCS 354 (eds de Bakker, de Roever, Rozenberg) (1988), 50\u2013122.","DOI":"10.1007\/BFb0013021"},{"key":"14_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-6819-9","volume-title":"Verifying temporal properties of systems","author":"J.C. Bradfield","year":"1992","unstructured":"Bradfield, J.C., Verifying temporal properties of systems. Birkh\u00c4user, Boston (1992)."},{"key":"14_CR4","first-page":"115","volume":"458","author":"J.C. Bradfield","year":"1990","unstructured":"Bradfield, J.C., and Stirling, C. P., Verifying temporal properties of processes. Proc. CONCUR '90, LNCS 458 (1990), 115\u2013125.","journal-title":"Proc. CONCUR '90, LNCS"},{"key":"14_CR5","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/BFb0084787","volume":"630","author":"O. Burkart","year":"1992","unstructured":"Burkart, O., and Steffen, B., Model checking for context-free processes. CONCUR '92, LNCS 630 (1992), 123\u2013137.","journal-title":"CONCUR '92, LNCS"},{"key":"14_CR6","unstructured":"Burkart, O., and Steffen, B., Pushdown processes: Parallel composition and model checking. Tech. Rep. Aachen\/Passau (1994), 17 p. (1992), 123\u2013137."},{"key":"14_CR7","first-page":"311","volume":"484","author":"D. Caucal","year":"1990","unstructured":"Caucal, D., and Monfort, R., On the transition graphs of automata and languages. WG 90, LNCS 484 (1990), 311\u2013337.","journal-title":"WG 90, LNCS"},{"key":"14_CR8","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., and Sistla, A.P., Automatic verification of finite state concurrent systems using temporal logic specifications. ACM TOPLAS 8 (1986), 244\u2013263.","journal-title":"ACM TOPLAS"},{"key":"14_CR9","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"Cleaveland, R., Tableau-based model checking in the propositional mucalculus. Acta Inf. 27 (1990), 725\u2013747.","journal-title":"Acta Inf."},{"key":"14_CR10","first-page":"24","volume":"407","author":"R. Cleaveland","year":"1989","unstructured":"Cleaveland, R., Parrow, J., and Steffen, B., The concurrency workbench. Workshop Automatic Verification Methods for Finite-State Systems, LNCS 407 (1989), 24\u201337.","journal-title":"LNCS"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Cleaveland, R., and Steffen, B., Computing behavioral relations, logically. ICALP '91, LNCS 510 (1991).","DOI":"10.1007\/3-540-54233-7_129"},{"key":"14_CR12","first-page":"48","volume":"575","author":"R. Cleaveland","year":"1992","unstructured":"Cleaveland, R., and Steffen, B., A linear-time model-checking algorithm for the alternation-free modal mu-calculus. CAV 91, LNCS 575 (1992), 48\u201358.","journal-title":"CAV 91, LNCS"},{"key":"14_CR13","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(82)90009-3","volume":"20","author":"W. Damm","year":"1982","unstructured":"Damm, W., The IO-and OI-hierarchies, TCS 20 (1982), 95\u2013205.","journal-title":"TCS"},{"key":"14_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0019-9958(86)80016-X","volume":"71","author":"W. Damm","year":"1986","unstructured":"Damm, W., and Goerdt, A., An automata-theoretic characterization of the OI-hierarchy, Inf. and Cont. 71 (1986), 1\u201332.","journal-title":"Inf. and Cont."},{"key":"14_CR15","unstructured":"Emerson, E.A., and Lei, C.-L., Efficient model checking in fragments of the propositional mu-calculus. 1st LiCS (1986), 267\u2013278."},{"key":"14_CR16","first-page":"328","volume":"15","author":"J. Engelfriet","year":"1977","unstructured":"Engelfriet, J., and Schmidt, E.M., IO and OI, JCSS 15 (1977), 328\u2013353, and JCSS 16 (1978), 67\u201399.","journal-title":"JCSS"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Fischer, M.J., Grammars with macro-like productions, 9th Conf. Switching and Automata Theory, IEEE (1968), 131\u2013142.","DOI":"10.1109\/SWAT.1968.12"},{"key":"14_CR18","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0890-5401(89)90040-0","volume":"83","author":"S. M. German","year":"1989","unstructured":"German, S. M., Clarke, E. M. and Halpern, J. Y., Reasoning about procedures as parameters in the language L4, Inf. and Comp. 83 (1989) 265\u2013359. (Earlier version: 1st LiCS (1986) 11\u201325)","journal-title":"Inf. and Comp."},{"key":"14_CR19","first-page":"106","volume":"193","author":"A. Goerdt","year":"1985","unstructured":"Goerdt, A., A Hoare calculus for functions defined by recursion on higher types, Logics of Programs 1985, LNCS 193, 106\u2013117.","journal-title":"LNCS"},{"key":"14_CR20","unstructured":"Habel, A., Hyperedge replacement: Grammars and languages. PhD thesis, Bremen (1989), 193 p."},{"key":"14_CR21","first-page":"15","volume":"291","author":"A. Habel","year":"1987","unstructured":"Habel, A., and Kreowski, H.-J., May we introduce to you: Hyperedge replacement, Graph-grammars and their application to computer science 1986, LNCS 291 (1987), 15\u201326.","journal-title":"LNCS"},{"key":"14_CR22","first-page":"459","volume":"526","author":"H. Hungar","year":"1991","unstructured":"Hungar, H., Complexity of proving program correctness, TACS '91, LNCS 526 (1991), 459\u2013474.","journal-title":"TACS '91, LNCS"},{"key":"14_CR23","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-56503-5_43","volume":"665","author":"H. Hungar","year":"1993","unstructured":"Hungar, H. The complexity of verifying functional programs, STACS '93, LNCS 665 (1993), 428\u2013439.","journal-title":"STACS '93, LNCS"},{"key":"14_CR24","first-page":"593","volume":"700","author":"H. Hungar","year":"1993","unstructured":"Hungar, H., and Steffen, B., Local model checking for context-free processes. ICALP '93, LNCS 700 (1993), 593\u2013605.","journal-title":"ICALP '93, LNCS"},{"key":"14_CR25","unstructured":"Huynh, D.T., and Tian, L., Deciding bisimilarity of normed context-free processes is in \u03c3 2 p . Tech. Rep. UTDCS-1-92, Univ. Texas Dallas (1992)."},{"key":"14_CR26","unstructured":"Iyer, S.P., A note on model checking context-free processes, North American Process Algebra Workshop '93 (ed. Bard Bloom)."},{"key":"14_CR27","first-page":"497","volume":"12","author":"W. Kowalczyk","year":"1989","unstructured":"Kowalczyk, W., Niwinski, D., and Tiuryn, J. A generalization of Cook's auxiliarypushdown-automata theorem, Fund. Inf. 12 (1989) 497\u2013506.","journal-title":"Fund. Inf."},{"key":"14_CR28","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D., Results on the propositional \u039c-calculus. TCS 27 (1983), 333\u2013354.","journal-title":"TCS"},{"key":"14_CR29","unstructured":"Kfoury, A. J., Tiuryn, J. and Urzyczyn, P., The hierarchie of finitely typed functions, 2nd LiCS (1987) 225\u2013235."},{"key":"14_CR30","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K. G. Larsen","year":"1990","unstructured":"Larsen, K. G., Proof systems for satisfiability in Hennessy-Milner logic with recursion. TCS 72 (1990), 265\u2013288.","journal-title":"TCS"},{"key":"14_CR31","unstructured":"Larsen, K.G., Efficient local correctness checking. CAV '92."},{"key":"14_CR32","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"Muller, D.E., and Schupp, P.E., The theory of ends, pushdown automata, and second-order logic. TCS 37 (1985), 51\u201375.","journal-title":"TCS"},{"key":"14_CR33","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-50939-9_144","volume":"351","author":"C. P. Stirling","year":"1989","unstructured":"Stirling, C. P., and Walker, D. J., Local model checking in the modal mu-calculus. TAPSOFT '89, LNCS 351 (1989), 369\u2013383.","journal-title":"TAPSOFT '89, LNCS"},{"key":"14_CR34","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/3-540-57208-2_31","volume":"715","author":"B. Vergauwen","year":"1993","unstructured":"Vergauwen, B., and Lewi, J., A linear local model checking algorithm for CTL. CONCUR '93, LNCS 715 (1993), 447\u2013461.","journal-title":"CONCUR '93, LNCS"},{"key":"14_CR35","first-page":"761","volume":"372","author":"G. Winskel","year":"1989","unstructured":"Winskel, G., A note on model checking the modal mu-calculus. ICALP '89, LNCS 372 (1989), 761\u2013772.","journal-title":"ICALP '89, LNCS"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_52.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:53Z","timestamp":1605647873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}