Model Checking Algorithms for Markov Reward Models

Lucia Cloth

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

72 Downloads (Pure)

Abstract

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.
Original languageEnglish
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Haverkort, Boudewijn Remigius Heinrich Maria, Supervisor
Award date13 Jan 2006
Place of PublicationEnschede
Publisher
Print ISBNs90-365-2317-6
Publication statusPublished - 13 Jan 2006

Fingerprint

Model checking
Formal methods
Disasters
Large scale systems
Communication systems
Information systems
Specifications

Keywords

  • EWI-9124
  • METIS-238765
  • IR-55445

Cite this

Cloth, L. (2006). Model Checking Algorithms for Markov Reward Models. Enschede: University of Twente.
Cloth, Lucia. / Model Checking Algorithms for Markov Reward Models. Enschede : University of Twente, 2006. 146 p.
@phdthesis{d5dec4438b1d47f5971481c3aeb3a304,
title = "Model Checking Algorithms for Markov Reward Models",
abstract = "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.",
keywords = "EWI-9124, METIS-238765, IR-55445",
author = "Lucia Cloth",
note = "CTIT Ph.D.-thesis Series No. 06-81",
year = "2006",
month = "1",
day = "13",
language = "English",
isbn = "90-365-2317-6",
publisher = "University of Twente",
address = "Netherlands",
school = "University of Twente",

}

Cloth, L 2006, 'Model Checking Algorithms for Markov Reward Models', University of Twente, Enschede.

Model Checking Algorithms for Markov Reward Models. / Cloth, Lucia.

Enschede : University of Twente, 2006. 146 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

TY - THES

T1 - Model Checking Algorithms for Markov Reward Models

AU - Cloth, Lucia

N1 - CTIT Ph.D.-thesis Series No. 06-81

PY - 2006/1/13

Y1 - 2006/1/13

N2 - 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.

AB - 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.

KW - EWI-9124

KW - METIS-238765

KW - IR-55445

M3 - PhD Thesis - Research UT, graduation UT

SN - 90-365-2317-6

PB - University of Twente

CY - Enschede

ER -

Cloth L. Model Checking Algorithms for Markov Reward Models. Enschede: University of Twente, 2006. 146 p.