A Markov Chain Model Checker

H. Hermanns, Joost P. Katoen, Joachim Meyer-Kayser, M. Siegle

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

58 Citations (Scopus)
41 Downloads (Pure)

Abstract

Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen Twente Markov Chain Checker $(E \vdash MC^2$), where properties are expressed in appropriate extensions of CTL. We illustrate the general bene ts of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of $(E \vdash MC^2$).
Original languageUndefined
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000
EditorsS. Graf, M.I. Schwartzbach
Place of PublicationBerlin
PublisherSpringer
Pages347-362
Number of pages16
ISBN (Print)3-540-67282-6
DOIs
Publication statusPublished - Apr 2000
Event6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000 - Berlin, Germany
Duration: 27 Mar 200031 Mar 2000
Conference number: 6

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume1785

Conference

Conference6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000
Abbreviated titleTACAS
CountryGermany
CityBerlin
Period27/03/0031/03/00

Keywords

  • EWI-6440
  • METIS-119649
  • IR-66266

Cite this

Hermanns, H., Katoen, J. P., Meyer-Kayser, J., & Siegle, M. (2000). A Markov Chain Model Checker. In S. Graf, & M. I. Schwartzbach (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000 (pp. 347-362). (Lecture Notes in Computer Science; Vol. 1785). Berlin: Springer. https://doi.org/10.1007/3-540-46419-0
Hermanns, H. ; Katoen, Joost P. ; Meyer-Kayser, Joachim ; Siegle, M. / A Markov Chain Model Checker. Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000. editor / S. Graf ; M.I. Schwartzbach. Berlin : Springer, 2000. pp. 347-362 (Lecture Notes in Computer Science).
@inproceedings{28b47a89f58746508cc5924c79b09662,
title = "A Markov Chain Model Checker",
abstract = "Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen Twente Markov Chain Checker $(E \vdash MC^2$), where properties are expressed in appropriate extensions of CTL. We illustrate the general bene ts of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of $(E \vdash MC^2$).",
keywords = "EWI-6440, METIS-119649, IR-66266",
author = "H. Hermanns and Katoen, {Joost P.} and Joachim Meyer-Kayser and M. Siegle",
year = "2000",
month = "4",
doi = "10.1007/3-540-46419-0",
language = "Undefined",
isbn = "3-540-67282-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "347--362",
editor = "S. Graf and M.I. Schwartzbach",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000",

}

Hermanns, H, Katoen, JP, Meyer-Kayser, J & Siegle, M 2000, A Markov Chain Model Checker. in S Graf & MI Schwartzbach (eds), Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000. Lecture Notes in Computer Science, vol. 1785, Springer, Berlin, pp. 347-362, 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, Berlin, Germany, 27/03/00. https://doi.org/10.1007/3-540-46419-0

A Markov Chain Model Checker. / Hermanns, H.; Katoen, Joost P.; Meyer-Kayser, Joachim; Siegle, M.

Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000. ed. / S. Graf; M.I. Schwartzbach. Berlin : Springer, 2000. p. 347-362 (Lecture Notes in Computer Science; Vol. 1785).

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - A Markov Chain Model Checker

AU - Hermanns, H.

AU - Katoen, Joost P.

AU - Meyer-Kayser, Joachim

AU - Siegle, M.

PY - 2000/4

Y1 - 2000/4

N2 - Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen Twente Markov Chain Checker $(E \vdash MC^2$), where properties are expressed in appropriate extensions of CTL. We illustrate the general bene ts of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of $(E \vdash MC^2$).

AB - Markov chains are widely used in the context of performance and reliability evaluation of systems of various nature. Model checking of such chains with respect to a given (branching) temporal logic formula has been proposed for both the discrete [17,6] and the continuous time setting [4,8]. In this paper, we describe a prototype model checker for discrete and continuous-time Markov chains, the Erlangen Twente Markov Chain Checker $(E \vdash MC^2$), where properties are expressed in appropriate extensions of CTL. We illustrate the general bene ts of this approach and discuss the structure of the tool. Furthermore we report on first successful applications of the tool to non-trivial examples, highlighting lessons learned during development and application of $(E \vdash MC^2$).

KW - EWI-6440

KW - METIS-119649

KW - IR-66266

U2 - 10.1007/3-540-46419-0

DO - 10.1007/3-540-46419-0

M3 - Conference contribution

SN - 3-540-67282-6

T3 - Lecture Notes in Computer Science

SP - 347

EP - 362

BT - Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000

A2 - Graf, S.

A2 - Schwartzbach, M.I.

PB - Springer

CY - Berlin

ER -

Hermanns H, Katoen JP, Meyer-Kayser J, Siegle M. A Markov Chain Model Checker. In Graf S, Schwartzbach MI, editors, Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000. Berlin: Springer. 2000. p. 347-362. (Lecture Notes in Computer Science). https://doi.org/10.1007/3-540-46419-0