Model Checking Algorithms for Markov Reward Models

Model checking Markov reward models unites two different approaches of model-based system validation. On the one hand, Markov reward models have a long tradition in model-based 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 so-called 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.