{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:28:06Z","timestamp":1777519686056,"version":"3.51.4"},"reference-count":79,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2021,7,31]],"date-time":"2021-07-31T00:00:00Z","timestamp":1627689600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["695614"],"award-info":[{"award-number":["695614"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Guangdong Province","award":["2018B010107004"],"award-info":[{"award-number":["2018B010107004"]}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["639.021.754"],"award-info":[{"award-number":["639.021.754"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Model. Comput. Simul."],"published-print":{"date-parts":[[2021,7,31]]},"abstract":"<jats:p>\n            Markov automata are a compositional modelling formalism with continuous stochastic time, discrete probabilities, and nondeterministic choices. In this article, we present extensions to M\n            <jats:sc>ODEST<\/jats:sc>\n            , an expressive high-level language with roots in process algebra, that allow large Markov automata models to be specified in a succinct, modular way. We illustrate the advantages of M\n            <jats:sc>ODEST<\/jats:sc>\n            over alternative languages. Model checking Markov automata models requires dedicated algorithms for time-bounded and long-run average reward properties. We describe and evaluate the state-of-the-art algorithms implemented in the mcsta model checker of the M\n            <jats:sc>ODEST<\/jats:sc>\n            T\n            <jats:sc>OOLSET<\/jats:sc>\n            . We find that mcsta improves the performance and scalability of Markov automata model checking compared to earlier and alternative tools. We explain a partial-exploration approach based on the BRTDP method designed to mitigate the state space explosion problem of model checking, and experimentally evaluate its effectiveness. This problem can be avoided entirely by purely simulation-based techniques, but the nondeterminism in Markov automata hinders their straightforward application. We explain how lightweight scheduler sampling can make simulation possible, and provide a detailed evaluation of its usefulness on several benchmarks using the M\n            <jats:sc>ODEST<\/jats:sc>\n            T\n            <jats:sc>OOLSET<\/jats:sc>\n            \u2019s modes simulator.\n          <\/jats:p>","DOI":"10.1145\/3449355","type":"journal-article","created":{"date-parts":[[2021,8,24]],"date-time":"2021-08-24T16:44:33Z","timestamp":1629823473000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["A Modest Approach to Markov Automata"],"prefix":"10.1145","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9678-1467","authenticated-orcid":false,"given":"Yuliya","family":"Butkova","sequence":"first","affiliation":[{"name":"Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3268-8674","authenticated-orcid":false,"given":"Arnd","family":"Hartmanns","sequence":"additional","affiliation":[{"name":"University of Twente, Drienerlolaan, Enschede, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Saarland University, Germany and Institute of Intelligent Software, Nansha, Guangzhou, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2021,8,24]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Principles of Performance and Reliability Modeling and Evaluation","author":"Amparore Elvio Gilberto","unstructured":"Elvio Gilberto Amparore , Gianfranco Balbo , Marco Beccuti , Susanna Donatelli , and Giuliana Franceschinis . 2016. 30 years of GreatSPN . In Principles of Performance and Reliability Modeling and Evaluation . Springer , 227\u2013254. DOI:https:\/\/doi.org\/10.1007\/978-3-319-30599-8_9 10.1007\/978-3-319-30599-8_9 Elvio Gilberto Amparore, Gianfranco Balbo, Marco Beccuti, Susanna Donatelli, and Giuliana Franceschinis. 2016. 30 years of GreatSPN. In Principles of Performance and Reliability Modeling and Evaluation. Springer, 227\u2013254. DOI:https:\/\/doi.org\/10.1007\/978-3-319-30599-8_9"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_21"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_19"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of AAMAS. International Foundation for Autonomous Agents and Multiagent Systems, 1750\u20131752","author":"Azevedo Carlos","unstructured":"Carlos Azevedo , Bruno Lacerda , Nick Hawes , and Pedro U. Lima . 2020. Long-run multi-robot planning with uncertain task durations . In Proceedings of AAMAS. International Foundation for Autonomous Agents and Multiagent Systems, 1750\u20131752 . Carlos Azevedo, Bruno Lacerda, Nick Hawes, and Pedro U. Lima. 2020. Long-run multi-robot planning with uncertain task durations. In Proceedings of AAMAS. International Foundation for Autonomous Agents and Multiagent Systems, 1750\u20131752."},{"key":"e_1_2_1_5_1","volume-title":"Handbook of Model Checking","author":"Baier Christel","unstructured":"Christel Baier , Luca de Alfaro , Vojtech Forejt , and Marta Kwiatkowska . 2018. Model checking probabilistic systems . In Handbook of Model Checking . Springer , 963\u2013999. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28 10.1007\/978-3-319-10575-8_28 Christel Baier, Luca de Alfaro, Vojtech Forejt, and Marta Kwiatkowska. 2018. Model checking probabilistic systems. In Handbook of Model Checking.Springer, 963\u2013999. DOI:https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810891.1810912"},{"key":"e_1_2_1_7_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"e_1_2_1_9_1","volume-title":"Viet Yen Nguyen, and Thomas Noll","author":"Bohlender Dimitri","year":"2014","unstructured":"Dimitri Bohlender , Harold Bruintjes , Sebastian Junges , Jens Katelaan , Viet Yen Nguyen, and Thomas Noll . 2014 . A review of statistical model checking pitfalls on real-time stochastic models. In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 8803 . Springer , 177\u2013192. Dimitri Bohlender, Harold Bruintjes, Sebastian Junges, Jens Katelaan, Viet Yen Nguyen, and Thomas Noll. 2014. A review of statistical model checking pitfalls on real-time stochastic models. In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 8803. Springer, 177\u2013192."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2006.104"},{"key":"e_1_2_1_11_1","volume-title":"Labeled RTDP: Improving the convergence of real-time dynamic programming","author":"Bonet Blai","unstructured":"Blai Bonet and Hector Geffner . 2003. Labeled RTDP: Improving the convergence of real-time dynamic programming . In Proceedings of ICAPS. AAAI Press , 12\u201321. Blai Bonet and Hector Geffner. 2003. Labeled RTDP: Improving the convergence of real-time dynamic programming. In Proceedings of ICAPS. AAAI Press, 12\u201321."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2009.45"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of FSTTCS (LIPIcs)","volume":"18","author":"Br\u00e1zdil Tom\u00e1s","year":"2012","unstructured":"Tom\u00e1s Br\u00e1zdil , Holger Hermanns , Jan Krc\u00e1l , Jan Kret\u00ednsk\u00fd , and Vojtech Reh\u00e1k . 2012 . Verification of open interactive Markov chains . In Proceedings of FSTTCS (LIPIcs) , Vol. 18 . Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik, 474\u2013485. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS. 2012.474 10.4230\/LIPIcs.FSTTCS.2012.474 Tom\u00e1s Br\u00e1zdil, Holger Hermanns, Jan Krc\u00e1l, Jan Kret\u00ednsk\u00fd, and Vojtech Reh\u00e1k. 2012. Verification of open interactive Markov chains. In Proceedings of FSTTCS (LIPIcs), Vol. 18. Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik, 474\u2013485. DOI:https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2012.474"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCIAIG.2012.2186810"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2019.01.006"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-020-00563-2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_9"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of ISoLA (Lecture Notes in Computer Science). Springer. To appear.","author":"Budde Carlos E.","year":"2021","unstructured":"Carlos E. Budde , Arnd Hartmanns , Michaela Klauck , Jan Kret\u00ednsk\u00fd , David Parker , Tim Quatmann , Andrea Turrini , and Zhen Zhang . 2021 . On correctness, precision, and performance in quantitative verification (QComp 2020 competition report) . In Proceedings of ISoLA (Lecture Notes in Computer Science). Springer. To appear. Carlos E. Budde, Arnd Hartmanns, Michaela Klauck, Jan Kret\u00ednsk\u00fd, David Parker, Tim Quatmann, Andrea Turrini, and Zhen Zhang. 2021. On correctness, precision, and performance in quantitative verification (QComp 2020 competition report). In Proceedings of ISoLA (Lecture Notes in Computer Science). Springer. To appear."},{"key":"#cr-split#-e_1_2_1_20_1.1","unstructured":"Yuliya Butkova. 2019. A Modest Approach to Modelling and Checking Markov Automata (Artifact). 4TU.ResearchData. DOI:https:\/\/doi.org\/10.4121\/uuid:98d571be-cdd4-4e5a-a589-7c5b1320e569 10.4121\/uuid:98d571be-cdd4-4e5a-a589-7c5b1320e569"},{"key":"#cr-split#-e_1_2_1_20_1.2","doi-asserted-by":"crossref","unstructured":"Yuliya Butkova. 2019. A Modest Approach to Modelling and Checking Markov Automata (Artifact). 4TU.ResearchData. DOI:https:\/\/doi.org\/10.4121\/uuid:98d571be-cdd4-4e5a-a589-7c5b1320e569","DOI":"10.1007\/978-3-030-30281-8_4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_11"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30281-8_4"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_12"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_11"},{"key":"e_1_2_1_25_1","volume-title":"Markov automata on discount! In Proceedings of MMB (Lecture Notes in Computer Science)","author":"Butkova Yuliya","unstructured":"Yuliya Butkova , Ralf Wimmer , and Holger Hermanns . 2018. Markov automata on discount! In Proceedings of MMB (Lecture Notes in Computer Science) , Vol. 10740 . Springer , 19\u201334. DOI:https:\/\/doi.org\/10.1007\/978-3-319-74947-1_2 10.1007\/978-3-319-74947-1_2 Yuliya Butkova, Ralf Wimmer, and Holger Hermanns. 2018. Markov automata on discount! In Proceedings of MMB (Lecture Notes in Computer Science), Vol. 10740. Springer, 19\u201334. DOI:https:\/\/doi.org\/10.1007\/978-3-319-74947-1_2"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25566-3_32"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3060139"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0383-0"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-55754-6_17"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_7"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_22"},{"key":"e_1_2_1_32_1","volume-title":"Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist.","author":"David Alexandre","year":"2015","unstructured":"Alexandre David , Peter Gj\u00f8l Jensen , Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist. 2015 . Uppaal Stratego. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 9035 . Springer , 206\u2013211. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16 10.1007\/978-3-662-46681-0_16 Alexandre David, Peter Gj\u00f8l Jensen, Kim Guldstrand Larsen, Marius Mikucionis, and Jakob Haahr Taankvist. 2015. Uppaal Stratego. In Proceedings of TACAS (Lecture Notes in Computer Science), Vol. 9035. Springer, 206\u2013211. DOI:https:\/\/doi.org\/10.1007\/978-3-662-46681-0_16"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_27"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/24.159800"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38697-8_6"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.41"},{"key":"e_1_2_1_39_1","volume-title":"CADP 2011: A toolbox for the construction and analysis of distributed processes. STTT 15","author":"Garavel Hubert","year":"2013","unstructured":"Hubert Garavel , Fr\u00e9d\u00e9ric Lang , Radu Mateescu , and Wendelin Serwe . 2013 . CADP 2011: A toolbox for the construction and analysis of distributed processes. STTT 15 , 2 (2013), 89\u2013107. Hubert Garavel, Fr\u00e9d\u00e9ric Lang, Radu Mateescu, and Wendelin Serwe. 2013. CADP 2011: A toolbox for the construction and analysis of distributed processes. STTT 15, 2 (2013), 89\u2013107."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11334-019-00349-z"},{"key":"e_1_2_1_41_1","volume-title":"Markov Automata Taken by Storm. Master\u2019s thesis","author":"Gros Timo P.","unstructured":"Timo P. Gros . 2018. Markov Automata Taken by Storm. Master\u2019s thesis . Saarland University , Germany. Timo P. Gros. 2018. Markov Automata Taken by Storm. Master\u2019s thesis. Saarland University, Germany."},{"key":"e_1_2_1_42_1","volume-title":"Neuh\u00e4u\u00dfer","author":"Guck Dennis","year":"2012","unstructured":"Dennis Guck , Tingting Han , Joost-Pieter Katoen , and Martin R . Neuh\u00e4u\u00dfer . 2012 . Quantitative timed analysis of interactive Markov chains. In Proceedings of NFM (Lecture Notes in Computer Science), Vol. 7226 . Springer , 8\u201323. DOI:https:\/\/doi.org\/10.1007\/978-3-642-28891-3_4 10.1007\/978-3-642-28891-3_4 Dennis Guck, Tingting Han, Joost-Pieter Katoen, and Martin R. Neuh\u00e4u\u00dfer. 2012. Quantitative timed analysis of interactive Markov chains. In Proceedings of NFM (Lecture Notes in Computer Science), Vol. 7226. Springer, 8\u201323. DOI:https:\/\/doi.org\/10.1007\/978-3-642-28891-3_4"},{"key":"e_1_2_1_43_1","volume-title":"Analysis of timed and long-run objectives for Markov automata. Logic. Methods Comput. Sci. 10, 3","author":"Guck Dennis","year":"2014","unstructured":"Dennis Guck , Hassan Hatefi , Holger Hermanns , Joost-Pieter Katoen , and Mark Timmer . 2014. Analysis of timed and long-run objectives for Markov automata. Logic. Methods Comput. Sci. 10, 3 ( 2014 ). DOI:https:\/\/doi.org\/10.2168\/LMCS-10(3:17)2014 10.2168\/LMCS-10(3:17)2014 Dennis Guck, Hassan Hatefi, Holger Hermanns, Joost-Pieter Katoen, and Mark Timmer. 2014. Analysis of timed and long-run objectives for Markov automata. Logic. Methods Comput. Sci. 10, 3 (2014). DOI:https:\/\/doi.org\/10.2168\/LMCS-10(3:17)2014"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11936-6_13"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.12.003"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17502-3_5"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0167-z"},{"key":"#cr-split#-e_1_2_1_48_1.1","unstructured":"Arnd Hartmanns. 2021. A Modest Approach to Markov Automata (Artifact). 4TU.ResearchData. DOI:https:\/\/doi.org\/10.4121\/14182523 10.4121\/14182523"},{"key":"#cr-split#-e_1_2_1_48_1.2","unstructured":"Arnd Hartmanns. 2021. A Modest Approach to Markov Automata (Artifact). 4TU.ResearchData. DOI:https:\/\/doi.org\/10.4121\/14182523"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_51"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_10"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31423-1_8"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_26"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17462-0_20"},{"key":"e_1_2_1_54_1","volume-title":"Proceedings of Winter Simulation Conference. IEEE, 1419\u20131430","author":"Hartmanns Arnd","year":"2017","unstructured":"Arnd Hartmanns , Sean Sedwards , and Pedro R . D\u2019Argenio. 2017. Efficient simulation-based verification of probabilistic timed automata . In Proceedings of Winter Simulation Conference. IEEE, 1419\u20131430 . DOI:https:\/\/doi.org\/10.1109\/WSC. 2017 .8247885 10.1109\/WSC.2017.8247885 Arnd Hartmanns, Sean Sedwards, and Pedro R. D\u2019Argenio. 2017. Efficient simulation-based verification of probabilistic timed automata. In Proceedings of Winter Simulation Conference. IEEE, 1419\u20131430. DOI:https:\/\/doi.org\/10.1109\/WSC.2017.8247885"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"e_1_2_1_57_1","volume-title":"Communicating Sequential Processes","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare . 1985. Communicating Sequential Processes . Prentice-Hall . C. A. R. Hoare. 1985. Communicating Sequential Processes. Prentice-Hall."},{"key":"e_1_2_1_58_1","first-page":"2","article-title":"A sparse sampling algorithm for near-optimal planning in large Markov decision processes","volume":"49","author":"Kearns Michael J.","year":"2002","unstructured":"Michael J. Kearns , Yishay Mansour , and Andrew Y. Ng . 2002 . A sparse sampling algorithm for near-optimal planning in large Markov decision processes . Mach. Learn. 49 , 2 - 3 (2002), 193\u2013208. Michael J. Kearns, Yishay Mansour, and Andrew Y. Ng. 2002. A sparse sampling algorithm for near-optimal planning in large Markov decision processes. Mach. Learn. 49, 2-3 (2002), 193\u2013208.","journal-title":"Mach. Learn."},{"key":"e_1_2_1_59_1","unstructured":"Michaela Klauck. 2020. Modest Fret-pi LRTDP. Retrieved from https:\/\/dgit.cs.uni-saarland.de\/Michaela\/modest-fret-pi-lrtdp.  Michaela Klauck. 2020. Modest Fret-pi LRTDP. Retrieved from https:\/\/dgit.cs.uni-saarland.de\/Michaela\/modest-fret-pi-lrtdp."},{"key":"e_1_2_1_60_1","volume-title":"Heuristic search for generalized stochastic shortest path MDPs","author":"Kolobov Andrey","unstructured":"Andrey Kolobov , Mausam, Daniel S. Weld , and Hector Geffner . 2011. Heuristic search for generalized stochastic shortest path MDPs . In Proceedings of ICAPS. AAAI Press . Andrey Kolobov, Mausam, Daniel S. Weld, and Hector Geffner. 2011. Heuristic search for generalized stochastic shortest path MDPs. In Proceedings of ICAPS. AAAI Press."},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2015.29"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1096166.1096174"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"e_1_2_1_65_1","volume-title":"Statistical model checking the 2018 edition! In Proceedings of ISoLA (Lecture Notes in Computer Science)","author":"Larsen Kim Guldstrand","unstructured":"Kim Guldstrand Larsen and Axel Legay . 2018. Statistical model checking the 2018 edition! In Proceedings of ISoLA (Lecture Notes in Computer Science) , Vol. 11245 . Springer , 261\u2013270. DOI:https:\/\/doi.org\/10.1007\/978-3-030-03421-4_17 10.1007\/978-3-030-03421-4_17 Kim Guldstrand Larsen and Axel Legay. 2018. Statistical model checking the 2018 edition! In Proceedings of ISoLA (Lecture Notes in Computer Science), Vol. 11245. Springer, 261\u2013270. DOI:https:\/\/doi.org\/10.1007\/978-3-030-03421-4_17"},{"key":"e_1_2_1_66_1","volume-title":"Proceedings of WS-FMDS at SEFM (Lecture Notes in Computer Science)","volume":"8938","author":"Legay Axel","year":"2014","unstructured":"Axel Legay , Sean Sedwards , and Louis-Marie Traonouez . 2014 . Scalable verification of Markov decision processes . In Proceedings of WS-FMDS at SEFM (Lecture Notes in Computer Science) , Vol. 8938 . Springer, 350\u2013362. DOI:https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23 10.1007\/978-3-319-15201-1_23 Axel Legay, Sean Sedwards, and Louis-Marie Traonouez. 2014. Scalable verification of Markov decision processes. In Proceedings of WS-FMDS at SEFM (Lecture Notes in Computer Science), Vol. 8938. Springer, 350\u2013362. DOI:https:\/\/doi.org\/10.1007\/978-3-319-15201-1_23"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2019\/68"},{"key":"e_1_2_1_68_1","volume-title":"Proceedings of ICML (ACM International Conference Proceeding Series)","volume":"119","author":"McMahan H. Brendan","unstructured":"H. Brendan McMahan , Maxim Likhachev , and Geoffrey J. Gordon . 2005. Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees . In Proceedings of ICML (ACM International Conference Proceeding Series) , Vol. 119 . ACM, 569\u2013576. DOI:https:\/\/doi.org\/10.1145\/1102351.1102423 10.1145\/1102351.1102423 H. Brendan McMahan, Maxim Likhachev, and Geoffrey J. Gordon. 2005. Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In Proceedings of ICML (ACM International Conference Proceeding Series), Vol. 119. ACM, 569\u2013576. DOI:https:\/\/doi.org\/10.1145\/1102351.1102423"},{"key":"e_1_2_1_69_1","volume-title":"Communication and Concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice-Hall . Robin Milner. 1989. Communication and Concurrency. Prentice-Hall."},{"key":"e_1_2_1_70_1","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman Martin L.","unstructured":"Martin L. Puterman . 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming . John Wiley & Sons, Inc. Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley & Sons, Inc."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_7"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_37"},{"key":"e_1_2_1_73_1","first-page":"5","article-title":"Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games","volume":"48","author":"Rabe Markus N.","year":"2011","unstructured":"Markus N. Rabe and Sven Schewe . 2011 . Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games . Acta Info. 48 , 5 - 6 (2011), 291\u2013315. DOI:https:\/\/doi.org\/10.1007\/s00236-011-0140-0 10.1007\/s00236-011-0140-0 Markus N. Rabe and Sven Schewe. 2011. Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. Acta Info. 48, 5-6 (2011), 291\u2013315. DOI:https:\/\/doi.org\/10.1007\/s00236-011-0140-0","journal-title":"Acta Info."},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0350-1"},{"key":"e_1_2_1_75_1","doi-asserted-by":"crossref","unstructured":"Gerardo Rubino and Bruno Tuffin (Eds.). 2009. Rare Event Simulation Using Monte Carlo Methods. Wiley.  Gerardo Rubino and Bruno Tuffin (Eds.). 2009. Rare Event Simulation Using Monte Carlo Methods. Wiley.","DOI":"10.1002\/9780470745403"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.5555\/3176748.3176754"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/FTCS.1999.781056"},{"key":"e_1_2_1_79_1","volume-title":"Proceedings of CONCUR (Lecture Notes in Computer Science)","author":"Timmer Mark","unstructured":"Mark Timmer , Joost-Pieter Katoen , Jaco van de Pol , and Mari\u00eblle Stoelinga . 2012. Efficient modelling and generation of Markov automata . In Proceedings of CONCUR (Lecture Notes in Computer Science) , Vol. 7454 . Springer , 364\u2013379. DOI:https:\/\/doi.org\/10.1007\/978-3-642-32940-1_26 10.1007\/978-3-642-32940-1_26 Mark Timmer, Joost-Pieter Katoen, Jaco van de Pol, and Mari\u00eblle Stoelinga. 2012. Efficient modelling and generation of Markov automata. In Proceedings of CONCUR (Lecture Notes in Computer Science), Vol. 7454. Springer, 364\u2013379. DOI:https:\/\/doi.org\/10.1007\/978-3-642-32940-1_26"},{"key":"e_1_2_1_80_1","volume-title":"Simmons","author":"Younes H\u00e5kan L. S.","year":"2002","unstructured":"H\u00e5kan L. S. Younes and Reid G . Simmons . 2002 . Probabilistic verification of discrete event systems using acceptance sampling. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 2404 . Springer , 223\u2013235. DOI:https:\/\/doi.org\/10.1007\/3-540-45657-0_17 10.1007\/3-540-45657-0_17 H\u00e5kan L. S. Younes and Reid G. Simmons. 2002. Probabilistic verification of discrete event systems using acceptance sampling. In Proceedings of CAV (Lecture Notes in Computer Science), Vol. 2404. Springer, 223\u2013235. DOI:https:\/\/doi.org\/10.1007\/3-540-45657-0_17"}],"container-title":["ACM Transactions on Modeling and Computer Simulation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3449355","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3449355","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:55Z","timestamp":1750197715000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3449355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,31]]},"references-count":79,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2021,7,31]]}},"alternative-id":["10.1145\/3449355"],"URL":"https:\/\/doi.org\/10.1145\/3449355","relation":{},"ISSN":["1049-3301","1558-1195"],"issn-type":[{"value":"1049-3301","type":"print"},{"value":"1558-1195","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,7,31]]},"assertion":[{"value":"2020-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-08-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}