Weighing Obese Timed Languages

The bandwidth of a timed language characterizes the quantity of information per time unit (with a finite observation precision $\varepsilon$). Obese timed automata have an unbounded frequency of events and produce information at the maximal possible rate. In this article, we compute the bandwidth of any such automaton in the form $\approxα/\varepsilon$. Our approach reduces the problem to computing the best reward-to-time ratio in a weighted timed graph constructed from the given timed automaton, with weights corresponding to the entropy of auxiliary finite automata.