{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:25:47Z","timestamp":1745994347116,"version":"3.37.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030010898"},{"type":"electronic","value":"9783030010904"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-030-01090-4_19","type":"book-chapter","created":{"date-parts":[[2018,9,29]],"date-time":"2018-09-29T11:23:23Z","timestamp":1538220203000},"page":"317-334","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Continuous-Time Markov Decisions Based on Partial Exploration"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1083-4741","authenticated-orcid":false,"given":"Pranav","family":"Ashok","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9678-1467","authenticated-orcid":false,"given":"Yuliya","family":"Butkova","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2766-9615","authenticated-orcid":false,"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8122-2881","authenticated-orcid":false,"given":"Jan","family":"K\u0159et\u00ednsk\u00fd","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,9,30]]},"reference":[{"key":"19_CR1","unstructured":"Ashok, P., Butkova, Y., Hermanns, H., K\u0159et\u00ednsk\u00fd, J.: Continuous-Time Markov Decisions Based on Partial Exploration. ArXiv e-prints (2018). https:\/\/arxiv.org\/abs\/1807.09641"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"Ashok, P., Chatterjee, K., Daca, P., Kret\u00ednsk\u00fd, J., Meggendorfer, T.: Value iteration for long-run average reward in Markov decision processes. In: CAV (2017)","DOI":"10.1007\/978-3-319-63387-9_10"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time Markov chains. In: CAV (1996)","DOI":"10.1007\/3-540-61474-5_75"},{"key":"19_CR4","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1016\/j.peva.2017.08.007","volume":"116","author":"E Bartocci","year":"2017","unstructured":"Bartocci, E., Bortolussi, L., Br\u00e1zdil, T., Milios, D., Sanguinetti, G.: Policy learning in continuous-time Markov decision processes using gaussian processes. Perform. Eval. 116, 84\u2013100 (2017)","journal-title":"Perform. Eval."},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., et al.: Verification of Markov decision processes using learning algorithms. In: ATVA (2014)","DOI":"10.1007\/978-3-319-11936-6_8"},{"issue":"1","key":"19_CR6","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":"19_CR7","unstructured":"Bertsekas, D.P.: Dynamic Programming and Optimal Control, vol. II. Athena Scientific (1995)"},{"key":"19_CR8","unstructured":"Br\u00e1zdil, T., Forejt, V., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., Ku\u010dera, A.: Continuous-time stochastic games with time-bounded reachability. In: FSTTCS (2009)"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Efficient computation of time-bounded reachability probabilities in uniform continuous-time Markov decision processes. In: TACAS (2004)","DOI":"10.1007\/978-3-540-24730-2_5"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Butkova, Y., Hatefi, H., Hermanns, H., Krc\u00e1l, J.: Optimal continuous time Markov decisions. In: ATVA (2015)","DOI":"10.1007\/978-3-319-24953-7_12"},{"issue":"3","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. Comput. OR 38(3), 651\u2013659 (2011)","journal-title":"Comput. OR"},{"key":"19_CR12","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, C., Hermanns, H., Katoen, J., Zhang, L.: A semantics for every GSPN. In: Petri Nets (2013)"},{"issue":"3","key":"19_CR13","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1287\/moor.1040.0089","volume":"29","author":"EA Feinberg","year":"2004","unstructured":"Feinberg, E.A.: Continuous time discounted jump Markov decision processes: a discrete-event approach. Math. Oper. Res. 29(3), 492\u2013524 (2004)","journal-title":"Math. Oper. Res."},{"key":"19_CR14","unstructured":"Fearnley, J., Rabe, M., Schewe, S., Zhang, L.: Efficient approximation of optimal control for continuous-time Markov games. In: FSTTCS (2011)"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Ghemawat, S., Gobioff, H., Leung, S.: The google file system. In: SOSP (2003)","DOI":"10.1145\/945449.945450"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Modelling, reduction and analysis of Markov automata. In: QEST (2013)","DOI":"10.1007\/978-3-642-40196-1_5"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Guck, D., Han, T., Katoen, J., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive Markov chains. In: NFM (2012)","DOI":"10.1007\/978-3-642-28891-3_4"},{"key":"19_CR18","unstructured":"Haverkort, B.R., Cloth, L., Hermanns, H., Katoen, J., Baier, C.: Model checking performability properties. In: DSN (2002)"},{"key":"19_CR19","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-642-40213-5_16","volume-title":"Fundamentals of Software Engineering","author":"Hassan Hatefi","year":"2013","unstructured":"Hatefi, H., Hermanns, H.: Improving time bounded reachability computations in interactive Markov chains. In: FSEN (2013)"},{"key":"19_CR20","unstructured":"Haverkort, B.R., Hermanns, H., Katoen, J.: On the use of model checking techniques for dependability evaluation. In: SRDS\u201900 (2000)"},{"key":"19_CR21","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"issue":"5","key":"19_CR22","doi-asserted-by":"publisher","first-page":"971","DOI":"10.1287\/opre.29.5.971","volume":"29","author":"C Lef\u00e8vre","year":"1981","unstructured":"Lef\u00e8vre, C.: Optimal control of a birth and death epidemic process. Oper. Res. 29(5), 971\u2013982 (1981)","journal-title":"Oper. Res."},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"McMahan, H.B., Likhachev, M., Gordon, G.J.: Bounded real-time dynamic programming: RTDP with monotone upper bounds and performance guarantees. In: ICML (2005)","DOI":"10.1145\/1102351.1102423"},{"key":"19_CR24","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University (2010)"},{"key":"19_CR25","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_CR26","doi-asserted-by":"crossref","unstructured":"Pavese, E., Braberman, V.A., Uchitel, S.: Automated reliability estimation over partial systematic explorations. In: ICSE, pp. 602\u2013611 (2013)","DOI":"10.1109\/ICSE.2013.6606606"},{"issue":"10","key":"19_CR27","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 and optimization. IEEE Trans. CAD Integr. Circuits Syst. 20(10), 1200\u20131217 (2001)","journal-title":"IEEE Trans. CAD Integr. Circuits Syst."},{"key":"19_CR28","volume-title":"Stochastic Dynamic Programming and the Control of Queueing Systems","author":"LI Sennott","year":"1999","unstructured":"Sennott, L.I.: Stochastic Dynamic Programming and the Control of Queueing Systems. Wiley-Interscience, New York (1999)"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Timmer, M.: Scoop: a tool for symbolic optimisations of probabilistic processes. In: QEST (2011)","DOI":"10.1109\/QEST.2011.27"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-642-32940-1_26","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"M Timmer","year":"2012","unstructured":"Timmer, M., Katoen, J.-P., van de Pol, J., Stoelinga, M.I.A.: Efficient modelling and generation of Markov automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 364\u2013379. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_26"},{"key":"19_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). https:\/\/doi.org\/10.1007\/978-3-642-40229-6_17"},{"key":"19_CR32","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":"Lijun 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). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_5"}],"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-030-01090-4_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,24]],"date-time":"2019-10-24T23:33:28Z","timestamp":1571960008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-01090-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030010898","9783030010904"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-01090-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Los Angeles, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/atva-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}