{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:32:11Z","timestamp":1777519931002,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221095","type":"print"},{"value":"9783642221101","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-22110-1_19","type":"book-chapter","created":{"date-parts":[[2011,7,4]],"date-time":"2011-07-04T13:08:45Z","timestamp":1309784925000},"page":"225-242","source":"Crossref","is-referenced-by-count":24,"title":["Model Checking Algorithms for CTMDPs"],"prefix":"10.1007","author":[{"given":"Peter","family":"Buchholz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ernst Moritz","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","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.K.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Log.\u00a01, 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"19_CR2","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.R., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng.\u00a029, 524\u2013541 (2003)","journal-title":"IEEE Trans. Software Eng."},{"key":"19_CR3","volume-title":"Dynamic Programming and Markov Processes","author":"R.A. Howard","year":"1960","unstructured":"Howard, R.A.: Dynamic Programming and Markov Processes. John Wiley and Sons, Inc., Chichester (1960)"},{"key":"19_CR4","volume-title":"Dynamic Programming and Optimal Control","author":"D.P. Bertsekas","year":"2005","unstructured":"Bertsekas, D.P.: Dynamic Programming and Optimal Control. Athena Scientific, Belmont (2005)"},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1016\/j.tcs.2005.07.022","volume":"345","author":"C. Baier","year":"2005","unstructured":"Baier, C., Hermanns, H., Katoen, J.P., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci.\u00a0345, 2\u201326 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"19_CR6","unstructured":"Br\u00e1zdil, T., Forejt, V., Krcal, J., Kret\u00ednsk\u00fd, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. In: FSTTCS. LIPIcs, vol.\u00a04, pp. 61\u201372 (2009)"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-00596-1_26","volume-title":"Foundations of Software Science and Computational Structures","author":"M.R. Neuh\u00e4u\u00dfer","year":"2009","unstructured":"Neuh\u00e4u\u00dfer, M.R., Stoelinga, M., Katoen, J.-P.: Delayed nondeterminism in continuous-time markov decision processes. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol.\u00a05504, pp. 364\u2013379. Springer, Heidelberg (2009)"},{"key":"19_CR8","unstructured":"Rabe, M., Schewe, S.: Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. In: CoRR, pp. 1004\u20134005 (2010)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: QEST (2010)","DOI":"10.1109\/QEST.2010.47"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Chen, T., Han, T., Katoen, J.P., Mereacre, A.: Computing maximum reachability probabilities in Markovian timed automata. Technical report, RWTH Aachen (2010)","DOI":"10.1109\/CDC.2011.6160992"},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1016\/j.cor.2010.08.011","volume":"38","author":"P. Buchholz","year":"2011","unstructured":"Buchholz, P., Schulz, I.: Numerical analysis of continuous time Markov decision processes over finite horizons. Computers & Operations Research\u00a038, 651\u2013659 (2011)","journal-title":"Computers & Operations Research"},{"key":"19_CR12","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1137\/0306020","volume":"6","author":"B.L. Miller","year":"1968","unstructured":"Miller, B.L.: Finite state continuous time Markov decision processes with a finite planning horizon. SIAM Journal on Control\u00a06, 266\u2013280 (1968)","journal-title":"SIAM Journal on Control"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate symbolic model checking of continuous-time markov chains (Extended abstract). In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, p. 146. Springer, Heidelberg (1999)"},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1214\/aos\/1176342621","volume":"2","author":"M.R. Lembersky","year":"1974","unstructured":"Lembersky, M.R.: On maximal rewards and \u03b5-optimal policies in continuous time Markov decision chains. The Annals of Statistics\u00a02, 159\u2013169 (1974)","journal-title":"The Annals of Statistics"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the logical characterisation of performability properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, p. 780. Springer, Heidelberg (2000)"},{"key":"19_CR16","doi-asserted-by":"publisher","first-page":"926","DOI":"10.1287\/opre.32.2.343","volume":"32","author":"D. Gross","year":"1984","unstructured":"Gross, D., Miller, D.: The randomization technique as a modeling tool and solution procedure for transient Markov processes. Operations Research\u00a032, 926\u2013944 (1984)","journal-title":"Operations Research"},{"key":"19_CR17","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1145\/42404.42409","volume":"31","author":"B.L. Fox","year":"1988","unstructured":"Fox, B.L., Glynn, P.W.: Computing Poisson probabilities. Comm. ACM\u00a031, 440\u2013445 (1988)","journal-title":"Comm. ACM"},{"key":"19_CR18","doi-asserted-by":"crossref","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. In: QEST, pp. 167\u2013176 (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"19_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-642-12002-2_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Zhang","year":"2010","unstructured":"Zhang, L., Neuh\u00e4u\u00dfer, M.R.: Model checking interactive markov chains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 53\u201368. Springer, Heidelberg (2010)"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"B\u00f6de, E., et al.: Compositional performability evaluation for statemate. In: QEST, pp. 167\u2013178 (2006)","DOI":"10.1109\/QEST.2006.10"},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1287\/opre.15.5.872","volume":"15","author":"A. Martin-L\u00f6fs","year":"1967","unstructured":"Martin-L\u00f6fs, A.: Optimal control of a continuous-time Markov chain with periodic transition probabilities. Operations Research\u00a015, 872\u2013881 (1967)","journal-title":"Operations Research"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-540-73368-3_37","volume-title":"Computer Aided Verification","author":"J.-P. Katoen","year":"2007","unstructured":"Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 311\u2013324. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22110-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,6]],"date-time":"2025-03-06T22:11:45Z","timestamp":1741299105000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22110-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221095","9783642221101"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22110-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}