Efficient CSL Model Checking Using Stratification

Lijun Zhang, David N. Jansen, Flemming Nielson, Holger Hermanns

    Research output: Contribution to journalJournal articleResearchpeer-review

    379 Downloads (Pure)


    For continuous-time Markov chains, the model-checking problem with respect to continuous-time stochastic logic (CSL) has been introduced and shown to be decidable by Aziz, Sanwal, Singhal and Brayton in 1996 [ 1, 2]. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen [ 4, 5] presented an efficient polynomial-time approximation algorithm for the sublogic in which only binary until is allowed. In this paper, we propose such an efficient polynomial-time approximation algorithm for full CSL. The key to our method is the notion of stratified CTMCs with respect to the CSL property to be checked. On a stratified CTMC, the probability to satisfy a CSL path formula can be approximated by a transient analysis in polynomial time (using uniformization). We present a measure-preserving, linear-time and - space transformation of any CTMC into an equivalent, stratified one. This makes the present work the centerpiece of a broadly applicable full CSL model checker. Recently, the decision algorithm by Aziz et al. was shown to work only for stratified CTMCs. As an additional contribution, our measure-preserving transformation can be used to ensure the decidability for general CTMCs.
    Original languageEnglish
    JournalLogical Methods in Computer Science
    Issue number2
    Pages (from-to)Paper 17
    Number of pages18
    Publication statusPublished - 2012

    Bibliographical note

    This is an Open Access article distributed under the terms of the Creative Commons Attribution-NoDerivs license (http://creativecommons.org/licenses/by-nd/2.0/).


    • Continuous-time Markov chains
    • Continuous stochastic logic
    • Model checking
    • Approximation algorithm
    • Stratification


    Dive into the research topics of 'Efficient CSL Model Checking Using Stratification'. Together they form a unique fingerprint.

    Cite this