Modelling and analysis of Markov reward automata

Dennis Guck; Mark Timmer; Hassan Hatefi; Enno J.J. Ruijters; Mariëlle I.A. Stoelinga

doi:10.1007/978-3-319-11936-6_13

Modelling and analysis of Markov reward automata

Dennis Guck, Mark Timmer, Hassan Hatefi, Enno J.J. Ruijters, Mariëlle I.A. Stoelinga

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

24 Citations (Scopus)

169 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
Editors	Franck Cassez, Jean-François Raskin
Place of Publication	Berlin
Publisher	Springer
Pages	168-184
Number of pages	17
ISBN (Electronic)	978-3-319-11936-6
ISBN (Print)	978-3-319-11935-9
DOIs	https://doi.org/10.1007/978-3-319-11936-6_13
Publication status	Published - Nov 2014
Event	12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia Duration: 3 Nov 2014 → 7 Nov 2014 Conference number: 12

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	8837
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
Abbreviated title	ATVA
Country/Territory	Australia
City	Sydney
Period	3/11/14 → 7/11/14

Keywords

EC Grant Agreement nr.: FP7/2007-2013
EC Grant Agreement nr.: FP7/295261
EC Grant Agreement nr.: FP7/318490
EC Grant Agreement nr.: FP7/318003
Rewards
Reachability
Markov automata
Analysis
Costs

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-319-11936-6_13

Guck2014modellingAccepted author version, 479 KB

24 Citations
1 Report

Modelling and analysis of Markov reward automata (extended version)
Guck, D., Timmer, M., Hatefi, H., Ruijters, E. J. J. & Stoelinga, M. I. A., 2014, Enschede: Centre for Telematics and Information Technology (CTIT). 35 p. (CTIT Technical Report Series; no. TR-CTIT-14-06)
Research output: Book/Report › Report › Professional

Open Access
File

Cite this

Guck, D., Timmer, M., Hatefi, H., Ruijters, E. J. J., & Stoelinga, M. I. A. (2014). Modelling and analysis of Markov reward automata. In F. Cassez, & J-F. Raskin (Eds.), Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 (pp. 168-184). (Lecture Notes in Computer Science; Vol. 8837). Springer. https://doi.org/10.1007/978-3-319-11936-6_13

@inproceedings{2f590fbbdcfb446db41b7fd192aea72c,

title = "Modelling and analysis of Markov reward automata",

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.",

keywords = "EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/295261, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/318003, Rewards, Reachability, Markov automata, Analysis, Costs",

author = "Dennis Guck and Mark Timmer and Hassan Hatefi and Ruijters, {Enno J.J.} and Stoelinga, {Mari{\"e}lle I.A.}",

note = "Foreground = 20% ; Type of activity = Conference ; Main leader = UT ; Type of audience = Scientific ; Size of audience = 100 ; Countries addressed = international ;; 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014, ATVA ; Conference date: 03-11-2014 Through 07-11-2014",

year = "2014",

month = nov,

doi = "10.1007/978-3-319-11936-6_13",

language = "English",

isbn = "978-3-319-11935-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "168--184",

editor = "Franck Cassez and Jean-Fran{\c c}ois Raskin",

booktitle = "Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014",

}

Guck, D, Timmer, M, Hatefi, H, Ruijters, EJJ & Stoelinga, MIA 2014, Modelling and analysis of Markov reward automata. in F Cassez & J-F Raskin (eds), Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014. Lecture Notes in Computer Science, vol. 8837, Springer, Berlin, pp. 168-184, 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014, Sydney, New South Wales, Australia, 3/11/14. https://doi.org/10.1007/978-3-319-11936-6_13

Modelling and analysis of Markov reward automata. / Guck, Dennis; Timmer, Mark; Hatefi, Hassan et al.
Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014. ed. / Franck Cassez; Jean-François Raskin. Berlin: Springer, 2014. p. 168-184 (Lecture Notes in Computer Science; Vol. 8837).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Modelling and analysis of Markov reward automata

AU - Guck, Dennis

AU - Timmer, Mark

AU - Hatefi, Hassan

AU - Ruijters, Enno J.J.

AU - Stoelinga, Mariëlle I.A.

N1 - Conference code: 12

PY - 2014/11

Y1 - 2014/11

N2 - 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.

AB - 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.

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - EC Grant Agreement nr.: FP7/295261

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/318003

KW - Rewards

KW - Reachability

KW - Markov automata

KW - Analysis

KW - Costs

U2 - 10.1007/978-3-319-11936-6_13

DO - 10.1007/978-3-319-11936-6_13

M3 - Conference contribution

SN - 978-3-319-11935-9

T3 - Lecture Notes in Computer Science

SP - 168

EP - 184

BT - Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014

A2 - Cassez, Franck

A2 - Raskin, Jean-François

PB - Springer

CY - Berlin

T2 - 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014

Y2 - 3 November 2014 through 7 November 2014

ER -

Modelling and analysis of Markov reward automata

Abstract

Publication series

Conference

Keywords

UN SDGs

Access to Document

Fingerprint

Research output

Modelling and analysis of Markov reward automata (extended version)

Cite this