Abstract
| 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 | |
| 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
Cite this
}
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 -