Model-checking large structured Markov chains

P Buchholz, Joost P. Katoen, P. Kemper, C. Tepper

Research output: Contribution to journalArticleAcademicpeer-review

29 Citations (Scopus)
46 Downloads (Pure)

Abstract

This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.
Original languageEnglish
Pages (from-to)69-97
Number of pages28
JournalJournal of logic and algebraic programming
Volume56
Issue number1-2
DOIs
Publication statusPublished - May 2003

Fingerprint

Continuous-time Markov Chain
Model checking
Markov processes
Model Checking
Markov chain
State Space
Petri nets
Logic
Algebra
Queuing Networks
Stochastic Petri Nets
Process Algebra
Bisimulation
Petri Nets
Explosion
Performance Measures
Elimination
Modulo
Aggregation
Express

Keywords

  • FMT-MC: MODEL CHECKING
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • FMT-PM: PROBABILISTIC METHODS

Cite this

Buchholz, P ; Katoen, Joost P. ; Kemper, P. ; Tepper, C. / Model-checking large structured Markov chains. In: Journal of logic and algebraic programming. 2003 ; Vol. 56, No. 1-2. pp. 69-97.
@article{bb950d22ff654308a7e805d11c003651,
title = "Model-checking large structured Markov chains",
abstract = "This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.",
keywords = "FMT-MC: MODEL CHECKING, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-PM: PROBABILISTIC METHODS",
author = "P Buchholz and Katoen, {Joost P.} and P. Kemper and C. Tepper",
year = "2003",
month = "5",
doi = "10.1016/S1567-8326(02)00067-X",
language = "English",
volume = "56",
pages = "69--97",
journal = "Journal of logic and algebraic programming",
issn = "1567-8326",
publisher = "Elsevier",
number = "1-2",

}

Model-checking large structured Markov chains. / Buchholz, P; Katoen, Joost P.; Kemper, P.; Tepper, C.

In: Journal of logic and algebraic programming, Vol. 56, No. 1-2, 05.2003, p. 69-97.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Model-checking large structured Markov chains

AU - Buchholz, P

AU - Katoen, Joost P.

AU - Kemper, P.

AU - Tepper, C.

PY - 2003/5

Y1 - 2003/5

N2 - This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.

AB - This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-PM: PROBABILISTIC METHODS

U2 - 10.1016/S1567-8326(02)00067-X

DO - 10.1016/S1567-8326(02)00067-X

M3 - Article

VL - 56

SP - 69

EP - 97

JO - Journal of logic and algebraic programming

JF - Journal of logic and algebraic programming

SN - 1567-8326

IS - 1-2

ER -