Document Open Access Logo

Energy Mean-Payoff Games

Authors Véronique Bruyère, Quentin Hautem, Mickael Randour, Jean-François Raskin

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.21.pdf
  • Filesize: 0.57 MB
  • 17 pages

Document Identifiers

Author Details

Véronique Bruyère
  • Université de Mons (UMONS), Belgium
Quentin Hautem
  • Université de Mons (UMONS), Belgium
Mickael Randour
  • Université de Mons (F.R.S.-FNRS & UMONS), Belgium
Jean-François Raskin
  • Université libre de Bruxelles (ULB), Belgium

Funding

Work partially supported by the PDR project Subgame perfection in graph games (F.R.S.-FNRS), the grant n°F.4520.18 ManySynth (F.R.S.-FNRS), the ARC project Non-Zero Sum Game Graphs: Applications to Reactive Synthesis and Beyond (Fédération Wallonie-Bruxelles), the EOS project Verifying Learning Artificial Intelligence Systems (F.R.S.-FNRS & FWO), and the COST Action 16228 GAMENET (European Cooperation in Science and Technology).

Cite AsGet BibTex

Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy Mean-Payoff Games. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CONCUR.2019.21

Abstract

In this paper, we study one-player and two-player energy mean-payoff games. Energy mean-payoff games are games of infinite duration played on a finite graph with edges labeled by 2-dimensional weight vectors. The objective of the first player (the protagonist) is to satisfy an energy objective on the first dimension and a mean-payoff objective on the second dimension. We show that optimal strategies for the first player may require infinite memory while optimal strategies for the second player (the antagonist) do not require memory. In the one-player case (where only the first player has choices), the problem of deciding who is the winner can be solved in polynomial time while for the two-player case we show co-NP membership and we give effective constructions for the infinite-memory optimal strategies of the protagonist.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Theory of computation → Logic and verification
  • Theory of computation → Solution concepts in game theory
Keywords
  • two-player zero-sum games played on graphs
  • energy and mean-payoff objectives
  • complexity study and construction of optimal strategies

Metrics

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

