Modelling and analysis of Markov reward automata (extended version)

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

    Research output: Book/ReportReportProfessional

    46 Downloads (Pure)


    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
    Publication statusPublished - 2014

    Publication series

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


    • EC Grant Agreement nr.: FP7/295261
    • MAPA
    • Process Algebra
    • Quantitative analysis
    • EC Grant Agreement nr.: FP7/318490
    • Rewards
    • Markov Automata
    • EC Grant Agreement nr.: FP7/2007-2013


    Dive into the research topics of 'Modelling and analysis of Markov reward automata (extended version)'. Together they form a unique fingerprint.
    • Modelling and analysis of Markov reward automata

      Guck, D., Timmer, M., Hatefi, H., Ruijters, E. J. J. & Stoelinga, M. I. A., Nov 2014, Proceedings of the 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014. Cassez, F. & Raskin, J-F. (eds.). Berlin: Springer, p. 168-184 17 p. (Lecture Notes in Computer Science; vol. 8837).

      Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

      Open Access
      24 Citations (Scopus)
      180 Downloads (Pure)

    Cite this