{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T01:07:25Z","timestamp":1788052045430,"version":"build-2784847793"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_21","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"367-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems"],"prefix":"10.1007","author":[{"given":"Milan","family":"\u010ce\u0161ka","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Petr","family":"Pila\u0159","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicola","family":"Paoletti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lubo\u0161","family":"Brim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102. Springer, Heidelberg (1996)"},{"issue":"04","key":"21_CR2","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1017\/S0960129512000254","volume":"23","author":"C Baier","year":"2013","unstructured":"Baier, C., Hahn, E.M., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model checking for performability. Math. Struct. Comput. Sci. 23(04), 751\u2013795 (2013)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"9","key":"21_CR3","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1016\/j.jpdc.2011.10.015","volume":"72","author":"J Barnat","year":"2012","unstructured":"Barnat, J., Bauch, P., Brim, L., \u010ce\u0161ka, M.: Designing fast LTL model checking algorithms for many-core GPUs. J. Parallel Distrib. Comput. 72(9), 1083\u20131097 (2012)","journal-title":"J. Parallel Distrib. Comput."},{"key":"21_CR4","unstructured":"Bell, N., Garland, M.: Efficient sparse matrix-vector multiplication on CUDA. NVIDIA Technical report NVR-2008-004, NVIDIA Corporation (2008)"},{"key":"21_CR5","doi-asserted-by":"publisher","DOI":"10.1002\/0471791571","volume-title":"Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications","author":"G Bolch","year":"2006","unstructured":"Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. Wiley, New Jersey (2006)"},{"key":"21_CR6","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time markov chains. CoRR ArXiv, 1402.1450 (2014)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-319-22264-6_6","volume-title":"Quantitative Evaluation of Systems","author":"L Bortolussi","year":"2015","unstructured":"Bortolussi, L., Milios, D., Sanguinetti, G.: U-check: model checking and parameter synthesis under uncertainty. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 89\u2013104. Springer, Heidelberg (2015)"},{"issue":"1","key":"21_CR8","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s10009-010-0176-4","volume":"13","author":"D Bo\u0161na\u010dki","year":"2010","unstructured":"Bo\u0161na\u010dki, D., Edelkamp, S., Sulewski, D., Wijs, A.: Parallel probabilistic model checking on general purpose graphics processors. Int. J. Softw. Tools Technol. Transf. 13(1), 21\u201335 (2010)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-642-38874-3_3","volume-title":"Formal Methods for Dynamical Systems","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., \u0160afr\u00e1nek, D.: Model checking of biological systems. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 63\u2013112. Springer, Heidelberg (2013)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-39799-8_7","volume-title":"Computer Aided Verification","author":"L Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 107\u2013123. Springer, Heidelberg (2013)"},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"Cardelli, L., Csik\u00e1sz-Nagy, A.: The cell cycle switch computes approximate majority. Scientific Reports, 2 (2012)","DOI":"10.1038\/srep00656"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1007\/978-3-319-12982-2_7","volume-title":"Computational Methods in Systems Biology","author":"M \u010ce\u0161ka","year":"2014","unstructured":"\u010ce\u0161ka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86\u201398. Springer, Heidelberg (2014)"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"\u010ce\u0161ka, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Submitted to Acta Informatica (2015)","DOI":"10.1007\/978-3-319-12982-2_7"},{"issue":"4","key":"21_CR14","doi-asserted-by":"publisher","first-page":"e94553","DOI":"10.1371\/journal.pone.0094553","volume":"9","author":"M \u010ceska","year":"2014","unstructured":"\u010ceska, M., \u0160afr\u00e1nek, D., Dra\u017ean, S., Brim, L.: Robustness analysis of stochastic biochemical systems. PLoS ONE 9(4), e94553 (2014)","journal-title":"PLoS ONE"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Hongyang, Q., Zhang, L.: Model repair for Markov decision processes. In: Theoretical Aspects of Software Engineering (TASE), pp. 85\u201392. IEEE (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Cloth, L., Haverkort, B.R.: Model checking for survivability! In: Quantitative Evaluation of Systems (QEST), pp. 145\u2013154. IEEE (2005)","DOI":"10.1109\/QEST.2005.21"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-319-21999-8_2","volume-title":"DNA Computing and Molecular Programming","author":"N Dalchau","year":"2015","unstructured":"Dalchau, N., Murphy, N., Petersen, R., Yordanov, B.: Synthesizing and tuning chemical reaction networks with specified behaviours. In: Phillips, A., Yin, P. (eds.) DNA 2015. LNCS, vol. 9211, pp. 16\u201333. Springer, Heidelberg (2015)"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-21690-4_13","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2015","unstructured":"Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., \u00c1brah\u00e1m, E.: PROPhESY: a probabilistic parameter synthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Heidelberg (2015)"},{"issue":"6","key":"21_CR19","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of bluetooth device discovery. Int. J. Softw. Tools Technol. Transfer 8(6), 621\u2013632 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Fang, J., Varbanescu, A.L., Sips, H.: A comprehensive performance comparison of CUDA and OpenCL. In: International Conference on Parallel Processing (ICCP). IEEE (2011)","DOI":"10.1109\/ICPP.2011.45"},{"issue":"4","key":"21_CR21","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"BL Fox","year":"1988","unstructured":"Fox, B.L., Glynn, P.W.: Computing poisson probabilities. Commun. ACM 31(4), 440\u2013445 (1988)","journal-title":"Commun. ACM"},{"issue":"25","key":"21_CR22","doi-asserted-by":"publisher","first-page":"2340","DOI":"10.1021\/j100540a008","volume":"81","author":"T Daniel","year":"1977","unstructured":"Daniel, T.: Gillespie.: exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340\u20132361 (1977)","journal-title":"J. Phys. Chem."},{"issue":"1","key":"21_CR23","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transfer (STTT) 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer (STTT)"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J.-P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Real-Time Systems Symposium (RTSS), pp. 173\u2013182. IEEE (2008)","DOI":"10.1109\/RTSS.2008.19"},{"key":"21_CR25","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Symposium on Reliable Distributed Systems (SRDS). IEEE (2000)"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"21_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"21_CR28","doi-asserted-by":"crossref","unstructured":"Madsen, C., Myers, C.J., Roehner, N., Winstead, C., Zhang, Z.: Utilizing stochastic model checking to analyze genetic circuits. In: Computational Intelligence in Bioinformatics and Computational Biology (CIBCB), pp. 379\u2013386. IEEE (2012)","DOI":"10.1109\/CIBCB.2012.6217255"},{"issue":"6","key":"21_CR29","doi-asserted-by":"crossref","first-page":"561","DOI":"10.3233\/JCS-2006-14604","volume":"14","author":"G Norman","year":"2006","unstructured":"Norman, G., Shmatikov, V.: Analysis of probabilistic contract signing. J. Comput. Secur. 14(6), 561\u2013589 (2006)","journal-title":"J. Comput. Secur."},{"key":"21_CR30","unstructured":"Pila\u0159, P.: Accelerating parameter synthesis for stochastic models. Master\u2019s thesis, Faculty of Informatics, Masaryk University, Czech Republic (2015)"},{"issue":"11","key":"21_CR31","doi-asserted-by":"publisher","first-page":"e1002218","DOI":"10.1371\/journal.pcbi.1002218","volume":"7","author":"R Steuer","year":"2011","unstructured":"Steuer, R., Waldherr, S., Sourjik, V., Kollmann, M.: Robust signal processing in living cells. PLoS Comput. Biol. 7(11), e1002218 (2011)","journal-title":"PLoS Comput. Biol."},{"issue":"3","key":"21_CR32","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1109\/MCSE.2010.69","volume":"12","author":"JE Stone","year":"2010","unstructured":"Stone, J.E., Gohara, D., Shi, G.: OpenCL: a parallel programming standard for heterogeneous computing systems. Comput. Sci. Eng. 12(3), 66\u201373 (2010)","journal-title":"Comput. Sci. Eng."},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1007\/978-3-642-31759-0_9","volume-title":"Model Checking Software","author":"AJ Wijs","year":"2012","unstructured":"Wijs, A.J., Bo\u0161na\u010dki, D.: Improving GPU sparse matrix-vector multiplication for probabilistic model checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 98\u2013116. Springer, Heidelberg (2012)"},{"key":"21_CR34","unstructured":"PRISM - Case Studies - Workstation Cluster. \n                      http:\/\/www.prismmodelchecker.org\/casestudies\/cluster.php\n                      \n                    . Accessed September 2015"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:13:44Z","timestamp":1585012424000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}