Modelling and analysis of Markov reward automata (extended version)

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

    Research output: Book/ReportReportProfessional

    16 Downloads (Pure)

    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
    Publication statusPublished - 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
    Data storage equipment

    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; TR-CTIT-14-06).
    @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{\"e}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",
    language = "English",
    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: Book/ReportReportProfessional

    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)

    CY - Enschede

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