Abstract
Costs and rewards are important ingredients for many types of systems, modelling critical aspects like energy consumption, task completion, repair costs, and memory usage. This paper introduces Markov reward automata, an extension of Markov automata that allows the modelling of systems incorporating rewards (or costs) in addition to nondeterminism, discrete probabilistic choice and continuous stochastic timing. Rewards come in two flavours: action rewards, acquired instantaneously when taking a transition; and state rewards, acquired while residing in a state. We present algorithms to optimise three reward functions: the expected cumulative reward until a goal is reached, the expected cumulative reward until a certain time bound, and the long-run average reward. We have implemented these algorithms in the SCOOP/IMCA tool chain and show their feasibility via several case studies.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.Ā 2791, pp. 88ā104. Springer, Heidelberg (2004)
Bamberg, R.: Non-deterministic generalised stochastic Petri nets modelling and analysis. Masterās thesis, University of Twente (2012)
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.Ā 1256, pp. 358ā368. Springer, Heidelberg (1997)
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Ā 7(2), 128ā143 (2010)
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Ā 54(5), 754ā775 (2011)
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.Ā 154, pp. 48ā63 (2014)
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ā42. IEEE (2011)
Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, pp. 1318ā1336. SIAM (2011)
Clark, G.: Formalising the specification of rewards with PEPA. In: PAPM, pp. 139ā160 (1996)
de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)
Deng, Y., Hennessy, M.: Compositional reasoning for weighted Markov decision processes. Science of Computer ProgrammingĀ 78(12), 2537ā2579 (2013), Special Section on International Software Product Line Conference 2010 and Fundamentals of Software Engineering (selected papers of FSEN 2011)
Deng, Y., Hennessy, M.: On the semantics of Markov automata. Information and ComputationĀ 222, 139ā168 (2013)
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ā109. Springer, Heidelberg (2013)
Eisentraut, C., Hermanns, H., Zhang, L.: Concurrency and composition in a stochastic world. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.Ā 6269, pp. 21ā39. Springer, Heidelberg (2010)
Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: LICS, pp. 342ā351. IEEE (2010)
Groote, J.F., Ponse, A.: The syntax and semantics of Ī¼CRL. In: ACP, Workshops in Computing, pp. 26ā62. Springer (1995)
Guck, D., Han, T., Katoen, J.-P., NeuhƤuĆer, M.R.: Quantitative timed analysis of interactive Markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol.Ā 7226, pp. 8ā23. Springer, Heidelberg (2012)
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āArgenio, P.R. (eds.) QEST 2013. LNCS, vol.Ā 8054, pp. 55ā71. Springer, Heidelberg (2013)
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)
Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. Electronic Communications of the EASSTĀ 53 (2012)
Haverkort, B.R., Cloth, L., Hermanns, H., Katoen, J.-P., Baier, C.: Model checking performability properties. In: DSN, pp. 103ā112. IEEE (2002)
Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: SRDS, pp. 228ā237. IEEE (2000)
Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol.Ā 2428. Springer, Heidelberg (2002)
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Ā 68(2), 90ā104 (2011)
NeuhƤuĆer, M.R.: Model Checking Nondeterministic and Randomly Timed Systems. PhD thesis, University of Twente (2010)
NeuhƤuĆer, 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.Ā 5504, pp. 364ā379. Springer, Heidelberg (2009)
Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Massachusetts Institute of Technology (1995)
Song, L., Zhang, L., Godskesen, J.C.: Late weak bisimulation for Markov automata. Technical report, Ar**v e-prints (2012)
Srinivasan, M.M.: Nondeterministic polling systems. Management ScienceĀ 37(6), 667ā681 (1991)
Timmer, M.: SCOOP: A tool for symbolic optimisations of probabilistic processes. In: QEST, pp. 149ā150. IEEE (2011)
Timmer, M.: Efficient Modelling, Generation and Analysis of Markov Automata. PhD thesis, University of Twente (2013)
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.Ā 7454, pp. 364ā379. Springer, Heidelberg (2012)
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ā257. Springer, Heidelberg (2013)
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.Ā 5799, pp. 54ā68. Springer, Heidelberg (2009)
Wunderling, R.: Paralleler und objektorientierter Simplex-Algorithmus. PhD thesis, Technische UniversitƤt Berlin (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M. (2014). Modelling and Analysis of Markov Reward Automata. In: Cassez, F., Raskin, JF. (eds) Automated Technology for Verification and Analysis. ATVA 2014. Lecture Notes in Computer Science, vol 8837. Springer, Cham. https://doi.org/10.1007/978-3-319-11936-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-319-11936-6_13
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11935-9
Online ISBN: 978-3-319-11936-6
eBook Packages: Computer ScienceComputer Science (R0)