{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T03:26:21Z","timestamp":1777519581056,"version":"3.51.4"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319249520","type":"print"},{"value":"9783319249537","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24953-7_12","type":"book-chapter","created":{"date-parts":[[2015,10,7]],"date-time":"2015-10-07T15:00:11Z","timestamp":1444230011000},"page":"166-182","source":"Crossref","is-referenced-by-count":25,"title":["Optimal Continuous Time Markov Decisions"],"prefix":"10.1007","author":[{"given":"Yuliya","family":"Butkova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hassan","family":"Hatefi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Kr\u010d\u00e1l","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"key":"12_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.K.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"issue":"6","key":"12_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.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Softw. Eng. 29(6), 524\u2013541 (2003)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"12_CR3","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., Haverkort, B.R.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. Theor. Comput. Sci. 345(1), 2\u201326 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR4","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1016\/j.ic.2013.01.001","volume":"224","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Forejt, V., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Kucera, A.: Continuous-time stochastic games with time-bounded reachability. Inf. Comput. 224, 46\u201370 (2013)","journal-title":"Inf. Comput."},{"issue":"1","key":"12_CR5","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1145\/322234.322242","volume":"28","author":"JL Bruno","year":"1981","unstructured":"Bruno, J.L., Downey, P.J., Frederickson, G.N.: Sequencing tasks with exponential service times to minimize the expected flow time or makespan. J. ACM 28(1), 100\u2013113 (1981)","journal-title":"J. ACM"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-642-22110-1_19","volume-title":"Computer Aided Verification","author":"P Buchholz","year":"2011","unstructured":"Buchholz, P., Hahn, E.M., Hermanns, H., Zhang, L.: Model checking algorithms for CTMDPs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 225\u2013242. Springer, Heidelberg (2011)"},{"issue":"3","key":"12_CR7","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. Comput. OR 38(3), 651\u2013659 (2011)","journal-title":"Comput. OR"},{"key":"12_CR8","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Kr\u010d\u00e1l, J.: Optimal continuous time Markov decisions. CoRR abs\/1507.02876 (2015). http:\/\/arxiv.org\/abs\/1507.02876"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/978-3-642-38697-8_6","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"Christian Eisentraut","year":"2013","unstructured":"Eisentraut, Christian, Hermanns, Holger, Katoen, Joost-Pieter, Zhang, Lijun: A semantics for every GSPN. In: Colom, Jos\u00e9-Manuel, Desel, J\u00f6rg (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 90\u2013109. Springer, Heidelberg (2013)"},{"key":"12_CR10","unstructured":"Fearnley, J., Rabe, M., Schewe, S., Zhang, L.: Efficient approximation of optimal control for continuous-time markov games. In: FSTTCS, pp. 399\u2013410 (2011)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Ghemawat, S., Gobioff, H., Leung, S.T.: The Google file system. In: SOSP, pp. 29\u201343. ACM (2003)","DOI":"10.1145\/1165389.945450"},{"key":"12_CR12","unstructured":"Guck, D.: Quantitative Analysis of Markov Automata. Master\u2019s thesis, RWTH Aachen University, June 2012"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-40196-1_5","volume-title":"Quantitative Evaluation of Systems","author":"D Guck","year":"2013","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J.-P., Timmer, M.: Modelling, reduction and analysis of markov automata. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 55\u201371. Springer, Heidelberg (2013)"},{"key":"12_CR14","unstructured":"Gurobi Optimization Inc: Gurobi optimizer reference manual, version 6.0 (2015)"},{"key":"12_CR15","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. In: ECEASST, vol. 53 (2012)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-40213-5_16","volume-title":"Fundamentals of Software Engineering","author":"H Hatefi","year":"2013","unstructured":"Hatefi, H., Hermanns, H.: Improving time bounded reachability computations in interactive markov chains. In: Arbab, F., Sirjani, M. (eds.) FSEN 2013. LNCS, vol. 8161, pp. 250\u2013266. Springer, Heidelberg (2013)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.: On the use of model checking techniques for dependability evaluation. In: SRDS 2000, pp. 228\u2013237. IEEE CS (2000)","DOI":"10.1109\/RELDI.2000.885410"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-642-17071-3_16","volume-title":"Formal Methods for Components and Objects","author":"H Hermanns","year":"2010","unstructured":"Hermanns, H., Katoen, J.-P.: The how and why of interactive markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 311\u2013338. Springer, Heidelberg (2010)"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1080\/03461238.1953.10419459","volume":"1953","author":"A Jensen","year":"1953","unstructured":"Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Scand. Actuarial J. 1953, 87\u201391 (1953)","journal-title":"Scand. Actuarial J."},{"issue":"2","key":"12_CR20","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J Katoen","year":"2011","unstructured":"Katoen, J., 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."},{"issue":"5","key":"12_CR21","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1287\/opre.29.5.971","volume":"29","author":"C Lef\u00e9vre","year":"1981","unstructured":"Lef\u00e9vre, C.: Optimal control of a birth and death epidemic process. Oper. Res. 29(5), 971\u2013982 (1981)","journal-title":"Oper. Res."},{"key":"12_CR22","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"MA Marsan","year":"1994","unstructured":"Marsan, M.A., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley, New York (1994)"},{"key":"12_CR23","unstructured":"Meyer, J.F., Movaghar, A., Sanders, W.H.: Stochastic activity networks: Structure, behavior, and application. In: PNPM, pp. 106\u2013115 (1985)"},{"issue":"2","key":"12_CR24","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1137\/0306020","volume":"6","author":"BL Miller","year":"1968","unstructured":"Miller, B.L.: Finite state continuous time Markov decision processes with a finite planning horizon. SIAM J. Control 6(2), 266\u2013280 (1968)","journal-title":"SIAM J. Control"},{"key":"12_CR25","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University (2010)"},{"key":"12_CR26","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":"MR 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. 5504, pp. 364\u2013379. Springer, Heidelberg (2009)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: QEST, pp. 209\u2013218 (2010)","DOI":"10.1109\/QEST.2010.47"},{"issue":"10","key":"12_CR28","doi-asserted-by":"publisher","first-page":"1200","DOI":"10.1109\/43.952737","volume":"20","author":"Q Qiu","year":"2001","unstructured":"Qiu, Q., Qu, Q., Pedram, M.: Stochastic modeling of a power-managed system-construction andoptimization. IEEE Trans. CAD Integr. Circ. Syst. 20(10), 1200\u20131217 (2001)","journal-title":"IEEE Trans. CAD Integr. Circ. Syst."},{"issue":"5\u20136","key":"12_CR29","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s00236-011-0140-0","volume":"48","author":"MN Rabe","year":"2011","unstructured":"Rabe, M.N., Schewe, S.: Finite optimal control for time-bounded reachability in CTMDPs and continuous-time Markov games. Acta Inf. 48(5\u20136), 291\u2013315 (2011)","journal-title":"Acta Inf."},{"key":"12_CR30","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/j.tcs.2012.10.001","volume":"467","author":"MN Rabe","year":"2013","unstructured":"Rabe, M.N., Schewe, S.: Optimal time-abstract schedulers for CTMDPs and continuous-time Markov games. Theor. Comput. Sci. 467, 53\u201367 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-40229-6_17","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Timmer","year":"2013","unstructured":"Timmer, M., van de Pol, J., Stoelinga, M.I.A.: Confluence reduction for markov automata. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 243\u2013257. Springer, Heidelberg (2013)"},{"key":"12_CR32","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. 6015, pp. 53\u201368. Springer, Heidelberg (2010)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24953-7_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T23:03:10Z","timestamp":1748646190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24953-7_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319249520","9783319249537"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24953-7_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}