Automata-Based CSL Model Checking

Publication: Research - peer-reviewArticle in proceedings – Annual report year: 2011

NullPointerException

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. The presented decision procedure, however, has exponential complexity. In this paper, we propose an effective 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. We present a measure-preservation theorem allowing us to reduce the problem to a transient analysis on stratified CTMCs. The corresponding probability can then be approximated in polynomial time (using uniformization). 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 be incorrect in general. In fact, it works only for stratified CTMCs. As an additional contribution, our measure-preservation theorem can be used to ensure the decidability for general CTMCs.
Original languageEnglish
TitleAutomata, Languages and Programming : 38th International Colloquium, ICALP 2011 - Zurich, Switzerland, July 4-8, 2011 - Proceedings, Part II
PublisherSpringer
Publication date2011
Pages271-282
ISBN (print)978-3-642-22011-1
ISBN (electronic)978-3-642-22012-8
DOIs
StatePublished

Conference

Conference38th International Colloquium on Automata, Languages and Programming
Number38
CountrySwitzerland
CityZürich
Period04/07/1108/07/11
NameLecture Notes in Computer Science
Number6756
ISSN (Print)0302-9743
CitationsWeb of Science® Times Cited: No match on DOI
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

ID: 5722669