{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T04:12:35Z","timestamp":1748664755042,"version":"3.41.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319259413"},{"type":"electronic","value":"9783319259420"}],"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-25942-0_2","type":"book-chapter","created":{"date-parts":[[2015,10,16]],"date-time":"2015-10-16T09:32:14Z","timestamp":1444987934000},"page":"19-34","source":"Crossref","is-referenced-by-count":4,"title":["Cost vs. Time in Stochastic Games and Markov Automata"],"prefix":"10.1007","author":[{"given":"Hassan","family":"Hatefi","sequence":"first","affiliation":[]},{"given":"Bettina","family":"Braitling","sequence":"additional","affiliation":[]},{"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[]},{"given":"Luis Mar\u00eda Ferrer","family":"Fioriti","sequence":"additional","affiliation":[]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,10,17]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-40903-8_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"S Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88\u2013104. Springer, Heidelberg (2004)"},{"key":"2_CR2","unstructured":"Ash, R.B., Dol\u00e9ans-Dade, C.A.: Probability & Measure Theory. Academic Press, 2nd edn. (1999)"},{"key":"2_CR3","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. 1853, p. 780. Springer, Heidelberg (2000)"},{"key":"2_CR4","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.: Reachability in continuous-time Markov reward decision processes. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Texts in Logic and Games, vol. 2, pp. 53\u201372. Amsterdam University Press (2008)"},{"key":"2_CR5","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)"},{"issue":"2","key":"2_CR6","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1109\/TDSC.2009.45","volume":"7","author":"H Boudali","year":"2010","unstructured":"Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Dependable Sec. Comput. 7(2), 128\u2013143 (2010)","journal-title":"IEEE Trans. Dependable Sec. Comput."},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-662-46081-8_10","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Braitling","year":"2015","unstructured":"Braitling, B., Ferrer Fioriti, L.M., Hatefi, H., Wimmer, R., Becker, B., Hermanns, H.: Abstraction-based computation of reward measures for markov automata. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 172\u2013189. Springer, Heidelberg (2015)"},{"key":"2_CR8","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. Information and Computation 224, 46\u201370 (2013)","journal-title":"Information and Computation"},{"issue":"1","key":"2_CR9","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. Journal of the ACM 28(1), 100\u2013113 (1981)","journal-title":"Journal of the ACM"},{"issue":"3","key":"2_CR10","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 38(3), 651\u2013659 (2011)","journal-title":"Computers & Operations Research"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Cloth, L., Katoen, J., Khattri, M., Pulungan, R.: Model checking Markov reward models with impulse rewards. In: Proceedings of DSN, pp. 722\u2013731. IEEE CS (2005)","DOI":"10.1109\/DSN.2005.64"},{"key":"2_CR12","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":"C Eisentraut","year":"2013","unstructured":"Eisentraut, C., Hermanns, H., Katoen, J.-P., Zhang, L.: A semantics for every GSPN. In: Colom, J.-M., Desel, J. (eds.) PETRI NETS 2013. LNCS, vol. 7927, pp. 90\u2013109. Springer, Heidelberg (2013)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: Proceedings of LICS, pp. 342\u2013351. IEEE CS (2010)","DOI":"10.1109\/LICS.2010.41"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-642-54830-7_5","volume-title":"Foundations of Software Science and Computation Structures","author":"H Fu","year":"2014","unstructured":"Fu, H.: Maximal cost-bounded reachability probability on continuous-time markov decision processes. In: Muscholl, A. (ed.) FOSSACS 2014 (ETAPS). LNCS, vol. 8412, pp. 73\u201387. Springer, Heidelberg (2014)"},{"key":"2_CR15","unstructured":"Fu, H.: Verifying Probabilistic Systems: New Algorithms and Complexity Results. Ph.D. thesis, RWTH Aachen University (2014)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-642-28891-3_4","volume-title":"NASA Formal Methods","author":"D Guck","year":"2012","unstructured":"Guck, D., Han, T., Katoen, J.-P., Neuh\u00e4u\u00dfer, M.R.: Quantitative timed analysis of interactive markov chains. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 8\u201323. Springer, Heidelberg (2012)"},{"key":"2_CR17","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":"2_CR18","doi-asserted-by":"crossref","unstructured":"Guck, D., Hatefi, H., Hermanns, H., Katoen, J., Timmer, M.: Analysis of timed and long-run objectives for Markov automata. Logical Methods in Computer Science 10(3) (2014). http:\/\/dx.doi.org\/10.2168\/LMCS-10(3:17)2014","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-319-11936-6_13","volume-title":"Automated Technology for Verification and Analysis","author":"D Guck","year":"2014","unstructured":"Guck, D., Timmer, M., Hatefi, H., Ruijters, E., Stoelinga, M.: Modelling and analysis of markov reward automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 168\u2013184. Springer, Heidelberg (2014)"},{"key":"2_CR20","unstructured":"Hatefi, H., Braitling, B., Wimmer, R., Ferrer Fioriti, L.M., Hermanns, H., Becker, B.: Cost vs. time in stochastic games and Markov automata (extended version). Reports of SFB\/TR 14 AVACS 113, SFB\/TR 14 AVACS (2015). http:\/\/www.avacs.org"},{"key":"2_CR21","unstructured":"Hatefi, H., Hermanns, H.: Model checking algorithms for Markov automata. ECEASST 53 (2012)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","year":"2002","unstructured":"Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol. 2428. Springer, Heidelberg (2002)"},{"key":"2_CR23","unstructured":"Johr, S.: Model checking compositional Markov systems. Ph.D. thesis, Saarland University, Germany (2008)"},{"issue":"2","key":"2_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 Journal on Control 6(2), 266\u2013280 (1968)","journal-title":"SIAM Journal on Control"},{"key":"2_CR25","unstructured":"Neuh\u00e4u\u00dfer, M.R.: Model checking nondeterministic and randomly timed systems. Ph.D. thesis, RWTH Aachen University and University of Twente (2010)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer, M.R., Zhang, L.: Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Proceedings of QEST, pp. 209\u2013218. IEEE CS (2010)","DOI":"10.1109\/QEST.2010.47"},{"issue":"10","key":"2_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 Transactions on CAD of Integrated Circuits and Systems 20(10), 1200\u20131217 (2001)","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/3-540-60218-6_17","volume-title":"CONCUR \u201995 Concurrency Theory","author":"R Segala","year":"1995","unstructured":"Segala, R.: A compositional trace-based semantics for probabilistic automata. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 234\u2013248. Springer, Heidelberg (1995)"},{"issue":"10","key":"2_CR29","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"LS Shapley","year":"1953","unstructured":"Shapley, L.S.: Stochastic games. Proc. of the National Academy of Sciences of the United States of America 39(10), 1095 (1953)","journal-title":"Proc. of the National Academy of Sciences of the United States of America"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Simunic, T., Benini, L., Glynn, P.W., Micheli, G.D.: Dynamic power management for portable systems. In: Proc. of MOBICOM, pp. 11\u201319 (2000)","DOI":"10.1145\/345910.345914"},{"key":"2_CR31","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)"},{"key":"2_CR32","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)"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering: Theories, Tools, and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25942-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T01:49:57Z","timestamp":1748656197000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25942-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319259413","9783319259420"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25942-0_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}