Efficient CSL Model Checking Using Stratification

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

Documents

DOI

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
Volume8
Issue2
PagesPaper 17
Number of pages18
ISSN1860-5974
DOIs
StatePublished

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

Keywords

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

Download statistics

No data available

ID: 10854164