{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T05:24:51Z","timestamp":1749878691133,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031606977"},{"type":"electronic","value":"9783031606984"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-60698-4_4","type":"book-chapter","created":{"date-parts":[[2024,5,27]],"date-time":"2024-05-27T00:01:51Z","timestamp":1716768111000},"page":"57-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Distributional Probabilistic Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0623-2323","authenticated-orcid":false,"given":"Ingy","family":"Elsayed-Aly","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4651-8441","authenticated-orcid":false,"given":"Lu","family":"Feng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,26]]},"reference":[{"key":"4_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"4_CR2","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/s00186-011-0367-0","volume":"74","author":"N B\u00e4uerle","year":"2011","unstructured":"B\u00e4uerle, N., Ott, J.: Markov decision processes with average-value-at-risk criteria. Math. Methods Oper. Res. 74(3), 361\u2013379 (2011)","journal-title":"Math. Methods Oper. Res."},{"doi-asserted-by":"crossref","unstructured":"Bellemare, M.G., Dabney, W., Rowland, M.: Distributional Reinforcement Learning. MIT Press (2023). http:\/\/www.distributional-rl.org","key":"4_CR3","DOI":"10.7551\/mitpress\/14207.001.0001"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol. 1026, pp. 499\u2013513. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60692-0_70"},{"issue":"9","key":"4_CR5","doi-asserted-by":"publisher","first-page":"2574","DOI":"10.1109\/TAC.2014.2309262","volume":"59","author":"V Borkar","year":"2014","unstructured":"Borkar, V., Jain, R.: Risk-constrained Markov decision processes. IEEE Trans. Autom. Control 59(9), 2574\u20132579 (2014)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jcss.2016.09.009","volume":"84","author":"T Brazdil","year":"2017","unstructured":"Brazdil, T., Chatterjee, K., Forejt, V., Kucera, A.: Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci. 84, 144\u2013170 (2017)","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-031-13185-1_5","volume-title":"Computer Aided Verification","author":"M Chen","year":"2022","unstructured":"Chen, M., Katoen, J.P., Klinkenberg, L., Winkler, T.: Does a program yield the right distribution? In: Shoham, S., Vizel, Y. (eds.) CAV 2022. LNCS, vol. 13371, pp. 79\u2013101. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_5"},{"unstructured":"Chow, Y., Ghavamzadeh, M.: Algorithms for CVaR optimization in MDPs. In: Advances in Neural Information Processing Systems, vol. 27 (2014)","key":"4_CR8"},{"unstructured":"Chow, Y., Tamar, A., Mannor, S., Pavone, M.: Risk-sensitive and robust decision-making: a CVaR optimization approach. In: Advances in Neural Information Processing Systems, vol. 28 (2015)","key":"4_CR9"},{"doi-asserted-by":"crossref","unstructured":"Cubuktepe, M., Topcu, U.: Verification of Markov decision processes with risk-sensitive measures. In: Proceedings of the Annual American Control Conference (ACC 2018), pp. 2371\u20132377. IEEE (2018)","key":"4_CR10","DOI":"10.23919\/ACC.2018.8430905"},{"doi-asserted-by":"crossref","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017) (2017)","key":"4_CR11","DOI":"10.1007\/978-3-319-63390-9_31"},{"doi-asserted-by":"crossref","unstructured":"Elsayed-Aly, I., Parker, D., Feng, L.: Distributional probabilistic model checking. arXiv preprint arXiv:2309.05584 (2023)","key":"4_CR12","DOI":"10.1007\/978-3-031-60698-4_4"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/TASE.2016.2530623","volume":"13","author":"L Feng","year":"2016","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Synthesis of human-in-the-loop control protocols for autonomous systems. IEEE Trans. Autom. Sci. Eng. 13(2), 450\u2013462 (2016)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"1","key":"4_CR14","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/9.362904","volume":"40","author":"JA Filar","year":"1995","unstructured":"Filar, J.A., Krass, D., Ross, K.W.: Percentile performance criteria for limiting average Markov decision processes. IEEE Trans. Autom. Control 40(1), 2\u201310 (1995)","journal-title":"IEEE Trans. Autom. Control"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-11439-2_10","volume-title":"Reachability Problems","author":"S Haddad","year":"2014","unstructured":"Haddad, S., Monmege, B.: Reachability in MDPs: refining convergence of value iteration. In: Ouaknine, J., Potapov, I., Worrell, J. (eds.) RP 2014. LNCS, vol. 8762, pp. 125\u2013137. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11439-2_10"},{"issue":"7","key":"4_CR16","doi-asserted-by":"publisher","first-page":"1483","DOI":"10.1007\/s10817-020-09574-9","volume":"64","author":"A Hartmanns","year":"2020","unstructured":"Hartmanns, A., Junges, S., Katoen, J.P., Quatmann, T.: Multi-cost bounded tradeoff analysis in MDP. J. Autom. Reason. 64(7), 1483\u20131522 (2020)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s10817-017-9413-9","volume":"60","author":"S Jha","year":"2018","unstructured":"Jha, S., Raman, V., Sadigh, D., Seshia, S.A.: Safe autonomy under perception uncertainty using chance-constrained temporal logic. J. Autom. Reason. 60(1), 43\u201362 (2018)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"4_CR18","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10009-017-0456-3","volume":"20","author":"J Klein","year":"2018","unstructured":"Klein, J., et al.: Advances in probabilistic model checking with PRISM: variable reordering, quantiles and weak deterministic B\u00fcchi automata. Int. J. Softw. Tools Technol. Transfer 20(2), 179\u2013194 (2018)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"issue":"6","key":"4_CR19","doi-asserted-by":"publisher","first-page":"1370","DOI":"10.1109\/TRO.2009.2030225","volume":"25","author":"H Kress-Gazit","year":"2009","unstructured":"Kress-Gazit, H., Fainekos, G.E., Pappas, G.J.: Temporal logic-based reactive mission and motion planning. IEEE Trans. Rob. 25(6), 1370\u20131381 (2009)","journal-title":"IEEE Trans. Rob."},{"doi-asserted-by":"crossref","unstructured":"K\u0159et\u00ednsk\u1ef3, J., Meggendorfer, T.: Conditional value-at-risk for reachability and mean payoff in Markov decision processes. In: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 609\u2013618 (2018)","key":"4_CR20","DOI":"10.1145\/3209108.3209176"},{"issue":"3","key":"4_CR21","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods Syst. Des. 19(3), 291\u2013314 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"4_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"},{"doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proceedings of the 9th International Conference on Quantitative Evaluation of SysTems (QEST 2012), pp. 203\u2013204. IEEE CS Press (2012)","key":"4_CR23","DOI":"10.1109\/QEST.2012.14"},{"doi-asserted-by":"crossref","unstructured":"Lyle, C., Bellemare, M.G., Castro, P.S.: A comparative analysis of expected and distributional reinforcement learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a033, pp. 4504\u20134511 (2019)","key":"4_CR24","DOI":"10.1609\/aaai.v33i01.33014504"},{"key":"4_CR25","series-title":"Springer Proceedings in Advanced Robotics","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-030-28619-4_10","volume-title":"Robotics Research","author":"A Majumdar","year":"2020","unstructured":"Majumdar, A., Pavone, M.: How should a robot assess risk? Towards an axiomatic theory of risk in robotics. In: Amato, N.M., Hager, G., Thomas, S., Torres-Torriti, M. (eds.) Robotics Research. SPAR, vol. 10, pp. 75\u201384. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-28619-4_10"},{"doi-asserted-by":"crossref","unstructured":"Meggendorfer, T.: Risk-aware stochastic shortest path. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol.\u00a036, pp. 9858\u20139867 (2022)","key":"4_CR26","DOI":"10.1609\/aaai.v36i9.21222"},{"key":"4_CR27","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","volume":"13","author":"A Pnueli","year":"1981","unstructured":"Pnueli, A.: The temporal semantics of concurrent programs. Theor. Comput. Sci. 13, 45\u201360 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/s10703-016-0262-7","volume":"50","author":"M Randour","year":"2017","unstructured":"Randour, M., Raskin, J.F., Sankur, O.: Percentile queries in multi-dimensional Markov decision processes. Formal Methods Syst. Des. 50, 207\u2013248 (2017)","journal-title":"Formal Methods Syst. Des."},{"doi-asserted-by":"crossref","unstructured":"Rigter, M., Duckworth, P., Lacerda, B., Hawes, N.: Planning for risk-aversion and expected value in MDPs. In: Proceedings of the International Conference on Automated Planning and Scheduling, vol.\u00a032, pp. 307\u2013315 (2022)","key":"4_CR29","DOI":"10.1609\/icaps.v32i1.19814"},{"issue":"7","key":"4_CR30","doi-asserted-by":"publisher","first-page":"1443","DOI":"10.1016\/S0378-4266(02)00271-6","volume":"26","author":"RT Rockafellar","year":"2002","unstructured":"Rockafellar, R.T., Uryasev, S.: Conditional value-at-risk for general loss distributions. J. Banking Financ. 26(7), 1443\u20131471 (2002)","journal-title":"J. Banking Financ."},{"issue":"4","key":"4_CR31","doi-asserted-by":"publisher","first-page":"794","DOI":"10.2307\/3213832","volume":"19","author":"MJ Sobel","year":"1982","unstructured":"Sobel, M.J.: The variance of discounted Markov decision processes. J. Appl. Probab. 19(4), 794\u2013802 (1982)","journal-title":"J. Appl. Probab."},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-37075-5_23","volume-title":"Foundations of Software Science and Computation Structures","author":"M Ummels","year":"2013","unstructured":"Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 353\u2013368. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_23"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-60698-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T01:23:30Z","timestamp":1732065810000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-60698-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031606977","9783031606984"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-60698-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 May 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 June 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 June 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}