Abstract
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 language | English |
---|---|
Journal | Logical Methods in Computer Science |
Volume | 8 |
Issue number | 2 |
Pages (from-to) | Paper 17 |
Number of pages | 18 |
ISSN | 1860-5974 |
DOIs | |
Publication status | Published - 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/).Keywords
- Continuous-time Markov chains
- Continuous stochastic logic
- Model checking
- Approximation algorithm
- Stratification