HIERARCHICAL MODELS OF TIMED CONCURRENT SYSTEMS: COMPOSITIONAL SEMANTICS

In the paper, we present the timed extension of the hierarchical state machines with the compositional semantics ensuring that the semantics of the model can be determined from the semantics of its components. We proposed the compositional semantics of traces with the goal of its successive utilization in the analysis and verification of the model properties. At the end of the paper, we discussed the computational complexity of the reachability problem, and its decomposition to subproblems with the lower complexity as the consequence of the compositional semantics and state refinement.