Back to University of Twente portal
| author: | Maneesh Khattri & Mhd. Reza M. I. Pulungan |
| title: | Model Checking Markov Reward Models with Impulse Rewards |
| keywords: | markov reward model, impulse rewards, model checking |
| topics: | |
| committee: |
Joost-Pieter Katoen
, Dipl. Inform. Lucia Cloth |
| end: | June 2004 |
Abstract
A Markov Reward Model (MRM) is a Stochastic Process satisfying the Markov property. MRMs have been used for the simultaneous analysis of performance and dependability issues of computer systems, sometimes referred to as performability. Previous work for Model Checking MRMs [Bai00, Bai02, Hav02] is restricted to state-based reward rates only. However, greater insight into the operation of systems can be obtained when impulse rewards are incorporated in these models which express the instantaneous cost imposed with the change of state of systems. The main aim of this thesis is to enable Model Checking of MRMs with impulse rewards. In this thesis methods for Model Checking MRMs have been extended for the incorporation of impulse rewards. To that end, the syntax and semantics of the temporal logic CSRL (Continuous Stochastic Reward Logic) have been adapted and algorithms have been developed and implemented that allow for the automated verification of properties expressed in that logic.