Integer Reset Timed Automata: Clock Reduction and Determinizability

Abstract

In this paper, we propose a procedure that given an integer reset timed automaton (IRTA) $\mathcal{A}$, produces a language equivalent deterministic one clock IRTA $\mathcal{B}$ whose size is at most doubly exponential in the size of $\mathcal{A}$. We prove that this bound on the number of locations is tight. Further, if integer resets are used in stopwatch automata, a subclass of stopwatch automata which is closed under all boolean operations and for which reachability is decidable is obtained.

submitted to LATA 2010