{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,30]],"date-time":"2025-06-30T00:40:08Z","timestamp":1751244008593,"version":"3.41.0"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319749464"},{"type":"electronic","value":"9783319749471"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-74947-1_2","type":"book-chapter","created":{"date-parts":[[2018,1,24]],"date-time":"2018-01-24T13:56:04Z","timestamp":1516802164000},"page":"19-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Markov Automata on Discount!"],"prefix":"10.1007","author":[{"given":"Yuliya","family":"Butkova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,1,25]]},"reference":[{"issue":"1","key":"2_CR1","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.tcs.2005.07.033","volume":"345","author":"L de Alfaro","year":"2005","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1), 139\u2013170 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1022","DOI":"10.1007\/3-540-45061-0_79","volume-title":"Automata, Languages and Programming","author":"L de Alfaro","year":"2003","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022\u20131037. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-45061-0_79"},{"key":"2_CR3","volume-title":"Dynamic Programming and Optimal Control","author":"DP Bertsekas","year":"2000","unstructured":"Bertsekas, D.P.: Dynamic Programming and Optimal Control, 2nd edn. Athena Scientific, Belmont (2000)","edition":"2"},{"issue":"2","key":"2_CR4","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 Secure Comput. 7(2), 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"2_CR5","unstructured":"Butkova, Y.: Discounted Markov automata. Technical Report 2018\u201301, ERC Grant POWVER (695614), Universit\u00e4t des Saarlandes, Saarland Informatics Campus, Saarbr\u00fccken, Germany (2018). http:\/\/www.powver.org\/publications\/TechRepRep\/ERC-POWVER-TechRep-2018-01.pdf"},{"key":"2_CR6","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). https:\/\/doi.org\/10.1007\/978-3-662-54580-5_11"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","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., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"2_CR8","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). https:\/\/doi.org\/10.1007\/978-3-642-38697-8_6"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS 2010, pp. 342\u2013351. IEEE CS (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-40196-1_5","volume-title":"Quantitative Evaluation of Systems","author":"D Guck","year":"2013","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 55\u201371. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40196-1_5"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. Log. Meth. Comput. Sci. 10(3) (2014)","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"2_CR12","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). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_13"},{"key":"2_CR13","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. In: Electronic Communication of the EASST, vol. 53 (2012)"},{"issue":"4","key":"2_CR14","doi-asserted-by":"publisher","first-page":"629","DOI":"10.1007\/s00165-016-0411-1","volume":"29","author":"H Hatefi","year":"2017","unstructured":"Hatefi, H., Wimmer, R., Braitling, B., Fioriti, L.M.F., Becker, B., Hermanns, H.: Cost vs. time in stochastic games and Markov automata. Formal Aspects Comput. 29(4), 629\u2013649 (2017)","journal-title":"Formal Aspects Comput."},{"key":"2_CR15","unstructured":"Hatefi Ardakani, H.: Finite horizon analysis of Markov automata. Ph.D. thesis, Universit\u00e4t des Saarlandes, Saarbr\u00fccken, Germany (2017)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.: On the use of model checking techniques for dependability evaluation. In: SRDS 2000, pp. 228\u2013237. IEEE CS (2000)","DOI":"10.1109\/RELDI.2000.885410"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-642-40229-6_10","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"DN Jansen","year":"2013","unstructured":"Jansen, D.N.: More or less true DCTL for continuous-time MDPs. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 137\u2013151. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40229-6_10"},{"key":"2_CR18","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1080\/03461238.1953.10419459","volume":"1953","author":"A Jensen","year":"1953","unstructured":"Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Scand. Actuarial J. 1953, 87\u201391 (1953)","journal-title":"Scand. Actuarial J."},{"key":"2_CR19","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, 1st edn. Wiley, New York (1994)","edition":"1"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Timmer, M.: SCOOP: a tool for symbolic optimisations of probabilistic processes. In: QEST 2011, pp. 149\u2013150. IEEE CS (2011)","DOI":"10.1109\/QEST.2011.27"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-40229-6_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Timmer","year":"2013","unstructured":"Timmer, M., van de Pol, J., Stoelinga, M.I.A.: Confluence reduction for Markov automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 243\u2013257. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40229-6_17"}],"container-title":["Lecture Notes in Computer Science","Measurement, Modelling and Evaluation of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-74947-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,30]],"date-time":"2025-06-30T00:18:05Z","timestamp":1751242685000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-74947-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319749464","9783319749471"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-74947-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"25 January 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MMB","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Measurement, Modelling and Evaluation of Computing Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Erlangen","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":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 February 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 February 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mmb2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.mmb2018.de\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}