{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:25:13Z","timestamp":1750843513802,"version":"3.40.4"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319119359"},{"type":"electronic","value":"9783319119366"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_13","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T19:12:03Z","timestamp":1414177923000},"page":"168-184","source":"Crossref","is-referenced-by-count":23,"title":["Modelling and Analysis of Markov Reward Automata"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Guck","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Timmer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hassan","family":"Hatefi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enno","family":"Ruijters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S. Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 88\u2013104. Springer, Heidelberg (2004)"},{"key":"13_CR2","unstructured":"Bamberg, R.: Non-deterministic generalised stochastic Petri nets modelling and analysis. Master\u2019s thesis, University of Twente (2012)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/3-540-63165-8_192","volume-title":"Automata, Languages and Programming","author":"M. Bernardo","year":"1997","unstructured":"Bernardo, M.: An algebra-based method to associate rewards with EMPA terms. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 358\u2013368. Springer, Heidelberg (1997)"},{"issue":"2","key":"13_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.I.A.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Transactions on Dependable and Secure Computing\u00a07(2), 128\u2013143 (2010)","journal-title":"IEEE Transactions on Dependable and Secure Computing"},{"issue":"5","key":"13_CR5","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. The Computer Journal\u00a054(5), 754\u2013775 (2011)","journal-title":"The Computer Journal"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Braitling, B., Fioriti, L.M.F., Hatefi, H., Wimmer, R., Becker, B., Hermanns, H.: MeGARA: Menu-based game abstraction and abstraction refinement of Markov automata. In: QAPL. EPTCS, vol.\u00a0154, pp. 48\u201363 (2014)","DOI":"10.4204\/EPTCS.154.4"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Brazdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: LICS, pp. 33\u201342. IEEE (2011)","DOI":"10.1109\/LICS.2011.10"},{"key":"13_CR8","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: SODA, pp. 1318\u20131336. SIAM (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"13_CR9","unstructured":"Clark, G.: Formalising the specification of rewards with PEPA. In: PAPM, pp. 139\u2013160 (1996)"},{"key":"13_CR10","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Deng, Y., Hennessy, M.: Compositional reasoning for weighted Markov decision processes. Science of Computer Programming\u00a078(12), 2537\u20132579 (2013), Special Section on International Software Product Line Conference 2010 and Fundamentals of Software Engineering (selected papers of FSEN 2011)","DOI":"10.1016\/j.scico.2013.02.009"},{"key":"13_CR12","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":"13_CR13","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":"13_CR14","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":"13_CR15","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342\u2013351. IEEE (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of \u03bcCRL. In: ACP, Workshops in Computing, pp. 26\u201362. Springer (1995)","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"13_CR17","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)"},{"key":"13_CR18","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":"13_CR19","doi-asserted-by":"crossref","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E.J.J., Stoelinga, M.I.A.: Modelling and analysis of Markov reward automata (extended version). Technical Report TR-CTIT-14-06, CTIT, University of Twente, Enschede (2014)","DOI":"10.1007\/978-3-319-11936-6_13"},{"key":"13_CR20","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Electronic Communications of the EASST\u00a053 (2012)"},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Cloth, L., Hermanns, H., Katoen, J.-P., Baier, C.: Model checking performability properties. In: DSN, pp. 103\u2013112. IEEE (2002)","DOI":"10.1109\/DSN.2002.1028891"},{"key":"13_CR22","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: SRDS, pp. 228\u2013237. IEEE (2000)","DOI":"10.1109\/RELDI.2000.885410"},{"key":"13_CR23","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)"},{"issue":"2","key":"13_CR24","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.-P. Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation\u00a068(2), 90\u2013104 (2011)","journal-title":"Performance Evaluation"},{"key":"13_CR25","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD thesis, University of Twente (2010)"},{"key":"13_CR26","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":"M.R. Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, M.R., Stoelinga, M.I.A., Katoen, J.-P.: Delayed nondeterminism in continuous-time Markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 364\u2013379. Springer, Heidelberg (2009)"},{"key":"13_CR27","unstructured":"Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)"},{"key":"13_CR28","unstructured":"Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. Technical report, ArXiv e-prints (2012)"},{"issue":"6","key":"13_CR29","doi-asserted-by":"publisher","first-page":"667","DOI":"10.1287\/mnsc.37.6.667","volume":"37","author":"M.M. Srinivasan","year":"1991","unstructured":"Srinivasan, M.M.: Nondeterministic polling systems. Management Science\u00a037(6), 667\u2013681 (1991)","journal-title":"Management Science"},{"key":"13_CR30","doi-asserted-by":"crossref","unstructured":"Timmer, M.: SCOOP: A tool for symbolic optimisations of probabilistic processes. In: QEST, pp. 149\u2013150. IEEE (2011)","DOI":"10.1109\/QEST.2011.27"},{"key":"13_CR31","unstructured":"Timmer, M.: Efficient Modelling, Generation and Analysis of Markov Automata. PhD thesis, University of Twente (2013)"},{"key":"13_CR32","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.C., 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":"13_CR33","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":"13_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-642-04761-9_5","volume-title":"Automated Technology for Verification and Analysis","author":"J. Pol van de","year":"2009","unstructured":"van de Pol, J., Timmer, M.: State space reduction of linear processes using control flow reconstruction. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 54\u201368. Springer, Heidelberg (2009)"},{"key":"13_CR35","unstructured":"Wunderling, R.: Paralleler und objektorientierter Simplex-Algorithmus. PhD thesis, Technische Universit\u00e4t Berlin (1996)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T13:08:52Z","timestamp":1746450532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}