{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T16:49:34Z","timestamp":1725814174396},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662460801"},{"type":"electronic","value":"9783662460818"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-46081-8_10","type":"book-chapter","created":{"date-parts":[[2014,12,11]],"date-time":"2014-12-11T09:25:44Z","timestamp":1418289944000},"page":"172-189","source":"Crossref","is-referenced-by-count":4,"title":["Abstraction-Based Computation of Reward Measures for Markov Automata"],"prefix":"10.1007","author":[{"given":"Bettina","family":"Braitling","sequence":"first","affiliation":[]},{"given":"Luis Mar\u00eda","family":"Ferrer Fioriti","sequence":"additional","affiliation":[]},{"given":"Hassan","family":"Hatefi","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proc. of LICS, pp. 342\u2013351. IEEE CS (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","year":"2002","unstructured":"Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)"},{"key":"10_CR3","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.\u00a07927, pp. 90\u2013109. Springer, Heidelberg (2013)"},{"key":"10_CR4","unstructured":"Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: Structure, behavior, and application. In: Proc. of PNPM, pp. 106\u2013115. IEEE CS (1985)"},{"key":"10_CR5","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., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol.\u00a07454, pp. 364\u2013379. Springer, Heidelberg (2012)"},{"key":"10_CR6","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST\u00a053 (2012)"},{"key":"10_CR7","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.\u00a08054, pp. 55\u201371. Springer, Heidelberg (2013)"},{"key":"10_CR8","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. Logical Methods in Computer Science 10(3) (2014)","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"10_CR9","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.\u00a08837, pp. 168\u2013184. Springer, Heidelberg (2014)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D. Guck","year":"2012","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.\u00a07226, pp. 8\u201323. Springer, Heidelberg (2012)"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M. Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M.Z., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Formal Methods in System Design\u00a036(3), 246\u2013280 (2010)","journal-title":"Formal Methods in System Design"},{"key":"10_CR12","doi-asserted-by":"crossref","first-page":"48","DOI":"10.4204\/EPTCS.154.4","volume":"154","author":"Bettina Braitling","year":"2014","unstructured":"Braitling, B., Ferrer Fioriti, L.M., Hatefi, H., Wimmer, R., Becker, B., Hermanns, H.: MeGARA: Menu-based game abstraction and abstraction refinement of Markov automata. In: Proc. of QAPL. EPTCS, vol.\u00a0154, pp. 48\u201363 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"10_CR13","first-page":"57","volume-title":"Lecture Notes in Computer Science","author":"Pedro R. D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PAPM-PROBMIV 2002. LNCS, vol.\u00a02399, pp. 57\u201376. Springer, Heidelberg (2002)"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"362","DOI":"10.1007\/978-3-642-11319-2_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Wachter","year":"2010","unstructured":"Wachter, B., Zhang, L.: Best probabilistic transformers. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 362\u2013379. Springer, Heidelberg (2010)"},{"key":"10_CR15","unstructured":"Wachter, B.: Refined probabilistic abstraction. PhD thesis, Saarland University (2011)"},{"key":"10_CR16","unstructured":"Braitling, B., Ferrer Fioriti, L.M., Hatefi, H., Wimmer, R., Hermanns, H., Becker, B.: Abstraction-based computation of reward measures for Markov automata (extended version). Reports of SFB\/TR 14 AVACS 106, SFB\/TR 14 AVACS (2014), http:\/\/www.avacs.org"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Proc. of QEST, pp. 209\u2013218. IEEE CS (2010)","DOI":"10.1109\/QEST.2010.47"},{"key":"10_CR18","unstructured":"Ash, R.B., Dol\u00e9ans-Dade, C.A.: Probability & Measure Theory, 2nd edn. Academic Press (1999)"},{"key":"10_CR19","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model checking nondeterministic and randomly timed systems. PhD thesis, RWTH Aachen University and University of Twente (2010)"},{"key":"10_CR20","unstructured":"Johr, S.: Model checking compositional Markov systems. PhD thesis, Saarland University, Germany (2008)"},{"issue":"10","key":"10_CR21","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L.S. Shapley","year":"1953","unstructured":"Shapley, L.S.: Stochastic games. Proceedings of the National Academy of Sciences of the United States of America\u00a039(10), 1095 (1953)","journal-title":"Proceedings of the National Academy of Sciences of the United States of America"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.ic.2013.01.001","volume":"224","author":"T. Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Forejt, V., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. Information and Computation\u00a0224, 46\u201370 (2013)","journal-title":"Information and Computation"},{"issue":"6","key":"10_CR23","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Software Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Software Eng."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-642-15375-4_3","volume-title":"CONCUR 2010 - Concurrency Theory","author":"C. Eisentraut","year":"2010","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 21\u201339. Springer, Heidelberg (2010)"},{"key":"10_CR25","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. Information and Computation\u00a0222, 139\u2013168 (2013)","journal-title":"Information and Computation"},{"key":"10_CR26","unstructured":"Fearnley, J., Rabe, M.N., Schewe, S., Zhang, L.: Efficient approximation of optimal control for continuous-time markov games. In: Proc. of FSTTCS. LIPIcs, vol.\u00a013, pp. 399\u2013410. Schloss Dagstuhl \u2013 Leibniz-Zentrum fuer Informatik (2011)"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: Proc. of SODA, pp. 1318\u20131336. SIAM (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"10_CR28","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.\u00a08053, pp. 243\u2013257. Springer, Heidelberg (2013)"},{"key":"10_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-12002-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Zhang","year":"2010","unstructured":"Zhang, L., Neuh\u00e4u\u00dfer, M.R.: Model checking interactive Markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 53\u201368. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46081-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T10:02:34Z","timestamp":1566122554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46081-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662460801","9783662460818"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46081-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}