Mean-Payoff Games on Timed Automata
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.
Timed Automata
Mean-Payoff Games
Controller-Synthesis
44:1-44:14
Regular Paper
Shibashis
Guha
Shibashis Guha
Marcin
Jurdzinski
Marcin Jurdzinski
Shankara Narayanan
Krishna
Shankara Narayanan Krishna
Ashutosh
Trivedi
Ashutosh Trivedi
10.4230/LIPIcs.FSTTCS.2016.44
R. Alur, M. Bernadsky, and P. Madhusudan. Optimal reachability for weighted timed games. In Proc. of ICALP, pages 122-133. Springer, 2004.
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
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.
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.
P. Bouyer. Weighted timed automata: Model-checking and games. In Proc. of MFPS, volume 158, pages 3-17, 2006.
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.
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.
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.
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.
http://dx.doi.org/10.1109/QEST.2012.28
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.
http://dx.doi.org/10.1145/2562059.2562116
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.
E. Dynkin and A. Yushkevich. Controlled Markov Processes. Springer, 1979.
A. Ehrenfeucht and A. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8:109-113, 1979.
J. Filar and K. Vrieze. Competitive Markov Decision Processes. Springer, 1997.
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.
http://arxiv.org/abs/1607.08480
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.
Thomas A. Henzinger. Quantitative reactive modeling and verification. Computer Science - Research and Development, 28(4):331-344, 2013.
R. A. Howard. Dynamic Programming and Markov Processes. MIT Press, 1960.
M. Jurdziński and A. Trivedi. Reachability-time games on timed automata. In Proc. of ICALP, pages 838-849. Springer, 2007.
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.
M. L. Puterman. Markov Decision Processes: Disc. Stoc. Dynamic Prog. Wiley, 1994.
P. J. Ramadge and W. M. Wonham. The control of discrete event systems. In IEEE, volume 77, pages 81-98, 1989.
A. Trivedi. Competitive Optimisation on Timed Automata. PhD thesis, Department of Computer Science, The University of Warwick, 2009.
U. Zwick and M. Paterson. The complexity of mean payoff games on graphs. Theoretical Computer Science, 158:343-359, 1996.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode