Reachability in hierarchical machines

In this paper we study the reachability analysis problem for timed systems specified in a hierarchical manner. First we provide a formal model, called hierarchical extended Mealy machine with timer, input and output events, as well with input, output and context variables. Then we present a synchronous semantics of the model. A main feature of this model is that the crossing of superstates´ boundaries is forbidden, i.e., transitions between states in different superstates are not allowed. Finally we propose a reachability analysis method for finding (minimal) executions between configurations of a given deterministic hierarchical machine. Executions may require resetting of some constituent machines by entering some of their ancestor states. The algorithm exploits the hierarchical structure of the machine. The complexity of our algorithm is linear in R where R is the complexity of the reachability analysis of constituent machines.