Automata with Timers

TL;DR

This paper investigates deterministic finite-state automata with timers, analyzing their reachability complexity and conditions for avoiding races, which are crucial for modeling and learning such timed automata efficiently.

Contribution

It provides complexity results for configuration reachability and race avoidance decision problems in automata with timers, advancing understanding of their computational properties.

Findings

Reachability problem is PSPACE-complete.

Race avoidance decision problem is in 3EXP and PSPACE-hard.

Characterization of race-avoiding automata is established.

Abstract

In this work, we study properties of deterministic finite-state automata with timers, a subclass of timed automata proposed by Vaandrager et al. as a candidate for an efficiently learnable timed model. We first study the complexity of the configuration reachability problem for such automata and establish that it is PSPACE-complete. Then, as simultaneous timeouts (we call these, races) can occur in timed runs of such automata, we study the problem of determining whether it is possible to modify the delays between the actions in a run, in a way to avoid such races. The absence of races is important for modelling purposes and to streamline learning of automata with timers. We provide an effective characterization of when an automaton is race-avoiding and establish that the related decision problem is in 3EXP and PSPACE-hard.