Model Checking Algorithms for Markov Reward Models

Lucia Cloth

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    98 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 UT

    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.