{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T10:41:15Z","timestamp":1753180875518,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642220111"},{"type":"electronic","value":"9783642220128"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22012-8_21","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T03:29:39Z","timestamp":1308367779000},"page":"271-282","source":"Crossref","is-referenced-by-count":11,"title":["Automata-Based CSL Model Checking"],"prefix":"10.1007","author":[{"given":"Lijun","family":"Zhang","sequence":"first","affiliation":[]},{"given":"David N.","family":"Jansen","sequence":"additional","affiliation":[]},{"given":"Flemming","family":"Nielson","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"issue":"1","key":"21_CR2","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continous-time Markov chains. ACM Trans. Comput. Log.\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Log."},{"issue":"4","key":"21_CR3","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1109\/TSE.2007.36","volume":"33","author":"C. Baier","year":"2007","unstructured":"Baier, C., Cloth, L., Haverkort, B.R., Kuntz, M., Siegle, M.: Model checking Markov chains with actions and state labels. IEEE Trans. Softw. Eng.\u00a033(4), 209\u2013224 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"21_CR4","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng.\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"21_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2009.02.002","volume":"229","author":"P. Ballarini","year":"2009","unstructured":"Ballarini, P., Mardare, R., Mura, I.: Analysing biochemical oscillation through probabilistic model checking. Electr. Notes Theor. Comp. Sc.\u00a0229(1), 3\u201319 (2009)","journal-title":"Electr. Notes Theor. Comp. Sc."},{"key":"21_CR6","first-page":"309","volume-title":"Twenty-fourth Annual IEEE Symposium on Logic in Computer Science","author":"T. Chen","year":"2009","unstructured":"Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: Twenty-fourth Annual IEEE Symposium on Logic in Computer Science, pp. 309\u2013318. IEEE Comp. Soc., Los Alamitos (2009)"},{"issue":"2","key":"21_CR7","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1109\/TSE.2008.108","volume":"35","author":"S. Donatelli","year":"2009","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSLTA. IEEE Trans. Software Eng.\u00a035(2), 224\u2013240 (2009)","journal-title":"IEEE Trans. Software Eng."},{"key":"21_CR8","series-title":"Probability, Pure and Applied","first-page":"357","volume-title":"Numerical Solution of Markov Chains","author":"W.K. Grassmann","year":"1991","unstructured":"Grassmann, W.K.: Finding transient solutions in Markovian event systems through randomization. In: Stewart, W.J. (ed.) Numerical Solution of Markov Chains. Probability, Pure and Applied, vol.\u00a08, pp. 357\u2013371. Marcel Dekker, New York (1991)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"unstructured":"Jansen, D.N.: Erratum to: Model-checking continuous-time Markov chains by Aziz et al. (February 2011), http:\/\/arxiv.org\/abs\/1102.2079v1","key":"21_CR10"},{"issue":"2","key":"21_CR11","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.P. Katoen","year":"2011","unstructured":"Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Performance Evaluation\u00a068(2), 90\u2013104 (2011)","journal-title":"Performance Evaluation"},{"key":"21_CR12","first-page":"319","volume-title":"29th Ann. Symp. on Foundations of Computer Science","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of \u03c9-automata. In: 29th Ann. Symp. on Foundations of Computer Science, pp. 319\u2013327. IEEE Comp. Soc., Los Alamitos (1988)"},{"unstructured":"Spieler, D.: Model checking of oscillatory and noisy periodic behavior in Markovian population models. Master\u2019s thesis, Saarland University, Saarbr\u00fccken (2009), http:\/\/alma.cs.uni-sb.de\/data\/david\/mt.pdf","key":"21_CR13"},{"key":"21_CR14","volume-title":"Introduction to the numerical solution of Markov chains","author":"W.J. Stewart","year":"1994","unstructured":"Stewart, W.J.: Introduction to the numerical solution of Markov chains. Princeton Univ. Pr., Princeton (1994)"},{"key":"21_CR15","first-page":"332","volume-title":"Symposium on Logic in Computer Science","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science, pp. 332\u2013345. IEEE Comp. Soc., Los Alamitos (1986)"},{"doi-asserted-by":"crossref","unstructured":"Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Automata-based CSL model checking (April 2011), http:\/\/arxiv.org\/abs\/1104.4983","key":"21_CR16","DOI":"10.1007\/978-3-642-22012-8_21"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22012-8_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,11]],"date-time":"2019-06-11T20:07:04Z","timestamp":1560283624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22012-8_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642220111","9783642220128"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22012-8_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}