{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T13:12:28Z","timestamp":1787317948496,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030451899","type":"print"},{"value":"9783030451905","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_16","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T05:03:02Z","timestamp":1587099782000},"page":"287-305","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Scenario-Based Verification of Uncertain MDPs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0409-2403","authenticated-orcid":false,"given":"Murat","family":"Cubuktepe","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1318-8973","authenticated-orcid":false,"given":"Nils","family":"Jansen","sequence":"additional","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"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Abraham Charnes and William W Cooper. Chance-Constrained Programming. Management science, 6(1):73\u201379, 1959.","DOI":"10.1287\/mnsc.6.1.73"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Amir Pnueli. The Temporal Logic of Programs. In FOCS, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"James Aspnes and Maurice Herlihy. Fast Randomized Consensus Using Shared Memory. Journal of Algorithms, 15(1):441\u2013460, 1990.","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Hans Hansson and Bengt Jonsson. A Logic for Reasoning about Time and Reliability. Formal Aspects of Computing, 6(5):512\u2013535, 1994.","DOI":"10.1007\/BF01211866"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"L. Helmink, M. Sellink, and F. Vaandrager. Proof-Checking a Data Link Protocol. In TYPES, volume 806 of LNCS, pages 127\u2013165. Springer, 1994.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"16_CR6","unstructured":"Anthony Cassandra, Michael L Littman, and Nevin L Zhang. Incremental Pruning: A Simple, Fast, Exact Method for Partially Observable Markov Decision Processes. In UAI, pages 54\u201361, 1997."},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Robert Givan, Sonia Leach, and Thomas Dean. Bounded-Parameter Markov Decision Processes. Artificial Intelligence, 122(1-2):71\u2013109, 2000.","DOI":"10.1016\/S0004-3702(00)00047-3"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Jie Han and Pieter Jonker. A System Architecture Solution for Unreliable Nanoelectronic Devices. IEEE Transactions on Nanotechnology, 1:201\u2013208, 2002.","DOI":"10.1109\/TNANO.2002.807393"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng., 29(6):524\u2013541, 2003.","DOI":"10.1109\/TSE.2003.1205180"},{"key":"16_CR10","unstructured":"Joelle Pineau, Geoff Gordon, and Sebastian Thrun. Point-Based Value Iteration: an Anytime Algorithm for POMDPs. In IJCAI, pages 1025\u20131030, 2003."},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Conrado Daws. Symbolic and Parametric Model Checking of Discrete-Time Markov chains. In ICTAC, volume 3407 of LNCS, pages 280\u2013294. Springer, 2004.","DOI":"10.1007\/978-3-540-31862-0_21"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Vitaly Shmatikov. Probabilistic Analysis of an Anonymity System. Journal of Computer Security, 12(3-4):355\u2013377, 2004.","DOI":"10.3233\/JCS-2004-123-403"},{"key":"16_CR13","unstructured":"G.C. Calafiore and M.C. Campi. Uncertain Convex Programs: Randomized Solutions and Confidence Levels. Mathematical Programming, 102(1):25\u201346, 2005."},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Arnab Nilim and Laurent El Ghaoui. Robust Control of Markov Decision Processes with Uncertain Transition Matrices. Operations Research, 53(5):780\u2013798, 2005.","DOI":"10.1287\/opre.1050.0216"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Giuseppe C. Calafiore and Marco C. Campi. The Scenario Approach to Robust Control Design. IEEE Trans. Automat. Contr., 51(5):742\u2013753, 2006.","DOI":"10.1109\/TAC.2006.875041"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Marco C. Campi and Simone Garatti. The Exact Feasibility of Randomized Solutions of Uncertain Convex Programs. SIAM Journal on Optimization, 19(3):1211\u20131230, 2008.","DOI":"10.1137\/07069821X"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic Reachability for Parametric Markov Models. STTT, 13(1):3\u201319, 2010.","DOI":"10.1007\/s10009-010-0146-x"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Dimitris Bertsimas, David B Brown, and Constantine Caramanis. Theory and Applications of Robust Optimization. SIAM review, 53(3):464\u2013501, 2011.","DOI":"10.1137\/080734510"},{"key":"16_CR19","unstructured":"Marco C Campi and Simone Garatti. A Sampling-and-Discarding Approach to Chance-Constrained Optimization: Feasibility and Optimality. Journal of Optimization Theory and Applications, 148(2):257\u2013280, 2011."},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Beno\u00eet Delahaye, Kim G. Larsen, Axel Legay, Mikkel L. Pedersen, and Andrzej Wasowski. Decision problems for interval Markov chains. In LATA, volume 6638 of LNCS, pages 274\u2013285. Springer, 2011.","DOI":"10.1007\/978-3-642-21254-3_21"},{"key":"16_CR21","doi-asserted-by":"crossref","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. PRISM 4.0: Verification of Probabilistic Real-Time Systems. In CAV, volume 6806 of LNCS, pages 585\u2013591. Springer, 2011.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"16_CR22","unstructured":"Hassan Hatefi and Holger Hermanns. Model Checking Algorithms for Markov Automata. ECEASST, 53, 2012."},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. The PRISM Benchmark Suite. In QEST, pages 203\u2013204. IEEE CS, 2012.","DOI":"10.1109\/QEST.2012.14"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Rowan McAllister, Thierry Peynot, Robert Fitch, and Salah Sukkarieh. Motion Planning and Stochastic Control with Experimental Validation on a Planetary Rover. In IROS, pages 4716\u20134723. IEEE, 2012.","DOI":"10.1109\/IROS.2012.6386229"},{"key":"16_CR25","doi-asserted-by":"crossref","unstructured":"Eric M. Wolff, Ufuk Topcu, and Richard M. Murray. Robust Control of Uncertain Markov Decision Processes with Temporal Logic Specifications. In CDC, pages 3372\u20133379, 2012.","DOI":"10.1109\/CDC.2012.6426174"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Taolue Chen, Ernst Moritz Hahn, Tingting Han, Marta Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model Repair for Markov Decision Processes. In TASE, pages 85\u201392. IEEE CS, 2013.","DOI":"10.1109\/TASE.2013.20"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Alberto Puggelli, Wenchao Li, Alberto L Sangiovanni-Vincentelli, and Sanjit A Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex Uncertainties. In CAV, pages 527\u2013542. Springer, 2013.","DOI":"10.1007\/978-3-642-39799-8_35"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Wolfram Wiesemann, Daniel Kuhn, and Ber\u00e7 Rustem. Robust Markov Decision Processes. Mathematics of Operations Research, 38(1):153\u2013183, 2013.","DOI":"10.1287\/moor.1120.0566"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Indika Meedeniya, Irene Moser, Aldeida Aleti, and Lars Grunske. Evaluating Probabilistic Models with Uncertain Model Parameters. Software & Systems Modeling, 13(4):1395\u20131415, 2014.","DOI":"10.1007\/s10270-012-0277-5"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Krishnendu Chatterjee, Martin Chmel\u00edk, and Mathieu Tracol. What is Decidable about Partially Observable Markov Decision Processes with $$\\omega $$-Regular Objectives. Journal of Computer and System Sciences, 82(5):878\u2013911, 2016.","DOI":"10.1016\/j.jcss.2016.02.009"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"B. O\u2019Donoghue, E. Chu, N. Parikh, and S. Boyd. Conic Optimization via Operator Splitting and Homogeneous Self-Dual Embedding. Journal of Optimization Theory and Applications, 169(3):1042\u20131068, 2016.","DOI":"10.1007\/s10957-016-0892-3"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Tim Quatmann, Christian Dehnert, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Parameter Synthesis for Markov Models: Faster Than Ever. In ATVA, volume 9938 of LNCS, pages 50\u201367, 2016.","DOI":"10.1007\/978-3-319-46520-3_4"},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Asrar Ahmed, Pradeep Varakantham, Meghna Lowalekar, Yossiri Adulyasak, and Patrick Jaillet. Sampling Based Approaches for Minimizing Regret in Uncertain Markov Decision Processes (MDPs). J. Artif. Intell. Res., 59:229\u2013264, 2017.","DOI":"10.1613\/jair.5242"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, and Ufuk Topcu. Sequential Convex Programming for the Efficient Verification of Parametric MDPs. In TACAS (2), volume 10206 of LNCS, pages 133\u2013150, 2017.","DOI":"10.1007\/978-3-662-54580-5_8"},{"key":"16_CR35","doi-asserted-by":"crossref","unstructured":"Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A Storm is Coming: A Modern Probabilistic Model Checker. In CAV (2), volume 10427 of LNCS, pages 592\u2013600. Springer, 2017.","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Dimitri Scheftelowitsch, Peter Buchholz, Vahid Hashemi, and Holger Hermanns. Multi-Objective Approaches to Markov Decision Processes with Uncertain Transition Parameters. In VALUETOOLS, pages 44\u201351, 2017.","DOI":"10.1145\/3150928.3150945"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Sebastian Arming, Ezio Bartocci, Krishnendu Chatterjee, Joost-Pieter Katoen, and Ana Sokolova. Parameter-Independent Strategies for pMDPs via POMDPs. In QEST, pages 53\u201370. Springer, 2018.","DOI":"10.1007\/978-3-319-99154-2_4"},{"key":"16_CR38","doi-asserted-by":"crossref","unstructured":"Luca Bortolussi and Simone Silvetti. Bayesian Statistical Parameter Synthesis for Linear Temporal Properties of Stochastic Models. In TACAS, pages 396\u2013413, 2018.","DOI":"10.1007\/978-3-319-89963-3_23"},{"key":"16_CR39","doi-asserted-by":"crossref","unstructured":"Marco Claudio Campi, Simone Garatti, and Federico Alessandro Ramponi. A General Scenario Theory for Nonconvex Optimization and Decision Making. IEEE Trans. Automat. Contr., 63(12):4067\u20134078, 2018.","DOI":"10.1109\/TAC.2018.2808446"},{"key":"16_CR40","doi-asserted-by":"crossref","unstructured":"Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. Synthesis in pmdps: A tale of 1001 parameters. In ATVA, volume 11138 of LNCS, pages 160\u2013176. Springer, 2018.","DOI":"10.1007\/978-3-030-01090-4_10"},{"key":"16_CR41","unstructured":"Paul Gainer, Ernst Moritz Hahn, and Sven Schewe. Incremental Verification of Parametric and Reconfigurable Markov Chains. CoRR, abs\/1804.01872, 2018."},{"key":"16_CR42","unstructured":"Chin Pang Ho and Marek Petrik. Fast Bellman Updates for Robust MDPs. In ICML, 2018."},{"key":"16_CR43","unstructured":"Yamilet R. Serrano Llerena, Marcel B\u00f6hme, Marc Br\u00fcnink, Guoxin Su, and David S. Rosenblum. Verifying the Long-run Behavior of Probabilistic System Models in the Presence of Uncertainty. In ESEC\/SIGSOFT FSE, pages 587\u2013597. ACM, 2018."},{"key":"16_CR44","unstructured":"Lauren N Steimle, David L Kaufman, and Brian T Denton. Multi-Model Markov Decision Processes. Optimization Online, 2018."},{"key":"16_CR45","doi-asserted-by":"crossref","unstructured":"Giovanni Bacci, Mikkel Hansen, and Kim Guldstrand Larsen. Model Checking Constrained Markov Reward Models with Uncertainties. In QEST, pages 37\u201351, 2019.","DOI":"10.1007\/978-3-030-30281-8_3"},{"key":"16_CR46","unstructured":"Sebastian Junges, Erika \u00c1brah\u00e1m, Christian Hensel, Nils Jansen, Joost-Pieter Katoen, Tim Quatmann, and Matthias Volk. Parameter Synthesis for Markov Models. CoRR, abs\/1903.07993, 2019."},{"key":"16_CR47","unstructured":"Tobias Winkler, Sebastian Junges, Guillermo A. P\u00e9rez, and Joost-Pieter Katoen. On the complexity of reachability in parametric markov decision processes. In CONCUR, volume 140 of LIPIcs, pages 14:1\u201314:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2019."},{"key":"16_CR48","unstructured":"Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008."},{"key":"16_CR49","unstructured":"S. Basu, R. Pollack, and M.F. Roy. Algorithms in Real Algebraic Geometry. Springer, 2010."},{"key":"16_CR50","doi-asserted-by":"crossref","unstructured":"Stephen Boyd and Lieven Vandenberghe. Convex Optimization. Cambridge University Press, New York, NY, USA, 2004.","DOI":"10.1017\/CBO9780511804441"},{"key":"16_CR51","unstructured":"Martin L Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, 2014."},{"key":"16_CR52","unstructured":"Stuart J Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. 2016."},{"key":"16_CR53","unstructured":"Richard S Sutton and Andrew G Barto. Reinforcement Learning: An Introduction. MIT press, 2018."}],"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-45190-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T09:12:57Z","timestamp":1597914777000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","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":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/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":"155","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":"40","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":"8","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":"26% - 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":"14","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 could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","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)"}}]}}