Document Open Access Logo

On the Value Problem in Weighted Timed Games

Authors Patricia Bouyer, Samy Jaziri, Nicolas Markey

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.311.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Patricia Bouyer
Samy Jaziri
Nicolas Markey

Cite AsGet BibTex

Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the Value Problem in Weighted Timed Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 311-324, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.311

Abstract

A weighted timed game is a timed game with extra quantitative information representing e.g. energy consumption. Optimizing the weight for reaching a target is a natural question, which has already been investigated for ten years. Existence of optimal strategies is known to be undecidable in general, and only very restricted classes of games have been identified for which optimal weight and almost-optimal strategies can be computed. In this paper, we show that the value problem is undecidable in weighted timed games. We then introduce a large subclass of weighted timed games (for which the undecidability proof above applies), and provide an algorithm to compute arbitrary approximations of the value in such games. To the best of our knowledge, this is the first approximation scheme for an undecidable class of weighted timed games.
Keywords
  • Timed games
  • undecidability
  • 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 in weighted timed games. In ICALP'04, volume 3142 of LNCS, pages 122-133. Springer, 2004. Google Scholar
  2. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho. Hybrid automata: an algorithmic approach to specification and verification of hybrid systems. In HSCC'91-'92, volume 736 of LNCS, pages 209-229. Springer, 1993. Google Scholar
  3. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  4. Rajeev Alur, Salvatore La Torre, and George J. Pappas. Optimal paths in weighted timed automata. In HSCC'01, volume 2034 of LNCS, pages 49-62. Springer, 2001. Google Scholar
  5. Eugene Asarin, Oded Maler, Amir Pnueli, and Joseph Sifakis. Controller synthesis for timed automata. In Proc. IFAC Symp. System Structure & Control, pages 469-474. Elsevier, 1998. Google Scholar
  6. Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim G. Larsen, Paul Pettersson, Judi Romijn, and Frits Vaandrager. Minimum-cost reachability for priced timed automata. In HSCC'01, volume 2034 of LNCS, pages 147-161. Springer, 2001. Google Scholar
  7. Gerd Behrmann, Kim G. Larsen, and Jacob I. Rasmussen. Optimal scheduling using priced timed automata. ACM Sigmetrics Performance Eval. Review, 32(4):34-40, 2005. Google Scholar
  8. Patricia Bouyer, Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On the optimal reachability problem. Formal Methods in System Design, 31(2):135-175, 2007. Google Scholar
  9. Patricia Bouyer, Thomas Brihaye, and Nicolas Markey. Improved undecidability results on weighted timed automata. Information Processing Letters, 98(5):188-194, 2006. Google Scholar
  10. Patricia Bouyer, Ed Brinksma, and Kim G. Larsen. Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design, 32(1):2-23, 2008. Google Scholar
  11. Patricia Bouyer, Franck Cassez, Emmanuel Fleury, and Kim G. Larsen. Optimal strategies in priced timed game automata. In FSTTCS'04, volume 3328 of LNCS, pages 148-160. Springer, 2004. Google Scholar
  12. Patricia Bouyer, Samy Jaziri, and Nicolas Markey. On the value problem in weighted timed games. Research Report LSV-14-12, Laboratoire Spécification et Vérification, ENS Cachan, France, October 2014. 24 pages. Google Scholar
  13. Patricia Bouyer, Kim G. Larsen, Nicolas Markey, and Jacob I. Rasmussen. Almost optimal strategies in one-clock priced timed automata. In FSTTCS'06, volume 4337 of LNCS, pages 345-356. Springer, 2006. Google Scholar
  14. Thomas Brihaye, Véronique Bruyère, and Jean-François Raskin. On optimal timed strategies. In FORMATS'05, volume 3821 of LNCS, pages 49-64. Springer, 2005. Google Scholar
  15. Thomas Brihaye, Gilles Geeraerts, Shankara Narayanan Krishna, Lakshmi Manasa, Benjamin Monmege, and Ashutosh Trivedi. Adding negative prices to priced timed games. In CONCUR'14, volume 8704 of LNCS, pages 560-575. Springer, 2014. Google Scholar
  16. Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, and Mariëlle Stoelinga. The element of surprise in timed games. In Roberto Amadio and Denis Lugiez, editors, CONCUR'03, volume 2761 of LNCS, pages 142-156. Springer, 2003. Google Scholar
  17. Thomas Dueholm Hansen, Rasmus Ibsen-Jensen, and Peter Bro Miltersen. A faster algorithm for solving one-clock priced timed games. In CONCUR'13, volume 8052 of LNCS, pages 531-545. Springer, 2013. Google Scholar
  18. Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94-124, 1998. Google Scholar
  19. Salvatore La Torre, Supratik Mukhopadhyay, and Aniello Murano. Optimal-reachability and control for acyclic weighted timed automata. In TCS'02, volume 223 of IFIP Conf. Proc., pages 485-497. Kluwer, 2002. Google Scholar
  20. Donald A. Martin. Borel determinacy. Annals of Mathematics, 102:363-371, 1975. Google Scholar
  21. Marvin Minsky. Computation: Finite and Infinite Machines. Prentice Hall, 1967. Google Scholar
  22. Michał Rutkowski. Two-player reachability-price games on single-clock timed automata. In QAPL'11, volume 57 of ENTCS, 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 Imprint Privacy Contact