Revisiting Robustness in Priced Timed Games

Authors Shibashis Guha, Shankara Narayanan Krishna, Lakshmi Manasa, Ashutosh Trivedi



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2015.261.pdf
  • Filesize: 0.65 MB
  • 17 pages

Document Identifiers

Author Details

Shibashis Guha
Shankara Narayanan Krishna
Lakshmi Manasa
Ashutosh Trivedi

Cite AsGet BibTex

Shibashis Guha, Shankara Narayanan Krishna, Lakshmi Manasa, and Ashutosh Trivedi. Revisiting Robustness in Priced Timed Games. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 261-277, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.FSTTCS.2015.261

Abstract

Priced timed games are optimal-cost reachability games played between two players---the controller and the environment---by moving a token along the edges of infinite graphs of configurations of priced timed automata. The goal of the controller is to reach a given set of target locations as cheaply as possible, while the goal of the environment is the opposite. Priced timed games are known to be undecidable for timed automata with 3 or more clocks, while they are known to be decidable for automata with 1 clock. In an attempt to recover decidability for priced timed games Bouyer, Markey, and Sankur studied robust priced timed games where the environment has the power to slightly perturb delays proposed by the controller. Unfortunately, however, they showed that the natural problem of deciding the existence of optimal limit-strategy---optimal strategy of the controller where the perturbations tend to vanish in the limit---is undecidable with 10 or more clocks. In this paper we revisit this problem and improve our understanding of the decidability of these games. We show that the limit-strategy problem is already undecidable for a subclass of robust priced timed games with 5 or more clocks. On a positive side, we show the decidability of the existence of almost optimal strategies for the same subclass of one-clock robust priced timed games by adapting a classical construction by Bouyer at al. for one-clock priced timed games.
Keywords
  • Priced Timed Games
  • Decidability
  • Optimal strategies
  • Robustness

Metrics

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

References

  1. R. Alur, M. Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In J. Díaz, J. Karhumäki, A. Lepistö, and D Sannella, editors, Proc. ICALP'04, volume 3142 of LNCS, pages 122-133. Springer, 2004. Google Scholar
  2. G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson, J. Romijn, and F. W. Vaandrager. Minimum-cost reachability for priced timed automata. In M. D. Di Benedetto and A. L. Sangiovanni-Vincentelli, editors, Proc. HSCC'01, volume 2034 of LNCS, pages 147-161, Heidelberg, 2001. Springer. Google Scholar
  3. P. Bouyer, T. Brihaye, and N. Markey. Improved undecidability results on weighted timed automata. Information Processing Letters, 98:188-194, 2006. Google Scholar
  4. P. Bouyer, F. Cassez, E. Fleury, and K. G. Larsen. Optimal strategies in priced timed game automata. In K. Lodaya and M. Mahajan, editors, FSTTCS'04, volume 3328 of LNCS, pages 148-160. Springer, 2004. Google Scholar
  5. Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey, and Jacob Illum Rasmussen. Almost optimal strategies in one clock priced timed games. In FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, pages 345-356, 2006. Google Scholar
  6. Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust reachability in timed automata: A game-based approach. In Automata, Languages, and Programming, volume 7392 of Lecture Notes in Computer Science, pages 128-140. Springer, 2012. Google Scholar
  7. Patricia Bouyer, Nicolas Markey, and Ocan Sankur. Robust weighted timed automata and games. In Víctor Braberman and Laurent Fribourg, editors, Proceedings of the 11th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS'13), volume 8053 of Lecture Notes in Computer Science, pages 31-46, Buenos Aires, Argentina, August 2013. Springer. Google Scholar
  8. T. Brihaye, V. Bruyère, and J. Raskin. On optimal timed strategies. In P. Pettersson and W. Yi, editors, Proc. FORMATS'05, volume 3829 of LNCS, pages 49-64. Springer, 2005. Google Scholar
  9. Krishnendu Chatterjee, Thomas A. Henzinger, and Vinayak S. Prabhu. Timed parity games: Complexity and robustness. Logical Methods in Computer Science, 7(4), 2011. Google Scholar
  10. Shibashis Guha, Shankara Narayanan Krishna, Lakshmi Manasa, and Ashutosh Trivedi. Revisiting robustness in priced timed games. CoRR, abs/1507.05787, 2015. Google Scholar
  11. T. D. Hansen, R. Ibsen-Jensen, and P. B. Miltersen. A faster algorithm for solving one-clock priced timed games. In PedroR. D’Argenio and Hernán Melgratti, editors, CONCUR 2013 – Concurrency Theory, volume 8052 of Lecture Notes in Computer Science, pages 531-545. Springer, 2013. Google Scholar
  12. N. Markey. Robustness in real-time systems. In Industrial Embedded Systems (SIES), 2011 6th IEEE International Symposium on, pages 28-34, June 2011. Google Scholar
  13. Michal Rutkowski. Two-player reachability-price games on single-clock timed automata. In QAPL, pages 31-46, 2011. Google Scholar
  14. Ocan Sankur, Patricia Bouyer, Nicolas Markey, and Pierre-Alain Reynier. Robust controller synthesis in timed automata. In CONCUR 2013 – Concurrency Theory, volume 8052 of Lecture Notes in Computer Science, pages 546-560. Springer, 2013. 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