Document Open Access Logo

Decidability of One-Clock Weighted Timed Games with Arbitrary Weights

Authors Benjamin Monmege , Julie Parreaux, Pierre-Alain Reynier

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.15.pdf
  • Filesize: 0.9 MB
  • 22 pages

Document Identifiers

Author Details

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

Funding

This work was partially funded by ANR project Ticktac (ANR-18-CE40-0015) and ANR project DeLTA (ANR-16-CE40-0007).

Cite As Get BibTex

Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of One-Clock Weighted Timed Games with Arbitrary Weights. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 15:1-15:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CONCUR.2022.15

Abstract

Weighted Timed Games (WTG for short) are the most widely used model to describe controller synthesis problems involving real-time issues. Unfortunately, they are notoriously difficult, and undecidable in general. As a consequence, one-clock WTG has attracted a lot of attention, especially because they are known to be decidable when only non-negative weights are allowed. However, when arbitrary weights are considered, despite several recent works, their decidability status was still unknown. In this paper, we solve this problem positively and show that the value function can be computed in exponential time (if weights are encoded in unary).

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
  • Timed automata

Metrics

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

Related Versions

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. URL: https://doi.org/10.1007/978-3-540-27836-8_13.
  2. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. URL: https://doi.org/10.1016/0304-3975(94)90010-8.
  3. 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. URL: https://doi.org/10.1007/3-540-48983-5_6.
  4. Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime. Uppaal-tiga: Time for playing games! In Werner Damm and Holger Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), volume 4590 of LNCS, pages 121-125. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73368-3_14.
  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. URL: https://doi.org/10.1007/3-540-45351-2_15.
  6. Béatrice Bérard, Antoine Petit, Volker Diekert, and Paul Gastin. Characterization of the expressive power of silent transitions in timed automata. Fundamenta Informaticae, 36(2-3):145-182, 1998. URL: https://doi.org/10.3233/FI-1998-36233.
  7. Patricia Bouyer. Erratum to the FSTTCS'04 paper "optimal strategies in priced timed game automata". Personal Communication, 2016. Google Scholar
  8. 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. URL: https://doi.org/10.1007/978-3-540-30538-5_13.
  9. 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: https://doi.org/10.4230/LIPIcs.CONCUR.2015.311.
  10. Patricia Bouyer, Kim G. 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, pages 345-356, Berlin, Heidelberg, 2006. Springer. URL: https://doi.org/10.1007/11944836_32.
  11. 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. URL: https://doi.org/10.1007/11603009_5.
  12. 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: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.278.
  13. Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, and Benjamin Monmege. One-clock priced timed games with negative weights. Research Report 2009.03074, arXiv, 2021. Google Scholar
  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, 54(1):85-125, February 2017. URL: https://doi.org/10.1007/s00236-016-0276-z.
  15. Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier. Optimal reachability in divergent weighted timed games. In Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2017), LNCS, pages 162-178. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_10.
  16. John Fearnley, Rasmus Ibsen-Jensen, and Rahul Savani. One-clock priced timed games are PSPACE-hard. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Sciences (LICS'20), pages 397-409. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394772.
  17. Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A faster algorithm for solving one-clock priced timed games. In Pedro R. D'Argenio and Hernán C. Melgratti, editors, Proceedings of the 24th International Conference on Concurrency Theory (CONCUR'13), volume 8052 of Lecture Notes in Computer Science, pages 531-545. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40184-8_37.
  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. François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. Model checking timed automata with one or two clocks. In Proceedings of CONCUR'04, pages 387-401, 2004. URL: https://doi.org/10.1007/978-3-540-28644-8_25.
  20. Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Playing Stochastically in Weighted Timed Games to Emulate Memory. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of LIPIcs, pages 137:1-137:17, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.137.
  21. Benjamin Monmege, Julie Parreaux, and Pierre-Alain Reynier. Decidability of one-clock weighted timed games with arbitrary weights. Research Report 2207.01608, arXiv, 2022. URL: http://arxiv.org/abs/2207.01608.
  22. 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