Efficient CSL Model Checking Using Stratification

Publication: Research - peer-reviewJournal article – Annual report year: 2012



View graph of relations

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
Publication date2012
PagesPaper 17
Number of pages18

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/).

CitationsWeb of Science® Times Cited: 0


  • Continuous-time Markov chains, Continuous stochastic logic, Model checking, Approximation algorithm, Stratification
Download as:
Download as PDF
Select render style:
Download as HTML
Select render style:
Download as Word
Select render style:

Download statistics

No data available

ID: 10854164