{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T19:57:06Z","timestamp":1743105426357,"version":"3.40.3"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319633862"},{"type":"electronic","value":"9783319633879"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63387-9_7","type":"book-chapter","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T08:53:43Z","timestamp":1499849623000},"page":"140-159","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Markov Automata with Multiple Objectives"],"prefix":"10.1007","author":[{"given":"Tim","family":"Quatmann","sequence":"first","affiliation":[]},{"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of LICS, IEEE CS, pp. 342\u2013351 (2010)","key":"7_CR1","DOI":"10.1109\/LICS.2010.41"},{"key":"7_CR2","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.: On the semantics of Markov automata. Inf. Comput. 222, 139\u2013168 (2013)","journal-title":"Inf. Comput."},{"issue":"2","key":"7_CR3","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.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Secur. Comput. 7(2), 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Secur. Comput."},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-02658-4_18","volume-title":"Computer Aided Verification","author":"N Coste","year":"2009","unstructured":"Coste, N., Hermanns, H., Lantreibecq, E., Serwe, W.: Towards performance prediction of compositional models in industrial GALS designs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 204\u2013218. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-02658-4_18"},{"issue":"1","key":"7_CR5","first-page":"15:1","volume":"22","author":"JP Katoen","year":"2016","unstructured":"Katoen, J.P., Wu, H.: Probabilistic model checking for uncertain scenario-aware data flow. ACM Trans. Embed. Comput. Sys. 22(1), 15:1\u201315:27 (2016)","journal-title":"ACM Trans. Embed. Comput. Sys."},{"issue":"5","key":"7_CR6","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, J.P., Nguyen, V.Y., Noll, T., Roveri, M.: Safety, dependability and performance analysis of extended AADL models. Comput. J. 54(5), 754\u2013775 (2011)","journal-title":"Comput. J."},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-38697-8_6","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"C Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 90\u2013109. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-38697-8_6"},{"unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53 (2012)","key":"7_CR8"},{"doi-asserted-by":"crossref","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.P., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. LMCS 10(3) (2014)","key":"7_CR9","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-319-11936-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"D Guck","year":"2014","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of Markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168\u2013184. Springer, Cham (2014). doi:10.1007\/978-3-319-11936-6_13"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-25942-0_2","volume-title":"Dependable Software Engineering: Theories, Tools, and Applications","author":"H Hatefi","year":"2015","unstructured":"Hatefi, H., Braitling, B., Wimmer, R., Fioriti, L.M.F., Hermanns, H., Becker, B.: Cost vs. time in stochastic games and Markov automata. In: Li, X., Liu, Z., Yi, W. (eds.) SETTA 2015. LNCS, vol. 9409, pp. 19\u201334. Springer, Cham (2015). doi:10.1007\/978-3-319-25942-0_2"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-662-54580-5_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Butkova","year":"2017","unstructured":"Butkova, Y., Wimmer, R., Hermanns, H.: Long-run rewards for Markov automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 188\u2013203. Springer, Heidelberg (2017). doi:10.1007\/978-3-662-54580-5_11"},{"issue":"1","key":"7_CR13","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1145\/322234.322242","volume":"28","author":"JL Bruno","year":"1981","unstructured":"Bruno, J.L., Downey, P.J., Frederickson, G.N.: Sequencing tasks with exponential service times to minimize the expected flow time or makespan. J. ACM 28(1), 100\u2013113 (1981)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Quatmann, T., Junges, S., Katoen, J.P.: Markov automata with multiple objectives (2017). CoRR abs\/1704.06648","key":"7_CR14","DOI":"10.1007\/978-3-319-63387-9_7"},{"key":"7_CR15","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). doi:10.1007\/978-3-642-22110-1_47"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 317\u2013332. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-33386-6_25"},{"key":"7_CR17","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1613\/jair.3987","volume":"48","author":"DM Roijers","year":"2013","unstructured":"Roijers, D.M., Vamplew, P., Whiteson, S., Dazeley, R.: A survey of multi-objective sequential decision-making. J. Artif. Intell. Res. 48, 67\u2013113 (2013)","journal-title":"J. Artif. Intell. Res."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/978-3-540-71209-1_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Etessami","year":"2007","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 50\u201365. Springer, Heidelberg (2007). doi:10.1007\/978-3-540-71209-1_6"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-19835-9_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 112\u2013127. Springer, Heidelberg (2011). doi:10.1007\/978-3-642-19835-9_11"},{"unstructured":"Bruy\u00e8re, V., Filiot, E., Randour, M., Raskin, J.F.: Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. In: Proceeding of STACS. LIPIcs, vol. 25, pp. 199\u2013213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)","key":"7_CR20"},{"doi-asserted-by":"crossref","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: CSL-LICS, pp. 1:1\u20131:10. ACM (2014)","key":"7_CR21","DOI":"10.1145\/2603088.2603089"},{"key":"7_CR22","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.: Trading performance for stability in Markov decision processes. J. Comput. Syst. Sci. 84, 144\u2013170 (2017)","journal-title":"J. Comput. Syst. Sci."},{"doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Markov decision processes with multiple long-run average objectives. LMCS 10(1) (2014)","key":"7_CR23","DOI":"10.2168\/LMCS-10(1:13)2014"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-662-46681-0_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Basset","year":"2015","unstructured":"Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 256\u2013271. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46681-0_22"},{"unstructured":"Teichteil-K\u00f6nigsbuch, F.: 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, pp. 744\u2013749. IOS Press (2012)","key":"7_CR25"},{"key":"7_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-662-46081-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M Randour","year":"2015","unstructured":"Randour, M., Raskin, J.-F., Sankur, O.: Variations on the stochastic shortest path problem. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 1\u201318. Springer, Heidelberg (2015). doi:10.1007\/978-3-662-46081-8_1"},{"key":"7_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-662-49674-9_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Junges","year":"2016","unstructured":"Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130\u2013146. Springer, Heidelberg (2016). doi:10.1007\/978-3-662-49674-9_8"},{"key":"7_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-319-11936-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"A David","year":"2014","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., S\u00f8rensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 129\u2013145. Springer, Cham (2014). doi:10.1007\/978-3-319-11936-6_10"},{"key":"7_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-40313-2_25","volume-title":"Mathematical Foundations of Computer Science 2013","author":"T Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Simaitis, A., Wiltsche, C.: On stochastic games with multiple objectives. In: Chatterjee, K., Sgall, J. (eds.) MFCS 2013. LNCS, vol. 8087, pp. 266\u2013277. Springer, Heidelberg (2013). doi:10.1007\/978-3-642-40313-2_25"},{"key":"7_CR30","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-00596-1_26","volume-title":"Foundations of Software Science and Computational Structures","author":"MR Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FoSSaCS 2009. LNCS, vol. 5504, pp. 364\u2013379. Springer, Heidelberg (2009). doi:10.1007\/978-3-642-00596-1_26"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"CAV 2017, Part I","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Ku\u010dnak, V. (eds.) CAV 2017, Part I. LNCS, vol. 10426, pp. 592\u2013600. Springer, Cham (2017)"},{"unstructured":"Quatmann, T.: Multi-objective model checking of Markov automata. Master\u2019s thesis, RWTH Aachen University (2016)","key":"7_CR33"},{"key":"7_CR34","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). doi:10.1007\/978-3-319-11439-2_10"},{"issue":"6","key":"7_CR35","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1287\/mnsc.37.6.667","volume":"37","author":"MM Srinivasan","year":"1991","unstructured":"Srinivasan, M.M.: Nondeterministic polling systems. Manag. Sci. 37(6), 667\u2013681 (1991)","journal-title":"Manag. Sci."},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 364\u2013379. Springer, Heidelberg (2012). doi:10.1007\/978-3-642-32940-1_26"},{"issue":"1","key":"7_CR37","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53\u201372 (1986)","journal-title":"Distrib. Comput."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63387-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,13]],"date-time":"2021-07-13T00:18:11Z","timestamp":1626135491000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-63387-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319633862","9783319633879"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63387-9_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"13 July 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Heidelberg","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/cavconference.org\/2017\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}