Document Open Access Logo

A Lattice-Theoretical View of Strategy Iteration

Authors Paolo Baldan , Richard Eggert , Barbara König , Tommaso Padoan

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.7.pdf
  • Filesize: 0.82 MB
  • 19 pages

Document Identifiers

Author Details

Paolo Baldan
  • University of Padova, Italy
Richard Eggert
  • Universität Duisburg-Essen, Germany
Barbara König
  • Universität Duisburg-Essen, Germany
Tommaso Padoan
  • University of Padova, Italy

Funding

Partially supported by the DFG project SpeQt and by the Ministero dell’Universtà e della Ricerca Scientifica of Italy, under Grant No. 201784YSZ5, PRIN2017 - ASPRA.

Cite AsGet BibTex

Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. A Lattice-Theoretical View of Strategy Iteration. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.7

Abstract

Strategy iteration is a technique frequently used for two-player games in order to determine the winner or compute payoffs, but to the best of our knowledge no general framework for strategy iteration has been considered. Inspired by previous work on simple stochastic games, we propose a general formalisation of strategy iteration for solving least fixpoint equations over a suitable class of complete lattices, based on MV-chains. We devise algorithms that can be used for non-expansive fixpoint functions represented as so-called min- respectively max-decompositions. Correspondingly, we develop two different techniques: strategy iteration from above, which has to solve the problem that iteration might reach a fixpoint that is not the least, and from below, which is algorithmically simpler, but requires a more involved correctness argument. We apply our method to solve energy games and compute behavioural metrics for probabilistic automata.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Solution concepts in game theory
Keywords
  • games
  • strategy iteration
  • fixpoints
  • energy games
  • behavioural metrics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. David Auger, Xavier Badin de Montjoye, and Yann Strozecki. A generic strategy improvement method for simple stochastic games. In Proc. of MFCS 2021, volume 202 of LIPIcs, pages 12:1-12:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. Logical Methods in Computer Science, 13(2:13):1-25, 2017. Google Scholar
  3. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, and Franck van Breugel. Computing probabilistic bisimilarity distances for probabilistic automata. Logical Methods in Computer Science, 17(1), 2021. Google Scholar
  4. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Logical Methods in Computer Science, 14(3), 2018. Selected Papers of the 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). URL: https://lmcs.episciences.org/4827.
  5. Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. Fixpoint theory - upside down. In Proc. of FOSSACS 2021, volume 12650 of Lecture Notes in Computer Science, pages 62-81. Springer, 2021. Google Scholar
  6. Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. Fixpoint theory - upside down. CoRR, abs/2101.08184, 2021. URL: http://arxiv.org/abs/2101.08184.
  7. Paolo Baldan, Richard Eggert, Barbara König, and Tommaso Padoan. A lattice-theoretical view of strategy iteration, 2022. URL: http://arxiv.org/abs/2207.09872.
  8. Filippo Bonchi, Barbara König, and Daniela Petrişan. Up-to techniques for behavioural metrics via fibrations. In Proc. of CONCUR 2018, volume 118 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz Center for Informatics, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17.
  9. Patricia Bouyer, Uli Fahrenberg, Kim G. Larsen, Nicolas Markey, and Jiří Srba. Infinite runs in weighted timed automata with energy constraints. In Franck Cassez and Claude Jard, editors, Formal Modeling and Analysis of Timed Systems, pages 33-47. Springer, 2008. Google Scholar
  10. Luboš Brim and Jakub Chaloupka. Using strategy improvement to stay alive. Electronic Proceedings in Theoretical Computer Science, 25:40-54, 2010. URL: https://doi.org/10.4204/eptcs.25.8.
  11. Cristian S. Calude, Sanjay Jain, Bakhadyr Khoussainov, Wei Li, and Frank Stephan. Deciding parity games in quasipolynomial time. In Proc. of STOC 2017, pages 252-263, 2017. Google Scholar
  12. Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource interfaces. In Rajeev Alur and Insup Lee, editors, Prof. of EMSOFT '03 (International Workshop on Embedded Software), volume 2855 of Lecture Notes in Computer Science, pages 117-133. Springer, 2003. Google Scholar
  13. Anne Condon. The complexity of stochastic games. Information and Computation, 96(2):203-224, 1992. URL: https://doi.org/10.1016/0890-5401(92)90048-K.
  14. Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of POPL 1977, pages 238-252. ACM, 1977. Google Scholar
  15. Patrick Cousot and Radhia Cousot. Temporal abstract interpretation. In Mark N. Wegman and Thomas W. Reps, editors, Proc. of POPL 2000, pages 12-25. ACM, 2000. Google Scholar
  16. Dani Dorfman, Haim Kaplan, and Uri Zwick. A faster deterministic exponential time algorithm for energy games and mean payoff games. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, Proc. of ICALP 2019, volume 132 of LIPIcs, pages 114:1-114:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.114.
  17. John Fearnley. Exponential lower bounds for policy iteration. In Proc. of ICALP 2010, volume 6199 of Lecture Notes in Computer Science, pages 551-562. Springer, 2010. Google Scholar
  18. Oliver Friedmann. An exponential lower bound for the latest deterministic strategy iteration algorithms. Log. Methods Comput. Sci., 7(3), 2011. Google Scholar
  19. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science. Springer, 2002. Google Scholar
  20. Daniel Hausmann and Lutz Schröder. Quasipolynomial computation of nested fixpoints. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Proc. of TACAS 2021, volume 12651 of Lecture Notes in Computer Science, pages 38-56. Springer, 2021. Google Scholar
  21. Ronald A. Howard. Dynamic Programming and Markov Processes. MIT Press, 1960. Google Scholar
  22. Marcin Jurdzinski and Ranko Lazic. Succinct progress measures for solving parity games. In Proc. of LICS 2017, pages 1-9. ACM/IEEE, 2017. Google Scholar
  23. Richard M. Karp and Alan J. Hoffman. On nonterminating stochastic games. Management Science, 12(5):359-370, 1966. Google Scholar
  24. Karoliina Lehtinen. A modal μ perspective on solving parity games in quasi-polynomial time. In Proc. of LICS 2018, pages 639-648. ACM/IEEE, 2018. Google Scholar
  25. Yu. M. Lifshits and D. S. Pavlov. Potential theory for mean payoff games. Zapiski Nauchnykh Seminarov POMI, 340:61-75, 2006. Google Scholar
  26. Facundo Mémoli. Gromov-Wasserstein distances and the metric approach to object matching. Foundations of Computational Mathematics, 11(4):417-487, 2011. Google Scholar
  27. Daniele Mundici. MV-algebras. A short tutorial. Available at URL: http://www.matematica.uns.edu.ar/IXCongresoMonteiro/Comunicaciones/Mundici_tutorial.pdf.
  28. Sven Schewe. An optimal strategy improvement algorithm for solving parity and payoff games. In Proc. of CSL 2008, volume 5213 of Lecture Notes in Computer Science, pages 369-384. Springer, 2008. Google Scholar
  29. Alfred Tarski. A lattice-theoretical theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955. Google Scholar
  30. Cédric Villani. Optimal Transport - Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics. Springer, 2009. Google Scholar
  31. Jens Vöge and Marcin Jurdzinski. A discrete strategy improvement algorithm for solving parity games. In Proc. of CAV 2000, volume 1855 of Lecture Notes in Computer Science, pages 202-215. Springer, 2000. Google Scholar
  32. Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158(1&2):343-359, 1996. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact