An Over-Approximation Forward Analysis for Nested Timed Automata

Nested timed automata (NeTAs), proposed by Li et al. are a pushdown system whose stack symbols are timed automata (TAs). With this formal models, we can model and analyze complex real-time frameworks with recursive context switches. The reachability problem of NeTAs is proved to be decidable, via encoding NeTAs to dense timed pushdown automata (DTPDAs). This paper gives a forward algorithm for reachability problem of NeTAs, by dividing the problem into two phases and integrating these two corresponding results. One phase is the reachability checking for the stack contents (i.e. TAs) and another is the state reachability problem for the TAs nested in an NeTA. The algorithm neglects time accumulation during context switches and thus an over-approximation of the original problem. As the result, the algorithm gains soundness in the sense that there exists one corresponding timed trace in the NeTA when the approximation has a timed trace to the state in less time-complexity.