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)
    54 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