{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T07:17:45Z","timestamp":1781075865454,"version":"3.54.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,10,13]],"date-time":"2010-10-13T00:00:00Z","timestamp":1286928000000},"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":[[2011,1]]},"DOI":"10.1007\/s10009-010-0176-4","type":"journal-article","created":{"date-parts":[[2010,10,13]],"date-time":"2010-10-13T12:36:13Z","timestamp":1286973373000},"page":"21-35","source":"Crossref","is-referenced-by-count":34,"title":["Parallel probabilistic model checking on general purpose graphics processors"],"prefix":"10.1007","volume":"13","author":[{"given":"Dragan","family":"Bo\u0161na\u010dki","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damian","family":"Sulewski","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anton","family":"Wijs","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,10,13]]},"reference":[{"key":"176_CR1","doi-asserted-by":"crossref","unstructured":"Allmaier, S.C., Kowarschik, M., Horton, G.: State space construction and steady-state solution of GSPNs on a Shared-Memory Multiprocessor. In: Proceedings of 7th Intt. Workshop on Petri Nets and Performance Models (PNPM\u201997), pp. 112\u2013121. IEEE Comp. Soc. Press (1997)","DOI":"10.1109\/PNPM.1997.595542"},{"key":"176_CR2","first-page":"950","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier C., Katoen J.-P.: Principles of Model Checking, pp. 950. MIT Press, Cambridge (2008)"},{"issue":"6","key":"176_CR3","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier C., Katoen J.-P., Hermanns H., Haverkort B.: Model-checking algorithms for contiuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"176_CR4","unstructured":"Bal, H., Barnat, J., Brim, L., Verstoep, K.: Efficient large-scale model checking. In: IEEE International Parallel & Distributed Processing Symposium (IPDPS) (2009)"},{"key":"176_CR5","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ceska, M., Lamr, T.: CUDA accelerated LTL model checking. In: Proceedings of international conference on parallel and distributed systems (ICPADS), pp. 34\u201341 (2009)","DOI":"10.1109\/ICPADS.2009.50"},{"key":"176_CR6","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: Scalable multi-core model-checking. In: Model checking software, 14th international SPIN workshop, SPIN 07 LNCS, vol. 4595, pp. 187\u2013203. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73370-6_13"},{"key":"176_CR7","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I.: Cluster-based LTL model checking of large systems formal methods for components and objects. In: LNCS, vol. 4111, pp. 259\u2013279. Springer, Berlin (2005)","DOI":"10.1007\/11804192_13"},{"key":"176_CR8","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., Ceska, M., Tumova, J.: ProbDiVinE-MC: multi-core LTL model checker for probabilistic systems. In: International conference on the quantitative evaluaiton of systems QEST 2008, pp. 77\u201378. IEEE Compuer Society Press (2008)","DOI":"10.1109\/QEST.2008.29"},{"key":"176_CR9","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Ro\u010dkai, P.: DiVinE multi-core\u2014a parallel LTL model-checker. In: Automated technology for verification and analysis, ATVA 2008, LNCS, vol. 5311, pp. 234\u2013239. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88387-6_20"},{"key":"176_CR10","doi-asserted-by":"crossref","unstructured":"Barnat, J., Brim, L., Str\u00edbrn\u00e1, J.: Distributed LTL model checking in SPIN. In: Proceedings of the 8th Intl. Spin Workshop on Model Checking of Software, SPIN 2001, LNCS, vol. 2057, pp. 200\u2013216. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45139-0_13"},{"key":"176_CR11","unstructured":"Baskaran, M.M., Bordawekar, R.: Optimzing sparse matrix\u2013vector multiplication on GPUs using compile-time and run-time strategies. IBM Reserach Report, RC24704 (W0812-047) (2008)"},{"key":"176_CR12","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1007\/s10703-006-0007-0","volume":"29","author":"A. Bell","year":"2006","unstructured":"Bell A., Haverkort J.-P., Hermanns B.R.: Distribute disk-based algorithms for model checking very large Markov chains. Formal Methods Syst. Design 29, 177\u2013196 (2006)","journal-title":"Formal Methods Syst. Design"},{"key":"176_CR13","doi-asserted-by":"crossref","unstructured":"Blom, S., van de Pol, J., Weber, M.: LTSmin: Distributed and symbolic reachability. In: Proceedings of 22th Intl. Conf. Computer Aided Verification (CAV). LNCS, vol. 6174, pp. 354\u2013359. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-14295-6_31"},{"key":"176_CR14","doi-asserted-by":"crossref","unstructured":"Bo\u0161na\u010dki, D., Edelkamp, S., Sulewski, D.: Efficient probabilistic model checking on general purpose graphics processors. In: Proceedings of 16th International SPIN Workshop, LNCS, vol. 3925, pp. 32\u201349. Springer, Berlin (2006)","DOI":"10.1007\/978-3-642-02652-2_7"},{"key":"176_CR15","doi-asserted-by":"crossref","unstructured":"Cooperman, G., Finkelstein, L.: New methods for using Cayley graphs in interconnection networks. Discrete Appl. Math. 37\u201338: 95118 (1992)","DOI":"10.1016\/0166-218X(92)90127-V"},{"key":"176_CR16","unstructured":"Ciardo, G.: Distributed and Structured Analysis Approaches to Study Large and Complex Systems. Eur. Educ. Forum School Formal Methods Perform. Anal. 2000, 344\u2013374 (2000)"},{"key":"176_CR17","unstructured":"CUDA Data Parallel Primitives Library. http:\/\/gpgpu.org\/developer\/cudpp"},{"key":"176_CR18","unstructured":"CUDA Programming Forum. http:\/\/www.nvidia.com\/object\/cuda_home.html"},{"key":"176_CR19","unstructured":"Dai, P., Mausam, Weld, D.S.: External memory value iteration. In: Proceedings of the Twenty-Third AAAI Conf. on Artificial Intelligence (AAAI), pp. 898\u2013904 (2008)"},{"key":"176_CR20","unstructured":"Edelkamp, S., Sulewski, D.: Model Checking via Delayed Duplicate Detection on the GPU. Technical Report 821, Universit\u00e4t Dortmund, Fachberich Informatik, ISSN 0933-6192 (2008)"},{"key":"176_CR21","unstructured":"Edelkamp, S., Jabbar, S., Bonet, B.: External memory value iteration. In: Proceedigs of 17th Int. Conf. on Automated Planning and Scheduling, pp. 128\u2013135, AAAI Press (2007)"},{"key":"176_CR22","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D., Y\u00fccel, C.: Perfect hashing for state space exploration on the GPU. In: Proceedings of 20th Int. Conf. International Conference on Automated Planning and Scheduling, pp. 57\u201364 (2010)","DOI":"10.1609\/icaps.v20i1.13414"},{"key":"176_CR23","unstructured":"Edelkamp, S., Sulewski, D., Y\u00fccel, C.: GPU exploration of two-player games with perfect hash functions. In: Proceedings of third international symposium of combinatorial search (To appear)"},{"key":"176_CR24","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Proceedings of 19th Intl. Conf. Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 158\u2013163. Springer, Berlin (2006)","DOI":"10.1007\/978-3-540-73368-3_18"},{"key":"176_CR25","doi-asserted-by":"crossref","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.M.: Parallel State space construction for model-checking model checking software. In: 8th International SPIN Workshop, LNCS, vol. 2057, pp. 217\u2013234. Springer, Berlin (2001)","DOI":"10.1007\/3-540-45139-0_14"},{"issue":"5","key":"176_CR26","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson H., Jonsson B.: A Logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Aspects Comput."},{"key":"176_CR27","doi-asserted-by":"crossref","unstructured":"Haverkort, B., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Proceedings of 19th IEEE Symposium on Reliable Distributed Systems (SRDS\u201900), pp. 228\u2013237 (2000)","DOI":"10.1109\/RELDI.2000.885410"},{"issue":"2","key":"176_CR28","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/0020-0190(90)90107-9","volume":"35","author":"T. Herman","year":"1990","unstructured":"Herman T.: Probabilistic self-stabilization. Inform. Process. Lett. 35(2), 63\u201367 (1990)","journal-title":"Inform. Process. Lett."},{"key":"176_CR29","unstructured":"Hermanns, H., Meyer-Kayser, J., Siegle, M.: Multi terminal binary decision diagrams to represent and analyse continuous time Markov Chains. In: Proceedings of 3rd International Workshop on Numerical Solution of Markov Chains (NSMC\u201999), pp. 188\u2013207 (1999)"},{"issue":"10","key":"176_CR30","doi-asserted-by":"crossref","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann G.J., Bo\u0161na\u010dki D.: The Design of a multi-core extension of the Spin Model Checker. IEEE Trans. Softw. Eng. 33(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"176_CR31","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., Bo\u0161na\u010dki, D.: Multi-core model checking with spin. In: Proceedings of Parallel and Distributed Processing Symposium, IPDPS 2007, pp. 1\u20138. IEEE International (2007)","DOI":"10.1109\/IPDPS.2007.370410"},{"issue":"4","key":"176_CR32","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/j.entcs.2004.10.022","volume":"128","author":"C.P. Inggs","year":"2005","unstructured":"Inggs C.P., Barringer H.: CTL* model checking on a shared memory architecture. Electronic Notes Theor. Comput. Sci. 128(4), 107\u2013123 (2005)","journal-title":"Electronic Notes Theor. Comput. Sci."},{"issue":"4","key":"176_CR33","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1016\/S1571-0661(05)80395-0","volume":"68","author":"C.P. Inggs","year":"2002","unstructured":"Inggs C.P., Barringer H.: Effective state exploration for model checking on a shared memory architecture. Electronic Notes Theor. Comput. Sci. 68(4), 605\u2013620 (2002)","journal-title":"Electronic Notes Theor. Comput. Sci."},{"key":"176_CR34","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Computer performance evaluation, modelling techniques and tools 12th international conference, TOOLS 2002, LNCS, vol. 2324, pp. 200\u2013204. Springer, Berlin (2005)","DOI":"10.1007\/3-540-46029-2_13"},{"key":"176_CR35","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal methods for the design of computer, communication and software systems: performance evaluation, LNCS, vol. 4486, pp. 220\u2013270. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"176_CR36","doi-asserted-by":"crossref","unstructured":"Lerda, F., Sisto, R.: Distributed model checking in SPIN. In: Theoretical and Practical Aspects of SPIN Model Checking, 5th and 6th International SPIN Workshops, LNCS, vol. 1680, pp. 22\u201339. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48234-2_3"},{"issue":"9","key":"176_CR37","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1145\/1284621.1284622","volume":"50","author":"A. Marowka","year":"2007","unstructured":"Marowka A.: Parallel computing on any desktop. Commun. ACM 50(9), 75\u201378 (2007)","journal-title":"Commun. ACM"},{"key":"176_CR38","unstructured":"OpenCL: The open standard for parallel programming of heterogeneous systems http:\/\/www.khronos.org\/opencl\/"},{"key":"176_CR39","doi-asserted-by":"crossref","first-page":"1781","DOI":"10.1002\/jcc.20289","volume":"26","author":"J.C. Philips","year":"2005","unstructured":"Philips J.C., Braun R., Wang W., Gumbart J., Tajkhorshid E., Villa E., Chipot C., Skeel R.D., Kale L., Sculten K.: Scalable molecular dynamics with NAMD. J. Comput. Chem. 26, 1781\u20131802 (2005)","journal-title":"J. Comput. Chem."},{"key":"176_CR40","unstructured":"Sengupta, S., Harris, M., Zhang, Y., Owens, J.D.: Scan primitives for GPU computing. In: Graphics Hardware 2007, pp. 97\u2013106 (2007)"},{"key":"176_CR41","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.: Parallelizing the Mur $${\\phi}$$ Verifier. In: Proceedings of 9th Intl. Conf. Computer Aided Verification (CAV), LNCS, vol. 1254, pp. 256\u2013278. Springer, Berlin (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"key":"176_CR42","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"W.J. Stewart","year":"1994","unstructured":"Stewart W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"key":"176_CR43","unstructured":"ATI Stream technology http:\/\/www.amd.com\/stream"},{"key":"176_CR44","doi-asserted-by":"crossref","unstructured":"Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models, LNCS Tutorials, LNCS, vol. 1491, pp. 429\u2013528. Springer, Berlin (1998)","DOI":"10.1007\/3-540-65306-6_21"}],"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-010-0176-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0176-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0176-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,3]],"date-time":"2023-06-03T20:08:35Z","timestamp":1685822915000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0176-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,10,13]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["176"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0176-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,10,13]]}}}