Average-Time Games on Timed Automata
Marcin Jurdzinski, Ashutosh Trivedi

TL;DR
This paper introduces a method to solve average-time games on timed automata by reducing them to average-price games, providing a new approach and complexity analysis for these infinite-state games.
Contribution
It presents a reduction technique for average-time games to finite graph average-price games and proves their determinacy and EXPTIME-completeness.
Findings
Reduction from average-time to average-price games
Elementary proof of determinacy for average-time games
EXPTIME-complete complexity for automata with two or more clocks
Abstract
An average-time game is played on the infinite graph of configurations of a finite timed automaton. The two players, Min and Max, construct an infinite run of the automaton by taking turns to perform a timed transition. Player Min wants to minimise the average time per transition and player Max wants to maximise it. A solution of average-time games is presented using a reduction to average-price game on a finite graph. A direct consequence is an elementary proof of determinacy for average-time games. This complements our results for reachability-time games and partially solves a problem posed by Bouyer et al., to design an algorithm for solving average-price games on priced timed automata. The paper also establishes the exact computational complexity of solving average-time games: the problem is EXPTIME-complete for timed automata with at least two clocks.
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.
