Timed Automata with Periodic Clock Constraints

Abstract

The traditional constraints on the clocks of a timed automaton are based on real intervals, e. g., the value of a clock belongs to the interval $(0, 1)$. Here, we introduce a new set of constraints, which we call "periodic", and which are based on regularly repeated real intervals, e.g., the value modulo 2 of a clock belongs to the interval $(0,1)$ which means that it belongs to $(0,1)$ or $(2,3)$ or $(4,5)$ $\ldots$ Automata with these new constraints have greater expressive power than the automata with traditional sets while satisfiability remains decidable. We address questions concerning $\epsilon$-moves and determinism: simulation of automata with periodic constraints by automata with traditional constraints, properties of deterministic automata with periodic constraints (like closure under Boolean operations and decidability of the inclusion problem) and removal of $\epsilon$-moves under certain conditions. Then, we enrich our model by introducing "count-down" clocks and show that the expressive power is not increased. Finally, we study three special cases: 1) all transitions reset clocks, 2) no transition reset clocks, and 3) the time domain is discrete and prove the decidability of the inclusion problem under each of these hypotheses