Automata with Timers
V\'eronique Bruy\`ere, Guillermo A. P\'erez, Ga\"etan Staquet, Frits, W. Vaandrager

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.
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.
Taxonomy
TopicsMachine Learning and Algorithms · semigroups and automata theory · Formal Methods in Verification
