{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T21:10:23Z","timestamp":1781298623185,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540421245","type":"print"},{"value":"9783540451396","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45139-0_14","type":"book-chapter","created":{"date-parts":[[2007,8,10]],"date-time":"2007-08-10T14:39:56Z","timestamp":1186756796000},"page":"217-234","source":"Crossref","is-referenced-by-count":79,"title":["Parallel state space construction for model-checking"],"prefix":"10.1007","author":[{"given":"Hubert","family":"Garavel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Mateescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Irina","family":"Smarandache","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"S. Allmaier, S. Dalibor, and D. Kreische. Parallel Graph Generation Algorithms for Shared and Distributed Memory Machines. In Proceedings of the Parallel Computing Conference PARCO\u201997 (Bonn, Germany). Springer-Verlag, 1997.","DOI":"10.1016\/S0927-5452(98)80074-9"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"S. Allmaier, M. Kowarschik, and G. Horton. State Space Construction and Steady-State Solution of GSPNs on a Shared-Memory Multiprocessor. In Proceedings of the 7th IEEE International Workshop on Petri Nets and Performance Models PNPM\u201997 (Saint Malo, France), pages 112\u2013121. IEEE CS-Press, 1997.","DOI":"10.1109\/PNPM.1997.595542"},{"key":"14_CR3","unstructured":"ANSI. Small Computer System Interface-2. Standard X3.131-1994, American National Standards Institute, January 1994."},{"key":"14_CR4","first-page":"109","volume":"60","author":"J. A. Bergstra","year":"1984","unstructured":"J. A. Bergstra and J. W. Klop. Process Algebra for Synchronous Communication. Information and Computation, 60:109\u2013137, 1984.","journal-title":"Information and Computation"},{"key":"14_CR5","series-title":"Lect Notes Comput Sci","volume-title":"Computer Performance Evaluation: Modelling Techniques and Tools","author":"S. Caselli","year":"1994","unstructured":"S. Caselli, G. Conte, F. Bonardi, and M. Fontanesi. Experiences on SIMD Massively Parallel GSPN Analysis. In G. Haring and G. Kotsis, editors, Computer Performance Evaluation: Modelling Techniques and Tools, volume 794. Lecture Notes in Computer Science, Springer-Verlag, 1994."},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1007\/3-540-60029-9_40","volume-title":"Applications and Theory of Petri Nets 1995","author":"S. Caselli","year":"1995","unstructured":"S. C aselli, G. Conte, and P. Marenzoni. Parallel State Space Exploration for GSPN Models. In G. De Michelis and M. Diaz, editors, Applications and Theory of Petri Nets 1995, volume 935, pages 181\u2013200. Lecture Notes in Computer Science, Springer-Verlag, 1995."},{"issue":"5","key":"14_CR7","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1145\/359104.359108","volume":"22","author":"E. Chang","year":"1979","unstructured":"Ernest Chang and Rosemary Roberts. An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes. Communications of the ACM, 22(5):281\u2013283, may 1979.","journal-title":"Communications of the ACM"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"G. Ciardo, J. Gluckman, and D. Nicol. Distributed State Space Generation of Discrete-State Stochastic Models. INFORMS Journal of Computing, 1997.","DOI":"10.1287\/ijoc.10.1.82"},{"issue":"4","key":"14_CR9","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"A. Cimatti","year":"2000","unstructured":"A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. NUSMV: a New Symbolic Model Checker. Springer International Journal on Software Tools for Technology Transfer (STTT), 2(4):410\u2013425, April 2000.","journal-title":"Springer International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"14_CR10","unstructured":"E. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2000."},{"key":"14_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Proceedings of the 8th International Conference on Computer-Aided Verification CAV\u201996","author":"D. Dill","year":"1996","unstructured":"D. Dill. The Mur\u03b5 Verification System. In R. Alur and T. Henzinger, editors, Proceedings of the 8th International Conference on Computer-Aided Verification CAV\u201996, volume 1102 of Lecture Notes in Computer Science, pages 390\u2013393. Springer Verlag, July 1996."},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA)","author":"J.-C. Fernandez","year":"1996","unstructured":"Jean-Claude Fernandez, Hubert Garavel, Alain Kerbrat, Radu Mateescu, Laurent Mounier, and Mihaela Sighireanu. CADP (C\u00c6SAR\/ALDEBARAN Development Package): A Protocol Validation and Verification Toolbox. In Rajeev Alur and Thomas A. Henzinger, editors, Proceedings of the 8th Conference on Computer-Aided Verification (New Brunswick, New Jersey, USA), volume 1102 of Lecture Notes in Computer Science, pages 437\u2013440. Springer Verlag, August 1996."},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"OPEN\/C\u00c6SAR: An Open Software Architecture for Verification, Simulation, and Testing","author":"H. Garavel","year":"1998","unstructured":"Hubert Garavel. OPEN\/C\u00c6SAR: An Open Software Architecture for Verification, Simulation, and Testing. In Bernhard Steffen, editor, Proceedings of the First International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS\u201998 (Lisbon, Portugal), volume 1384 of Lecture Notes in Computer Science, pages 68\u201384, Berlin, March 1998. Springer Verlag. Full version available as INRIA Research Report RR-3352."},{"issue":"1-2","key":"14_CR14","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00034-2","volume":"29","author":"H. Garavel","year":"1997","unstructured":"Hubert Garavel and Laurent Mounier. Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks. Science of Computer Programming, 29(1-2):171\u2013197, July 1997. Special issue on Industrially Relevant Applications of Formal Analysis Techniques. Full version available as INRIA Research Report RR-2986.","journal-title":"Science of Computer Programming"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"W. Gropp, S. Huss-Lederman, A. Lumsdaine, E. Lusk, B. Nitzberg, W. Saphir, and M. Snir. MPI: The Complete Reference, Vol. 2 \u2014 The MPI-2 Extensions. MIT Press, 1998.","DOI":"10.7551\/mitpress\/4789.001.0001"},{"key":"14_CR16","unstructured":"B. Haverkort, H. Bohnenkamp, and A. Bell. On the Efficient Sequential and Distributed Evaluation of Very Large Stochastic Petri Nets. In Proceedings PNPM\u201999 (Petri Nets and Performance Models). IEEE CS-Press, 1999."},{"key":"14_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1007\/10722167_6","volume-title":"Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits","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 E. A. Emerson and A. P. Sistla, editors, Proceedings of the 12th International Conference on Computer-Aided Verification CAV\u20192000 (Chicago, IL, USA), volume 1855 of Lecture Notes in Computer Science, pages 20\u201335. Springer Verlag, July 2000."},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"5","key":"14_CR19","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The Model Checker SPIN. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"14_CR20","unstructured":"Gerard J. Holzmann. Design and Validation of Computer Protocols. Software Series. Prentice Hall, 1991."},{"key":"14_CR21","unstructured":"ISO\/IEC. LOTOS \u2014 A Formal Description Technique Based on the Temporal Ordering of Observational Behavior. International Standard 8807, International Organization for Standardization \u2014 Information Processing Systems \u2014 Open Systems Interconnection, Gen\u00e8ve, September 1988."},{"key":"14_CR22","unstructured":"J-M. J\u00e9z\u00e9quel, W.M. Ho, A. Le Guennec, and F. Pennaneac\u2019h. UMLAUT: an Extendible UML Transformation Framework. In R.J. Hall and E. Tyugu, editors, Proceedings of the 14th IEEE International Conference on Automated Software Engineering ASE\u201999. IEEE, 1999. Also available as INRIA Technical Report RR-3775."},{"key":"14_CR23","unstructured":"W. J. Knottenbelt and P. G. Harrison. Distributed Disk-Based Solution Techniques for Large Markov Models. In Proceedings of the 3rd International Meeting on the Numerical Solution of Markov Chains NSMC\u201999, Zaragoza, Spain, September 1999."},{"key":"14_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"165","DOI":"10.1007\/3-540-68061-6_14","volume-title":"Proceedings of the 10th International Conference on Modelling, Techniques and Tools (TOOLS\u2019 98)","author":"W. J. Knottenbelt","year":"1998","unstructured":"W. J. Knottenbelt, M. A. Mestern, P. G. Harrison, and P. Kritzinger. Probability, Parallelism and the State Space Exploration Problem. In Proceedings of the 10th International Conference on Modelling, Techniques and Tools (TOOLS\u2019 98), pages 165\u2013179. LNCS 1469, September 1998."},{"key":"14_CR25","first-page":"155","volume-title":"Information Processing","author":"G. L. Lann","year":"1977","unstructured":"G\u00e9rard Le Lann. Distributed Systems \u2014 Towards a Formal Approach. In B. Gilchrist, editor, Information Processing 77, pages 155\u2013160. IFIP, North-Holland, 1977."},{"key":"14_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking SPIN\u201999","author":"F. Lerda","year":"1999","unstructured":"F. Lerda and R. Sista. Distributed-Memory Model Checking with SPIN. In D. Dams, R. Gerth, S. Leue, and M. Massink, editors, Proceedings of the 5th and 6th International SPIN Workshops on Theoretical and Practical Aspects of SPIN Model Checking SPIN\u201999, volume 1680 of Lecture Notes in Computer Science, pages 22\u201339. Springer Verlag, July 1999."},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"P. Marenzoni, S. Caselli, and G. Conte. Analysis of Large GSPN Models: a Distributed Solution Tool. In Proceedings of the 7th International Workshop on Petri Nets and Performance Models, pages 122\u2013131. IEEE Computer Society Press, 1997.","DOI":"10.1109\/PNPM.1997.595543"},{"key":"14_CR28","unstructured":"Radu Mateescu and Mihaela Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. In Stefania Gnesi, Ina Schieferdecker, and Axel Rennoch, editors, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS\u20192000 (Berlin, Germany), GMD Report 91, pages 65\u201386, Berlin, April 2000. Also available as INRIA Research Report RR-3899."},{"key":"14_CR29","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/BF01782776","volume":"2","author":"F. Mattern","year":"1987","unstructured":"F. Mattern. Algorithms for Distributed Termination Detection. Distributed Computing, 2:161\u2013175, 1987.","journal-title":"Distributed Computing"},{"key":"14_CR30","unstructured":"Robin Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"key":"14_CR31","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1006\/jpdc.1997.1409","volume":"47","author":"D. Nicol","year":"1997","unstructured":"D. Nicol and G. Ciardo. Automated Parallelization of Discrete State-Space Generation. Journal of Parallel and Distributed Computing, 47:153\u2013167, 1997.","journal-title":"Journal of Parallel and Distributed Computing"},{"key":"14_CR32","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/3-540-63141-0_2","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory CONCUR\u201997","author":"Y.S. Ramakrishna","year":"1997","unstructured":"Y.S. Ramakrishna and S.A. Smolka. Partial-Order Reduction in the Weak Modal Mu-Calculus. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the 8th International Conference on Concurrency Theory CONCUR\u201997, volume 1243 of Lecture Notes in Computer Science, pages 5\u201324. Springer Verlag, 1997."},{"key":"14_CR33","series-title":"Technical Report SEN-R9915","volume-title":"Model Checking the HAVi Leader Election Protocol","author":"J. Romijn","year":"1999","unstructured":"Judi Romijn. Model Checking the HAVi Leader Election Protocol. Technical Report SEN-R9915, CWI, Amsterdam, The Netherlands, June 1999. submitted to Formal Methods in System Design."},{"key":"14_CR34","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","author":"U. Stern","year":"1997","unstructured":"U. Stern and D. Dill. Parallelizing the Mur\u03b5 Verifier. In Computer Aided Verification, volume 1254, pages 256\u2013267. Lecture Notes in Computer Science, Springer-Verlag, 1997."}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45139-0_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,13]],"date-time":"2023-05-13T19:05:13Z","timestamp":1684004713000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45139-0_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421245","9783540451396"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-45139-0_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}