Document Open Access Logo

Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games

Author Isa Vialard

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.33.pdf
  • Filesize: 0.99 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Timed and hybrid models
Keywords
  • Weighted timed games
  • decidability
  • real-time systems

Metrics

Abstract

The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When restrained to wtgs with non-negative weight, this problem is known to be undecidable for weighted timed games with three or more clocks, and decidable for one-clock wtgs. The Value Problem for two-clock non-negative wtgs, which remained stubbornly open for a decade, was recently shown to be undecidable. In this paper, we show that the Value Problem is decidable when considering two-clock almost non-Zeno wtgs.

Cite As Get BibTex

Isa Vialard. Deciding the Value of Two-Clock Almost Non-Zeno Weighted Timed Games. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.33

Author Details

Isa Vialard
  • Max Planck Institute for Informatics, Saarland Informatics Campus, Saarbrücken, Germany

Acknowledgements

I want to thank Quentin Guilmant for his help in formalizing the proofs in Appendix A.1.

References

  1. Rajeev Alur, Mikhail Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella, editors, Automata, Languages and Programming, pages 122-133, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-540-27836-8_13.
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theor. Comput. Sci., 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  3. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, and Frits W. Vaandrager. Minimum-cost reachability for priced timed automata. In Maria Domenica Di Benedetto and Alberto L. Sangiovanni-Vincentelli, editors, Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Proceedings, volume 2034 of Lecture Notes in Computer Science, pages 147-161, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-45351-2_15.
  4. Patricia Bouyer, Ed Brinkshma, and Kim G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods Syst. Des., 32:3-23, 2008. URL: https://doi.org/10.1007/s10703-007-0043-4.
  5. Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim Guldstrand 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, 24th International Conference, Chennai, India, December 16-18, 2004, Proceedings, volume 3328 of Lecture Notes in Computer Science, pages 148-160, Berlin, Heidelberg, 2004. Springer. URL: https://doi.org/10.1007/978-3-540-30538-5_13.
  6. Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In Luca Aceto and David de Frutos Escrig, editors, 26th International Conference on Concurrency Theory (CONCUR 2015), volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pages 311-324, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2015.311.
  7. Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost optimal strategies in one clock priced timed games. In S. Arun-Kumar and Naveen Garg, editors, FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, volume 4337 of Lecture Notes in Computer Science, pages 345-356, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11944836_32.
  8. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. One-clock priced timed games with negative weights. Logical Methods in Computer Science, Volume 18, Issue 3, August 2022. URL: https://doi.org/10.46298/lmcs-18(3:17)2022.
  9. 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, February 2017. URL: https://doi.org/10.1007/s00236-016-0276-z.
  10. Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding negative prices to priced timed games. CoRR, abs/1404.5894, 2014. URL: https://doi.org/10.48550/arXiv.1404.5894.
  11. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures, pages 162-178, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-54458-7_10.
  12. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. In Sumit Ganguly and Paritosh Pandya, editors, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), volume 122 of Leibniz International Proceedings in Informatics (LIPIcs), pages 28:1-28:16, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2018.28.
  13. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal controller synthesis for timed systems. Log. Methods Comput. Sci., 19(1), 2023. URL: https://doi.org/10.46298/lmcs-19(1:20)2023.
  14. Quentin Guilmant and Joël Ouaknine. Inaproximability in Weighted Timed Games. In Rupak Majumdar and Alexandra Silva, editors, 35th International Conference on Concurrency Theory (CONCUR 2024), volume 311 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1-27:15, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.27.
  15. Quentin Guilmant, Joël Ouaknine, and Isa Vialard. The value problem for weighted timed games with two clocks is undecidable, 2025. URL: https://doi.org/10.48550/arXiv.2507.10550.
  16. Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of one-clock weighted timed games with arbitrary weights. CoRR, abs/2207.01608, 2022. URL: https://doi.org/10.48550/arXiv.2207.01608.
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