A.: Emptiness and Universality Problems in Timed Automata with Positive Frequency

Abstract. The languages of infinite timed words accepted by timed au-tomata are traditionally defined using Büchi-like conditions. These ac-ceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. We study various properties of timed languages accepted with positive frequency, and in particular the empti-ness and universality problems.