Playing Stochastically in Weighted Timed Games to Emulate Memory

Authors Benjamin Monmege , Julie Parreaux, Pierre-Alain Reynier



PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.137.pdf
  • Filesize: 0.82 MB
  • 17 pages

Document Identifiers

Author Details

Benjamin Monmege
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, France
Julie Parreaux
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, France
Pierre-Alain Reynier
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, France

Cite As Get BibTex

Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Playing Stochastically in Weighted Timed Games to Emulate Memory. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 137:1-137:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.137

Abstract

Weighted timed games are two-player zero-sum games played in a timed automaton equipped with integer weights. We consider optimal reachability objectives, in which one of the players, that we call Min, wants to reach a target location while minimising the cumulated weight. While knowing if Min has a strategy to guarantee a value lower than a given threshold is known to be undecidable (with two or more clocks), several conditions, one of them being the divergence, have been given to recover decidability. In such weighted timed games (like in untimed weighted games in the presence of negative weights), Min may need finite memory to play (close to) optimally. This is thus tempting to try to emulate this finite memory with other strategic capabilities. In this work, we allow the players to use stochastic decisions, both in the choice of transitions and of timing delays. We give for the first time a definition of the expected value in weighted timed games, overcoming several theoretical challenges. We then show that, in divergent weighted timed games, the stochastic value is indeed equal to the classical (deterministic) value, thus proving that Min can guarantee the same value while only using stochastic choices, and no memory.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Theory of computation → Algorithmic game theory
Keywords
  • Weighted timed games
  • Algorithmic game theory
  • Randomisation

Metrics

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

References

  1. Rajeev Alur, Mikhail Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP'04), volume 3142 of LNCS, pages 122-133. Springer, 2004. Google Scholar
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  3. Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. Theoretical Computer Science, 318(3):297-322, 2004. Google Scholar
  4. Eugene Asarin and Oded Maler. As soon as possible: Time optimal control for timed automata. In Hybrid Systems: Computation and Control, volume 1569 of LNCS, pages 19-30. Springer, 1999. Google Scholar
  5. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimum-cost reachability for priced time automata. In International Workshop on Hybrid Systems: Computation and Control, pages 147-161. Springer, 2001. Google Scholar
  6. Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, and Pierre P. Carlier. When are stochastic transition systems tameable? Journal of Logical and Algebraic Methods in Programming, 99:41-96, 2018. Google Scholar
  7. Nathalie Bertrand, Patricia Bouyer, Thomas Brihaye, Quentin Menet, Christel Baier, Marcus Größer, and Marcin Jurdzinski. Stochastic timed automata. Log. Methods Comput. Sci., 10(4), 2014. Google Scholar
  8. Patricia Bouyer, Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On the optimal reachability problem of weighted timed automata. Formal Methods in System Design, 31(2):135-175, 2007. Google Scholar
  9. Patricia Bouyer, Thomas Brihaye, Pierre Carlier, and Quentin Menet. Compositional design of stochastic timed automata. In Alexander S. Kulikov and Gerhard J. Woeginger, editors, Computer Science - Theory and Applications - 11th International Computer Science Symposium in Russia, CSR 2016, St. Petersburg, Russia, June 9-13, 2016, Proceedings, volume 9691 of Lecture Notes in Computer Science, pages 117-130. Springer, 2016. Google Scholar
  10. Patricia Bouyer, Thomas Brihaye, Mickael Randour, Cédric Rivière, and Pierre Vandenhove. Decisiveness of stochastic systems and its application to hybrid models. In Davide Bresolin and Jean-François Raskin, editors, Proceedings of the 11th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF'20), volume 326 of Electronic Proceedings in Theoretical Computer Science, 2020. Google Scholar
  11. Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal strategies in priced timed game automata. In Kamal Lodaya and Meena Mahajan, editors, FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science, pages 148-160, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  12. Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. In Proceedings of the 26th International Conference on Concurrency Theory (CONCUR'15), volume 42 of Leibniz International Proceedings in Informatics, pages 311-324. Leibniz-Zentrum für Informatik, 2015. Google Scholar
  13. Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In Paul Pettersson and Wang Yi, editors, Formal Modeling and Analysis of Timed Systems, pages 49-64, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. Google Scholar
  14. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple priced timed games are not that simple. In Proceedings of the 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'15), volume 45 of LIPIcs, pages 278-292. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015. Google Scholar
  15. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games. Acta Informatica, 54(1):85-125, 2017. Google Scholar
  16. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In 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, pages 162-178, 2017. Google Scholar
  17. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic approximation of weighted timed games. In Sumit Ganguly and Paritosh Pandya, editors, Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'18), volume 122 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:16. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2018. Google Scholar
  18. Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Trading infinite memory for uniform randomness in timed games. In Hybrid Systems: Computation and Control, 11th International Workshop, HSCC 2008, St. Louis, MO, USA, April 22-24, 2008. Proceedings, pages 87-100, 2008. Google Scholar
  19. Marcin Jurdziński and Ashutosh Trivedi. Reachability-time games on timed automata. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP'07), volume 4596 of LNCS, pages 838-849. Springer, 2007. Google Scholar
  20. Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Reaching your goal optimally by playing at random with no memory. In Igor Konnov and Laura Kovács, editors, Proceedings of the 31st International Conference on Concurrency Theory (CONCUR 2020), volume 171 of LIPIcs, pages 26:1-26:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  21. Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Playing stochastically in weighted timed games to emulate memory. Technical Report 2105.00984, arXiv, 2021. URL: http://arxiv.org/abs/2105.00984.
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