{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:52:18Z","timestamp":1740099138946,"version":"3.37.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319961446"},{"type":"electronic","value":"9783319961453"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_27","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"507-526","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Monitoring CTMCs by Multi-clock Timed Automata"],"prefix":"10.1007","author":[{"given":"Yijun","family":"Feng","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Haokun","family":"Li","sequence":"additional","affiliation":[]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3298-3817","authenticated-orcid":false,"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"issue":"2","key":"27_CR1","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-319-07734-5_19","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"EG Amparore","year":"2014","unstructured":"Amparore, E.G., Beccuti, M., Donatelli, S.: (Stochastic) model checking in GreatSPN. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 354\u2013363. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-07734-5_19"},{"issue":"1","key":"27_CR3","doi-asserted-by":"crossref","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. 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Log."},{"issue":"4","key":"27_CR4","doi-asserted-by":"crossref","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. 33(4), 209\u2013224 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"6","key":"27_CR5","doi-asserted-by":"crossref","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. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"27_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-19835-9_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Barbot","year":"2011","unstructured":"Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128\u2013142. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-19835-9_12"},{"issue":"4","key":"27_CR8","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/2528935","volume":"14","author":"T Chen","year":"2013","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Verification of linear duration properties over continuous-time Markov chains. ACM Trans. Comput. Log. 14(4), 33 (2013)","journal-title":"ACM Trans. Comput. Log."},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/978-3-642-24310-3_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T Chen","year":"2011","unstructured":"Chen, T., Diciolla, M., Kwiatkowska, M., Mereacre, A.: Time-bounded verification of CTMCs against real-time specifications. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 26\u201342. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24310-3_4"},{"key":"27_CR10","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Quantitative model checking of continuous-time Markov chains against timed automata specifications. In: LICS, pp. 309\u2013318 (2009)","DOI":"10.1109\/LICS.2009.21"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J., Mereacre, A.: Model checking of continuous-time Markov chains against timed automata specifications. Log. Methods Comput. Sci. 7(1) (2011)","DOI":"10.2168\/LMCS-7(1:12)2011"},{"key":"27_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-24288-5_2","volume-title":"Reachability Problems","author":"T Chen","year":"2011","unstructured":"Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Observing continuous-time MDPs by 1-clock timed automata. In: Delzanno, G., Potapov, I. (eds.) RP 2011. LNCS, vol. 6945, pp. 2\u201325. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-24288-5_2"},{"issue":"1","key":"27_CR13","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/s001650050034","volume":"11","author":"VH Dang","year":"1999","unstructured":"Dang, V.H., Zhou, C.: Probabilistic duration calculus for continuous time. Formal Aspects Comput. 11(1), 21\u201344 (1999)","journal-title":"Formal Aspects Comput."},{"key":"27_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4899-4483-2","volume-title":"Markov Models and Optimization","author":"MH Davis","year":"1993","unstructured":"Davis, M.H.: Markov Models and Optimization, vol. 49. CRC Press, Boca Raton (1993)"},{"key":"27_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with $${\\rm CSL}^{{T\\!\\!A}}$$CSLTA. IEEE Trans. Softw. Eng. 35(2), 224\u2013240 (2009)","DOI":"10.1109\/TSE.2008.108"},{"key":"27_CR17","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W Feller","year":"1968","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, vol. 3. Wiley, New York (1968)"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"Fu, H.: Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata. In: HSCC, pp. 323\u2013332. ACM (2013)","DOI":"10.1145\/2461328.2461376"},{"issue":"1\u20132","key":"27_CR19","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1016\/j.ipl.2012.09.009","volume":"113","author":"Y Gao","year":"2013","unstructured":"Gao, Y., Xu, M., Zhan, N., Zhang, L.: Model checking conditional CSL for continuous-time Markov chains. Inf. Process. Lett. 113(1\u20132), 44\u201350 (2013)","journal-title":"Inf. Process. Lett."},{"key":"27_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-71584-9","volume-title":"Numerical Treatment of Partial Differential Equations","author":"C Grossmann","year":"2007","unstructured":"Grossmann, C., Roos, H.-G., Stynes, M.: Numerical Treatment of Partial Differential Equations, vol. 154. Springer, Heidelberg (2007)"},{"key":"27_CR21","volume-title":"Numerical Solution of Partial Differential Equations by the Finite Element Method","author":"C Johnson","year":"2012","unstructured":"Johnson, C.: Numerical Solution of Partial Differential Equations by the Finite Element Method. Courier Corporation, Chelmsford (2012)"},{"issue":"2","key":"27_CR22","doi-asserted-by":"crossref","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. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"2","key":"27_CR24","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/s10703-012-0165-1","volume":"43","author":"L Mikeev","year":"2013","unstructured":"Mikeev, L., Neuh\u00e4u\u00dfer, M.R., Spieler, D., Wolf, V.: On-the-fly verification and optimization of DTA-properties for large Markov chains. Formal Methods Syst. Des. 43(2), 313\u2013337 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"27_CR25","doi-asserted-by":"crossref","unstructured":"Wisniewski, R., Sloth, C., Bujorianu, M.L., Piterman, N.: Safety verification of piecewise-deterministic Markov processes. In: HSCC, pp. 257\u2013266. ACM (2016)","DOI":"10.1145\/2883817.2883836"},{"key":"27_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-4346-9","volume-title":"Continuous-Time Markov Chains and Applications: A Two-Time-Scale Approach","author":"GG Yin","year":"2012","unstructured":"Yin, G.G., Zhang, Q.: Continuous-Time Markov Chains and Applications: A Two-Time-Scale Approach, vol. 37. Springer, New York (2012). \nhttps:\/\/doi.org\/10.1007\/978-1-4614-4346-9"},{"issue":"2:17","key":"27_CR27","first-page":"1","volume":"8","author":"L Zhang","year":"2012","unstructured":"Zhang, L., Jansen, D.N., Nielson, F., Hermanns, H.: Efficient CSL model checking using stratification. Log. Methods Comput. Sci. 8(2:17), 1\u201318 (2012)","journal-title":"Log. Methods Comput. Sci."},{"issue":"5","key":"27_CR28","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:52:42Z","timestamp":1532112762000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}