{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:40Z","timestamp":1761611260649},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434771"},{"type":"electronic","value":"9783540460176"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-46017-9_11","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:12:13Z","timestamp":1269882733000},"page":"128-147","source":"Crossref","is-referenced-by-count":14,"title":["Local Parallel Model Checking for the Alternation-Free \u03bc-Calculus"],"prefix":"10.1007","author":[{"given":"Benedikt","family":"Bollig","sequence":"first","affiliation":[]},{"given":"Martin","family":"Leucker","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Weber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,23]]},"reference":[{"issue":"1","key":"11_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)90266-6","volume":"126","author":"H. R. Andersen","year":"1994","unstructured":"H. R. Andersen. Model checking and Boolean graphs. Theoretical Computer Science, 126(1):3\u201330, 11 Apr. 1994.","journal-title":"Theoretical Computer Science"},{"key":"11_CR2","unstructured":"S. Basonov. Parallel implementation of BDD on DSM systems. Master\u2019s thesis, Computer Science Department, Technion, 1998."},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"Proc. of the 13th Conference on Computer-Aided Verification (CAV\u201901)","author":"S. Blom","year":"2001","unstructured":"S. Blom, W. Fokkink, J. F. Groote, I. van Langevelde, B. Lisser, and J. van de Pol. \u03bcCRL: a toolset for analysing algebraic specifications. In G. Berry, H. Comon, and A. Finkel, editors, Proc. of the 13th Conference on Computer-Aided Verification (CAV\u201901), LNCS 2102, p. 250\u2013254. Springer, July 2001."},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"B. Bollig, M. Leucker, and M. Weber. Local parallel model checking for the alternation free \u03bc-calculus. Technical Report AIB-04-2001, RWTH Aachen, 03\/2001.","DOI":"10.1007\/3-540-45319-9_37"},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/3-540-45319-9_37","volume-title":"Proc. of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901)","author":"B. Bollig","year":"2001","unstructured":"B. Bollig, M. Leucker, and M. Weber. Parallel model checking for the alternation free \u03bc-calculus. In T. Margaria and W. Yi, editors, Proc. of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201901), LNCS 2031, p. 543\u2013558. Springer, Apr. 2001."},{"key":"11_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Distributed LTL model-checking based on negative cycle detection","author":"L. Brim","year":"2001","unstructured":"L. Brim, I. \u010cern\u00e1, P. Kr\u010d\u00e1l, and R. Pel\u00e1nek. Distributed LTL model-checking based on negative cycle detection. In Proc. of 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201901), LNCS. Springer, Dec. 2001."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Que. Improved reachability analysis of large FSM. In Proc. of the IEEE International Conference on Computer-Aided Design, p. 354\u2013360. IEEE Computer Society Press, June 1996.","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"11_CR8","volume-title":"Model Checking","author":"E. M. Clarke","year":"1999","unstructured":"E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. The MIT Press, Cambridge, Massachusetts, 1999."},{"issue":"5","key":"11_CR9","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0020-0190(83)90092-3","volume":"16","author":"E. W. Dijkstra","year":"1983","unstructured":"E. W. Dijkstra, W. H. J. Feijen, and A. J. M. van Gasteren. Derivation of a termination detection algorithm for distributed computations. Information Processing Letters, 16(5):217\u2013219, June 1983.","journal-title":"Information Processing Letters"},{"issue":"3","key":"11_CR10","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"E. A. Emerson and E. M. Clarke. Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming, 2(3):241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"key":"11_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Proc. 5th International Computer-Aided Verification Conference","author":"E. A. Emerson","year":"1993","unstructured":"E. A. Emerson, C. S. Jutla, and A. P. Sistla. On model-checking for fragments of mu-calculus. In C. Courcoubetis, editor, Proc. 5th International Computer-Aided Verification Conference, LNCS 697, p. 385\u2013396. Springer, 1993."},{"key":"11_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"350","DOI":"10.1007\/3-540-44585-4_32","volume-title":"Proc. of the 13th Conference on Computer-Aided Verification (CAV\u201901)","author":"O. Grumberg","year":"2001","unstructured":"O. Grumberg, T. Heyman, and A. Schuster. Distributed symbolic model checking for \u03bc-calculus. In G. Berry, H. Comon, and A. Finkel, editors, Proc. of the 13th Conference on Computer-Aided Verification (CAV\u201901), of LNCS 2102, p. 350\u2013362. Springer, July 2001."},{"key":"11_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1007\/3-540-55179-4_21","volume-title":"Proc. of Computer Aided Verification (CAV\u2019 91)","author":"H. Hiraishi","year":"1992","unstructured":"H. Hiraishi, K. Hamaguchi, H. Ochi, and S. Yajima. Vectorized symbolic model checking of computation tree logic for sequential machine verification. In K. G. Larsen and A. Skou, editors, Proc. of Computer Aided Verification (CAV\u2019 91), LNCS 575, p. 214\u2013224, Berlin, Germany, July 1992. Springer."},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333\u2013354, Dec. 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"issue":"2","key":"11_CR15","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"O. Kupferman, M. Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. Journal of the ACM, 47(2):312\u2013360, Mar. 2000.","journal-title":"Journal of the ACM"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"M. Leucker. Model checking games for the alternation free mu-calculus and alternating automata. In H. Ganzinger, D. McAllester, and A. Voronkov, editors, Proc. of the 6th International Conference on Logic for Programming and Automated Reasoning \u201c(LPAR\u201999)\u201d, LNAI 1705, p. 77\u201391. Springer, 1999.","DOI":"10.1007\/3-540-48242-3_6"},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-44585-4_24","volume-title":"Proc. of the 13th Conference on Computer-Aided Verification (CAV\u201901)","author":"M. Leucker","year":"2001","unstructured":"M. Leucker and T. Noll. Truth\/SLC-A parallel verification platform for concurrent systems. In G. Berry, H. Comon, and A. Finkel, editors, Proc. of the 13th Conference on Computer-Aided Verification (CAV\u201901), LNCS 2102, p. 255\u2013259. Springer, July 2001."},{"key":"11_CR18","unstructured":"A. Mader. Verification of Modal Properties Using Boolean Equation Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen, 1996."},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"A. A. Narayan, J. J. J. Isles, R. K. Brayton, and A. L. Sangiovanni-Vincentelli. Reachability analysis using partitioned-roBBDs. In Proc. of the IEEE International Conference on Computer-Aided Design, p. 388\u2013393. IEEE Computer Society Press, June 1997.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"11_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Computer-Aided Verification, 9th International Conference","author":"U. Stern","year":"1997","unstructured":"U. Stern and D. L. Dill. Parallelizing the Mur\u03c6 verifier. In O. Grumberg, editor, Computer-Aided Verification, 9th International Conference, LNCS 1254, p. 256\u2013267. Springer, June 1997. Haifa, Israel, June 22-25."},{"key":"11_CR21","unstructured":"C. Stirling. Games for bisimulation and model checking, July 1996. Notes for Mathfit Workshop on finite model theory, University of Wales, Swansea,."},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"A. L. Stornetta. Implementation of an efficient parallel BDD package. Master\u2019s thesis, University of California, Santa Barbara, 1995.","DOI":"10.1145\/240518.240639"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"S. Zhang, O. Sokolsky, and S. A. Smolka. On the parallel complexity of model checking in the modal mu-calculus. In Proc. of the 9th Annual IEEE Symposium on Logic in Computer Science, p. 154\u2013163, Paris, France, 4\u20137 July 1994. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1994.316075"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46017-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T14:45:48Z","timestamp":1558968348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46017-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434771","9783540460176"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-46017-9_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}