A Flattening Algorithm for Hierarchical Timed Automata

Abstract

We propose a coherent algorithm for the translation of hierarchical timed automata into networks of (planar) timed automata. This kind of translation is called flattening. The two types of timed automata are used in formal verification of real-time systems: systems of parallel interacting components whose execution essentially depends not only on the order of the events in the system, but also on the real time of these events. The concept of hierarchical timed automaton covers the syntactic variations that are used in existing studies and are non-comparable by their expressive power. The number of states in a flattened network of time automata is of the least order among the flattening results of existing studies.