Document Open Access Logo

Solving Odd-Fair Parity Games

Authors Irmak Sağlam, Anne-Kathrin Schmuck

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2023.34.pdf
  • Filesize: 1.46 MB
  • 24 pages

Document Identifiers

Author Details

Irmak Sağlam
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
Anne-Kathrin Schmuck
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany

Funding

This work was partially supported by the DFG projects SCHM 3541/1-1 and 389792660 TRR 248–CPEC.

Acknowledgements

We are grateful for the immense support provided by Munko Tsyrempilon for the experimental validation.

Cite AsGet BibTex

Irmak Sağlam and Anne-Kathrin Schmuck. Solving Odd-Fair Parity Games. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 34:1-34:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSTTCS.2023.34

Abstract

This paper discusses the problem of efficiently solving parity games where player Odd has to obey an additional strong transition fairness constraint on its vertices - given that a player Odd vertex v is visited infinitely often, a particular subset of the outgoing edges (called live edges) of v has to be taken infinitely often. Such games, which we call Odd-fair parity games, naturally arise from abstractions of cyber-physical systems for planning and control. In this paper, we present a new Zielonka-type algorithm for solving Odd-fair parity games. This algorithm not only shares the same worst-case time complexity as Zielonka’s algorithm for (normal) parity games but also preserves the algorithmic advantage Zielonka’s algorithm possesses over other parity solvers with exponential time complexity. We additionally introduce a formalization of Odd player winning strategies in such games, which were unexplored previous to this work. This formalization serves dual purposes: firstly, it enables us to prove our Zielonka-type algorithm; secondly, it stands as a noteworthy contribution in its own right, augmenting our understanding of additional fairness assumptions in two-player games.

Subject Classification

ACM Subject Classification
  • Theory of computation → Solution concepts in game theory
Keywords
  • parity games
  • strong transition fairness
  • algorithmic game theory

Metrics

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

Related Versions

