{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:20Z","timestamp":1725487220388},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_37","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:50:47Z","timestamp":1184601047000},"page":"543-558","source":"Crossref","is-referenced-by-count":22,"title":["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":[[2001,3,23]]},"reference":[{"key":"37_CR1","unstructured":"S. Basonov. Parallel implementation of BDD on DSM systems. Master\u2019s thesis, Computer Science Department, Technion, 1998."},{"key":"37_CR2","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Que. Improved reachability analysis of large FSM. In Proc. IEEE Int. Conf. on Computer Aided Design, pages 354\u2013360. IEEE Computer Society Press, June 1996.","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"37_CR3","unstructured":"E. M. Clarke and J. Wing. Formal methods: State of the art and future directions. Technical Report CMU-CS-96-178, Carnegie Mellon University (CMU), Sept. 1996."},{"key":"37_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0084777","volume-title":"Proc. Computer Aided Verification (CAV\u2019 91)","author":"R. Cleaveland","year":"1992","unstructured":"R. Cleaveland and B. Ste\u00e9n. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In Proc. Computer Aided Verification (CAV\u2019 91), volume 575 of LNCS, Springer, 1992"},{"issue":"5","key":"37_CR5","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":"37_CR6","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":"37_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_36","volume-title":"Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Gnesi","year":"2000","unstructured":"S. Gnesi et. al., A formal specification and validation of a critical system in presence of byzantine errors. In Proc. 6th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, number 1785 in LNCS. Springer, 2000."},{"key":"37_CR8","doi-asserted-by":"crossref","unstructured":"R. Greenlaw, H. J. Hoover, and W. L. Ruzzo. Limits to Parallel Computation: P-Completeness Theory. Oxford University Press, 1995.","DOI":"10.1093\/oso\/9780195085914.001.0001"},{"key":"37_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Computer Aided Verification, 12th Int. Conf.","author":"T. Heyman","year":"2000","unstructured":"T. Heyman, D. Geist, O. Grumberg, and A. Schuster. Achieving scalability in parallel reachability analysis of very large circuits. In Computer Aided Verification, 12th Int. Conf., volume 1855 of LNCS, pages 20\u201335. Springer-Verlag, June 2000."},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"A. J. Hu, G. York, and D. L. Dill. New techniques for efficient verification with implicitly conjoined BDDs. In 31st Design Automation Conference, 1994.","DOI":"10.1145\/196244.196377"},{"key":"37_CR11","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 mu-calculus. Theoretical Computer Science, 27:333\u2013354, Dec. 1983.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"37_CR12","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":"37_CR13","unstructured":"M. Lange. Spielbasiertes Model-Checking f\u00ecr den alternierungsfreien mu-Kalk\u00ecl. Master\u2019s thesis, Aachen, University of Technology, 1999. (German)."},{"key":"37_CR14","doi-asserted-by":"crossref","unstructured":"M. Lange, M. Leucker, T. Noll, and S. Tobies. Truth-a verification platform for concurrent systems. In Tool Support for System Specification, Development, and Verification, Advances in Computing Science. Springer-Verlag, 1999.","DOI":"10.1007\/978-3-7091-6355-9_11"},{"key":"37_CR15","unstructured":"B. P. Lester. The Art of Parallel Programming. Prentice Hall, 1993."},{"key":"37_CR16","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-48242-3_6","volume":"1705","author":"M. Leucker","year":"1999","unstructured":"M. Leucker. Model checking games for the alternation free mu-calculus and alternating automata. In Proc. 6th Int. Conf. on Logic for Programming and Automated Reasoning, volume 1705 of LNAI, pages 77\u201391. Springer, 1999.","journal-title":"Proc. 6th Int. Conf. on Logic for Programming and Automated Reasoning"},{"key":"37_CR17","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"37_CR18","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"37_CR19","doi-asserted-by":"crossref","unstructured":"A. A. Narayan, J. J. J. Isles, R. K. Brayto, and A. L. Sangiovanni-Vincentelli. Reachability analysis using partitioned-roBBDs. In Proc. IEEE Int. Conf. on Computer Aided Design, pages 388\u2013393. IEEE Computer Society Press, June 1997.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"37_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BFb0028727","volume-title":"CAV, Computer Aided Verification","author":"D. Peled","year":"1998","unstructured":"D. Peled. Ten years of partial order reduction. In CAV, Computer Aided Verification, number 1427 in LNCS, pages 17\u201328, Vancouver, BC, Canada, 1998. Springer."},{"issue":"5","key":"37_CR21","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","volume":"20","author":"J. H. Reif","year":"1985","unstructured":"J. H. Reif. Depth-first search is inherently sequential. Information Processing Letters, 20(5):229\u2013234, June 1985.","journal-title":"Information Processing Letters"},{"key":"37_CR22","doi-asserted-by":"crossref","unstructured":"S. H. Roosta. Parallel Processing and Parallel Algorithms. Springer, 1999.","DOI":"10.1007\/978-1-4612-1220-1"},{"key":"37_CR23","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 9th Int. Conf. Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"U. Stern and D. L. Dill. Parallelizing the Mur\u03d5 verifier. In Proc. 9th Int. Conf. Computer Aided Verification, volume 1254 of LNCS, Springer, 1997."},{"key":"37_CR24","volume-title":"Games for bisimulation and model checking","author":"C. Stirling","year":"1996","unstructured":"C. Stirling. Games for bisimulation and model checking, July 1996. Notes for Mathfit Workshop on finite model theory, University of Wales, Swansea,."},{"key":"37_CR25","volume-title":"Implementation of an effcient parallel BDD package","author":"A. L. Stornetta","year":"1995","unstructured":"A. L. Stornetta. Implementation of an effcient parallel BDD package. Master\u2019s thesis, University of California, Santa Barbara, 1995."},{"key":"37_CR26","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. 9th Annual IEEE Symposium on Logic in Computer Science, pages 154\u2013163, 1994. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1994.316075"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45319-9_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:43:48Z","timestamp":1629369828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_37","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}