Document Open Access Logo

Inaproximability in Weighted Timed Games

Authors Quentin Guilmant , Joël Ouaknine

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2024.27.pdf
  • Filesize: 1.35 MB
  • 15 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • Weighted timed games
  • approximation
  • undecidability

Metrics

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

Abstract

We consider two-player, turn-based weighted timed games played on timed automata equipped with (positive and negative) integer weights, in which one player seeks to reach a goal location whilst minimising the cumulative weight of the underlying path. Although the value problem for such games (is the value of the game below a given threshold?) is known to be undecidable, the question of whether one can approximate this value has remained a longstanding open problem. In this paper, we resolve this question by showing that approximating arbitrarily closely the value of a given weighted timed game is computationally unsolvable.

Cite As Get BibTex

Quentin Guilmant and Joël Ouaknine. Inaproximability in Weighted Timed Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 27:1-27:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CONCUR.2024.27

Author Details

Quentin Guilmant
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany
Joël Ouaknine
  • Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • Ouaknine, Joël: Also affiliated with Keble College, Oxford as https://emmy.network/ Fellow, and supported by DFG grant 389792660 as part of https://perspicuous-computing.science.

References

  1. Rajeev Alur, Mikhail Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In ICALP, volume 3142 of Lecture Notes in Computer Science, pages 122-133. Springer, 2004. Google Scholar
  2. Rajeev Alur and Thomas A. Henzinger. Modularity for timed and hybrid systems. In CONCUR, volume 1243 of Lecture Notes in Computer Science, pages 74-88. Springer, 1997. Google Scholar
  3. Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved undecidability results on weighted timed automata. Inf. Process. Lett., 98(5):188-194, 2006. Google Scholar
  4. Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand Larsen. Optimal strategies in priced timed game automata. In FSTTCS, volume 3328 of Lecture Notes in Computer Science, pages 148-160. Springer, 2004. Google Scholar
  5. Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. In CONCUR, volume 42 of LIPIcs, pages 311-324. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  6. Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost optimal strategies in one clock priced timed games. In FSTTCS, volume 4337 of Lecture Notes in Computer Science, pages 345-356. Springer, 2006. Google Scholar
  7. Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In FORMATS, volume 3829 of Lecture Notes in Computer Science, pages 49-64. Springer, 2005. Google Scholar
  8. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. Simple priced timed games are not that simple. In FSTTCS, volume 45 of LIPIcs, pages 278-292. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  9. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. One-clock priced timed games with negative weights. Log. Methods Comput. Sci., 18(3), 2022. Google Scholar
  10. Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding negative prices to priced timed games. In CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 560-575. Springer, 2014. Google Scholar
  11. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 162-178, 2017. Google Scholar
  12. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic approximation of weighted timed games. In FSTTCS, volume 122 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. Google Scholar
  13. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal controller synthesis for timed systems. Log. Methods Comput. Sci., 19(1), 2023. Google Scholar
  14. Anne Condon and Richard J. Lipton. On the complexity of space bounded interactive proofs (extended abstract). In FOCS, pages 462-467. IEEE Computer Society, 1989. Google Scholar
  15. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In CONCUR, volume 2761 of Lecture Notes in Computer Science, pages 142-156. Springer, 2003. Google Scholar
  16. Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A faster algorithm for solving one-clock priced timed games. In CONCUR, volume 8052 of Lecture Notes in Computer Science, pages 531-545. Springer, 2013. Google Scholar
  17. Thomas A. Henzinger, Benjamin Horowitz, and Rupak Majumdar. Rectangular hybrid games. In CONCUR, volume 1664 of Lecture Notes in Computer Science, pages 320-335. Springer, 1999. Google Scholar
  18. Omid Madani, Steve Hanks, and Anne Condon. On the undecidability of probabilistic planning and related stochastic optimization problems. Artif. Intell., 147(1-2):5-34, 2003. Google Scholar
  19. Oded Maler, Amir Pnueli, and Joseph Sifakis. On the synthesis of discrete controllers for timed systems (an extended abstract). In STACS, volume 900 of Lecture Notes in Computer Science, pages 229-242. Springer, 1995. Google Scholar
  20. Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of one-clock weighted timed games with arbitrary weights. In CONCUR, volume 243 of LIPIcs, pages 15:1-15:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  21. Joël Ouaknine, Alexander Rabinovich, and James Worrell. Time-bounded verification. In CONCUR, volume 5710 of Lecture Notes in Computer Science, pages 496-510. Springer, 2009. Google Scholar
  22. Michal Rutkowski. Two-player reachability-price games on single-clock timed automata. In QAPL, volume 57 of EPTCS, pages 31-46, 2011. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact