A Markov Chain Model Checker

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

doi:10.1007/3-540-46419-0

A Markov Chain Model Checker

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

58 Citations (Scopus)

67 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 language	Undefined
Title of host publication	Tools and Algorithms for the Construction and Analysis of Systems, 6th International Conference, TACAS 2000
Editors	S. Graf, M.I. Schwartzbach
Place of Publication	Berlin
Publisher	Springer
Pages	347-362
Number of pages	16
ISBN (Print)	3-540-67282-6
DOIs	https://doi.org/10.1007/3-540-46419-0
Publication status	Published - Apr 2000
Event	6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000 - Berlin, Germany Duration: 27 Mar 2000 → 31 Mar 2000 Conference number: 6

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	1785

Conference

Conference	6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000
Abbreviated title	TACAS
Country	Germany
City	Berlin
Period	27/03/00 → 31/03/00

Keywords

EWI-6440
METIS-119649
IR-66266

Access to Document

10.1007/3-540-46419-0

fulltext
open
fulltext
open

http://www.springerlink.com/content/33f6plvj7e9vutwb/

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

@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 proceeding › Conference contribution › Academic › peer-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 -