{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,8]],"date-time":"2026-04-08T21:37:03Z","timestamp":1775684223209,"version":"3.50.1"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319119359","type":"print"},{"value":"9783319119366","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_10","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T15:12:03Z","timestamp":1414163523000},"page":"129-145","source":"Crossref","is-referenced-by-count":49,"title":["On Time with Minimal Expected Cost!"],"prefix":"10.1007","author":[{"given":"Alexandre","family":"David","sequence":"first","affiliation":[]},{"given":"Peter G.","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]},{"given":"Didier","family":"Lime","sequence":"additional","affiliation":[]},{"given":"Mathias Grund","family":"S\u00f8rensen","sequence":"additional","affiliation":[]},{"given":"Jakob H.","family":"Taankvist","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Abdedda\u00efm, Y., Kerbaa, A., Maler, O.: Task graph scheduling using timed automata. In: IPDPS, p. 237. IEEE Computer Society (2003)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/3-540-44585-4_46","volume-title":"Computer Aided Verification","author":"Y. Abdedda\u00efm","year":"2001","unstructured":"Abdedda\u00efm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 478\u2013492. Springer, Heidelberg (2001)"},{"issue":"2","key":"10_CR3","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. Theor. Comput. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 121\u2013125. Springer, Heidelberg (2007)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1007\/3-540-45351-2_15","volume-title":"Hybrid Systems: Computation and Control","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.W.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, pp. 147\u2013161. Springer, Heidelberg (2001)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-02017-9_16","volume-title":"Theory and Applications of Models of Computation","author":"J. Berendsen","year":"2009","unstructured":"Berendsen, J., Chen, T., Jansen, D.N.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol.\u00a05532, pp. 128\u2013137. Springer, Heidelberg (2009)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Berendsen, J., Jansen, D.N., Vaandrager, F.W.: Fortuna: Model checking priced probabilistic timed automata. In: QEST, pp. 273\u2013281. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.41"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-33365-1_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"N. Bertrand","year":"2012","unstructured":"Bertrand, N., Schewe, S.: Playing optimally on timed automata with random delays. In: Jurdzi\u0144ski, M., Ni\u010dkovi\u0107, D. (eds.) FORMATS 2012. LNCS, vol.\u00a07595, pp. 43\u201358. Springer, Heidelberg (2012)"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-28540-0_20","volume-title":"Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance","author":"J. Bogdoll","year":"2012","unstructured":"Bogdoll, J., Hartmanns, A., Hermanns, H.: Simulation and statistical model checking for modestly nondeterministic models. In: Schmitt, J.B. (ed.) MMB & DFT 2012. LNCS, vol.\u00a07201, pp. 249\u2013252. Springer, Heidelberg (2012)"},{"issue":"1","key":"10_CR10","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1016\/j.entcs.2004.07.006","volume":"119","author":"P. Bouyer","year":"2005","unstructured":"Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Synthesis of optimal strategies using hytech. Electr. Notes Theor. Comput. Sci.\u00a0119(1), 11\u201331 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"345","DOI":"10.1007\/11944836_32","volume-title":"FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science","author":"P. Bouyer","year":"2006","unstructured":"Bouyer, P., Larsen, K.G., Markey, N., Rasmussen, J.I.: Almost optimal strategies in one clock priced timed games. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol.\u00a04337, pp. 345\u2013356. Springer, Heidelberg (2006)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Krc\u00e1l, J., Kret\u00ednsk\u00fd, J., Kucera, A., Reh\u00e1k, V.: Measuring performance of continuous-time stochastic processes using timed automata. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) HSCC, pp. 33\u201342. ACM (2011)","DOI":"10.1145\/1967701.1967709"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/11603009_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T. Brihaye","year":"2005","unstructured":"Brihaye, T., Bruy\u00e8re, V., Raskin, J.F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol.\u00a03829, pp. 49\u201364. Springer, Heidelberg (2005)"},{"key":"10_CR14","unstructured":"Bruy\u00e8re, V., Filiot, E., Randour, M., Raskin, J.F.: Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In: Mayr, E.W., Portier, N. (eds.) STACS. LIPIcs, vol.\u00a025, pp. 199\u2013213. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2014)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"David, A., Du, D., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. In: Bartocci, E., Bortolussi, L. (eds.) HSB. EPTCS, vol.\u00a092, pp. 122\u2013136 (2012)","DOI":"10.4204\/EPTCS.92.9"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-642-22110-1_27","volume-title":"Computer Aided Verification","author":"A. David","year":"2011","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Wang, Z.: Time for statistical model checking of real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 349\u2013355. Springer, Heidelberg (2011)"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"10_CR18","first-page":"1871","volume":"9","author":"R.E. Fan","year":"2008","unstructured":"Fan, R.E., Chang, K.W., Hsieh, C.J., Wang, X.R., Lin, C.J.: LIBLINEAR: A library for large linear classification. Journal of Machine Learning Research\u00a09, 1871\u20131874 (2008)","journal-title":"Journal of Machine Learning Research"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Fu, H.: Maximal cost-bounded reachability probability on continuous-time markov decision processes. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol.\u00a08412, pp. 73\u201387. Springer, Heidelberg (2014)","DOI":"10.1007\/978-3-642-54830-7_5"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Henriques, D., Martins, J., Zuliani, P., Platzer, A., Clarke, E.: Statistical model checking for markov decision processes. In: 2012 Ninth International Conference on Quantitative Evaluation of Systems (QEST), pp. 84\u201393 (2012)","DOI":"10.1109\/QEST.2012.19"},{"key":"10_CR21","first-page":"247","volume":"7","author":"H.E. Jensen","year":"1996","unstructured":"Jensen, H.E., Gregersen, H.: Model checking probabilistic real time systems. Nordic Workshop on Programming Theory\u00a07, 247\u2013261 (1996)","journal-title":"Nordic Workshop on Programming Theory"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Kempf, J.F., Bozga, M., Maler, O.: As soon as probable: Optimal scheduling under stochastic uncertainty. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 385\u2013400. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_27"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-46002-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.Z. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Probabilistic symbolic model checking with prism: A hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 52\u201366. Springer, Heidelberg (2002)"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-44618-4_11","volume-title":"CONCUR 2000 - Concurrency Theory","author":"M.Z. Kwiatkowska","year":"2000","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 123\u2013137. Springer, Heidelberg (2000)"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large markov decision processes. In: Ossowski, S., Lecca, P. (eds.) SAC, pp. 1314\u20131319. ACM (2012)","DOI":"10.1145\/2245276.2231984"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A. Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 122\u2013135. Springer, Heidelberg (2010)"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/3-540-59042-0_76","volume-title":"STACS 95","author":"O. Maler","year":"1995","unstructured":"Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems (an extended abstract). In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol.\u00a0900, pp. 229\u2013242. Springer, Heidelberg (1995)"},{"key":"10_CR28","unstructured":"Poulsen, D.B., van Vliet, J.: Duration probabilistic automata, http:\/\/www.cs.aau.dk\/~adavid\/smc\/DurationProbabilisticAutomata.pdf"},{"key":"10_CR29","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1145\/2020408.2020421","volume-title":"Proceedings of the 17th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD 2011","author":"G.X. Yuan","year":"2011","unstructured":"Yuan, G.X., Ho, C.H., Lin, C.J.: An improved glmnet for l1-regularized logistic regression. In: Proceedings of the 17th ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, KDD 2011, pp. 33\u201341. ACM, New York (2011), http:\/\/doi.acm.org\/10.1145\/2020408.2020421"}],"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-11936-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,20]],"date-time":"2022-04-20T12:30:37Z","timestamp":1650457837000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}