Document Open Access Logo

Symbolic Approximation of Weighted Timed Games

Authors Damien Busatto-Gaston, Benjamin Monmege , Pierre-Alain Reynier

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2018.28.pdf
  • Filesize: 0.52 MB
  • 16 pages

Document Identifiers

Author Details

Damien Busatto-Gaston
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Benjamin Monmege
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France
Pierre-Alain Reynier
  • Aix Marseille Univ, Université de Toulon, CNRS, LIS, Marseille, France

Funding

This work has been funded by the DeLTA project (ANR-16-CE40-0007).

Cite As Get BibTex

Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.FSTTCS.2018.28

Abstract

Weighted timed games are zero-sum games played by two players on a timed automaton equipped with weights, where one player wants to minimise the accumulated weight while reaching a target. Weighted timed games are notoriously difficult and quickly undecidable, even when restricted to non-negative weights. For non-negative weights, the largest class that can be analysed has been introduced by Bouyer, Jaziri and Markey in 2015. Though the value problem is undecidable, the authors show how to approximate the value by considering regions with a refined granularity. In this work, we extend this class to incorporate negative weights, allowing one to model energy for instance, and prove that the value can still be approximated, with the same complexity. In addition, we show that a symbolic algorithm, relying on the paradigm of value iteration, can be used as an approximation schema on this class.

Subject Classification

ACM Subject Classification
  • Theory of computation → Algorithmic game theory
  • Theory of computation → Timed and hybrid models
  • Theory of computation → Quantitative automata
Keywords
  • Weighted timed games
  • Real-time systems
  • Game theory
  • Approximation

Metrics

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

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 G. Larsen, Judi Romijn, and Frits W. Vaandrager. Minimum-cost Reachability for Priced Timed Automata. In Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01), volume 2034 of LNCS, pages 147-161. Springer, 2001. Google Scholar
  6. 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
  7. Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved Undecidability Results on Weighted Timed Automata. Information Processing Letters, 98(5):188-194, 2006. Google Scholar
  8. Patricia Bouyer, Ed Brinksma, and Kim G. Larsen. Optimal Infinite Scheduling for Multi-Priced Timed Automata. Formal Methods in System Design, 32(1):3-23, 2008. Google Scholar
  9. Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal Strategies in Priced Timed Game Automata. In Proceedings of the 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), volume 3328 of LNCS, pages 148-160. Springer, 2004. Google Scholar
  10. 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. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.311.
  11. Romain Brenguier, Franck Cassez, and Jean-François Raskin. Energy and mean-payoff timed games. In 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC'14, Berlin, Germany, April 15-17, 2014, pages 283-292. ACM, 2014. Google Scholar
  12. Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On Optimal Timed Strategies. In Proceedings of the Third international conference on Formal Modeling and Analysis of Timed Systems (FORMATS'05), volume 3829 of LNCS, pages 49-64. Springer, 2005. Google Scholar
  13. 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. URL: http://dx.doi.org/10.4230/LIPIcs.FSTTCS.2015.278.
  14. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege. Pseudopolynomial Iterative Algorithm to Solve Total-Payoff Games and Min-Cost Reachability Games. Acta Informatica, 2016. URL: http://dx.doi.org/10.1007/s00236-016-0276-z.
  15. Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding Negative Prices to Priced Timed Games. In Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14), volume 8704, pages 560-575. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-44584-6_38.
  16. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal Reachability in Divergent Weighted Timed Games. In Javier Esparza and Andrzej S. Murawski, editors, Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17), volume 10203 of Lecture Notes in Computer Science, pages 162-178, Uppsala, Sweden, April 2017. Springer. URL: http://dx.doi.org/10.1007/978-3-662-54458-7_10.
  17. Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A Faster Algorithm for Solving One-Clock Priced Timed Games. In Proceedings of the 24th International Conference on Concurrency Theory (CONCUR'13), volume 8052 of LNCS, pages 531-545. Springer, 2013. Google Scholar
  18. 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
  19. Michał Rutkowski. Two-Player Reachability-Price Games on Single-Clock Timed Automata. In Proceedings of the Ninth Workshop on Quantitative Aspects of Programming Languages (QAPL'11), volume 57 of EPTCS, pages 31-46, 2011. 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 About DROPS Imprint Privacy Contact