{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T04:01:16Z","timestamp":1749960076554,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100010007","name":"Sino-German Center for Research Promotion","doi-asserted-by":"crossref","award":["Project CAP (GZ 1023)"],"award-info":[{"award-number":["Project CAP (GZ 1023)"]}],"id":[{"id":"10.13039\/501100010007","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["EXC 1086"],"award-info":[{"award-number":["EXC 1086"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Costs and rewards are important tools for analysing quantitative aspects of models like energy consumption and costs of maintenance and repair. Under the assumption of transient costs, this paper considers the computation of expected cost-bounded rewards and cost-bounded reachability for Markov automata and Markov games. We provide a fixed point characterization of this class of properties under early schedulers. Additionally, we give a transformation to expected time-bounded rewards and time-bounded reachability, which can be computed by available algorithms. We prove the correctness of the transformation and show its effectiveness on a number of Markov automata case studies.<\/jats:p>","DOI":"10.1007\/s00165-016-0411-1","type":"journal-article","created":{"date-parts":[[2017,1,9]],"date-time":"2017-01-09T09:17:38Z","timestamp":1483953458000},"page":"629-649","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Cost vs. time in stochastic games and Markov automata"],"prefix":"10.1145","volume":"29","author":[{"given":"Hassan","family":"Hatefi","sequence":"first","affiliation":[{"name":"Chair for Dependable Systems and Software, Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4973-7479","authenticated-orcid":false,"given":"Ralf","family":"Wimmer","sequence":"additional","affiliation":[{"name":"Chair of Computer Architecture, Albert-Ludwigs-Universit\u00e4t Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bettina","family":"Braitling","sequence":"additional","affiliation":[{"name":"Chair of Computer Architecture, Albert-Ludwigs-Universit\u00e4t Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luis Mar\u00eda Ferrer","family":"Fioriti","sequence":"additional","affiliation":[{"name":"Chair for Dependable Systems and Software, Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[{"name":"Chair of Computer Architecture, Albert-Ludwigs-Universit\u00e4t Freiburg, Freiburg im Breisgau, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[{"name":"Chair for Dependable Systems and Software, Saarland University, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Ash RB Dol\u00e9ans-Dade CA (1999) Probability & measure theory 2nd edn. Academic Press New York"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Andova S Hermanns H Katoen JP (2003) Discrete-time rewards model-checked. In: Int\u2019l conf. on formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science. vol 2791. Springer Berlin pp 88\u2013104","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2009.45"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322242"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Braitling B Mar\u00eda Ferrer Fioriti L Hatefi H Wimmer R Becker B Hermanns H (2014) MeGARA: menu-based game abstraction refinement for Markov automata. In: Bertrand N Bertolussi L (eds) Int\u2019l workshop on quantitative aspects of programming languages and systems (QAPL). In: Electronic proceedings in theoretical computer science vol 154. Open Publishing Association Grenoble pp 48\u201363","DOI":"10.4204\/EPTCS.154.4"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Braitling B Mar\u00eda Ferrer FL Hatefi H Wimmer R Hermanns H Becker B (2015) Abstraction-based computation of reward measures for Markov automata. In: Int\u2019l conf. on verification model checking and abstract interpretation (VMCAI). Lecture Notes in Computer Science vol 8931. Springer Berlin pp 172\u2013189","DOI":"10.1007\/978-3-662-46081-8_10"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2013.01.001"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Baier C Haverkort BR Hermanns H Katoen JP (2000) On the logical characterisation of performability properties. In: Int\u2019l colloquium on automata languages and programming (ICALP). In: Lecture notes in computer science vol 1853. Springer Berlin pp 780\u2013792","DOI":"10.1007\/3-540-45022-X_65"},{"key":"e_1_2_1_2_9_2","unstructured":"Baier C Haverkort BR Hermanns H Katoen JP (2008) Reachability in continuous-time Markov reward decision processes. In: Logic and automata: history and perspectives. Honor of Wolfgang Thomas. Texts in logic and games vol 2. Amsterdam University Press Amsterdam pp 53\u201372"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Butkova Y Hatefi H Hermanns H Krc\u00e1l J (2015) Optimal continuous time Markov decisions. In: Finkbeiner B Pu G Zhang L (eds) Int\u2019l symp. on automated technology for verification and analysis (ATVA). Lecture notes in computer science vol 9364. Springer Shanghai pp 166\u2013182","DOI":"10.1007\/978-3-319-24953-7_12"},{"key":"e_1_2_1_2_11_2","unstructured":"Baier C Katoen J-P (2008) Principles of model checking. The MIT Press Massachusetts"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.cor.2010.08.011"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Cloth L Katoen J-P Khattri M Pulungan R (2005) Model checking Markov reward models with impulse rewards. In: Int\u2019l conf. on dependable systems and networks (DSN). IEEE Computer Society New York pp 722\u2013731","DOI":"10.1109\/DSN.2005.64"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Eisentraut C Hermanns H Katoen J-P Zhang L (2013) A semantics for every GSPN. In: Proc. of petri nets. Lecture notes in computer science vol 7927. Springer Berlin pp 90\u2013109","DOI":"10.1007\/978-3-642-38697-8_6"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Eisentraut C Hermanns H Zhang L (2010) On probabilistic automata in continuous time. In: Annual IEEE symp. on logic in computer science (LICS). IEEE Computer Society New York pp 342\u2013351","DOI":"10.1109\/LICS.2010.41"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Fu H (2014) Maximal cost-bounded reachability probability on continuous-time Markov decision processes. In: Int\u2019l conf. on foundations of software science and computation structures (FoSSaCS). Lecture notes in computer science vol 8412. Springer Berlin pp 73\u201387","DOI":"10.1007\/978-3-642-54830-7_5"},{"key":"e_1_2_1_2_17_2","unstructured":"Fu H (2014) Verifying probabilistic systems: new algorithms and complexity results. PhD thesis RWTH Aachen University"},{"key":"e_1_2_1_2_18_2","unstructured":"Gburek D Baier C Kl\u00fcppelholz S (2016) Composition of stochastic transition systems based on spans and couplings. In: 43rd international colloquium on automata languages and programming ICALP 2016 July 11\u201315 2016 Rome Italy pp 102:1\u2013102:15"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Guck D Hatefi H Hermanns H Katoen J.-P. Timmer M (2013) Modelling reduction and analysis of Markov automata. In: Int\u2019l conf. on quantitative evaluation of systems (QEST). Lecture notes in computer science vol 8054. Springer Berlin pp 55\u201371","DOI":"10.1007\/978-3-642-40196-1_5"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Guck D Hatefi H Hermanns H Katoen JP Timmer M (2014) Analysis of timed and long-run objectives for Markov automata. Logical Methods Comput Sci 10(3)","DOI":"10.2168\/LMCS-10(3:17)2014"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Guck D Han T Katoen JP Neuh\u00e4u\u00dfer MR (2012) Quantitative timed analysis of interactive Markov chains. In: NASA formal methods symposium (NFM). Lecture notes in computer science vol 7226. Springer Berlin pp 8\u201323","DOI":"10.1007\/978-3-642-28891-3_4"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Guck D Timmer M Hatefi H Ruijters E Stoelinga M (2014) Modelling and analysis of Markov reward automata. In: Int\u2019l symp. on automated technology for verification and analysis (ATVA). Lecture notes in computer science vol 8837. Springer Berlin pp 168\u2013184","DOI":"10.1007\/978-3-319-11936-6_13"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Hatefi H Braitling B Wimmer R Mar\u00eda Ferrer Fioriti L Hermanns H Becker B (2015) Cost vs. time in stochastic games and Markov automata. In: Li X Liu Z Yi W (eds) int\u2019l symp. on dependable software engineering: theory tools and applications (SETTA). Lecture notes in computer science vol 9409. Springer Nanjing pp 19\u201334","DOI":"10.1007\/978-3-319-25942-0_2"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Hermanns H (2002) Interactive Markov chains: the quest for quantified quality. In: Lecture notes in computer science vol 2428. Springer Berlin","DOI":"10.1007\/3-540-45804-2"},{"key":"e_1_2_1_2_25_2","unstructured":"Hatefi H Hermanns H (2012) Model checking algorithms for Markov automata. ECEASST 53"},{"key":"e_1_2_1_2_26_2","unstructured":"Johr S (2008) Model checking compositional Markov systems. PhD thesis Saarland University Saarbr\u00fccken"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1137\/0306020"},{"key":"e_1_2_1_2_28_2","unstructured":"Neuh\u00e4u\u00dfer MR (2010) Model checking nondeterministic and randomly timed systems. PhD thesis RWTH Aachen University and University of Twente"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-010-0189-2","volume-title":"Stochastic games and applications","author":"Neyman A","year":"2003"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Neuh\u00e4u\u00dfer MR Zhang L (2010) Time-bounded reachability probabilities in continuous-time Markov decision processes. In: Int\u2019l conf. on quantitative evaluation of systems (QEST). IEEE Computer Society New York pp 209\u2013218","DOI":"10.1109\/QEST.2010.47"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/43.952737"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Simunic T Benini L Glynn P.W De Micheli G (2000) Dynamic power management for portable systems. In: Annual int\u2019l conf. on mobile computing and networking (MOBICOM) Boston MA USA August pp 11\u201319","DOI":"10.1145\/345910.345914"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Segala R (1995) A compositional trace-based semantics for probabilistic automata. In: Int\u2019l conf. on concurrency theory (CONCUR). Lecture notes in computer science vol 962. Springer Berlin pp 234\u2013248","DOI":"10.1007\/3-540-60218-6_17"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Shapley LS (1953) Stochastic games. Proc Natl Acad Sci USA 39(10):1095","DOI":"10.1073\/pnas.39.10.1953"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Timmer M Katoen J-P van de Pol J Stoelinga M (2012) Efficient modelling and generation of Markov automata. In: Int\u2019l conf. on concurrency theory (CONCUR). Lecture notes in computer science vol 7454. Springer Berlin pp 364\u2013379","DOI":"10.1007\/978-3-642-32940-1_26"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Timmer M van de Pol J Stoelinga M (2013) Confluence reduction for Markov automata. In: Int\u2019l conf. on formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science vol 8053. Springer Berlin pp 243\u2013257","DOI":"10.1007\/978-3-642-40229-6_17"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Wolovick N Johr S (2006) A characterization of meaningful schedulers for continuous-time Markov decision processes. In: Asarin E Bouyer P (eds) Int\u2019l conf. on formal modeling and analysis of timed systems (FORMATS). Lecture notes in computer science vol 4202. Springer Paris pp 352\u2013367","DOI":"10.1007\/11867340_25"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0411-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0411-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0411-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0411-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T03:45:55Z","timestamp":1749872755000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0411-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7]]},"references-count":38,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["10.1007\/s00165-016-0411-1"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0411-1","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,7]]}}}