{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T15:49:47Z","timestamp":1776181787899,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642198342","type":"print"},{"value":"9783642198359","type":"electronic"}],"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-19835-9_12","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T15:03:16Z","timestamp":1300114996000},"page":"128-142","source":"Crossref","is-referenced-by-count":23,"title":["Efficient CTMC Model Checking of Linear Real-Time Objectives"],"prefix":"10.1007","author":[{"given":"Beno\u00eet","family":"Barbot","sequence":"first","affiliation":[]},{"given":"Taolue","family":"Chen","sequence":"additional","affiliation":[]},{"given":"Tingting","family":"Han","sequence":"additional","affiliation":[]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[]},{"given":"Alexandru","family":"Mereacre","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","unstructured":"PRISM website, http:\/\/www.prismmodelchecker.org"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","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. TCS\u00a0126(2), 183\u2013235 (1994)","journal-title":"TCS"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Amparore, E.G., Donatelli, S.: Model checking CSLTA with deterministic and stochastic Petri Nets. In: Dependable Systems and Networks (DSN), pp. 605\u2013614 (2010)","DOI":"10.1109\/DSN.2010.5544425"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Gr\u00f6sser, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: LICS, pp. 217\u2013226 (2008)","DOI":"10.1109\/LICS.2008.25"},{"issue":"4","key":"12_CR5","first-page":"209","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 TSE\u00a033(4), 209\u2013224 (2007)","journal-title":"IEEE TSE"},{"issue":"6","key":"12_CR6","first-page":"524","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE\u00a029(6), 524\u2013541 (2003)","journal-title":"IEEE TSE"},{"issue":"9","key":"12_CR7","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C. Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Commun. of the ACM\u00a053(9), 74\u201385 (2010)","journal-title":"Commun. of the ACM"},{"issue":"2-3","key":"12_CR8","first-page":"145","volume":"36","author":"B. B\u00e9rard","year":"1998","unstructured":"B\u00e9rard, B., Petit, A., Diekert, V., Gastin, P.: Characterization of the expressive power of silent transitions in timed automata. Fund. Inf.\u00a036(2-3), 145\u2013182 (1998)","journal-title":"Fund. Inf."},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST, pp. 55\u201364 (2008)","DOI":"10.1109\/QEST.2008.19"},{"issue":"2","key":"12_CR10","first-page":"35","volume":"220","author":"S. Blom","year":"2008","unstructured":"Blom, S., Haverkort, B.R., Kuntz, M., van de Pol, J.: Distributed Markovian bisimulation reduction aimed at CSL model checking. ENTCS\u00a0220(2), 35\u201350 (2008)","journal-title":"ENTCS"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-642-15375-4_15","volume-title":"CONCUR 2010 - Concurrency Theory","author":"T. Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil, T., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A., \u0158eh\u00e1k, V.: Stochastic real-time games with qualitative timed automata objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol.\u00a06269, pp. 207\u2013221. Springer, Heidelberg (2010)"},{"key":"12_CR12","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 specification. In: LICS, pp. 309\u2013318 (2009)","DOI":"10.1109\/LICS.2009.21"},{"issue":"6","key":"12_CR13","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1016\/S0020-0190(03)00343-0","volume":"87","author":"S. Derisavi","year":"2003","unstructured":"Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett.\u00a087(6), 309\u2013315 (2003)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"12_CR14","first-page":"224","volume":"35","author":"S. Donatelli","year":"2009","unstructured":"Donatelli, S., Haddad, S., Sproston, J.: Model checking timed and stochastic properties with CSLTA. IEEE TSE\u00a035(2), 224\u2013240 (2009)","journal-title":"IEEE TSE"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1038\/nri1374","volume":"4","author":"B. Goldstein","year":"2004","unstructured":"Goldstein, B., Faeder, J.R., Hlavacek, W.S.: Mathematical and computational models of immune-receptor signalling. Nat. Reviews Immunology\u00a04, 445\u2013456 (2004)","journal-title":"Nat. Reviews Immunology"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R.: Performance evaluation of polling-based communication systems using SPNs. In: Appl. of Petri Nets to Comm. Networks, pp. 176\u2013209 (1999)","DOI":"10.1007\/BFb0097777"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Hahn, E.M., Hermanns, H., Jansen, D.N., Zapreev, I.: The ins and outs of the probabilistic model checker MRMC. In: QEST, pp. 167\u2013176 (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.-P. Katoen","year":"2007","unstructured":"Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.: Bisimulation minimisation mostly speeds up probabilistic model checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 87\u2013101. Springer, Heidelberg (2007)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-642-12002-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Valmari","year":"2010","unstructured":"Valmari, A., Franceschinis, G.: Simple O(m logn) time markov chain lumping. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 38\u201352. Springer, Heidelberg (2010)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338 (1985)","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19835-9_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,4]],"date-time":"2025-03-04T07:44:45Z","timestamp":1741074285000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19835-9_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198342","9783642198359"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19835-9_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}