Emptiness and Universality Problems in Timed Automata with Positive Frequency

TL;DR

This paper introduces a quantitative semantics for timed automata based on frequency, analyzing how much time is spent in accepting locations, and investigates the emptiness and universality problems under this new framework.

Contribution

It proposes a novel frequency-based semantics for timed automata and studies the associated emptiness and universality decision problems.

Findings

Frequency semantics provides a new way to evaluate timed automata behaviors.

The paper characterizes the decidability of emptiness and universality under positive frequency.

Results highlight differences from traditional Büchi-like acceptance conditions.

Abstract

The languages of infinite timed words accepted by timed automata are traditionally defined using Buchi-like conditions. These acceptance 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 emptiness and universality problems.