Model Checking Markov Reward Models with Impulse Rewards

Lucia Cloth, Joost-Pieter Katoen, Maneesh Khattri, Reza Pulungan

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

    28 Citations (Scopus)
    14 Downloads (Pure)


    This paper considers model checking of Markov reward models (MRMs), continuous-time Markov chains with state rewards as well as impulse rewards. The reward extension of the logic CSL (Continuous Stochastic Logic) is interpreted over such MRMs, and two numerical algorithms are provided to check the reachability of a set of goal states under a time and an accumulated reward constraint. This extends existing model-checking techniques for MRMs with just state rewards, and improves the applicability to thousands of states. Our approach is illustrated by using rewards for energy consumption in the setting of dynamic power management.
    Original languageEnglish
    Title of host publication2005 International Conference on Dependable Systems and Networks (DSN'05)
    EditorsAndrea Bondavalli, Boudewijn Haverkort, Dong Tang
    Place of PublicationLos Alamitos, NJ
    PublisherIEEE Computer Society
    Number of pages10
    ISBN (Print)0-7695-2282-3
    Publication statusPublished - Jul 2005
    EventInternational Conference on Dependable Systems and Networks, DSN 2005 - Yokohama, Japan
    Duration: 28 Jun 20051 Jul 2005


    ConferenceInternational Conference on Dependable Systems and Networks, DSN 2005
    Abbreviated titleDSN


    • EWI-1542
    • IR-53159
    • METIS-225539


    Dive into the research topics of 'Model Checking Markov Reward Models with Impulse Rewards'. Together they form a unique fingerprint.

    Cite this