Nested timed automata with various clocks

It is a great challenge to analyze a timed system extended with recursions,e.g.interrupt,since two dimensions of infinity,an unbounded stack,dense time recorded by clocks,occur in such a system.Furthermore,when investigating a recursive timed system,various types of clocks,such as global clocks,local clocks,frozen clocks,should be taken into consideration.The mixture of different types of clocks affects the expressiveness of recursive timed models.This paper gives detailed and complete investigation on the decidability results of a recursive timed system with different kinds of clocks,under a model named nested timed automata.These results can be naturally extended to other recursive timed systems.

It is a great challenge to analyze a timed system extended with recursions,e．g．interrupt,sincetwo dimensions of infinity,anunbounded stack,dense timer ecorded by clocks,occur in such asystem．