{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:58Z","timestamp":1760202658727,"version":"3.41.2"},"reference-count":22,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,7,31]],"date-time":"2012-07-31T00:00:00Z","timestamp":1343692800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["295261"],"award-info":[{"award-number":["295261"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["214755"],"award-info":[{"award-number":["214755"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>For continuous-time Markov chains, the model-checking problem with respect to\ncontinuous-time stochastic logic (CSL) has been introduced and shown to be\ndecidable by Aziz, Sanwal, Singhal and Brayton in 1996. Their proof can be\nturned into an approximation algorithm with worse than exponential complexity.\nIn 2000, Baier, Haverkort, Hermanns and Katoen presented an efficient\npolynomial-time approximation algorithm for the sublogic in which only binary\nuntil is allowed. In this paper, we propose such an efficient polynomial-time\napproximation algorithm for full CSL. The key to our method is the notion of\nstratified CTMCs with respect to the CSL property to be checked. On a\nstratified CTMC, the probability to satisfy a CSL path formula can be\napproximated by a transient analysis in polynomial time (using uniformization).\nWe present a measure-preserving, linear-time and -space transformation of any\nCTMC into an equivalent, stratified one. This makes the present work the\ncenterpiece of a broadly applicable full CSL model checker. Recently, the\ndecision algorithm by Aziz et al. was shown to work only for stratified CTMCs.\nAs an additional contribution, our measure-preserving transformation can be\nused to ensure the decidability for general CTMCs.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:17)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":5,"title":["Efficient CSL Model Checking Using Stratification"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Lijun","family":"Zhang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6636-3301","authenticated-orcid":false,"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7362-6176","authenticated-orcid":false,"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,7,31]]},"reference":[{"key":"10.2168\/LMCS-8(2:17)2012_AzizSSB96","doi-asserted-by":"crossref","unstructured":"A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. Verifying continuous time Markov chains. In R. Alur and T. A. Henzinger, editors,Computer aided verification: ...CAV, volume 1102 ofLNCS, pages 269-276. Springer, Berlin, 1996.","DOI":"10.1007\/3-540-61474-5_75"},{"issue":"1","key":"10.2168\/LMCS-8(2:17)2012_AzizSSB00","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz, K. Sanwal, V. Singhal, and R. B","year":"2000","journal-title":"ACM trans. comput. log."},{"issue":"4","key":"10.2168\/LMCS-8(2:17)2012_BaierCHKS07-asCSL","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C. Baier, L. Cloth, B. R. Haverkort, M.","year":"2007","journal-title":"IEEE trans. softw. eng."},{"key":"10.2168\/LMCS-8(2:17)2012_BaierHHK00","doi-asserted-by":"crossref","unstructured":"C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model checking continuous-time Markov chains by transient analysis. In E. A. Emerson and A. P. Sistla, editors,Computer aided verification: ...CAV, volume 1855 ofLNCS, pages 358-372, Berlin, 2000. Springer.","DOI":"10.1007\/10722167_28"},{"issue":"6","key":"10.2168\/LMCS-8(2:17)2012_hermanns_ctmc","doi-asserted-by":"crossref","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier, B. Haverkort, H. Hermanns, and","year":"2003","journal-title":"IEEE trans. softw. eng."},{"issue":"1","key":"10.2168\/LMCS-8(2:17)2012_ballarini","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2009.02.002","volume":"229","author":"P. Ballarini, R. Mardare, and I. Mura","year":"2009","journal-title":"Electr. notes theor. comp. sc."},{"issue":"1","key":"10.2168\/LMCS-8(2:17)2012_ChenHKM09-lmcs","volume":"7","author":"T. Chen, T. Han, J.-P. Katoen, and A. Me","year":"2011","journal-title":"Logical Methods in Computer Science"},{"issue":"2","key":"10.2168\/LMCS-8(2:17)2012_DonatelliHS09","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S. Donatelli, S. Haddad, and J. Sproston","year":"2009","journal-title":"IEEE trans. software eng."},{"issue":"4","key":"10.2168\/LMCS-8(2:17)2012_FoxG88","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"B. L. Fox and P. W. Glynn","year":"1988","journal-title":"Commun. ACM"},{"key":"10.2168\/LMCS-8(2:17)2012_Grassmann91","doi-asserted-by":"crossref","unstructured":"W. K. Grassmann. Finding transient solutions in Markovian event systems through randomization. In W. J. Stewart, editor,Numerical solution of Markov chains, volume 8 ofProbability, pure and applied, pages 357-371, New York, 1991. Marcel Dekker.","DOI":"10.1201\/9781003210160-18"},{"issue":"1","key":"10.2168\/LMCS-8(2:17)2012_HahnHWZ09","doi-asserted-by":"crossref","first-page":"129","DOI":"10.3233\/FI-2009-145","volume":"95","author":"E. M. Hahn, H. Hermanns, B. Wachter, and","year":"2009","journal-title":"Fundam. inform."},{"key":"10.2168\/LMCS-8(2:17)2012_HenzingerMW09","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, M. Mateescu, and V. Wolf. Sliding window abstraction for infinite Markov chains. In A. Bouajjani and O. Maler, editors,Computer aided verification: ...CAV, volume 5643 ofLNCS, pages 337-352, Berlin, 2009. Springer.","DOI":"10.1007\/978-3-642-02658-4_27"},{"key":"10.2168\/LMCS-8(2:17)2012_Jansen11-ErratumAziz","unstructured":"D. N. Jansen. Erratum to: Model-checking continuous-time Markov chains by Aziz et al. http:\/\/arxiv.org\/abs\/1102.2079v1, February 2011."},{"key":"10.2168\/LMCS-8(2:17)2012_2011-Jansen-UnderstandingFoxGlynn","unstructured":"D. N. Jansen. Understanding Fox and Glynn's ``Computing Poisson probabilities''. Technical Report ICIS-R11001, Radboud University Nijmegen, February 2011."},{"key":"10.2168\/LMCS-8(2:17)2012_KatoenKLW07","doi-asserted-by":"crossref","unstructured":"J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf. Three-valued abstraction for continuous-time Markov chains. In W. Damm and H. Hermanns, editors,Computer aided verification: ...CAV, volume 4590 ofLNCS, pages 311-324, Berlin, 2007. Springer.","DOI":"10.1007\/978-3-540-73368-3_37"},{"issue":"2","key":"10.2168\/LMCS-8(2:17)2012_KatoenZHHJ09","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.-P. Katoen, I. S. Zapreev, E. M. Hahn,","year":"2011","journal-title":"Performance evaluation"},{"key":"10.2168\/LMCS-8(2:17)2012_KwiatkowskaNP11","unstructured":"M. Z. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In G. Gopalakrishnan and S. Qadeer, editors,Computer aided verification: ...CAV, volume 6806 ofLNCS, pages 585-591. Springer, 2011."},{"key":"10.2168\/LMCS-8(2:17)2012_prakash","doi-asserted-by":"crossref","unstructured":"P. Panangaden.Labelled Markov processes. Imperial College Press, London, 2009.","DOI":"10.1142\/p595"},{"key":"10.2168\/LMCS-8(2:17)2012_spieler","unstructured":"D. Spieler. Model checking of oscillatory and noisy periodic behavior in Markovian population models. Master's thesis, Saarland University, Saarbr\u00fccken, 2009. http:\/\/alma.cs.uni-sb.de\/data\/david\/mt.pdf."},{"key":"10.2168\/LMCS-8(2:17)2012_Steward94","doi-asserted-by":"crossref","unstructured":"W. J. Stewart.Introduction to the numerical solution of Markov chains. Princeton Univ. Pr., Princeton, N. J., 1994.","DOI":"10.1515\/9780691223384"},{"key":"10.2168\/LMCS-8(2:17)2012_VardiW86","unstructured":"M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. InSymposium on logic in computer science, pages 332-345, Los Alamitos, Calif., 1986. IEEE Comp. Soc."},{"key":"10.2168\/LMCS-8(2:17)2012_icalp","doi-asserted-by":"crossref","unstructured":"L. Zhang, D. N. Jansen, F. Nielson, and H. Hermanns. Automata-based CSL model checking. In L. Aceto, M. Henzinger, and J. Sgall, editors,Automata, languages and programming: ...ICALP. Part II, volume 6756 ofLNCS, pages 271-282, Berlin, 2011. Springer.","DOI":"10.1007\/978-3-642-22012-8_21"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1085\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1085\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:03Z","timestamp":1681243383000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1085"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,31]]},"references-count":22,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:17)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1104.4983","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1104.4983","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,7,31]]},"article-number":"1085"}}