Efficient CSL Model Checking Using Stratification
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. Their proof can be turned into an approximation algorithm with worse than exponential compl...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2012-07-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1085/pdf |
| _version_ | 1797268693921562624 |
|---|---|
| author | Lijun Zhang David N. Jansen Flemming Nielson Holger Hermanns |
| author_facet | Lijun Zhang David N. Jansen Flemming Nielson Holger Hermanns |
| author_sort | Lijun Zhang |
| collection | DOAJ |
| description | 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. Their proof can be
turned into an approximation algorithm with worse than exponential complexity.
In 2000, Baier, Haverkort, Hermanns and Katoen 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. |
| first_indexed | 2024-04-25T01:36:33Z |
| format | Article |
| id | doaj.art-5c7885929a2a40b5ab101174893d7c37 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:33Z |
| publishDate | 2012-07-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-5c7885929a2a40b5ab101174893d7c372024-03-08T09:27:56ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742012-07-01Volume 8, Issue 210.2168/LMCS-8(2:17)20121085Efficient CSL Model Checking Using StratificationLijun ZhangDavid N. Jansenhttps://orcid.org/0000-0002-6636-3301Flemming Nielsonhttps://orcid.org/0000-0001-7362-6176Holger Hermannshttps://orcid.org/0000-0002-2766-9615For 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. Their proof can be turned into an approximation algorithm with worse than exponential complexity. In 2000, Baier, Haverkort, Hermanns and Katoen 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.https://lmcs.episciences.org/1085/pdfcomputer science - logic in computer scienceg.3, f.4.1, f.3.1 |
| spellingShingle | Lijun Zhang David N. Jansen Flemming Nielson Holger Hermanns Efficient CSL Model Checking Using Stratification Logical Methods in Computer Science computer science - logic in computer science g.3, f.4.1, f.3.1 |
| title | Efficient CSL Model Checking Using Stratification |
| title_full | Efficient CSL Model Checking Using Stratification |
| title_fullStr | Efficient CSL Model Checking Using Stratification |
| title_full_unstemmed | Efficient CSL Model Checking Using Stratification |
| title_short | Efficient CSL Model Checking Using Stratification |
| title_sort | efficient csl model checking using stratification |
| topic | computer science - logic in computer science g.3, f.4.1, f.3.1 |
| url | https://lmcs.episciences.org/1085/pdf |
| work_keys_str_mv | AT lijunzhang efficientcslmodelcheckingusingstratification AT davidnjansen efficientcslmodelcheckingusingstratification AT flemmingnielson efficientcslmodelcheckingusingstratification AT holgerhermanns efficientcslmodelcheckingusingstratification |