Shoji Yuen (Nagoya)

Reachability Analysis for Nested Timed Automata

A nested timed automaton (NeTA) is a pushdown system whose control
locations and stack alphabet are timed automata. Nested timed
automata behaves as the automaton on the stack top. NeTA switches
the top-most automaton either by pushing it to the stack and
starting a new instance of timed automata, or by popping up an
automaton from the stack. While being not on the top of the stack,
clocks are either proceeding or frozen. When all the clocks
proceed, the reachability problem is shown to be decidable by
translating a NeTA to a dense-time pushdown automata. We further
investigated NeTA with frozen clocks. It is shown that the
reachability problem is decidable even with a proceeding global
clock with value exchanges with local clocks. While, allowing more
than two global clocks with value exchanges with local clocks make
NeTA make the reachability undecidable. For the reachability
analysis for NeTA with frozen clocks, we translate NeTA to Well
Structured PDS by Cai and Ogawa.

(Joint work with Guoqiang Li and Mizuhito Ogawa.)