|  |
| Title:
|
Automata-Based CSL Model Checking |
| Type:
|
Article in proceedingsArticle in proceedings |
| Participant(s):
|
Technical University of Denmark
Email:
Forfatter:
Jansen, David N.
Radboud Universiteit, Model-based system design
Technical University of Denmark
Email:
Forfatter:
Hermanns, Holger
Saarland University, Computer Science
|
| 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. 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. |
| Published:
|
part of: Automata, Languages and Programming (ISBN: 978-3-642-22011-1), pages: 271-282, 2011, Springer, |
| DOI:
|
|
| Presented at:
|
38th International Colloquium on Automata, Languages and Programming, Zürich |
|
|