Related Versions

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke. Infinite-state energy games. In Thomas A. Henzinger and Dale Miller, editors, Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, pages 7:1-7:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603100.
  2. Parosh Aziz Abdulla, Richard Mayr, Arnaud Sangnier, and Jeremy Sproston. Solving Parity Games on Integer Vectors. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, CONCUR 2013 - Concurrency Theory - 24th International Conference, CONCUR 2013, Buenos Aires, Argentina, August 27-30, 2013, Proceedings, volume 8052 of Lecture Notes in Computer Science, pages 106-120. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_9.
  3. Roderick Bloem, Krishnendu Chatterjee, and Barbara Jobstmann. Graph Games and Reactive Synthesis. In Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 921-962. Springer, 2018. Google Scholar
  4. Udi Boker, Thomas A. Henzinger, and Arjun Radhakrishna. Battery transition systems. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 595-606. ACM, 2014. URL: https://doi.org/10.1145/2535838.2535875.
  5. Patricia Bouyer, Ulrich Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, and Jirí Srba. Infinite Runs in Weighted Timed Automata with Energy Constraints. In Franck Cassez and Claude Jard, editors, Formal Modeling and Analysis of Timed Systems, 6th International Conference, FORMATS 2008, Saint Malo, France, September 15-17, 2008, Proceedings, volume 5215 of Lecture Notes in Computer Science, pages 33-47. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85778-5_4.
  6. Patricia Bouyer, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann. Bounding Average-Energy Games. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 179-195, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_11.
  7. Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, and Simon Laursen. Average-energy games. Acta Inf., 55(2):91-127, 2018. URL: https://doi.org/10.1007/s00236-016-0274-1.
  8. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, and Petr Novotný. Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. In P. Madhusudan and Sanjit A. Seshia, editors, Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012, Proceedings, volume 7358 of Lecture Notes in Computer Science, pages 23-38. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-31424-7_8.
  9. Tomás Brázdil, Petr Jancar, and Antonín Kucera. Reachability Games on Extended Vector Addition Systems with States. CoRR, abs/1002.2557, 2010. URL: http://arxiv.org/abs/1002.2557.
  10. Tomás Brázdil, David Klaska, Antonín Kucera, and Petr Novotný. Minimizing Running Costs in Consumption Systems. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014, Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 457-472. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_30.
  11. Tomás Brázdil, Antonín Kucera, and Petr Novotný. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, pages 32-49, 2016. URL: https://doi.org/10.1007/978-3-319-46520-3_3.
  12. Lubos Brim, Jakub Chaloupka, Laurent Doyen, Raffaella Gentilini, and Jean-François Raskin. Faster algorithms for mean-payoff games. Formal Methods in System Design, 38(2):97-118, 2011. URL: https://doi.org/10.1007/s10703-010-0105-x.
  13. Véronique Bruyère. Computer Aided Synthesis: A Game-Theoretic Approach. In Émilie Charlier, Julien Leroy, and Michel Rigo, editors, Developments in Language Theory - 21st International Conference, DLT 2017, Liège, Belgium, August 7-11, 2017, Proceedings, volume 10396 of Lecture Notes in Computer Science, pages 3-35. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-62809-7_1.
  14. Véronique Bruyère, Quentin Hautem, Mickael Randour, and Jean-François Raskin. Energy mean-payoff games. CoRR, abs/1907.01359, 2019. URL: http://arxiv.org/abs/1907.01359.
  15. Véronique Bruyère, Quentin Hautem, and Jean-François Raskin. On the Complexity of Heterogeneous Multidimensional Games. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 11:1-11:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.11.
  16. Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource Interfaces. In Rajeev Alur and Insup Lee, editors, Embedded Software, Third International Conference, EMSOFT 2003, Philadelphia, PA, USA, October 13-15, 2003, Proceedings, volume 2855 of Lecture Notes in Computer Science, pages 117-133. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45212-6_9.
  17. Krishnendu Chatterjee and Laurent Doyen. Energy parity games. Theor. Comput. Sci., 458:49-60, 2012. URL: https://doi.org/10.1016/j.tcs.2012.07.038.
  18. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized Mean-payoff and Energy Games. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 505-516. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.505.
  19. Krishnendu Chatterjee, Laurent Doyen, Mickael Randour, and Jean-François Raskin. Looking at mean-payoff and total-payoff through windows. Inf. Comput., 242:25-52, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.010.
  20. Krishnendu Chatterjee, Thomas A. Henzinger, and Marcin Jurdzinski. Mean-Payoff Parity Games. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings, pages 178-187. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/LICS.2005.26.
  21. Krishnendu Chatterjee, Mickael Randour, and Jean-François Raskin. Strategy synthesis for multi-dimensional quantitative objectives. Acta Inf., 51(3-4):129-163, 2014. URL: https://doi.org/10.1007/s00236-013-0182-6.
  22. Krishnendu Chatterjee and Yaron Velner. The Complexity of Mean-Payoff Pushdown Games. J. ACM, 64(5):34:1-34:49, 2017. URL: https://doi.org/10.1145/3121408.
  23. Thomas Colcombet, Marcin Jurdzinski, Ranko Lazic, and Sylvain Schmitz. Perfect half space games. In LICS Proceedings, pages 1-11. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005105.
  24. Laure Daviaud, Marcin Jurdzinski, and Ranko Lazic. A pseudo-quasi-polynomial algorithm for mean-payoff parity games. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 325-334. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209162.
  25. A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8:109-113, 1979. URL: https://doi.org/10.1007/BF01768705.
  26. Uli Fahrenberg, Line Juhl, Kim G. Larsen, and Jirí Srba. Energy Games in Multiweighted Automata. In Antonio Cerone and Pekka Pihlajasaari, editors, Theoretical Aspects of Computing - ICTAC 2011 - 8th International Colloquium, Johannesburg, South Africa, August 31 - September 2, 2011, Proceedings, volume 6916 of Lecture Notes in Computer Science, pages 95-115. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23283-1_9.
  27. Hugo Gimbert and Wieslaw Zielonka. Games Where You Can Play Optimally Without Any Memory. In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science, pages 428-442. Springer, 2005. URL: https://doi.org/10.1007/11539452_33.
  28. Line Juhl, Kim Guldstrand Larsen, and Jean-François Raskin. Optimal Bounds for Multiweighted and Parametrised Energy Games. In Zhiming Liu, Jim Woodcock, and Huibiao Zhu, editors, Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science, pages 244-255. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39698-4_15.
  29. Marcin Jurdzinski, Ranko Lazic, and Sylvain Schmitz. Fixed-Dimensional Energy Games are in Pseudo-Polynomial Time. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, Automata, Languages, and Programming - 42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II, volume 9135 of Lecture Notes in Computer Science, pages 260-272. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_21.
  30. Eryk Kopczynski and Damian Niwinski. A simple indeterminate infinite game. In Vasco Brattka, Hannes Diener, and Dieter Spreen, editors, Logic, Computation, Hierarchies, volume 4 of Ontos Mathematical Logic, pages 205-212. De Gruyter, 2014. URL: https://doi.org/10.1515/9781614518044.205.
  31. S. Rao Kosaraju and Gregory F. Sullivan. Detecting Cycles in Dynamic Graphs in Polynomial Time (Preliminary Version). In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, May 2-4, 1988, Chicago, Illinois, USA, pages 398-406. ACM, 1988. URL: https://doi.org/10.1145/62212.62251.
  32. Antonín Kucera. Playing Games with Counter Automata. In Alain Finkel, Jérôme Leroux, and Igor Potapov, editors, Reachability Problems - 6th International Workshop, RP 2012, Bordeaux, France, September 17-19, 2012, Proceedings, volume 7550 of Lecture Notes in Computer Science, pages 29-41. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33512-9_4.
  33. Amir Pnueli and Roni Rosner. On the Synthesis of an Asynchronous Reactive Module. In Giorgio Ausiello, Mariangiola Dezani-Ciancaglini, and Simona Ronchi Della Rocca, editors, Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings, volume 372 of Lecture Notes in Computer Science, pages 652-671. Springer, 1989. URL: https://doi.org/10.1007/BFb0035790.
  34. Yaron Velner. Robust Multidimensional Mean-Payoff Games are Undecidable. In Andrew M. Pitts, editor, Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, volume 9034 of Lecture Notes in Computer Science, pages 312-327. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_20.
  35. Yaron Velner, Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, Alexander Moshe Rabinovich, and Jean-François Raskin. The complexity of multi-mean-payoff and multi-energy games. Inf. Comput., 241:177-196, 2015. URL: https://doi.org/10.1016/j.ic.2015.03.001.
  36. U. Zwick and M. 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