Mean-Payoff Games on Timed Automata
Document Open Access Logo

Mean-Payoff Games on Timed Automata

Authors Shibashis Guha, Marcin Jurdzinski, Shankara Narayanan Krishna, Ashutosh Trivedi

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.44.pdf
  • Filesize: 0.63 MB
  • 14 pages

Document Identifiers

Author Details

Shibashis Guha
Marcin Jurdzinski
Shankara Narayanan Krishna
Ashutosh Trivedi

Cite As Get BibTex

Shibashis Guha, Marcin Jurdzinski, Shankara Narayanan Krishna, and Ashutosh Trivedi. Mean-Payoff Games on Timed Automata. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 44:1-44:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSTTCS.2016.44

Abstract

Mean-payoff games on timed automata are played on the infinite weighted graph of configurations of priced timed automata between two players - Player Min and Player Max - by moving a token along the states of the graph to form an infinite run. The goal of Player Min is to minimize the limit average weight of the run, while the goal of the Player Max is the opposite. Brenguier, Cassez, and Raskin recently studied a variation of these games and showed that mean-payoff games are undecidable for timed automata with five or more clocks. We refine this result by proving the undecidability of mean-payoff games with three clocks. On a positive side, we show the decidability of mean-payoff games on one-clock timed automata with binary price-rates. A key contribution of this paper is the application of dynamic programming based proof techniques applied in the context of average reward optimization on an uncountable state and action space.

Subject Classification

Keywords
  • Timed Automata
  • Mean-Payoff Games
  • Controller-Synthesis

Metrics

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

References

  1. R. Alur, M. Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In Proc. of ICALP, pages 122-133. Springer, 2004. Google Scholar
  2. R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994. Google Scholar
  3. E. Asarin and O. Maler. As soon as possible: Time optimal control for timed automata. In F. W. Vaandrager and J. H. van Schuppen, editors, Proc. of HSCC, pages 19-30, 1999. Google Scholar
  4. H. Björklund, S. Sandberg, and S. Vorobyov. A combinatorial strongly subexponential strategy improvement algorithm for mean payoff games. In Proc. of MFCS, pages 673-685, 2004. Google Scholar
  5. P. Bouyer. Weighted timed automata: Model-checking and games. In Proc. of MFPS, volume 158, pages 3-17, 2006. Google Scholar
  6. P. Bouyer, T. Brihaye, M. Jurdzinski, R. Lazic, and M. Rutkowski. Average-price and reachability-price games on hybrid automata with strong resets. In FORMATS, volume 5215 of LNCS, pages 63-77, 2008. Google Scholar
  7. P. Bouyer, E. Brinksma, and K. G. Larsen. Staying alive as cheaply as possible. In Proc. of HSCC, volume 2993 of LNCS, pages 203-218. Springer, 2004. Google Scholar
  8. P. Bouyer, F. Cassez, E. Fleury, and K. G. Larsen. Optimal strategies in priced timed game automata. In Proc. of FSTTCS, volume 3328 of LNCS, pages 148-160. Springer, 2004. Google Scholar
  9. P. Bouyer, K. G. Larsen, and N. Markey. Lower-bound constrained runs in weighted timed automata. In Proc. of QEST, pages 128-137, 2012. URL: http://dx.doi.org/10.1109/QEST.2012.28.
  10. R. Brenguier, F. Cassez, and J. F. Raskin. Energy and mean-payoff timed games. In Proc. of HSCC, pages 283-292, 2014. URL: http://dx.doi.org/10.1145/2562059.2562116.
  11. T. Brihaye, G. Geeraerts, S. N. Krishna, L. Manasa, B. Monmege, and A. Trivedi. Adding negative prices to priced timed games. In Proc. of CONCUR, pages 560-575, 2014. Google Scholar
  12. E. Dynkin and A. Yushkevich. Controlled Markov Processes. Springer, 1979. Google Scholar
  13. A. Ehrenfeucht and A. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8:109-113, 1979. Google Scholar
  14. J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer, 1997. Google Scholar
  15. S. Guha, M. Jurdziński, S. N. Krishna, and A. Trivedi. Mean-payoff games on timed automata. CoRR, abs/1607.08480, 2016. URL: http://arxiv.org/abs/1607.08480.
  16. V. A. Gurvich, A. V. Karzanov, and L. G. Khachiyan. Cyclic games and an algorithm to find minimax cycle means in directed graphs. USSR Computational Mathematics and Mathematical Physics, 28:85-91, 1988. Google Scholar
  17. Thomas A. Henzinger. Quantitative reactive modeling and verification. Computer Science - Research and Development, 28(4):331-344, 2013. Google Scholar
  18. R. A. Howard. Dynamic Programming and Markov Processes. MIT Press, 1960. Google Scholar
  19. M. Jurdziński and A. Trivedi. Reachability-time games on timed automata. In Proc. of ICALP, pages 838-849. Springer, 2007. Google Scholar
  20. M. Jurdziński and A. Trivedi. Average-time games. In R. Hariharan, M. Mukund, and V. Vinay, editors, Proc. of FSTTCS, Dagstuhl Seminar Proceedings, 2008. Google Scholar
  21. M. L. Puterman. Markov Decision Processes: Disc. Stoc. Dynamic Prog. Wiley, 1994. Google Scholar
  22. P. J. Ramadge and W. M. Wonham. The control of discrete event systems. In IEEE, volume 77, pages 81-98, 1989. Google Scholar
  23. A. Trivedi. Competitive Optimisation on Timed Automata. PhD thesis, Department of Computer Science, The University of Warwick, 2009. Google Scholar
  24. U. Zwick and M. Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158:343-359, 1996. 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