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 languageUndefined
Title of host publicationProceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
Place of PublicationBerlin
PublisherSpringer
Pages168-184
Number of pages17
ISBN (Print)978-3-319-11935-9
DOIs
StatePublished - Nov 2014
Event12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8837
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
Abbreviated titleATVA
CountryAustralia
CitySydney
Period3/11/147/11/14

Fingerprint

Costs
Flavors
Repair
Energy utilization

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
  • EWI-25349
  • METIS-309681
  • Rewards
  • Reachability
  • IR-93331
  • Markov Automata
  • Analysis
  • Costs

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 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). Berlin: Springer. DOI: 10.1007/978-3-319-11936-6_13

Guck, Dennis; Timmer, Mark; Hatefi, Hassan; Ruijters, Enno Jozef Johannes; Stoelinga, Mariëlle Ida Antoinette / Modelling and analysis of Markov reward automata.

Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014. Berlin : Springer, 2014. p. 168-184 (Lecture Notes in Computer Science; Vol. 8837).

Research output: Scientific - peer-reviewConference contribution

@inbook{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, EWI-25349, METIS-309681, Rewards, Reachability, IR-93331, Markov Automata, Analysis, Costs",
author = "Dennis Guck and Mark Timmer and Hassan Hatefi and Ruijters, {Enno Jozef Johannes} and Stoelinga, {Mariëlle Ida Antoinette}",
note = "Foreground = 20% ; Type of activity = Conference ; Main leader = UT ; Type of audience = Scientific ; Size of audience = 100 ; Countries addressed = international ;",
year = "2014",
month = "11",
doi = "10.1007/978-3-319-11936-6_13",
isbn = "978-3-319-11935-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "168--184",
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 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, Australia, 3-7 November. DOI: 10.1007/978-3-319-11936-6_13

Modelling and analysis of Markov reward automata. / Guck, Dennis; Timmer, Mark; Hatefi, Hassan; Ruijters, Enno Jozef Johannes; Stoelinga, Mariëlle Ida Antoinette.

Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014. Berlin : Springer, 2014. p. 168-184 (Lecture Notes in Computer Science; Vol. 8837).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Modelling and analysis of Markov reward automata

AU - Guck,Dennis

AU - Timmer,Mark

AU - Hatefi,Hassan

AU - Ruijters,Enno Jozef Johannes

AU - Stoelinga,Mariëlle Ida Antoinette

N1 - Foreground = 20% ; Type of activity = Conference ; Main leader = UT ; Type of audience = Scientific ; Size of audience = 100 ; Countries addressed = international ;

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 - EWI-25349

KW - METIS-309681

KW - Rewards

KW - Reachability

KW - IR-93331

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

PB - Springer

ER -

Guck D, Timmer M, Hatefi H, Ruijters EJJ, Stoelinga MIA. Modelling and analysis of Markov reward automata. In Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014. Berlin: Springer. 2014. p. 168-184. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-11936-6_13