Analysis of Timed Recursive State Machines

Abstract

The paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs). A TRSM is an indexed collection of Timed Automata allowed to invoke other Timed Automata (procedural calls). The classes of TRSMs are related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. A number of subclasses of TRSMs and EPTAs are considered and compared through bisimulation of their timed LTSs. It is shown that EPTAs and TRSMs can be used to recognize classes of timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case, but decidable for meaningful subclasses. The complexity is stated for a TRSMs subclass.