{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:40:07Z","timestamp":1755909607369,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:00:00Z","timestamp":1715644800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Knut and Alice Wallenberg Foundation","award":["Wallenberg Scholar Grant"],"award-info":[{"award-number":["Wallenberg Scholar Grant"]}]},{"name":"Swedish Research Council","award":["Distinguished Professor Grant 2017-01078"],"award-info":[{"award-number":["Distinguished Professor Grant 2017-01078"]}]},{"name":"Swedish Research Council","award":["International Postdoc Grant 2021-06727"],"award-info":[{"award-number":["International Postdoc Grant 2021-06727"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,5,14]]},"DOI":"10.1145\/3641513.3651397","type":"proceedings-article","created":{"date-parts":[[2024,5,2]],"date-time":"2024-05-02T18:05:48Z","timestamp":1714673148000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["CTL Model Checking of MDPs over Distribution Spaces: Algorithms and Sampling-based Computations"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2338-5487","authenticated-orcid":false,"given":"Yulong","family":"Gao","sequence":"first","affiliation":[{"name":"Imperial College London, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9940-5929","authenticated-orcid":false,"given":"Karl H.","family":"Johansson","sequence":"additional","affiliation":[{"name":"KTH Royal Institute of Technology, Sweden"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[{"name":"University of Oxford, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n. d.]. MOSEK Software. https:\/\/www.mosek.com\/"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629417"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2014.08.013"},{"volume-title":"International Conference on Computer Aided Verification. 86\u2013112","author":"Akshay S","key":"e_1_3_2_1_4_1","unstructured":"S Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, and \u0110or\u0111e \u017dikeli\u0107. 2023. MDPs as distribution transformers: affine invariant synthesis for safety objectives. In International Conference on Computer Aided Verification. 86\u2013112."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209185"},{"volume-title":"Constrained Markov Decision Processes: Stochastic Modeling","author":"Altman Eitan","key":"e_1_3_2_1_6_1","unstructured":"Eitan Altman. 1999. Constrained Markov Decision Processes: Stochastic Modeling. Routledge."},{"volume-title":"Principles of Model Checking","author":"Baier Christel","key":"e_1_3_2_1_7_1","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT press."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/235815.235821"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45793-3_21"},{"volume-title":"Formal Methods for Discrete-time Dynamical Systems","author":"Belta Calin","key":"e_1_3_2_1_10_1","unstructured":"Calin Belta, Boyan Yordanov, and Ebru\u00a0Aydin Gol. 2017. Formal Methods for Discrete-time Dynamical Systems. Springer."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2011.22"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNSE.2015.2438818"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3194656"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_18"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Vojt\u011bch Forejt Marta Kwiatkowska Gethin Norman and David Parker. 2011. Automated verification techniques for probabilistic systems. In International School on Formal Methods for the Design of Computer Communication and Software Systems. 53\u2013113.","DOI":"10.1007\/978-3-642-21455-4_3"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2020.3018438"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"volume-title":"European Control Conference. 502\u2013510","author":"Herceg M.","key":"e_1_3_2_1_21_1","unstructured":"M. Herceg, M. Kvasnica, C.N. Jones, and M. Morari. 2013. Multi-Parametric Toolbox 3.0. In European Control Conference. 502\u2013510."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_18"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-60026-6_16"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760628"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934574"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.35"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"crossref","unstructured":"Marta Kwiatkowska Gethin Norman and David Parker. 2007. Stochastic model checking. In International School on Formal Methods for the Design of Computer Communication and Software Systems. 220\u2013270.","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530882"},{"volume-title":"Formal System Verification","author":"Kwiatkowska Marta","key":"e_1_3_2_1_29_1","unstructured":"Marta Kwiatkowska, Gethin Norman, and David Parker. 2018. Probabilistic model checking: advances and applications. In Formal System Verification. Springer, 73\u2013121."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30482-1_21"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.80"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/CACSD.2004.1393890"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00186-016-0554-0"},{"volume-title":"Symbolic Model Checking","author":"McMillan L","key":"e_1_3_2_1_34_1","unstructured":"Kenneth\u00a0L McMillan. 1993. Symbolic Model Checking. Springer."},{"volume-title":"Variational Analysis","author":"Rockafellar R\u00a0Tyrrell","key":"e_1_3_2_1_35_1","unstructured":"R\u00a0Tyrrell Rockafellar and Roger J-B Wets. 2009. Variational Analysis. Springer."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2013.09.032"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(02)00250-9"},{"volume-title":"ACM Symposium on Theory of Computing. 240\u2013251","author":"Vardi Y.","key":"e_1_3_2_1_38_1","unstructured":"M.\u00a0Y. Vardi and L. Stockmeyer. 1985. Improved upper and lower bounds for modal logics of programs. In ACM Symposium on Theory of Computing. 240\u2013251."},{"key":"e_1_3_2_1_39_1","volume-title":"An extension of Karmarkar\u2019s projective algorithm for convex quadratic programming. Mathematical programming 44","author":"Ye Yinyu","year":"1989","unstructured":"Yinyu Ye and Edison Tse. 1989. An extension of Karmarkar\u2019s projective algorithm for convex quadratic programming. Mathematical programming 44 (1989), 157\u2013179."}],"event":{"name":"HSCC '24: Computation and Control","sponsor":["SIGCHI ACM Special Interest Group on Computer-Human Interaction"],"location":"Hong Kong SAR China","acronym":"HSCC '24"},"container-title":["Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3651397","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641513.3651397","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:13:06Z","timestamp":1755907986000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3651397"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,14]]},"references-count":39,"alternative-id":["10.1145\/3641513.3651397","10.1145\/3641513"],"URL":"https:\/\/doi.org\/10.1145\/3641513.3651397","relation":{},"subject":[],"published":{"date-parts":[[2024,5,14]]},"assertion":[{"value":"2024-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}