As an extension of Timed Automata (TAs), Updatable Timed Automata (UTAs) proposed by Bouyer et al. have the ability to update clocks in a more elaborate way than simply reset them to zero. The reachability of general UTAs is undecidable, by regarding a pair of updatable clocks as counters updatable with incrementation and decrementation operations. This paper investigates the model of subclass of UTAs by restricting the number of updateable clocks. It is shown that the reachability of UTAs with one updatable clock (UTA1s) under diagonal-free constraints is decidable. The decidability is proved by treating a region of a UTA1 as an unbounded digiword, and encoding sets of digiwords that are accepted by a pushdown system where regions are generated on-the-fly on the stack.
展开▼
