Abstract

Costs and rewards are important ingredients for cyberphysical 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 accumulative reward until a goal is reached; the expected accumulative 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 languageEnglish
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages35
StatePublished - 2014

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-14-06
ISSN (Print)1381-3625

Fingerprint

Costs
Flavors
Repair
Energy utilization

Keywords

  • EC Grant Agreement nr.: FP7/295261
  • MAPA
  • Process Algebra
  • Quantitative analysis
  • EC Grant Agreement nr.: FP7/318490
  • Rewards
  • Markov Automata
  • EWI-24800
  • METIS-304117
  • IR-91270
  • EC Grant Agreement nr.: FP7/2007-2013

Cite this

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

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

Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 35 p. (CTIT Technical Report Series; No. TR-CTIT-14-06).

Research output: ProfessionalReport

@book{70bf3bdeea444dbc947ded9a5c1cea97,
title = "Modelling and analysis of Markov reward automata (extended version)",
abstract = "Costs and rewards are important ingredients for cyberphysical 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 accumulative reward until a goal is reached; the expected accumulative 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/295261, MAPA, Process Algebra, Quantitative analysis, EC Grant Agreement nr.: FP7/318490, Rewards, Markov Automata, EWI-24800, METIS-304117, IR-91270, EC Grant Agreement nr.: FP7/2007-2013",
author = "Dennis Guck and Mark Timmer and Hassan Hatefi and Ruijters, {Enno Jozef Johannes} and Stoelinga, {Mariëlle Ida Antoinette}",
note = "A revised version of this technical report has been published as a conference paper in ATVA 2014; see http://eprints.eemcs.utwente.nl/25349.",
year = "2014",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-14-06",
address = "Netherlands",

}

Guck, D, Timmer, M, Hatefi, H, Ruijters, EJJ & Stoelinga, MIA 2014, Modelling and analysis of Markov reward automata (extended version). CTIT Technical Report Series, no. TR-CTIT-14-06, Centre for Telematics and Information Technology (CTIT), Enschede.

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

Enschede : Centre for Telematics and Information Technology (CTIT), 2014. 35 p. (CTIT Technical Report Series; No. TR-CTIT-14-06).

Research output: ProfessionalReport

TY - BOOK

T1 - Modelling and analysis of Markov reward automata (extended version)

AU - Guck,Dennis

AU - Timmer,Mark

AU - Hatefi,Hassan

AU - Ruijters,Enno Jozef Johannes

AU - Stoelinga,Mariëlle Ida Antoinette

N1 - A revised version of this technical report has been published as a conference paper in ATVA 2014; see http://eprints.eemcs.utwente.nl/25349.

PY - 2014

Y1 - 2014

N2 - Costs and rewards are important ingredients for cyberphysical 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 accumulative reward until a goal is reached; the expected accumulative 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 cyberphysical 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 accumulative reward until a goal is reached; the expected accumulative 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/295261

KW - MAPA

KW - Process Algebra

KW - Quantitative analysis

KW - EC Grant Agreement nr.: FP7/318490

KW - Rewards

KW - Markov Automata

KW - EWI-24800

KW - METIS-304117

KW - IR-91270

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

M3 - Report

T3 - CTIT Technical Report Series

BT - Modelling and analysis of Markov reward automata (extended version)

PB - Centre for Telematics and Information Technology (CTIT)

ER -

Guck D, Timmer M, Hatefi H, Ruijters EJJ, Stoelinga MIA. Modelling and analysis of Markov reward automata (extended version). Enschede: Centre for Telematics and Information Technology (CTIT), 2014. 35 p. (CTIT Technical Report Series; TR-CTIT-14-06).