Modelling and analysis of Markov reward automata

Dennis Guck, Mark Timmer, Hassan Hatefi, Enno Jozef Johannes Ruijters, Mariëlle Ida Antoinette Stoelinga

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

    21 Citations (Scopus)
    97 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 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
    Publication statusPublished - Nov 2014
    Event12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia
    Duration: 3 Nov 20147 Nov 2014
    Conference number: 12

    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

    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. https://doi.org/10.1007/978-3-319-11936-6_13