Model-checking large structured Markov chains

P Buchholz, Joost P. Katoen, P. Kemper, C. Tepper

    Research output: Contribution to journalArticleAcademicpeer-review

    29 Citations (Scopus)
    78 Downloads (Pure)

    Abstract

    This paper presents algorithms and experimental results for model-checking continuous-time Markov chains (CTMCs) based on a structured analysis approach. In this approach, a CTMC is represented as a term in Kronecker algebra that reflects the component structure of the system model. Such representations can be obtained in a natural way from various high-level specification formalisms, such as stochastic extensions of Petri nets, process algebras or activity networks. Properties are expressed in continuous stochastic logic (CSL) which includes means to express transient, steady-state and path performance measures. This paper describes novel model-checking algorithms for CSL that fully exploit the compositional description of the CTMC. This yields an effective way to combat the state-space explosion problem and enables the model-checking of fairly large Markov chains. Furthermore, we show how state-space aggregation (modulo bisimulation) and the elimination of vanishing states can be done in a component-wise manner. To demonstrate the applicability of the approach, and to assess the efficiency of our algorithms, we analyze a stochastic Petri net-model of a workstation cluster system and a simple queuing network.
    Original languageEnglish
    Pages (from-to)69-97
    Number of pages28
    JournalJournal of logic and algebraic programming
    Volume56
    Issue number1-2
    DOIs
    Publication statusPublished - May 2003

      Fingerprint

    Keywords

    • FMT-MC: MODEL CHECKING
    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-PM: PROBABILISTIC METHODS

    Cite this