{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T23:37:15Z","timestamp":1762299435274,"version":"3.40.3"},"publisher-location":"Cham","reference-count":59,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030532901"},{"type":"electronic","value":"9783030532918"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:00:00Z","timestamp":1594684800000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53291-8_22","type":"book-chapter","created":{"date-parts":[[2020,7,15]],"date-time":"2020-07-15T20:03:35Z","timestamp":1594843415000},"page":"421-447","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Qualitative Controller Synthesis for Consumption Markov Decision Processes"],"prefix":"10.1007","author":[{"given":"Franti\u0161ek","family":"Blahoudek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Br\u00e1zdil","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Melkior","family":"Ornik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pranay","family":"Thangeda","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ufuk","family":"Topcu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,7,14]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Atig, M.F., Hofman, P., Mayr, R., Kumar, K.N., Totzke, P.: Infinite-state energy games. In: Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 7:1\u20137:10 (2014)","DOI":"10.1145\/2603088.2603100"},{"key":"22_CR2","volume-title":"Probability and Measure Theory","author":"R Ash","year":"2000","unstructured":"Ash, R., Dol\u00e9ans-Dade, C.: Probability and Measure Theory. Harcourt\/Academic Press, San Diego (2000)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-319-95582-7_12","volume-title":"Formal Methods","author":"G Bacci","year":"2018","unstructured":"Bacci, G., Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Reynier, P.-A.: Optimal and robust controller synthesis. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 203\u2013221. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-95582-7_12"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-319-90089-6_3","volume-title":"It\u2019s All About Coordination","author":"C Baier","year":"2018","unstructured":"Baier, C., Chrszon, P., Dubslaff, C., Klein, J., Kl\u00fcppelholz, S.: Energy-utility analysis of probabilistic systems with exogenous coordination. In: de Boer, F., Bonsangue, M., Rutten, J. (eds.) It\u2019s All About Coordination. LNCS, vol. 10865, pp. 38\u201356. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-90089-6_3"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1007\/978-3-319-06200-6_24","volume-title":"NASA Formal Methods","author":"C Baier","year":"2014","unstructured":"Baier, C., Daum, M., Dubslaff, C., Klein, J., Kl\u00fcppelholz, S.: Energy-utility quantiles. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 285\u2013299. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06200-6_24"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-319-06880-0_5","volume-title":"Horizons of the Mind. A Tribute to Prakash Panangaden","author":"C Baier","year":"2014","unstructured":"Baier, C., Dubslaff, C., Klein, J., Kl\u00fcppelholz, S., Wunderlich, S.: Probabilistic model checking for energy-utility analysis. In: van Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden. LNCS, vol. 8464, pp. 96\u2013123. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-06880-0_5"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-319-07734-5_2","volume-title":"Application and Theory of Petri Nets and Concurrency","author":"C Baier","year":"2014","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S., Leuschner, L.: Energy-utility analysis for resilient systems using probabilistic model checking. In: Ciardo, G., Kindler, E. (eds.) PETRI NETS 2014. LNCS, vol. 8489, pp. 20\u201339. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07734-5_2"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Balaram, B., et al.: Mars helicopter technology demonstrator. In: AIAA Atmospheric Flight Mechanics Conference (2018)","DOI":"10.2514\/6.2018-0023"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Boker, U., Henzinger, T.A., Radhakrishna, A.: Battery transition systems. In: 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 595\u2013606 (2014)","DOI":"10.1145\/2578855.2535875"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed automata with observers under energy constraints. In: 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 61\u201370. ACM (2010)","DOI":"10.1145\/1755952.1755963"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-85778-5_4","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"P Bouyer","year":"2008","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33\u201347. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85778-5_4"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-662-54458-7_11","volume-title":"Foundations of Software Science and Computation Structures","author":"P Bouyer","year":"2017","unstructured":"Bouyer, P., Hofman, P., Markey, N., Randour, M., Zimmermann, M.: Bounding average-energy games. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 179\u2013195. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54458-7_11"},{"issue":"2","key":"22_CR13","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s00236-016-0274-1","volume":"55","author":"P Bouyer","year":"2018","unstructured":"Bouyer, P., Markey, N., Randour, M., Larsen, K.G., Laursen, S.: Average-energy games. Acta Informatica 55(2), 91\u2013127 (2018)","journal-title":"Acta Informatica"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-31424-7_8","volume-title":"Computer Aided Verification","author":"T Br\u00e1zdil","year":"2012","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Ku\u010dera, A., Novotn\u00fd, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 23\u201338. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_8"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-642-14162-1_40","volume-title":"Automata, Languages and Programming","author":"T Br\u00e1zdil","year":"2010","unstructured":"Br\u00e1zdil, T., Jan\u010dar, P., Ku\u010dera, A.: Reachability games on extended vector addition systems with states. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 478\u2013489. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14162-1_40"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-319-08867-9_30","volume-title":"Computer Aided Verification","author":"T Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Kla\u0161ka, D., Ku\u010dera, A., Novotn\u00fd, P.: Minimizing running costs in consumption systems. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 457\u2013472. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_30"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-319-46520-3_3","volume-title":"Automated Technology for Verification and Analysis","author":"T Br\u00e1zdil","year":"2016","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Novotn\u00fd, P.: Optimizing the expected mean payoff in energy Markov decision processes. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 32\u201349. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_3"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Brenguier, R., Cassez, F., Raskin, J.-F.: Energy and mean-payoff timed games. In: 17th International Conference on Hybrid Systems: Computation and Control, pp. 283\u2013292 (2014)","DOI":"10.1145\/2562059.2562116"},{"issue":"1","key":"22_CR19","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s00236-016-0276-z","volume":"54","author":"T Brihaye","year":"2017","unstructured":"Brihaye, T., Geeraerts, G., Haddad, A., Monmege, B.: Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games. Acta Informatica 54(1), 85\u2013125 (2017)","journal-title":"Acta Informatica"},{"issue":"2","key":"22_CR20","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s10703-010-0105-x","volume":"38","author":"L Brim","year":"2011","unstructured":"Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.: Faster algorithms for mean-payoff games. Form. Methods Syst. Des. 38(2), 97\u2013118 (2011)","journal-title":"Form. Methods Syst. Des."},{"key":"22_CR21","unstructured":"Bruy\u00e8re, V., Hautem, Q., Randour, M., Raskin, J.-F.: Energy mean-payoff games. In: 30th International Conference on Concurrency Theory, pp. 21:1\u201321:17 (2019)"},{"key":"22_CR22","unstructured":"Cachera, D., Fahrenberg, U., Legay, A.: An $$\\omega $$-algebra for real-time energy problems. Log. Methods Comput. Sci. 15(2) (2019)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/978-3-540-45212-6_9","volume-title":"Embedded Software","author":"A Chakrabarti","year":"2003","unstructured":"Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117\u2013133. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45212-6_9"},{"issue":"1","key":"22_CR24","doi-asserted-by":"publisher","first-page":"15","DOI":"10.3233\/FI-2013-798","volume":"123","author":"J Chaloupka","year":"2013","unstructured":"Chaloupka, J.: Z-reachability problem for games on 2-dimensional vector addition systems with states is in P. Fundamenta Informaticae 123(1), 15\u201342 (2013)","journal-title":"Fundamenta Informaticae"},{"key":"22_CR25","unstructured":"Chatterjee, K.: Stochastic $$\\omega $$-regular games. Ph.D. thesis, University of California, Berkeley (2007)"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-642-22993-0_21","volume-title":"Mathematical Foundations of Computer Science 2011","author":"K Chatterjee","year":"2011","unstructured":"Chatterjee, K., Doyen, L.: Energy and mean-payoff parity Markov decision processes. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 206\u2013218. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22993-0_21"},{"key":"22_CR27","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/j.tcs.2012.07.038","volume":"458","author":"K Chatterjee","year":"2012","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. Theor. Comput. Sci. 458, 49\u201360 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR28","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T., Raskin, J.-F.: Generalized mean-payoff and energy games. In: 30th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 505\u2013516 (2010)"},{"key":"22_CR29","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M., Krinninger, S., Nanongkai, D.: Polynomial-time algorithms for energy games with special weight structures. In: 20th Annual European Symposium on Algorithms, pp. 301\u2013312 (2012)","DOI":"10.1007\/978-3-642-33090-2_27"},{"key":"22_CR30","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Jurdzi\u0144ski, M., Henzinger, T.: Quantitative stochastic parity games. In: 15th Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 121\u2013130 (2004)","DOI":"10.21236\/ADA603293"},{"issue":"3\u20134","key":"22_CR31","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/s00236-013-0182-6","volume":"51","author":"K Chatterjee","year":"2014","unstructured":"Chatterjee, K., Randour, M., Raskin, J.-F.: Strategy synthesis for multi-dimensional quantitative objectives. Acta informatica 51(3\u20134), 129\u2013163 (2014)","journal-title":"Acta informatica"},{"issue":"4","key":"22_CR32","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"22_CR33","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University (1998)"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-15205-4_22","volume-title":"Computer Science Logic","author":"A Degorre","year":"2010","unstructured":"Degorre, A., Doyen, L., Gentilini, R., Raskin, J.-F., Toru\u0144czyk, S.: Energy and mean-payoff games with imperfect information. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 260\u2013274. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15205-4_22"},{"issue":"1","key":"22_CR35","doi-asserted-by":"crossref","first-page":"203","DOI":"10.14232\/actacyb.23.1.2017.13","volume":"23","author":"Z \u00c9sik","year":"2017","unstructured":"\u00c9sik, Z., Fahrenberg, U., Legay, A., Quaas, K.: An algebraic approach to energy problems I - continuous Kleene $$ \\omega $$-algebras. Acta Cybernetica 23(1), 203\u2013228 (2017)","journal-title":"Acta Cybernetica"},{"issue":"1","key":"22_CR36","doi-asserted-by":"publisher","first-page":"229","DOI":"10.14232\/actacyb.23.1.2017.14","volume":"23","author":"Z \u00c9sik","year":"2017","unstructured":"\u00c9sik, Z., Fahrenberg, U., Legay, A., Quaas, K.: An algebraic approach to energy problems II - the algebra of energy functions. Acta Cybernetica 23(1), 229\u2013268 (2017)","journal-title":"Acta Cybernetica"},{"key":"22_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-23283-1_9","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2011","author":"U Fahrenberg","year":"2011","unstructured":"Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 95\u2013115. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23283-1_9"},{"key":"22_CR38","doi-asserted-by":"crossref","unstructured":"Fahrenberg, U., Legay, A.: Featured weighted automata. In: 5th International FME Workshop on Formal Methods in Software Engineering, pp. 51\u201357 (2017)","DOI":"10.1109\/FormaliSE.2017.2"},{"key":"22_CR39","unstructured":"Fijalkow, N., Zimmermann, M.: Cost-parity and cost-Streett games. In: 32nd Annual Conference on Foundations of Software Technology and Theoretical Computer Science, pp. 124\u2013135 (2012)"},{"key":"22_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-32940-1_11","volume-title":"CONCUR 2012 \u2013 Concurrency Theory","author":"E Filiot","year":"2012","unstructured":"Filiot, E., Gentilini, R., Raskin, J.-F.: Quantitative languages defined by functional automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 132\u2013146. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32940-1_11"},{"key":"22_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-030-45190-5_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"EM Hahn","year":"2020","unstructured":"Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Good-for-MDPs automata for probabilistic analysis and reinforcement learning. TACAS 2020. LNCS, vol. 12078, pp. 306\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_17"},{"key":"22_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-030-02227-3_6","volume-title":"Computer Performance Engineering","author":"L Herrmann","year":"2018","unstructured":"Herrmann, L., Baier, C., Fetzer, C., Kl\u00fcppelholz, S., Napierkowski, M.: Formal parameter synthesis for energy-utility-optimal fault tolerance. In: Bakhshi, R., Ballarini, P., Barbot, B., Castel-Taleb, H., Remke, A. (eds.) EPEW 2018. LNCS, vol. 11178, pp. 78\u201393. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02227-3_6"},{"key":"22_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-39698-4_15","volume-title":"Theories of Programming and Formal Methods","author":"L Juhl","year":"2013","unstructured":"Juhl, L., Guldstrand Larsen, K., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 244\u2013255. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39698-4_15"},{"key":"22_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-662-47666-6_21","volume-title":"Automata, Languages, and Programming","author":"M Jurdzi\u0144ski","year":"2015","unstructured":"Jurdzi\u0144ski, M., Lazi\u0107, R., Schmitz, S.: Fixed-dimensional energy games are in pseudo-polynomial time. In: Halld\u00f3rsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 260\u2013272. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_21"},{"issue":"3","key":"22_CR45","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0020-0190(98)00150-1","volume":"68","author":"M Jurdzi\u0144ski","year":"1998","unstructured":"Jurdzi\u0144ski, M.: Deciding the winner in parity games is in UP $$ \\cap $$ co-UP. Inf. Process. Lett. 68(3), 119\u2013124 (1998)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"22_CR46","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/s00224-007-9025-6","volume":"43","author":"L Khachiyan","year":"2008","unstructured":"Khachiyan, L., et al.: On short paths interdiction problems: total and node-wise limited interdiction. Theory Comput. Syst. 43(2), 204\u2013233 (2008)","journal-title":"Theory Comput. Syst."},{"key":"22_CR47","unstructured":"Kla\u0161ka, D.: Complexity of Consumption Games. Bachelor\u2019s thesis, Masaryk University (2014)"},{"key":"22_CR48","doi-asserted-by":"crossref","unstructured":"Larsen, K.G., Laursen, S., Zimmermann, M.: Limit your consumption! Finding bounds in average-energy games. In: 14th International Workshop Quantitative Aspects of Programming Languages and Systems, pp. 1\u201314 (2016)","DOI":"10.4204\/EPTCS.227.1"},{"key":"22_CR49","doi-asserted-by":"crossref","unstructured":"Mayr, R., Schewe, S., Totzke, P., Wojtczak, D.: MDPs with energy-parity objectives. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 1\u201312 (2017)","DOI":"10.1109\/LICS.2017.8005131"},{"key":"22_CR50","doi-asserted-by":"crossref","unstructured":"Jupyter, P., et al.: Binder 2.0 - reproducible, interactive, sharable environments for science at scale. In: 17th Python in Science Conference, pp. 113\u2013120 (2018)","DOI":"10.25080\/Majora-4af1f417-011"},{"key":"22_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-41540-6_17","volume-title":"Computer Aided Verification","author":"S Sickert","year":"2016","unstructured":"Sickert, S., Esparza, J., Jaax, S., K\u0159et\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312\u2013332. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17"},{"key":"22_CR52","unstructured":"Straubel, J.B.: Roadster efficiency and range (2008). https:\/\/www.tesla.com\/blog\/roadster-efficiency-and-range"},{"key":"22_CR53","doi-asserted-by":"crossref","unstructured":"Sugumar, G., Selvamuthukumaran, R., Dragicevic, T., Nyman, U., Larsen, K.G., Blaabjerg, F.: Formal validation of supervisory energy management systems for microgrids. In: 43rd Annual Conference of the IEEE Industrial Electronics Society, pp. 1154\u20131159 (2017)","DOI":"10.1109\/IECON.2017.8216197"},{"key":"22_CR54","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"2018","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT Press, Cambridge (2018)"},{"key":"22_CR55","unstructured":"Uber Movement: Traffic speed data for New York City (2019). https:\/\/movement.uber.com\/"},{"key":"22_CR56","unstructured":"United States Department of Energy. Alternative fuels data center (2019). https:\/\/afdc.energy.gov\/stations\/"},{"key":"22_CR57","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/j.ic.2015.03.001","volume":"241","author":"Y Velner","year":"2015","unstructured":"Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.: The complexity of multi-mean-payoff and multi-energy games. Inf. Comput. 241, 177\u2013196 (2015)","journal-title":"Inf. Comput."},{"key":"22_CR58","doi-asserted-by":"crossref","unstructured":"Wognsen, E.R., Hansen, R.R., Larsen, K.G., Koch, P.: Energy-aware scheduling of FIR filter structures using a timed automata model. In: 19th International Symposium on Design and Diagnostics of Electronic Circuits and Systems, pp. 1\u20136 (2016)","DOI":"10.1109\/DDECS.2016.7482468"},{"key":"22_CR59","doi-asserted-by":"crossref","unstructured":"Zhang, H., Sheppard, C.J.R., Lipman, T.E., Moura, S.J.: Joint fleet sizing and charging system planning for autonomous electric vehicles. IEEE Trans. Intell. Transp. Syst. (2019)","DOI":"10.1109\/TITS.2019.2946152"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53291-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,2]],"date-time":"2022-11-02T22:03:40Z","timestamp":1667426620000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-53291-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030532901","9783030532918"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53291-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"14 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","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":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair.org","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"240","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"18% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}