An Alternative Definition for Timed Automata Composition

Due to the complexity and time-based aspects of modern systems, compositional verification and abstraction-based verification techniques have been proposed to deal with these issues by considering the verification of system components separately (composition) and working on more abstract structures (refinement). In this paper, we propose a revised definition of the product of timed automata (TA) and give a compositional semantics based on individual timed transition system (TTS) semantics. Moreover, we establish a new compositional refinement property where the refinement of timed systems composition is given by the refinement of each component. For this purpose, starting from the basic timed transition systems, we introduce an original composition operator endowed with good properties (associativity, trace inclusion, etc) and supporting communications via shared variables and synchronization of actions. Thereafter, we instantiate this framework for timed automata where we show how to associate such a TTS with two-levels static priority (committedness) to a TA and establish the compositionality theorem introduced by [5] with the mentioned refinement property.