Reactive Synthesis Without Regret

Authors Paul Hunter, Guillermo A. Pérez, Jean-François Raskin



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.114.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

Paul Hunter
Guillermo A. Pérez
Jean-François Raskin

Cite AsGet BibTex

Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive Synthesis Without Regret. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 114-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.114

Abstract

Two-player zero-sum games of infinite duration and their quantitative versions are used in verification to model the interaction between a controller (Eve) and its environment (Adam). The question usually addressed is that of the existence (and computability) of a strategy for Eve that can maximize her payoff against any strategy of Adam. In this work, we are interested in strategies of Eve that minimize her regret, i.e. strategies that minimize the difference between her actual payoff and the payoff she could have achieved if she had known the strategy of Adam in advance. We give algorithms to compute the strategies of Eve that ensure minimal regret against an adversary whose choice of strategy is (i) unrestricted, (ii) limited to positional strategies, or (iii) limited to word strategies, and show that the two last cases have natural modelling applications. We also show that our notion of regret minimization in which Adam is limited to word strategies generalizes the notion of good for games introduced by Henzinger and Piterman, and is related to the notion of determinization by pruning due to Aminof, Kupferman and Lampert.
Keywords
  • Quantitative games
  • regret
  • verification
  • synthesis
  • game theory

Metrics

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

References

  1. Benjamin Aminof, Orna Kupferman, and Robby Lampert. Reasoning about online algorithms with weighted automata. ACM Transactions on Algorithms, 2010. Google Scholar
  2. David E. Bell. Regret in decision making under uncertainty. Operations Research, 30(5):961-981, 1982. Google Scholar
  3. 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. Google Scholar
  4. Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga. Resource interfaces. In EMSOFT, volume 2855 of LNCS, pages 117-133. Springer, 2003. Google Scholar
  5. Krishnendu Chatterjee, Laurent Doyen, Emmanuel Filiot, and Jean-François Raskin. Doomsday equilibria for omega-regular games. In VMCAI, volume 8318, pages 78-97. Springer, 2014. Google Scholar
  6. Krishnendu Chatterjee, Laurent Doyen, and Thomas A. Henzinger. Quantitative languages. ACM Trans. Comput. Log., 11(4), 2010. Google Scholar
  7. Krishnendu Chatterjee, Laurent Doyen, Thomas A. Henzinger, and Jean-François Raskin. Generalized mean-payoff and energy games. In FSTTCS, pages 505-516, 2010. Google Scholar
  8. Werner Damm and Bernd Finkbeiner. Does it pay to extend the perimeter of a world model? In FM, volume 6664 of LNCS, pages 12-26. Springer, 2011. Google Scholar
  9. Aldric Degorre, Laurent Doyen, Raffaella Gentilini, Jean-François Raskin, and Szymon Toruńczyk. Energy and mean-payoff games with imperfect information. In CSL, pages 260-274, 2010. Google Scholar
  10. A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8:109-113, 1979. Google Scholar
  11. Tali Eilam-Tzoreff. The disjoint shortest paths problem. Discrete Applied Mathematics, 85(2):113-138, 1998. Google Scholar
  12. Emmanuel Filiot, Tristan Le Gall, and Jean-François Raskin. Iterated regret minimization in game graphs. In MFCS, volume 6281 of LNCS, pages 342-354. Springer, 2010. Google Scholar
  13. Joseph Y. Halpern and Rafael Pass. Iterated regret minimization: A new solution concept. Games and Economic Behavior, 74(1):184-207, 2012. Google Scholar
  14. Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In CSL, pages 395-410, 2006. Google Scholar
  15. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Mean-payoff games with partial-observation (extended abstract). In Reachability Problems, pages 163-175, 2014. Google Scholar
  16. Paul Hunter, Guillermo A. Pérez, and Jean-François Raskin. Reactive synthesis without regret. CoRR, abs/1504.01708, 2015. Google Scholar
  17. Marcin Jurdziński. Deciding the winner in parity games is in \UP ∩ \coUP. Information Processing Letters, 68(3):119-124, 1998. Google Scholar
  18. Marcin Jurdzinski, Jeremy Sproston, and François Laroussinie. Model checking probabilistic timed automata with one or two clocks. LMCS, 4(3), 2008. Google Scholar
  19. Christos H. Papadimitriou and Mihalis Yannakakis. Shortest paths without a map. Theoretical Computer Science, 84(1):127-150, 1991. Google Scholar
  20. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In POPL, pages 179-190. ACM, ACM Press, 1989. Google Scholar
  21. Min Wen, Ruediger Ehlers, and Ufuk Topcu. Correct-by-synthesis reinforcement learning with temporal logic constraints. arXiv preprint arXiv:1503.01793, 2015. Google Scholar
  22. Martin Zinkevich, Michael Johanson, Michael Bowling, and Carmelo Piccione. Regret minimization in games with incomplete information. In NIPS, pages 905-912, 2008. Google Scholar
  23. Uri Zwick and Mike Paterson. The complexity of mean payoff games on graphs. TCS, 158(1):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