{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T11:46:39Z","timestamp":1787312799603,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720155","type":"print"},{"value":"9783030720162","type":"electronic"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,20]],"date-time":"2021-03-20T00:00:00Z","timestamp":1616198400000},"content-version":"vor","delay-in-days":78,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Parametric Markov chains (pMCs) are Markov chains with symbolic (aka: parametric) transition probabilities. They are a convenient operational model to treat robustness against uncertainties. A typical objective is to find the parameter values that maximize the reachability of some target states. In this paper, we consider automatically proving robustness, that is, an\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\varepsilon $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>\u03b5<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -close upper bound on the maximal reachability probability. The result of our procedure actually provides an almost-optimal parameter valuation along with this upper bound.\n                  <\/jats:p>\n                  <jats:p>We propose to tackle these ETR-hard problems by a tight combination of two significantly different techniques: monotonicity checking and parameter lifting. The former builds a partial order on states to check whether a pMC is (local or global) monotonic in a certain parameter, whereas parameter lifting is an abstraction technique based on the iterative evaluation of pMCs without parameter dependencies. We explain our novel algorithmic approach and experimentally show that we significantly improve the time to determine almost-optimal synthesis.<\/jats:p>","DOI":"10.1007\/978-3-030-72016-2_10","type":"book-chapter","created":{"date-parts":[[2021,3,19]],"date-time":"2021-03-19T18:03:37Z","timestamp":1616177017000},"page":"173-190","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Finding Provably Optimal Markov Chains"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9113-2791","authenticated-orcid":false,"given":"Jip","family":"Spel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,20]]},"reference":[{"key":"10_CR1","unstructured":"\u00c1brah\u00e1m, E., Bartocci, E., Bonakdarpour, B., Dobe, O.: Parameter synthesis for probabilistic hyperproperties. In: Proc. of LPAR. EPiC Series in Computing, vol.\u00a073, pp. 12\u201331. EasyChair (2020)"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Aflaki, S., Volk, M., Bonakdarpour, B., Katoen, J.P., Storjohann, A.: Automated fine tuning of probabilistic self-stabilizing algorithms. In: SRDS. IEEE CS (2017)","DOI":"10.1109\/SRDS.2017.22"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., de\u00a0Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. In: Handbook of Model Checking. Springer (2018)","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"10_CR4","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Ceska, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Inf. 54(6) (2017)","DOI":"10.1007\/s00236-016-0265-2"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Ceska, M., Jansen, N., Junges, S., Katoen, J.: Shepherding hordes of markov chains. In: TACAS (2). Lecture Notes in Computer Science, vol. 11428, pp. 172\u2013190. Springer (2019)","DOI":"10.1007\/978-3-030-17465-1_10"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE. IEEE (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J., Papusha, I., Poonawala, H.A., Topcu, U.: Sequential convex programming for the efficient verification of parametric MDPs. In: Proc. of TACAS. LNCS, vol. 10206, pp. 133\u2013150 (2017)","DOI":"10.1007\/978-3-662-54580-5_8"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.P., Topcu, U.: Synthesis in pMDPs: A tale of 1001 parameters. In: ATVA. LNCS, vol. 11138. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_10"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov chains. In: Proc. of ICTAC. LNCS, vol.\u00a03407. Springer (2004)","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: A modern probabilistic model checker. In: CAV (2). LNCS, vol. 10427. Springer (2017)","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Gainer, P., Hahn, E.M., Schewe, S.: Accelerated model checking of parametric Markov chains. In: ATVA. LNCS, vol. 11138. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_18"},{"key":"10_CR13","unstructured":"Gouberman, A., Siegle, M., Tati, B.: Markov chains with perturbed rates to absorption: Theory and application to model repair. Perform. Evaluation 130, 32\u201350 (2019)"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric markov decision processes. In: Proc. of NFM. LNCS, vol.\u00a06617, pp. 146\u2013161. Springer (2011)","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Software Tools for Technology Transfer 13(1) (2010)","DOI":"10.1007\/s10009-010-0146-x"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Hutschenreiter, L., Baier, C., Klein, J.: Parametric Markov chains: PCTL complexity and fraction-free Gaussian elimination. In: GandALF. EPTCS, vol.\u00a0256 (2017)","DOI":"10.4204\/EPTCS.256.2"},{"key":"10_CR17","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS. IEEE CS (1991)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Junges, S., Jansen, N., Seshia, S.A.: Enforcing almost-sure reachability in POMDPs. CoRR abs\/2007.00085 (2020)","DOI":"10.1007\/978-3-030-81688-9_28"},{"key":"10_CR19","unstructured":"Junges, S., Jansen, N., Wimmer, R., Quatmann, T., Winterer, L., Katoen, J.P., Becker, B.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI. AUAI Press (2018)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Katoen, J.P.: The probabilistic model checking landscape. In: LICS. ACM (2016)","DOI":"10.1145\/2933575.2934574"},{"key":"10_CR21","unstructured":"Kozine, I., Utkin, L.V.: Interval-valued finite Markov chains. Reliab. Comput. 8(2), 97\u2013113 (2002)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects Comput. 19(1), 93\u2013109 (2007)","DOI":"10.1007\/s00165-006-0015-2"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. Real Time Syst. 53(3), 354\u2013402 (2017)","DOI":"10.1007\/s11241-017-9269-4"},{"key":"10_CR24","doi-asserted-by":"crossref","unstructured":"Pathak, S., \u00c1brah\u00e1m, E., Jansen, N., Tacchella, A., Katoen, J.P.: A greedy approach for the efficient repair of stochastic models. In: NFM. LNCS, vol.\u00a09058 (2015)","DOI":"10.1007\/978-3-319-17524-9_21"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.P.: Parameter synthesis for Markov models: Faster than ever. In: ATVA. LNCS, vol.\u00a09938 (2016)","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Rietbergen, M.T., van\u00a0der Gaag, L.C.: Attaining monotonicity for Bayesian networks. In: ECSQARU. LNCS, vol.\u00a06717, pp. 134\u2013145. Springer (2011)","DOI":"10.1007\/978-3-642-22152-1_12"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Spel, J., Junges, S., Katoen, J.: Are parametric Markov chains monotonic? In: Proc. of ATVA. LNCS, vol. 11781, pp. 479\u2013496. Springer (2019)","DOI":"10.1007\/978-3-030-31784-3_28"},{"key":"10_CR28","unstructured":"Winkler, T., Junges, S., P\u00e9rez, G.A., Katoen, J.: On the complexity of reachability in parametric Markov decision processes. In: Proc. of CONCUR. LIPIcs, vol.\u00a0140, pp. 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"}],"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-030-72016-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,26]],"date-time":"2024-08-26T07:48:34Z","timestamp":1724658514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72016-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720155","9783030720162"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72016-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","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":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","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":"141","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":"41","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":"21","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":"29% - 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":"12","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}