{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,28]],"date-time":"2024-06-28T21:34:07Z","timestamp":1719610447258},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,7,8]],"date-time":"2006-07-08T00:00:00Z","timestamp":1152316800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,9]]},"DOI":"10.1007\/s10703-006-0007-0","type":"journal-article","created":{"date-parts":[[2006,7,7]],"date-time":"2006-07-07T14:03:05Z","timestamp":1152280985000},"page":"177-196","source":"Crossref","is-referenced-by-count":9,"title":["Distributed disk-based algorithms for model checking very large Markov chains"],"prefix":"10.1007","volume":"29","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":[[2006,7,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","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 Comp Syst 2(2):93\u2013122","DOI":"10.1145\/190.191"},{"key":"7_CR2","unstructured":"Ajmone Marsanan M, Balbo G, Conte G, Donatelli S, Franceschinis G (1995) Modelling with Generalized Stochastic Petri Nets, Wiley Series in Parallel Computing. Wiley"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Allmaier S, Kowarschik M, Horton G (1997) State space construction and steady-state solution of GSPNs on a shared-memory multiprocessor. In: Proceedings of the 7th International Workshop on Petri Nets and Performance Models. pp 112\u2013121","DOI":"10.1109\/PNPM.1997.595542"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Baier C, Haverkort B, Hermanns H, Katoen J (2003) Model-checking algorithms for continuous-Time Markov Chains. IEEE Trans Softw Eng 29(6):524\u2013541","DOI":"10.1109\/TSE.2003.1205180"},{"key":"7_CR5","unstructured":"Bell A (2004) Distributed evaluation of stochastic Petri nets. Ph.D. thesis, Rheinisch-Westfalische Technischen Hochschule Aachen. ISBN-Nr.: 3-930376-36-9"},{"key":"7_CR6","unstructured":"Bell A, Haverkort B (2001) Serial and parallel out-of-core solution of linear systems arising from generalised stochastic Petri net models. In: Tentner A (ed) Proceedings high performance computing symposium HPC 2001. pp 242\u2013247"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Bell A, Haverkort B (2005) Sequential and distributed model checking of Petri nets. Softw Tools Technol Transf 7(1):43\u201360","DOI":"10.1007\/s10009-003-0129-2"},{"key":"7_CR8","unstructured":"Carney S, Heroux M, Li G (1993) A proposal for a sparse BLAS toolkit. Technical Report TR\/PA\/92\/90 (Revised), CERFACS, Toulouse, France"},{"key":"7_CR31","unstructured":"Ciardo G, Tilgner M (1996) On the use of Kronecker Operators for the Solution of Generalized Stochastic Petri Nets, ICASE, No. 96-35"},{"key":"7_CR9","unstructured":"Ciardo G, Fricks R, Muppala J, Trivedi K (1994) SPNP Reference Guide Version 3.1"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Ciardo G, Gluckman J, Nicol D (1998) Distributed state space generation of discrete-state stochastic models. INFORMS J Comput 10(1):82\u201393","DOI":"10.1287\/ijoc.10.1.82"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Ciardo G, Trivedi K (1993) A decomposition approach for stochastic reward Net Models. Perform Eval 18(3):37\u201359","DOI":"10.1016\/0166-5316(93)90026-Q"},{"key":"7_CR12","unstructured":"Cormen T, Leiserson C, Rivest R (1990) Introduction to Algorithms. MIT Press"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Deavours D, Sanders W (1998) An efficient disk-based tool for solving large Markov Models. Perform Eval 33(1):67\u201384","DOI":"10.1016\/S0166-5316(98)00010-8"},{"key":"7_CR14","unstructured":"Dutt I, Grimes R, Lewis J (1992) \u2018Users\u2019 Guide for the Harwell-Boeing Sparse Matrix Collection (Release I). Technical Report RAL 92-086, Rutherford Appleton Laboratory, Chilton, Oxon, England"},{"key":"7_CR15","unstructured":"Forum MPI (1994) MPI: A message-passing interface standard. Technical Report UT-CS-94-230, University of Tennessee Computer Science Department"},{"key":"7_CR16","unstructured":"Foster I (1995) Designing and building parallel programs. Addison-Wesley"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Gropp W, Lusk E, Doss N, Skjellum A (1996) A high-performance, portable implementation of the MPI message passing interface standard. Parallel Comput 22(6):789\u2013828","DOI":"10.1016\/0167-8191(96)00024-5"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Gropp WD, Lusk E (1996) User's Guide for $${\\tt mpich}$$ , a portable implementation of MPI. Mathematics and Computer Science Division, Argonne National Laboratory. ANL-96\/6","DOI":"10.2172\/378910"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Haverkort B (1998) Performance of computer communication systems: A model-based approach. Wiley","DOI":"10.1002\/0470841923"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"Haverkort B, 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. pp 12\u201321","DOI":"10.1109\/PNPM.1999.796528"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Hermanns H, Kwiatkowska M, Norman G, Parker D, Siegle M (2003) On the use of MTBDDs for performability analysis and verication of stochastic systems. J Log Algeb Progr: Special Issue on Probabilistic Techniques for the Design and Analysis of Systems 56(1\u20132):23\u201367","DOI":"10.1016\/S1567-8326(02)00066-8"},{"key":"7_CR22","unstructured":"Hermanns H, Meyer-Kayser J, Siegle M (1999) Multi-terminal binary decision diagrams to represent and analyse continuous time markov chains. In: Plateau B, Stewart W, Silva M (eds) Proceedings of the 3rd Int. workshop on the numerical solution of Markov chains. pp 188\u2013207"},{"key":"7_CR23","unstructured":"Knottenbelt W, Harrison P (1999) Distributed disk-based solution techniques for large Markov models. In: Proceedings of the 3rd International meeting on the numerical solution of Markov chains. pp 58\u201375"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Knottenbelt W, Harrison P, Mestern M, Kritzinger P (2000) A probabilistic dynamic technique for the distributed generation of very large state spaces. Perform Eval 39(1\u20134):127\u2013148","DOI":"10.1016\/S0166-5316(99)00061-9"},{"key":"7_CR25","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 N, Serra B (eds) Computer performance evaluation, Vol 1469 of Lecture Notes in Computer Science. pp 165\u2013179","DOI":"10.1007\/3-540-68061-6_14"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Mehmood R (2002) Out-of-core solution of large linear systems of equations arising from stochastic modelling. In: Proc PAPM-PROBMIV, Vol. 2399 of Lecture Notes in Computer Science. pp 135\u2013151","DOI":"10.1007\/3-540-45605-8_9"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Mehmood R, Norman G, Parker D (2002) A symbolic out-of-core solution method for markov models. Electr Notes Theor Comput Sci 68(4)","DOI":"10.1016\/S1571-0661(05)80394-9"},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Parker D, Zhang Y, Mehmood R (2004) Dual-processor parallelisation of symbolic probabilistic model checking. In: Proceedings IEEE MASCOTS. pp 123\u2013130","DOI":"10.1109\/MASCOT.2004.1348189"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Marenzoni P, Caselli S, Conte G (1997) Analysis of large GSPN models: a distributed solution tool. In: Proceedings of the 7th International workshop on petri nets and performance models. pp 122\u2013131","DOI":"10.1109\/PNPM.1997.595543"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Stewart W (1994) Introduction to the mumerical solution of Markov chains. Princeton University Press","DOI":"10.1515\/9780691223384"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0007-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0007-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0007-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,8]],"date-time":"2023-05-08T00:16:10Z","timestamp":1683504970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0007-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,8]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["7"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0007-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,7,8]]}}}