Abstract
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 
Fingerprint
Keywords
 EWI9124
 METIS238765
 IR55445
Cite this
}
Model Checking Algorithms for Markov Reward Models. / Cloth, Lucia.
Enschede : University of Twente, 2006. 146 p.Research output: Thesis › PhD Thesis  Research UT, graduation UT
TY  THES
T1  Model Checking Algorithms for Markov Reward Models
AU  Cloth, Lucia
N1  CTIT Ph.D.thesis Series No. 0681
PY  2006/1/13
Y1  2006/1/13
N2  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.
AB  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.
KW  EWI9124
KW  METIS238765
KW  IR55445
M3  PhD Thesis  Research UT, graduation UT
SN  9036523176
PB  University of Twente
CY  Enschede
ER 