Mean-Payoff Games on Timed Automata
Shibashis Guha, Marcin Jurdzinski, Krishna S., Ashutosh, Trivedi

TL;DR
This paper investigates the computational complexity of mean-payoff games on timed automata, establishing undecidability results for three clocks and decidability for one clock with binary prices, using dynamic programming techniques.
Contribution
It refines previous undecidability results to three clocks and proves decidability for one-clock automata with binary prices, applying dynamic programming methods.
Findings
Undecidability of mean-payoff games with three clocks.
Decidability of these games on one-clock automata with binary prices.
Application of dynamic programming techniques to uncountable state spaces.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
