A tool for model-checking Markov chains

Holger Hermanns; Joost-Pieter Katoen; Joachim Meyer-Kayser; Markus Siegle

doi:10.1007/s100090100072

A tool for model-checking Markov chains

Holger Hermanns, Joost-Pieter Katoen, Joachim Meyer-Kayser, Markus Siegle

Research output: Contribution to journal › Article › Academic › peer-review

58 Citations (Scopus)

44 Downloads (Pure)

Abstract

Markov chains are widely used in the context of the performance and reliability modeling of various systems. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both discrete [34, 10] and continuous time settings [7, 12]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker EÎMC2, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore, we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of EÎMC2.

Original language	English
Pages (from-to)	153-172
Number of pages	20
Journal	International journal on software tools for technology transfer
Volume	4
Issue number	2
DOIs	https://doi.org/10.1007/s100090100072
Publication status	Published - 2003

Keywords

FMT-MC: MODEL CHECKING
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
FMT-PM: PROBABILISTIC METHODS
Markov chain
Model checking
Numerical mathematics
Performance evaluation
Probabilistic systems
Temporal logic

Access to Document

10.1007/s100090100072

Cite this

@article{e55136072ed445af8f68aa8db9a7308b,

title = "A tool for model-checking Markov chains",

abstract = "Markov chains are widely used in the context of the performance and reliability modeling of various systems. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both discrete [34, 10] and continuous time settings [7, 12]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker E{\^I}MC2, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore, we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of E{\^I}MC2.",

keywords = "FMT-MC: MODEL CHECKING, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-PM: PROBABILISTIC METHODS, Markov chain, Model checking, Numerical mathematics, Performance evaluation, Probabilistic systems, Temporal logic",

author = "Holger Hermanns and Joost-Pieter Katoen and Joachim Meyer-Kayser and Markus Siegle",

year = "2003",

doi = "10.1007/s100090100072",

language = "English",

volume = "4",

pages = "153--172",

journal = "International journal on software tools for technology transfer",

issn = "1433-2779",

publisher = "Springer",

number = "2",

}

TY - JOUR

T1 - A tool for model-checking Markov chains

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

AU - Meyer-Kayser, Joachim

AU - Siegle, Markus

PY - 2003

Y1 - 2003

N2 - Markov chains are widely used in the context of the performance and reliability modeling of various systems. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both discrete [34, 10] and continuous time settings [7, 12]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker EÎMC2, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore, we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of EÎMC2.

AB - Markov chains are widely used in the context of the performance and reliability modeling of various systems. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both discrete [34, 10] and continuous time settings [7, 12]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen-Twente Markov Chain Checker EÎMC2, where properties are expressed in appropriate extensions of CTL. We illustrate the general benefits of this approach and discuss the structure of the tool. Furthermore, we report on successful applications of the tool to some examples, highlighting lessons learned during the development and application of EÎMC2.

KW - FMT-MC: MODEL CHECKING

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-PM: PROBABILISTIC METHODS

KW - Markov chain

KW - Model checking

KW - Numerical mathematics

KW - Performance evaluation

KW - Probabilistic systems

KW - Temporal logic

U2 - 10.1007/s100090100072

DO - 10.1007/s100090100072

M3 - Article

SN - 1433-2779

VL - 4

SP - 153

EP - 172

JO - International journal on software tools for technology transfer

JF - International journal on software tools for technology transfer

IS - 2

ER -

A tool for model-checking Markov chains

Abstract

Keywords

Access to Document

Fingerprint

Cite this