References

  1. Rajeev Alur, Salar Moarref, and Ufuk Topcu. Counter-strategy guided refinement of GR(1) temporal logic specifications. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 26-33. IEEE, 2013. Google Scholar
  2. Benjamin Aminof, Giuseppe De Giacomo, and Sasha Rubin. Stochastic fairness and language-theoretic fairness in planning in nondeterministic domains. In J. Christopher Beck, Olivier Buffet, Jörg Hoffmann, Erez Karpas, and Shirin Sohrabi, editors, Proceedings of the Thirtieth International Conference on Automated Planning and Scheduling, Nancy, France, October 26-30, 2020, pages 20-28. AAAI Press, 2020. Google Scholar
  3. André Arnold, Damian Niwiński, and Paweł Parys. A quasi-polynomial black-box algorithm for fixed point evaluation. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), volume 183 of LIPIcs, pages 9:1-9:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  4. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  5. Tamajit Banerjee, Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. Fast symbolic algorithms for omega-regular games under strong transition fairness. TheoretiCS, 2, 2023. Google Scholar
  6. Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. Formal methods for discrete-time dynamical systems, volume 15. Springer, 2017. Google Scholar
  7. Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa'ar. Synthesis of reactive(1) designs. J. Comput. Syst. Sci., 78(3):911-938, 2012. Google Scholar
  8. Krishnendu Chatterjee, Luca de Alfaro, Marco Faella, Rupak Majumdar, and Vishwanath Raman. Code aware resource management. Formal Methods Syst. Des., 42(2):146-174, 2013. Google Scholar
  9. Alessandro Cimatti, Marco Pistore, Marco Roveri, and Paolo Traverso. Weak, strong, and strong cyclic planning via symbolic model checking. Artif. Intell., 147(1-2):35-84, 2003. Google Scholar
  10. Marco Daniele, Paolo Traverso, and Moshe Y. Vardi. Strong cyclic planning revisited. In Susanne Biundo and Maria Fox, editors, Recent Advances in AI Planning, 5th European Conference on Planning, ECP'99, Durham, UK, September 8-10, 1999, Proceedings, volume 1809 of Lecture Notes in Computer Science, pages 35-48. Springer, 1999. Google Scholar
  11. Nicolás D'Ippolito, Natalia Rodríguez, and Sebastian Sardiña. Fully observable non-deterministic planning as assumption-based reactive synthesis. J. Artif. Intell. Res., 61:593-621, 2018. Google Scholar
  12. E. Allen Emerson and Charanjit S. Jutla. On simultaneously determinizing and complementing omega-automata (extended abstract). In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989, pages 333-342. IEEE Computer Society, 1989. Google Scholar
  13. E. Allen Emerson and Charanjit S. Jutla. Tree automata, mu-calculus and determinacy (extended abstract). In 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, pages 368-377. IEEE Computer Society, 1991. Google Scholar
  14. E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. SIAM J. Comput., 29(1):132-158, 1999. Google Scholar
  15. Nissim Francez. Fairness. Springer-Verlag, Berlin, Heidelberg, 1986. Google Scholar
  16. Yuri Gurevich and Leo Harrington. Trees, automata, and games. In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors, Proceedings of the 14th Annual ACM Symposium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 60-65. ACM, 1982. Google Scholar
  17. Daniel Hausmann and Lutz Schröder. Quasipolynomial computation of nested fixpoints. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part I, volume 12651 of Lecture Notes in Computer Science, pages 38-56. Springer, 2021. Google Scholar
  18. Swen Jacobs, Guillermo A. Pérez, Remco Abraham, Véronique Bruyère, Michaël Cadilhac, Maximilien Colange, Charly Delfosse, Tom van Dijk, Alexandre Duret-Lutz, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Michael Luttenberger, Klara J. Meyer, Thibaud Michaud, Adrien Pommellet, Florian Renkin, Philipp Schlehuber-Caissier, Mouhammad Sakr, Salomon Sickert, Gaëtan Staquet, Clement Tamines, Leander Tentrup, and Adam Walker. The reactive synthesis competition (SYNTCOMP): 2018-2021. CoRR, abs/2206.00251, 2022. URL: https://doi.org/10.48550/arXiv.2206.00251.
  19. Marcin Jurdzinski. Small progress measures for solving parity games. In Horst Reichel and Sophie Tison, editors, STACS 2000, 17th Annual Symposium on Theoretical Aspects of Computer Science, Lille, France, February 2000, Proceedings, volume 1770 of Lecture Notes in Computer Science, pages 290-301. Springer, 2000. Google Scholar
  20. Marcin Jurdzinski, Rémi Morvan, and K. S. Thejaswini. Universal algorithms for parity games and nested fixpoints. In Jean-François Raskin, Krishnendu Chatterjee, Laurent Doyen, and Rupak Majumdar, editors, Principles of Systems Design - Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday, volume 13660 of Lecture Notes in Computer Science, pages 252-271. Springer, 2022. Google Scholar
  21. Jeroen J. A. Keiren. Benchmarks for parity games. In Mehdi Dastani and Marjan Sirjani, editors, Fundamentals of Software Engineering - 6th International Conference, FSEN 2015 Tehran, Iran, April 22-24, 2015, Revised Selected Papers, volume 9392 of Lecture Notes in Computer Science, pages 127-142. Springer, 2015. Google Scholar
  22. Nils Klarlund. Progress Measures and Finite Arguments for Infinite Computations. PhD thesis, Cornell University, USA, 1990. Google Scholar
  23. Nils Klarlund. Progress measures, immediate determinacy, and a subset construction for tree automata. Ann. Pure Appl. Log., 69(2-3):243-268, 1994. Google Scholar
  24. Nils Klarlund and Dexter Kozen. Rabin measures and their applications to fairness and automata theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 256-265. IEEE Computer Society, 1991. Google Scholar
  25. Dexter Kozen. Results on the propositional mu-calculus. Theor. Comput. Sci., 27:333-354, 1983. Google Scholar
  26. Hadas Kress-Gazit, Georgios E. Fainekos, and George J. Pappas. Where’s waldo? sensor-based temporal logic motion planning. In 2007 IEEE International Conference on Robotics and Automation, ICRA 2007, 10-14 April 2007, Roma, Italy, pages 3116-3121. IEEE, 2007. Google Scholar
  27. Hadas Kress-Gazit, Georgios E. Fainekos, and George J. Pappas. Temporal-logic-based reactive mission and motion planning. IEEE Trans. Robotics, 25(6):1370-1381, 2009. Google Scholar
  28. Ralf Küsters. Memoryless determinacy of parity games. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors, Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], volume 2500 of Lecture Notes in Computer Science, pages 95-106. Springer, 2001. Google Scholar
  29. Rupak Majumdar, Kaushik Mallik, Anne-Kathrin Schmuck, and Sadegh Soudjani. Symbolic control for stochastic systems via parity games. CoRR, abs/2101.00834, 2021. Google Scholar
  30. Shahar Maoz and Jan Oliver Ringert. Synthesizing a lego forklift controller in GR(1): A case study. In Pavol Cerný, Viktor Kuncak, and Parthasarathy Madhusudan, editors, Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015, volume 202 of EPTCS, pages 58-72, 2015. Google Scholar
  31. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. Google Scholar
  32. Petter Nilsson, Necmiye Ozay, and Jun Liu. Augmented finite transition systems as abstractions for control synthesis. Discret. Event Dyn. Syst., 27(2):301-340, 2017. Google Scholar
  33. Paweł Parys. Parity games: Zielonka’s algorithm in quasi-polynomial time. In Peter Rossmanith, Pinar Heggernes, and Joost-Pieter Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 10:1-10:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  34. Marco Pistore and Paolo Traverso. Planning as model checking for extended goals in non-deterministic domains. In Bernhard Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI 2001, Seattle, Washington, USA, August 4-10, 2001, pages 479-486. Morgan Kaufmann, 2001. Google Scholar
  35. Jean-Pierre Queille and Joseph Sifakis. Fairness and related properties in transition systems - A temporal logic to deal with fairness. Acta Informatica, 19:195-220, 1983. Google Scholar
  36. Miquel Ramírez and Sebastian Sardiña. Directed fixed-point regression-based planning for non-deterministic domains. In Steve A. Chien, Minh Binh Do, Alan Fern, and Wheeler Ruml, editors, Proceedings of the Twenty-Fourth International Conference on Automated Planning and Scheduling, ICAPS 2014, Portsmouth, New Hampshire, USA, June 21-26, 2014. AAAI, 2014. Google Scholar
  37. Irmak Sağlam and Anne-Kathrin Schmuck. Solving odd-fair parity games, 2023. URL: https://arxiv.org/abs/2307.13396.
  38. Sven Schewe. An optimal strategy improvement algorithm for solving parity and payoff games. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings, volume 5213 of Lecture Notes in Computer Science, pages 369-384. Springer, 2008. Google Scholar
  39. Robert S. Streett and E. Allen Emerson. The propositional mu-calculus is elementary. In Jan Paredaens, editor, Automata, Languages and Programming, 11th Colloquium, Antwerp, Belgium, July 16-20, 1984, Proceedings, volume 172 of Lecture Notes in Computer Science, pages 465-472. Springer, 1984. Google Scholar
  40. María Svorenová, Jan Kretínský, Martin Chmelik, Krishnendu Chatterjee, Ivana Cerná, and Calin Belta. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In Antoine Girard and Sriram Sankaranarayanan, editors, Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC'15, Seattle, WA, USA, April 14-16, 2015, pages 259-268. ACM, 2015. Google Scholar
  41. Paulo Tabuada. Verification and Control of Hybrid Systems - A Symbolic Approach. Springer, 2009. Google Scholar
  42. John G Thistle and RP Malhamé. Control of ω-automata under state fairness assumptions. Systems & control letters, 33(4):265-274, 1998. Google Scholar
  43. Tom van Dijk. Attracting tangles to solve parity games. In Hana Chockler and Georg Weissenbacher, editors, Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, volume 10982 of Lecture Notes in Computer Science, pages 198-215. Springer, 2018. Google Scholar
  44. Tom van Dijk. Oink: An implementation and evaluation of modern parity game solvers. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part I, volume 10805 of Lecture Notes in Computer Science, pages 291-308. Springer, 2018. Google Scholar
  45. Kai Weng Wong, Rüdiger Ehlers, and Hadas Kress-Gazit. Resilient, provably-correct, and high-level robot behaviors. IEEE Trans. Robotics, 34(4):936-952, 2018. Google Scholar
  46. Wiesław Zielonka. Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theor. Comput. Sci., 200(1-2):135-183, 1998. 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