Nested Timed Automata with Frozen Clocks

A nested timed automaton (NeTA) is a pushdown system whose control locations and stack alphabet are timed automata (TAs). A control location describes a working TA, and the stack presents a pile of interrupted TAs. In NeTAs, all local clocks of TAs proceed uniformly also in the stack. This paper extends NeTAs with frozen local clocks (NeTAFs). All clocks of a TA in the stack can be either frozen or proceeding when it is pushed. A NeTA-F also allows global clocks adding to local clocks in the working TA, which can be referred and/or updated from the working TA. We investigate the reachability of NeTA-Fs showing that (1) the reachability with a single global clock is decidable, and (2) the reachability with multiple global clocks is undecidable.