A tool for model-checking Markov chains

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

    Research output: Contribution to journalArticleAcademicpeer-review

    53 Citations (Scopus)
    32 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 languageEnglish
    Pages (from-to)153-172
    Number of pages20
    JournalInternational journal on software tools for technology transfer
    Volume4
    Issue number2
    DOIs
    Publication statusPublished - 2003

      Fingerprint

    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

    Cite this