Abstract
Model checking Markov reward models unites two different
approaches of modelbased system validation. On the one hand, Markov
reward models have a long tradition in modelbased performance
and dependability evaluation. On the other hand, a formal method like
model checking allows for the precise specification and verification
of complex qualitative system properties. The logic CSRL
(an extension
of CTL) provides
the specific means to formulate desired
properties of Markov reward models,
including constraints on time and accumulated reward. The most involved
operator of CSRL
is the socalled until operator with quantitative constraints
in the form of a time and
a reward interval. Its model checking is closely
connected to the computation of the distribution of accumulated
reward in the Markov reward model. So far, suitable numerical algorithms
have only been published for the restricted case where the time and the
reward interval have lower bounds equal to zero.
In this thesis we close the gap
and present the theoretical basis as well as the numerical algorithms
needed for model checking CSRL
until formulas with arbitrary time and
reward intervals.
CSRL is useful for the assessment of many interesting properties,
for example, the survivability of an information or communication system.
A system is survivable
if it is able to recover properly after is has been affected by a disaster.
We translate this general definition of
survivability into a CSRL formula which then
can easily be instantiated for the system model under study.
The basic building blocks for CSRL formulas are atomic propositions
that are assigned to the states of a Markov reward model. We extend
CSRL to pathCSRL, where we can reason about the actions occurring in
a Markov reward model as well. The logic pathCSRL additionally includes
regular expressions as a more flexible mechanism for defining path properties
and, hence, effectively extends the expressive power of CSRL.
Throughout the thesis we illustrate all concepts and techniques with a
small running example. A number of larger case studies are also provided.
Original language  English 

Awarding Institution 

Supervisors/Advisors 

Award date  13 Jan 2006 
Place of Publication  Enschede 
Publisher  
Print ISBNs  9036523176 
Publication status  Published  13 Jan 2006 
Keywords
 EWI9124
 METIS238765
 IR55445
Fingerprint Dive into the research topics of 'Model Checking Algorithms for Markov Reward Models'. Together they form a unique fingerprint.
Cite this
Cloth, L. (2006). Model Checking Algorithms for Markov Reward Models. Enschede: University of Twente.