{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:31Z","timestamp":1779087571078,"version":"3.51.4"},"reference-count":51,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,3,29]],"date-time":"2021-03-29T00:00:00Z","timestamp":1616976000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2021,3,29]],"date-time":"2021-03-29T00:00:00Z","timestamp":1616976000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["RTG 2236"],"award-info":[{"award-number":["RTG 2236"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2022,2]]},"DOI":"10.1007\/s10703-021-00364-6","type":"journal-article","created":{"date-parts":[[2021,3,29]],"date-time":"2021-03-29T16:03:01Z","timestamp":1617033781000},"page":"33-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Markov automata with multiple objectives"],"prefix":"10.1007","volume":"60","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2843-5511","authenticated-orcid":false,"given":"Tim","family":"Quatmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,3,29]]},"reference":[{"key":"364_CR1","volume-title":"Probability and measure theory","author":"RB Ash","year":"2000","unstructured":"Ash RB, Dol\u00e9ans-Dade C (2000) Probability and measure theory. Academic Press, New York"},{"key":"364_CR2","doi-asserted-by":"crossref","unstructured":"Ashok P, Butkova Y, Hermanns H, Kret\u00ednsk\u00fd J (2018) Continuous-time Markov decisions based on partial exploration. In: ATVA, LNCS, vol 11138. Springer, pp 317\u2013334","DOI":"10.1007\/978-3-030-01090-4_19"},{"key":"364_CR3","doi-asserted-by":"crossref","unstructured":"Ashok P, Chatterjee K, Daca P, Kret\u00ednsk\u00fd J, Meggendorfer T (2017) Value iteration for long-run average reward in Markov decision processes. In: CAV (1), LNCS, vol 10426. Springer, pp 201\u2013221","DOI":"10.1007\/978-3-319-63387-9_10"},{"key":"364_CR4","doi-asserted-by":"crossref","unstructured":"Baier C, Bertrand N, Dubslaff C, Gburek D, Sankur O (2018) Stochastic shortest paths and weight-bounded properties in Markov decision processes. In: LICS. ACM, pp 86\u201394","DOI":"10.1145\/3209108.3209184"},{"key":"364_CR5","doi-asserted-by":"crossref","unstructured":"Baier C, Dubslaff C, Kl\u00fcppelholz S (2014) Trade-off analysis meets probabilistic model checking. In: CSL-LICS. ACM, pp 1:1\u20131:10","DOI":"10.1145\/2603088.2603089"},{"key":"364_CR6","doi-asserted-by":"crossref","unstructured":"Baier C, Klein J, Leuschner L, Parker D, Wunderlich S (2017) Ensuring the reliability of your model checker: interval iteration for Markov decision processes. In: CAV (1), LNCS, vol 10426. Springer, pp 160\u2013180","DOI":"10.1007\/978-3-319-63387-9_8"},{"key":"364_CR7","doi-asserted-by":"crossref","unstructured":"Basset N, Kwiatkowska MZ, Topcu U, Wiltsche C (2015) Strategy synthesis for stochastic games with multiple long-run objectives. In: Proceedings of of TACAS, LNCS, vol 9035. Springer, pp 256\u2013271","DOI":"10.1007\/978-3-662-46681-0_22"},{"issue":"2","key":"364_CR8","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H Boudali","year":"2010","unstructured":"Boudali H, Crouzen P, Stoelinga M (2010) A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans Dependable Secur Comput 7(2):128\u2013143","journal-title":"IEEE Trans Dependable Secur Comput"},{"issue":"5","key":"364_CR9","doi-asserted-by":"publisher","first-page":"754","DOI":"10.1093\/comjnl\/bxq024","volume":"54","author":"M Bozzano","year":"2011","unstructured":"Bozzano M, Cimatti A, Katoen JP, Nguyen VY, Noll T, Roveri M (2011) Safety, dependability and performance analysis of extended AADL models. Comput J 54(5):754\u2013775","journal-title":"Comput J"},{"issue":"1","key":"364_CR10","first-page":"1156","volume":"10","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil T, Brozek V, Chatterjee K, Forejt V, Kucera A (2014) Markov decision processes with multiple long-run average objectives. LMCS 10(1):1156","journal-title":"LMCS"},{"key":"364_CR11","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jcss.2016.09.009","volume":"84","author":"T Br\u00e1zdil","year":"2017","unstructured":"Br\u00e1zdil T, Chatterjee K, Forejt V, Kucera A (2017) Trading performance for stability in Markov decision processes. J Comput Syst Sci 84:144\u2013170","journal-title":"J Comput Syst Sci"},{"issue":"1","key":"364_CR12","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1145\/322234.322242","volume":"28","author":"JL Bruno","year":"1981","unstructured":"Bruno JL, Downey PJ, Frederickson GN (1981) Sequencing tasks with exponential service times to minimize the expected flow time or makespan. J ACM 28(1):100\u2013113","journal-title":"J ACM"},{"key":"364_CR13","unstructured":"Bruy\u00e8re V, Filiot E, Randour M, Raskin JF (2014) Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. In: Proceedings of STACS, LIPIcs, vol 25. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp 199\u2013213"},{"key":"364_CR14","doi-asserted-by":"crossref","unstructured":"Butkova Y, Fox G (2019) Optimal time-bounded reachability analysis for concurrent systems. In: TACAS (2), LNCS, vol 11428. Springer, pp 191\u2013208","DOI":"10.1007\/978-3-030-17465-1_11"},{"key":"364_CR15","doi-asserted-by":"crossref","unstructured":"Butkova Y, Hatefi H, Hermanns H, Krc\u00e1l J (2015) Optimal continuous time Markov decisions. In: ATVA, LNCS, vol 9364. Springer, pp 166\u2013182","DOI":"10.1007\/978-3-319-24953-7_12"},{"key":"364_CR16","doi-asserted-by":"crossref","unstructured":"Butkova Y, Wimmer R, Hermanns H (2017) Long-run rewards for Markov automata. In: Proceedings of TACAS, LNCS. Springer https:\/\/link.springer.com\/chapter\/10.1007%2F978-3-662-54580-5_11","DOI":"10.1007\/978-3-662-54580-5_11"},{"key":"364_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee K, Henzinger M (2011) Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: Proceedings of SODA, pp 1318\u20131336","DOI":"10.1137\/1.9781611973082.101"},{"key":"364_CR18","doi-asserted-by":"crossref","unstructured":"Chen T, Forejt V, Kwiatkowska MZ, Simaitis A, Wiltsche C (2013) On stochastic games with multiple objectives. In: Proceedings of MFCS, LNCS, vol 8087. Springer, pp 266\u2013277","DOI":"10.1007\/978-3-642-40313-2_25"},{"key":"364_CR19","doi-asserted-by":"crossref","unstructured":"Coste N, Hermanns H, Lantreibecq E, Serwe W (2009) Towards performance prediction of compositional models in industrial GALS designs. In: Proceedings of CAV, LNCS, vol 5643. Springer, pp 204\u2013218","DOI":"10.1007\/978-3-642-02658-4_18"},{"key":"364_CR20","doi-asserted-by":"crossref","unstructured":"David A, Jensen PG, Larsen KG, Legay A, Lime D, S\u00f8rensen MG, Taankvist JH (2014) On time with minimal expected cost! In: Proceedings of ATVA, LNCS, vol 8837. Springer, pp 129\u2013145","DOI":"10.1007\/978-3-319-11936-6_10"},{"key":"364_CR21","unstructured":"de Alfaro L (1997) Formal verification of probabilistic systems. Ph.D. thesis, Stanford University"},{"key":"364_CR22","doi-asserted-by":"crossref","unstructured":"Dehnert C, Junges S, Katoen JP, Volk M (2017) A storm is coming: a modern probabilistic model checker. In: Proceedings of CAV","DOI":"10.1007\/978-3-319-63390-9_31"},{"key":"364_CR23","doi-asserted-by":"crossref","unstructured":"Delgrange F, Katoen J, Quatmann T, Randour M (2020) Simple strategies in multi-objective MDPs. In: TACAS (1), LNCS, vol 12078. Springer, pp 346\u2013364","DOI":"10.1007\/978-3-030-45190-5_19"},{"key":"364_CR24","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.ic.2012.10.010","volume":"222","author":"Y Deng","year":"2013","unstructured":"Deng Y, Hennessy M (2013) On the semantics of Markov automata. Inf Comput 222:139\u2013168","journal-title":"Inf Comput"},{"key":"364_CR25","doi-asserted-by":"crossref","unstructured":"Eisentraut C, Hermanns H, Katoen JP, Zhang L (2013) A semantics for every GSPN. In: Petri Nets, LNCS, vol 7927. Springer, pp 90\u2013109","DOI":"10.1007\/978-3-642-38697-8_6"},{"key":"364_CR26","doi-asserted-by":"crossref","unstructured":"Eisentraut C, Hermanns H, Zhang L (2010) On probabilistic automata in continuous time. In: Proceedings of LICS. IEEE CS, pp 342\u2013351","DOI":"10.1109\/LICS.2010.41"},{"issue":"4","key":"364_CR27","first-page":"1","volume":"4","author":"K Etessami","year":"2008","unstructured":"Etessami K, Kwiatkowska MZ, Vardi MY, Yannakakis M (2008) Multi-objective model checking of Markov decision processes. LMCS 4(4):1\u201321","journal-title":"LMCS"},{"key":"364_CR28","doi-asserted-by":"crossref","unstructured":"Forejt V, Kwiatkowska M, Parker D (2012) Pareto curves for probabilistic model checking. In: Proceedings of ATVA, LNCS, vol 7561. Springer, pp 317\u2013332","DOI":"10.1007\/978-3-642-33386-6_25"},{"key":"364_CR29","doi-asserted-by":"crossref","unstructured":"For\u011bjt V, Kwiatkowska MZ, Norman G, Parker D, Qu H ()20119 Quantitative multi-objective verification for probabilistic systems. In: Proceedings of TACAS, LNCS, vol 6605. Springer, pp 112\u2013127","DOI":"10.1007\/978-3-642-19835-9_11"},{"issue":"3","key":"364_CR30","first-page":"943","volume":"10","author":"D Guck","year":"2014","unstructured":"Guck D, Hatefi H, Hermanns H, Katoen JP, Timmer M (2014) Analysis of timed and long-run objectives for Markov automata. LMCS 10(3):943","journal-title":"LMCS"},{"key":"364_CR31","doi-asserted-by":"crossref","unstructured":"Guck D, Timmer M, Hatefi H, Ruijters E, Stoelinga M (2014) Modelling and analysis of Markov reward automata. In: Proceedings of ATVA, LNCS, vol 8837. Springer, pp 168\u2013184","DOI":"10.1007\/978-3-319-11936-6_13"},{"key":"364_CR32","doi-asserted-by":"crossref","unstructured":"Haddad S, Monmege B (2014) Reachability in MDPs: refining convergence of value iteration. In: RP, LNCS, vol 8762. Springer, pp 125\u2013137","DOI":"10.1007\/978-3-319-11439-2_10"},{"issue":"7","key":"364_CR33","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, Quatmann T (2020) Multi-cost bounded tradeoff analysis in MDP. J Autom Reason 64(7):1483\u20131522","journal-title":"J Autom Reason"},{"key":"364_CR34","doi-asserted-by":"crossref","unstructured":"Hatefi H, Braitling B, Wimmer R, Fioriti LMF, Hermanns H, Becker B (2015) Cost vs. time in stochastic games and Markov automata. In: Proceedings of SETTA, LNCS, vol 9409. Springer, pp 19\u201334","DOI":"10.1007\/978-3-319-25942-0_2"},{"key":"364_CR35","unstructured":"Hatefi H, Hermanns H (2012) Model checking algorithms for Markov automata. ECEASST, vol 53. http:\/\/journal.ub.tu-berlin.de\/eceasst\/article\/view\/783"},{"key":"364_CR36","unstructured":"Hensel C, Junges S, Katoen J, Quatmann T, Volk M (2020) The probabilistic model checker Storm. CoRR abs\/2002.07080"},{"key":"364_CR37","doi-asserted-by":"crossref","unstructured":"Junges S, Jansen N, Dehnert C, Topcu U, Katoen JP (2016) Safety-constrained reinforcement learning for MDPs. In: Proceedings of TACAS, LNCS, vol 9636. Springer, pp 130\u2013146","DOI":"10.1007\/978-3-662-49674-9_8"},{"issue":"1","key":"364_CR38","first-page":"15:1","volume":"22","author":"JP Katoen","year":"2016","unstructured":"Katoen JP, Wu H (2016) Probabilistic model checking for uncertain scenario-aware data flow. ACM Trans Embedded Comput Syst 22(1):15:1\u201315:27","journal-title":"ACM Trans Embedded Comput Syst"},{"key":"364_CR39","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: verification of probabilistic real-time systems. In: Proceedings of CAV, LNCS, vol 6806. Springer, pp 585\u2013591","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"364_CR40","unstructured":"Neuh\u00e4u\u00dfer MR (2010) Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University"},{"key":"364_CR41","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer MR, Stoelinga M, Katoen JP (2009) Delayed nondeterminism in continuous-time Markov decision processes. In: Proceedings of FOSSACS, LNCS, vol 5504. Springer, pp 364\u2013379","DOI":"10.1007\/978-3-642-00596-1_26"},{"issue":"1","key":"364_CR42","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A Pnueli","year":"1986","unstructured":"Pnueli A, Zuck L (1986) Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1):53\u201372","journal-title":"Distrib. Comput."},{"key":"364_CR43","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov decision processes: discrete stochastic dynamic programming","author":"ML Puterman","year":"1994","unstructured":"Puterman ML (1994) Markov decision processes: discrete stochastic dynamic programming. Wiley, New York"},{"key":"364_CR44","doi-asserted-by":"crossref","unstructured":"Quatmann T, Junges S, Katoen J (2017) Markov automata with multiple objectives. In: CAV (1), LNCS, vol 10426. Springer, pp 140\u2013159","DOI":"10.1007\/978-3-319-63387-9_7"},{"key":"364_CR45","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.4298642","author":"T Quatmann","year":"2020","unstructured":"Quatmann T, Junges S, Katoen J (2020) Markov automata with multiple objectives: supplemental material. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.4298642","journal-title":"Zenodo"},{"key":"364_CR46","doi-asserted-by":"crossref","unstructured":"Randour M, Raskin JF, Sankur O (2015) Variations on the stochastic shortest path problem. In: Proceedings of VMCAI, LNCS, vol 8931. Springer, pp 1\u201318","DOI":"10.1007\/978-3-662-46081-8_1"},{"key":"364_CR47","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1613\/jair.3987","volume":"48","author":"DM Roijers","year":"2013","unstructured":"Roijers DM, Vamplew P, Whiteson S, Dazeley R (2013) A survey of multi-objective sequential decision-making. J Artif Intell Res 48:67\u2013113","journal-title":"J Artif Intell Res"},{"issue":"6","key":"364_CR48","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1287\/mnsc.37.6.667","volume":"37","author":"MM Srinivasan","year":"1991","unstructured":"Srinivasan MM (1991) Nondeterministic polling systems. Manag Sci 37(6):667\u2013681","journal-title":"Manag Sci"},{"key":"364_CR49","unstructured":"Teichteil-K\u00f6nigsbuch F (2012) Path-constrained Markov decision processes: bridging the gap between probabilistic model-checking and decision-theoretic planning. In: Proceedings of ECAI, frontiers in AI and applications, vol 242. IOS Press, pp 744\u2013749"},{"key":"364_CR50","doi-asserted-by":"crossref","unstructured":"Timmer M, Katoen JP, van\u00a0de Pol J, Stoelinga M (2012) Efficient modelling and generation of Markov automata. In: Proceedings of CONCUR, LNCS, vol 7454. Springer, pp 364\u2013379","DOI":"10.1007\/978-3-642-32940-1_26"},{"issue":"1","key":"364_CR51","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1109\/TII.2017.2710316","volume":"14","author":"M Volk","year":"2018","unstructured":"Volk M, Junges S, Katoen J (2018) Fast dynamic fault tree analysis by model checking techniques. IEEE Trans Ind Inform 14(1):370\u2013379","journal-title":"IEEE Trans Ind Inform"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00364-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-021-00364-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-021-00364-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,8]],"date-time":"2023-02-08T17:31:19Z","timestamp":1675877479000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-021-00364-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,3,29]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,2]]}},"alternative-id":["364"],"URL":"https:\/\/doi.org\/10.1007\/s10703-021-00364-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,3,29]]},"assertion":[{"value":"18 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 February 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 March 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}