{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:24Z","timestamp":1761611124622},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2004,4,6]],"date-time":"2004-04-06T00:00:00Z","timestamp":1081209600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2005,2]]},"DOI":"10.1007\/s10009-003-0129-2","type":"journal-article","created":{"date-parts":[[2004,4,7]],"date-time":"2004-04-07T08:17:12Z","timestamp":1081325832000},"page":"43-60","source":"Crossref","is-referenced-by-count":25,"title":["Sequential and distributed model checking of Petri nets"],"prefix":"10.1007","volume":"7","author":[{"given":"Alexander","family":"Bell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boudewijn R.","family":"Haverkort","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,4,6]]},"reference":[{"key":"129_CR1","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"Ajmone","year":"1984","unstructured":"Ajmone Marsan M, Conte G, Balbo G (1984) A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans Comput Sys 2(2):93\u2013122","journal-title":"ACM Trans Comput Sys"},{"key":"129_CR2","doi-asserted-by":"crossref","unstructured":"Baier C, Haverkort BR, Katoen J-P, Hermanns H (2000a) Formal specification and verification of performability properties. In: Montanari U, Rolin JDP, Welzl E (eds) Proceedings of ICALP 2000, Geneva, Switzerland, 9\u201315 July 2000. Lecture notes in computer science, vol 1853. Springer, Berlin Heidelberg New York, pp 780\u2013792","DOI":"10.1007\/3-540-45022-X_65"},{"key":"129_CR3","doi-asserted-by":"crossref","unstructured":"Baier C, Haverkort BR, Katoen J-P, Hermanns H (2000b) Model checking continuous-time Markov chains by transient analysis. In: Emerson EA, Sistla AP (eds) Proceedings of CAV 2000, Chicago, 15\u201319 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 358\u2013372","DOI":"10.1007\/10722167_28"},{"key":"129_CR4","unstructured":"Bell A (1999) Verteilte Bewertung stochastischer Petrinetze. Diploma thesis, RWTH Aachen, Department of Computer Science, March 1999"},{"key":"129_CR5","doi-asserted-by":"crossref","unstructured":"Ben-David S, Heyman T, Grumberg O, Schuster A (2000) Scalable distributed on-the-fly symbolic model checking. In: Proceedings of the 3rd international conference on formal methods in computer-aided design, Austin, TX, 1\u20133 November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 390\u2013404","DOI":"10.1007\/3-540-40922-X_24"},{"key":"129_CR6","doi-asserted-by":"crossref","unstructured":"Bollig B, Leucker M, Weber M (2001) Parallel model checking for the alternation-free \u03bc-calculus. In: Margaria T, Yi W (eds) Proceedings of the conference on tools and algorithms for the construction and analysis of systems (TACAS 2001), Genoa, Italy 2\u20136 April 2001. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 543\u2013558","DOI":"10.1007\/3-540-45319-9_37"},{"key":"129_CR7","doi-asserted-by":"crossref","unstructured":"Bollig B, Leucker M, Weber M (2002) Local parallel model checking for the alternation-free \u03bc-calculus. In: Bosnacki D, Leue S (eds) Proceedings of the 9th international SPIN workshop on model checking of software, Grenoble, France, 11\u201313 April 2002. Lecture notes in computer science, vol 2318. Springer, Berlin Heidelberg New York, pp 128\u2013147","DOI":"10.1007\/3-540-46017-9_11"},{"key":"129_CR8","doi-asserted-by":"crossref","unstructured":"Brim L, Crhova J, Yorav K (2002) Using assumptions to distribute CTL model checking. In: Brim L, Grumberg O (eds) Electronic notes in theoretical computer science, vol. 68. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(05)80758-3"},{"key":"129_CR9","unstructured":"Ciardo G, Tilgner M (1996) On the use of Kronecker operators for the solution of generalized stochastic Petri nets. Technical Report No. 96\u201335, ICASE, 1996"},{"key":"129_CR10","unstructured":"Ciardo G, Muppala JK, Trivedi KS (1989) SPNP: stochastic Petri net package. In: Proceedings of the 3rd international workshop on Petri nets and performance models, Kyoto, Japan, 11\u201313 December 1989. IEEE Press, New York, pp 142\u2013151"},{"key":"129_CR11","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1287\/ijoc.10.1.82","volume":"10","author":"Ciardo","year":"1998","unstructured":"Ciardo G, Gluckman J, Nicol D (1998) Distributed state space generation of discrete-state stochastic models. INFORMS J Comput 10(1):82\u201393","journal-title":"INFORMS J Comput"},{"key":"129_CR12","doi-asserted-by":"crossref","unstructured":"Ciardo G, L\u00fcttgen G, Siminiceanu R (2001a) Saturation: an efficient iteration strategy for symbolic state-space generation. Lecture notes in computer science, vol 2031. Springer, Berlin Heidelberg New York, pp 328\u2013342","DOI":"10.1007\/3-540-45319-9_23"},{"key":"129_CR13","doi-asserted-by":"crossref","unstructured":"Ciardo G, L\u00fcttgen G, Siminiceanu R (2001b) Saturation: an efficient iteration strategy for symbolic state-space generation. Technical report, ICASE, 2001","DOI":"10.1007\/3-540-45319-9_23"},{"key":"129_CR14","unstructured":"Clarke EM, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"129_CR15","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Programm Lang Sys 8(2):244\u2013263","journal-title":"ACM Trans Programm Lang Sys"},{"key":"129_CR16","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1109\/88.281869","volume":"2","author":"Crowl","year":"1994","unstructured":"Crowl LA (1994) How to measure, present, and compare parallel performance. IEEE Parallel Distrib Technol 2(1):9\u201325","journal-title":"IEEE Parallel Distrib Technol"},{"key":"129_CR17","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specification for finite-state verification. In: Proceedings of the 21st international conference on softwware engineering, Los Angeles, 16\u201322 May 1999. IEEE Press, New York, pp 411\u2013420","DOI":"10.1145\/302405.302672"},{"key":"129_CR18","first-page":"143","volume":"30","author":"Esparza","year":"1994","unstructured":"Esparza J, Nielsen M (1994) Decidability issues for Petri nets: a survey. Elektron Informationsverarbeit Kybern 30(3):143\u2013160","journal-title":"Elektron Informationsverarbeit Kybern"},{"key":"129_CR19","doi-asserted-by":"crossref","unstructured":"Garavel H, Mateescu R, Smarandache I (2001) Parallel state space construction for model-checking. In: Dwyer M (ed) Proceedings of SPIN 2001, Toronto, 19\u201320 May 2001. Lecture notes in computer science, vol 2057. Springer, Berlin Heidelberg New York, pp 217\u2013234","DOI":"10.1007\/3-540-45139-0_14"},{"key":"129_CR20","doi-asserted-by":"crossref","unstructured":"Grumberg O, Heyman T, Schuster A (2001) Distributed symbolic model checking for \u03bc-calculus. In: Finkel A, Berry G, Comon H (ed) Proceedings of the international conference on computer aided verification, Paris, 18\u201323 July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 350\u2013362","DOI":"10.1007\/3-540-44585-4_32"},{"key":"129_CR21","doi-asserted-by":"crossref","unstructured":"Haverkort BR (1998) Performance of computer-communication systems: a model-based approach. Wiley, New York","DOI":"10.1002\/0470841923"},{"key":"129_CR22","doi-asserted-by":"crossref","unstructured":"Haverkort BR, Bell A, Bohnenkamp H (1999) On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets. In: Proceedings of the 8th international workshop on Petri nets and performance models, Zaragosa, Spain, 8\u201310 September 1999. IEEE Press, New York, pp 12\u201321","DOI":"10.1109\/PNPM.1999.796528"},{"key":"129_CR23","doi-asserted-by":"crossref","unstructured":"Heyman T, Geist D, Grumberg O, Schuster A (2000) Achieving scalability in parallel reachability analysis of very large circuits. In: Grumberg O (ed) Proceedings of the 12th international conference on computer-aided verification, Chicago, 15\u201319 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 20\u201335","DOI":"10.1007\/10722167_6"},{"key":"129_CR24","first-page":"modelling","volume":"science","author":"Huth","year":"2000","unstructured":"Huth MRA, Ryan MD (2000) Logic in computer science: modelling and reasoning about systems. Cambridge University Press, Cambridge, UK","journal-title":"Logic in computer"},{"key":"129_CR25","unstructured":"Johr S (2002) MMD-based reachability set generation of stochastic models. Diploma thesis, Department of Computer Science, RWTH Aachen, Aachen, Germany, September 2002"},{"key":"129_CR26","unstructured":"Katoen J-P (1999) Concepts, algorithms, and tools for model checking, IMMD Berichte, vol 32. Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Germany, June 1999"},{"key":"129_CR27","doi-asserted-by":"crossref","unstructured":"Knottenbelt W, Mestern M, Harrison P, Kritzinger P (1998) Probability, parallelism and the state space exploration problem. In: Puigjaner R, Savino NN, Serra B (eds) Computer performance evaluation. Lecture notes in computer science, vol 1469. Springer, Berlin Heidelberg New York, pp 165\u2013179","DOI":"10.1007\/3-540-68061-6_14"},{"key":"129_CR28","unstructured":"Knuth DE (1973) The art of computer programming, vol 3: Sorting and searching. Addison-Wesley, Reading, MA"},{"key":"129_CR29","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2002) PRISM: probabilistic symbolic model checker. In: Proceedings of TOOLS 2002, London, 14\u201317 April 2002. Lecture notes in computer science, vol 2324. Springer, Berlin Heidelberg New York, pp 200\u2013204","DOI":"10.1007\/3-540-46029-2_13"},{"key":"129_CR30","doi-asserted-by":"crossref","unstructured":"Laster K, Grumberg O (1998) Modular model checking of software. In: Proceedings of the conference on tools and algorithms for the construction and analysis of systems (TACAS 1998), Lisbon, Portugal, 28 March\u20134 April 1998. Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 20\u201335","DOI":"10.1007\/BFb0054162"},{"key":"129_CR31","unstructured":"MPICH \u2013 a portable implementation of MPI. www.mcs.anl.gov\/mpi\/mpich"},{"key":"129_CR32","doi-asserted-by":"crossref","unstructured":"Stern U, Dill DL (1997) Parallelizing the Mur\u03d5 verifier. In: Grumberg O (ed) Proceedings of the conference on computer aided verification, Haifa, Israel, 22\u201325 June 1997. Lecture notes in computer science, vol 1254. Springer, Berlin Heidelberg New York, pp 256\u2013267","DOI":"10.1007\/3-540-63166-6_26"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0129-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0129-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0129-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T22:26:29Z","timestamp":1585693589000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0129-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,4,6]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,2]]}},"alternative-id":["129"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0129-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,4,6]]}}}