{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T20:00:55Z","timestamp":1743019255386,"version":"3.40.3"},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030918248"},{"type":"electronic","value":"9783030918255"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91825-5_5","type":"book-chapter","created":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T12:02:50Z","timestamp":1637928170000},"page":"79-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["DiPS: A Tool for Data-Informed Parameter Synthesis for Markov Chains from Multiple-Property Specifications"],"prefix":"10.1007","author":[{"given":"Matej","family":"Hajnal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"\u0160afr\u00e1nek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tatjana","family":"Petrov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,27]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-030-61362-4_19","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"P Ashok","year":"2020","unstructured":"Ashok, P., Daca, P., K\u0159et\u00ednsk\u00fd, J., Weininger, M.: Statistical model checking: black or white? In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 331\u2013349. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_19"},{"key":"5_CR2","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, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22264-6_6"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1214\/ss\/1009213286","volume":"16","author":"LD Brown","year":"2001","unstructured":"Brown, L.D., Cai, T.T., DasGupta, A.: Interval estimation for a binomial proportion. Stat. Sci. 16, 101\u2013117 (2001)","journal-title":"Stat. Sci."},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-319-66335-7_20","volume-title":"Quantitative Evaluation of Systems","author":"R Calinescu","year":"2017","unstructured":"Calinescu, R., \u010ce\u0161ka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: RODES: a robust-design synthesis tool for\u00a0probabilistic systems. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 304\u2013308. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66335-7_20"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-662-49674-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M \u010ce\u0161ka","year":"2016","unstructured":"\u010ce\u0161ka, M., Pila\u0159, P., Paoletti, N., Brim, L., Kwiatkowska, M.: PRISM-PSY: precise GPU-accelerated parameter synthesis for stochastic systems. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 367\u2013384. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_21"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"issue":"4","key":"5_CR7","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1093\/jssam\/smv024","volume":"3","author":"N Dean","year":"2015","unstructured":"Dean, N., Pagano, M.: Evaluating confidence interval methods for binomial proportions in clustered surveys. J. Surv. Stat. Methodol. 3(4), 484\u2013503 (2015)","journal-title":"J. Surv. Stat. Methodol."},{"key":"5_CR8","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., et al.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214\u2013231. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_13"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"5_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-030-01090-4_18","volume-title":"Automated Technology for Verification and Analysis","author":"P Gainer","year":"2018","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 300\u2013316. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_18"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-20398-5_12","volume-title":"NASA Formal Methods","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146\u2013161. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_12"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_56"},{"issue":"1","key":"5_CR13","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. Transf. 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-030-31304-3_32","volume-title":"Computational Methods in Systems Biology","author":"M Hajnal","year":"2019","unstructured":"Hajnal, M., Nouvian, M., Petrov, T., \u0160afr\u00e1nek, D.: Data-informed parameter synthesis for population Markov chains. In: Bortolussi, L., Sanguinetti, G. (eds.) CMSB 2019. LNCS, vol. 11773, pp. 383\u2013386. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31304-3_32"},{"issue":"4","key":"5_CR15","first-page":"445","volume":"128","author":"YS Han","year":"2013","unstructured":"Han, Y.S.: State elimination heuristics for short regular expressions. Fund. Inform. 128(4), 445\u2013462 (2013)","journal-title":"Fund. Inform."},{"issue":"13","key":"5_CR16","doi-asserted-by":"publisher","first-page":"1743","DOI":"10.1001\/jama.1983.03330370053031","volume":"249","author":"J Hanley","year":"1983","unstructured":"Hanley, J., Lippman-Hand, A.: If nothing goes wrong, is everything all right? Interpreting zero numerators. JAMA 249(13), 1743\u20131745 (1983)","journal-title":"JAMA"},{"issue":"5","key":"5_CR17","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Aspects Comput."},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-10696-0_31","volume-title":"Quantitative Evaluation of Systems","author":"N Jansen","year":"2014","unstructured":"Jansen, N., et al.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol. 8657, pp. 404\u2013420. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10696-0_31"},{"key":"5_CR19","unstructured":"Junges, S., et al.: Parameter synthesis for Markov models. CoRR abs\/1903.07993 (2019). http:\/\/arxiv.org\/abs\/1903.07993"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 31\u201345. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"5_CR21","unstructured":"Knuth, D., Yao, A.: The complexity of nonuniform random number generation. In: Algorithms and Complexity: New Directions and Recent Results. Academic Press (1976)"},{"key":"5_CR22","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"6","key":"5_CR23","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1063\/1.1699114","volume":"21","author":"N Metropolis","year":"1953","unstructured":"Metropolis, N., Rosenbluth, A.W., Rosenbluth, M.N., Teller, A.H., Teller, E.: Equation of state calculations by fast computing machines. J. Chem. Phys. 21(6), 1087\u20131092 (1953)","journal-title":"J. Chem. Phys."},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-43425-4_3","volume-title":"Quantitative Evaluation of Systems","author":"E Polgreen","year":"2016","unstructured":"Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A.: Data-efficient Bayesian verification of parametric Markov chains. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 35\u201351. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43425-4_3"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-319-46520-3_4","volume-title":"Automated Technology for Verification and Analysis","author":"T Quatmann","year":"2016","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50\u201367. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_4"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Seabold, S., Perktold, J.: Statsmodels: econometric and statistical modeling with Python. In: 9th Python in Science Conference (2010)","DOI":"10.25080\/Majora-92bf1922-011"},{"key":"5_CR27","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-030-72016-2_10","volume":"12651","author":"J Spel","year":"2021","unstructured":"Spel, J., Junges, S., Katoen, J.P.: Finding provably optimal Markov chains. Tools Algorithms Const. Anal. Syst. 12651, 173 (2021)","journal-title":"Tools Algorithms Const. Anal. Syst."}],"container-title":["Lecture Notes in Computer Science","Performance Engineering and Stochastic Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91825-5_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,26]],"date-time":"2021-11-26T12:03:30Z","timestamp":1637928210000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91825-5_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030918248","9783030918255"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91825-5_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"27 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"EPEW","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Workshop on Performance Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 December 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 December 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"epew2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}