{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:41:04Z","timestamp":1764402064803,"version":"3.46.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031906527"},{"type":"electronic","value":"9783031906534"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T00:00:00Z","timestamp":1746057600000},"content-version":"vor","delay-in-days":120,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We study algorithms for solving parity, mean-payoff and energy games. We propose a systematic framework, which we call Fast value iteration, for describing, comparing, and proving correctness of such algorithms. The approach is based on potential reductions, as introduced by Gurvich, Karzanov and Khachiyan (1988). This framework allows us to provide simple presentations and correctness proofs of known algorithms, unifying the Optimal strategy improvement algorithm by Schewe (2008) and the quasi dominions approach by Benerecetti et al. (2020), amongst others. The new approach also leads to novel symmetric versions of these algorithms, highly efficient in practice, but for which we are unable to prove termination. We report on empirical evaluation, comparing the different fast value iteration algorithms, and showing that they are competitive even to top parity game solvers.<\/jats:p>","DOI":"10.1007\/978-3-031-90653-4_16","type":"book-chapter","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T07:21:52Z","timestamp":1746170512000},"page":"323-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fast value iteration: A uniform approach to efficient algorithms for energy games"],"prefix":"10.1007","author":[{"given":"Micha\u00ebl","family":"Cadilhac","sequence":"first","affiliation":[]},{"given":"Antonio","family":"Casares","sequence":"additional","affiliation":[]},{"given":"Pierre","family":"Ohlmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,5,1]]},"reference":[{"key":"16_CR1","unstructured":"Beffara, E., Vorobyov, S.: Is randomized Gurvich-Karzanov-Khachiyan\u2019s algorithm for parity games polynomial? In: Technical report 2001-025. Uppsala University, Sweden (2001)"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Benerecetti, M., Dell\u2019Erba, D., Mogavero, F.: Solving mean-payoff games via quasi dominions. Inf. Comput. 297, 105151 (2024). https:\/\/doi.org\/10.1016\/J.IC.2024.105151","DOI":"10.1016\/J.IC.2024.105151"},{"key":"16_CR3","doi-asserted-by":"publisher","unstructured":"Bj\u00f6rklund, H., Sandberg, S., Vorobyov, S.G.: A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. In: MFCS. Lecture Notes in Computer Science, vol.\u00a03153, pp. 673\u2013685. Springer (2004). https:\/\/doi.org\/10.1007\/978-3-540-28629-5_52","DOI":"10.1007\/978-3-540-28629-5_52"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Bj\u00f6rklund, H., Vorobyov, S.G.: Combinatorial structure and randomized subexponential algorithms for infinite games. Theor. Comput. Sci. 349(3), 347\u2013360 (2005)","DOI":"10.1016\/j.tcs.2005.07.041"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: FORMATS. Lecture Notes in Computer Science, vol.\u00a05215, pp. 33\u201347. Springer (2008)","DOI":"10.1007\/978-3-540-85778-5_4"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.: Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2), 97\u2013118 (2011)","DOI":"10.1007\/s10703-010-0105-x"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Calude, C.S., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: STOC. pp. 252\u2013263 (2017)","DOI":"10.1145\/3055399.3055409"},{"key":"16_CR8","doi-asserted-by":"publisher","unstructured":"van Dijk, T.: Attracting tangles to solve parity games. In: CAV. Lecture Notes in Computer Science, vol. 10982, pp. 198\u2013215. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_14","DOI":"10.1007\/978-3-319-96142-2_14"},{"key":"16_CR9","doi-asserted-by":"publisher","unstructured":"van Dijk, T.: Oink: An implementation and evaluation of modern parity game solvers. In: TACAS. Lecture Notes in Computer Science, vol. 10805, pp. 291\u2013308. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"van Dijk, T.: A parity game tale of two counters. In: GandALF. EPTCS, vol.\u00a0305, pp. 107\u2013122 (2019). https:\/\/doi.org\/10.4204\/EPTCS.305.8","DOI":"10.4204\/EPTCS.305.8"},{"key":"16_CR11","unstructured":"Dorfman, D., Kaplan, H., Zwick, U.: A faster deterministic exponential time algorithm for energy games and mean payoff games. In: ICALP. pp. 114:1\u2013114:14 (2019)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. International Journal of Game Theory 109(8), 109\u2013113 (1979)","DOI":"10.1007\/BF01768705"},{"key":"16_CR13","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, $$\\mu $$-calculus and determinacy. In: FOCS. pp. 368\u2013377. IEEE Computer Society (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"16_CR14","doi-asserted-by":"publisher","unstructured":"Fearnley, J.: Non-oblivious strategy improvement. In: LPAR. Lecture Notes in Computer Science, vol.\u00a06355, pp. 212\u2013230. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_13","DOI":"10.1007\/978-3-642-17511-4_13"},{"key":"16_CR15","unstructured":"Fijalkow, N., Gawrychowski, P., Ohlmann, P.: Value iteration using universal graphs and the complexity of mean payoff games. In: MFCS. LIPIcs, vol.\u00a0170, pp. 34:1\u201334:15. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"16_CR16","unstructured":"Friedmann, O.: Exponential Lower Bounds for Solving Infinitary Payoff Games and Linear Programs. Ph.D. thesis, Ludwig Maximilians University Munich (2011), http:\/\/edoc.ub.uni-muenchen.de\/13294\/"},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Gallai, T.: Maximum-minimum s\u00e4tze \u00fcber graphen. Acta Math. Acad. Sci. Hung. (9), 395-434 (1958)","DOI":"10.1007\/BF02020271"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Gurvich, V.A., Karzanov, A.V., Khachiyan, L.G.: Cyclic games and an algorithm to find minimax cycle means in directed graphs. USSR Computational Mathematics and Mathematical Physics 28, 85\u201391 (1988)","DOI":"10.1016\/0041-5553(88)90012-2"},{"key":"16_CR19","unstructured":"Jacobs, S., Perez, G.A., Abraham, R., Bruyere, V., Cadilhac, M., Colange, M., Delfosse, C., van Dijk, T., Duret-Lutz, A., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, K., Michaud, T., Pommellet, A., Renkin, F., Schlehuber-Caissier, P., Sakr, M., Sickert, S., Staquet, G., Tamines, C., Tentrup, L., Walker, A.: The reactive synthesis competition (SYNTCOMP): 2018-2021 (2022)"},{"key":"16_CR20","unstructured":"Jurdzi\u0144ski, M., Morvan, R., Ohlmann, P., Thejaswini, K.S.: A symmetric attractor-decomposition lifting algorithm for parity games. CoRR abs\/2010.08288 (2020), https:\/\/arxiv.org\/abs\/2010.08288"},{"key":"16_CR21","doi-asserted-by":"publisher","unstructured":"Jurdzinski, M., Morvan, R., Thejaswini, K.S.: Universal algorithms for parity games and nested fixpoints. In: Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 13660, pp. 252\u2013271. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22337-2_12","DOI":"10.1007\/978-3-031-22337-2_12"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Keiren, J.J.A.: Benchmarks for parity games. In: Dastani, M., Sirjani, M. (eds.) Fundamentals of Software Engineering. pp. 127\u2013142. Springer International Publishing, Cham (2015)","DOI":"10.1007\/978-3-319-24644-4_9"},{"key":"16_CR23","doi-asserted-by":"crossref","unstructured":"Khachiyan, L., Gurvich, V., Zhao, J.: Extending Dijkstra\u2019s algorithm to maximize the shortest path by node-wise limited arc interdiction. In: CSR. Lecture Notes in Computer Science, vol.\u00a03967, pp. 221\u2013234. Springer (2006)","DOI":"10.1007\/11753728_24"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Lebedev, V.: Exponential examples of solving parity games. Computational Mathematics and Mathematical Physics 56, 688\u2013697 (2016)","DOI":"10.1134\/S0965542516040114"},{"key":"16_CR25","doi-asserted-by":"publisher","unstructured":"Loff, B., Skomra, M.: Smoothed analysis of deterministic discounted and mean-payoff games. In: ICALP. LIPIcs, vol.\u00a0297, pp. 147:1\u2013147:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.ICALP.2024.147","DOI":"10.4230\/LIPICS.ICALP.2024.147"},{"key":"16_CR26","unstructured":"Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games. CoRR (2008), http:\/\/arxiv.org\/abs\/0806.2923"},{"key":"16_CR27","doi-asserted-by":"crossref","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Informatica 57(1-2), 3\u201336 (2020)","DOI":"10.1007\/s00236-019-00349-3"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: CAV. Lecture Notes in Computer Science, vol. 10981, pp. 578\u2013586. Springer (2018)","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"16_CR29","unstructured":"Mostowski, A.W.: Games with forbidden positions. Tech. Rep.\u00a078, University of Gdansk (1991)"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Ohlmann, P.: The GKK algorithm is the fastest over simple mean-payoff games. In: CSR. Lecture Notes in Computer Science, vol. 13296, pp. 269\u2013288. Springer (2022)","DOI":"10.1007\/978-3-031-09574-0_17"},{"key":"16_CR31","unstructured":"Puri, A.: Theory of Hybrid Systems and Discrete Event Systems. Ph.D. thesis, EECS Department, University of California, Berkeley (dec 1995)"},{"key":"16_CR32","doi-asserted-by":"crossref","unstructured":"Schewe, S.: An optimal strategy improvement algorithm for solving parity and payoff games. In: CSL. Lecture Notes in Computer Science, vol.\u00a05213, pp. 369\u2013384. Springer (2008)","DOI":"10.1007\/978-3-540-87531-4_27"},{"key":"16_CR33","doi-asserted-by":"publisher","unstructured":"Schewe, S., Trivedi, A., Varghese, T.: Symmetric strategy improvement. In: ICALP. Lecture Notes in Computer Science, vol.\u00a09135, pp. 388\u2013400. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-47666-6_31","DOI":"10.1007\/978-3-662-47666-6_31"},{"key":"16_CR34","doi-asserted-by":"publisher","unstructured":"Spielman, D.A., Teng, S.: Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time. J. ACM 51(3), 385\u2013463 (2004). https:\/\/doi.org\/10.1145\/990308.990310","DOI":"10.1145\/990308.990310"},{"key":"16_CR35","doi-asserted-by":"publisher","unstructured":"Thejaswini, K.S., Ohlmann, P., Jurdzinski, M.: A technique to speed up symmetric attractor-based algorithms for parity games. In: FSTTCS. LIPIcs, vol.\u00a0250, pp. 44:1\u201344:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.FSTTCS.2022.44","DOI":"10.4230\/LIPICS.FSTTCS.2022.44"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-90653-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:36:43Z","timestamp":1764401803000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-90653-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031906527","9783031906534"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-90653-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"1 May 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hamilton, ON","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 May 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 May 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2025\/conferences\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}