A New Definition of Composition of LTIHA? Antonia Reißner[0000−0002−1282−1450] and Matthias Werner[0000−0002−3963−2246] TU Chemnitz Germany {antonia.reissner|matthias.werner}@informatik.tu-chemnitz.de Abstract. The aim of this paper is to solve some issues of linear time- invariant hybrid automata as defined in [9]. First these issues are ex- plained on a small example, before the revised definitions of linear time- invariant hybrid automata and their composition operator are presented. Furthermore it is shown that this new composition operator is commu- tative and associative. Keywords: Linear Time-Invariant Hybrid Automata · Composition · Hybrid Systems 1 Introduction Modern systems are becoming more and more complex and hence harder to formally analyze. Because of many catastrophes of well-tested systems in the past the importance of formal verification of systems is widely recognized. Since most modern systems - like embedded systems - have to interact with the phys- ical world but also make discrete computations, a model is needed which can represent both properties. These systems which have analogue (continuous) and digital (discrete) properties are called hybrid systems. A widely considered ap- proach to model a hybrid system is a hybrid automata. These automata are used for example in the field of embedded systems [6]. To model a system as a hybrid automaton all possible states of the sys- tem have to be known in advance. Since even small systems could have an immense number of states, modeling errors are quite likely. These considerably small mistakes would invalidate the verification. Hence it is favorable to design only smaller components with fewer states and afterwards construct the whole system using composition. This property allows to reuse automata which are already known, as well as to incorporate small changes in one of the components of the system with comparatively less effort. A general goal of composition is to transfer properties from the components of a system to the whole system. A special case of the hybrid automata are the so called linear hybrid au- tomata [2]. For a linear hybrid automaton, the change of a continuous variable ? Copyright c 2019 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). Antonia Reißner, Matthias Werner is described by a linear differential equation. These automata have many subcat- egories like the timed automata, rectangular automata or hybrid I/O automata. Many aspects of the class of linear hybrid automata are still unknown and in the focus of active research ([3],[4]). Linear time-invariant hybrid automata (LTIHA) and their composition were first defined by Akhundov et al. ([2],[9]) to model space missions. Properties with regard to the composition were discussed in [1]. In the current paper we are discussing drawbacks of the original approach for LTIHA. We suggest an alternative definition and show some properties of this composition. 2 Linear Time-Invariant Hybrid Automata In the first part of this section the original approach is analyzed and two main issues are explained. To overcome these issues a new definition of linear time- invariant hybrid automata and their composition operator is presented in the second part. In the last part the effects of changing the definitions are discussed. 2.1 Issues of the Original Approach The original definition of LTIHA [9] is based on events. However, in contrast to the typical concept of an event that is connected with an instantaneous change of a system state, events in [9] are associated with a duration. While this may be seen as a clumsy choice of terms, a more crucial issue is an ambiguity in the definition of these events: It is not clear from the definition, what the length of the so-called activation phase is in case of a composition. A further issue of the former composition operator is discussed using an ex- ample. Consider the following automata:1 g2c l1 l2 (l1 , l3 ) (l1 , l4 ) g1 g1c g4c g3c l3 l4 (l2 , l3 ) (l2 , l4 ) g2 g5c A guard is defined by [9] as a triple consisting of three sets. The first is a set of constraints, the second and third sets of events. The transition will only be taken if all constraints are fulfilled and all events in the second set are active. When the transition is taken the events in the third set will be set to active. Consider the guards g1 = (C1 , E1 , A1 ) and g2 = (C2 , E2 , A2 ) for 1 For the sake of shortness, we assume that the reader is aware of the concepts of [9]. A New Definition of Composition of LTIHA which E1 ∩ A2 = E2 ∩ A1 = ∅ holds. Then the resulting automaton contains the guards g1c = g4c = g1 = (C1 , E1 , A1 ), g2c = g5c = g2 = (C2 , E2 , A2 ) and g3c = (C1 ∪ C2 , E1 ∪ E2 , A1 ∪ A2 ) by definition of the composition operator. In this case when the events in the set E1 ∪ E2 are active and the constraints C1 ∪ C2 are fulfilled, there will always be three guards which are active. Hence this operator constructs a non-determinism that was not present in the former two automata. To overcome this problem guards were changed to two-valued functions mapping to one if a constraint is evaluated to true depending on the variables and their valuation. The new operator was constructed in such a way that if the guard of the diagonal transition is active none of the other guards can be active if there was no non-determinism in the former automata. To overcome the first issue described above, we suggest a modified approach for LTIHA, that enriches the state by additional variables. Their values at each time point are explicitly described by a function. Alterations of the value at discrete times take the role of events in the original model. 2.2 New Definition First the formal definition of the linear time-invariant hybrid automata and the corresponding composition operator will be given. To illustrate the changes the aforementioned example is modeled using the new definition. Definition 1. A linear time-invariant hybrid automaton is a six tuple H = (L, X, W, B, T, F) consisting of: – Set of locations L = {l1 , .., ln } – Set X of real valued state variables, decomposable in sets of internal state variables XI , external state variables XE with t ∈ XE and synchronization variables XS . The variable t denotes the time of the system. – A set of valuations W = {v | v : X × R → R, for t it holds that v(t, r1 ) = v(t, r2 )∀r1 , r2 ∈ R} consisting of functions v which map each variable x ∈ X to their value at time point v(t, r0 ) with r0 being any real number. This is abbreviated to tv = v(t, r0 ). The valuations for t and all elements in XE are neither determined nor influenced by the automaton, but given e.g. from the outside world. The valuations of the synchronization variables s ∈ XS have the form: ( 1 tv ∈ Es v(s, tv ) = 0 otherwise Where Es ⊆ R denotes the set of discrete time points at which a synchro- nization event occurs. Antonia Reißner, Matthias Werner – A set of constraints B depending on a subset M of the set of variables X and their valuation v. All elements in B have to be evaluable to either true (1) or false (0) for every valuation. For each element b in B there is a function ( 1 b evaluates to true gb (M, v) = 0 otherwise. The set containing these functions is called guard set C. – A set of transitions T ⊆ L×C×P(XS )×L containing transitions (l1 , g, N, l2 ) with l1 , l2 ∈ L, g ∈ C and N ∈ P(XS ) which can only be taken if g(M, v) = 1 holds. In this case M denotes a subset of the variable set X and v a valuation. The set N is a set of events which are generated if the transition is taken. If the transition is taken at the time point t̄v , then the valuation is modified to: ( 1 tv ∈ Es ∪ {t̄v } v(s, tv ) = 0 otherwise This holds for all variables s ∈ N . The set Es is extended to the set Es ∪{t̄v } – A set of flow functions F = {flx | ∀l ∈ L ∀x ∈ XI } containing functions which describe the change of each state variable for each location. These flow functions are solutions to linear ordinary differential equations. These equations have the form : f˙(t) = A · f (tv ) + b u(tv ). Where A and b are constants. The functions f (tv ) and u(tv ) can be vector valued functions. Definition 2. The state (lj , v) of a linear time-invariant hybrid automaton con- sists of the location lj ∈ L and the valuation v. These changes of the linear time-invariant hybrid automata enable a redef- inition of the corresponding composition operator. Without the change of the underlying automata the new composition operator would produce an automa- ton which is not necessarily a LTIHA. Definition 3. Two automata H 1 = (L1 , X 1 , W 1 , B 1 , T 1 , F 1 ) and H 2 = (L2 , X 2 , W 2 , B 2 , T 2 , F 2 ) can be composed using the operator || if ∀x ∈ X 1 ∩ X 2 : v 1 (x, tv1 ) = v 2 (x, tv2 ) holds. The resulting automaton H c = H 1 || H 2 equals (Lc , X c , W c , B c , T c , F c ) with the following properties: – The set of locations Lc equals L1 × L2 . – The set of variables X c is equal to X 1 ∪ X 2 and can be decomposed in the set of internal variables XIc = XI1 ∪ XI2 , A New Definition of Composition of LTIHA c 1 2 the set of external variables XE = XE ∪ XE \ XIc and the set of synchronization variables XS = XS ∪ XS2 . c 1 – The set W c consists of valuations v c having the form ( c v 1 (x, tvc ) x ∈ X 1 v (x, tvc ) = v 2 (x, tvc ) otherwise. – The set of constraints B c equals the set of all to true or false evaluable constraints over a subset of the set of variables X c and the valuation v c . The set C c is the set of two-valued functions which map to 1 if and only if the respective constraint evaluates to true. – Let (li1 , gb1 , N 1 , lk1 ) ∈ T 1 and (lj2 , gb2 , N 2 , ll2 ) ∈ T 2 be transitions in the cor- responding automata. • The transitions ((li1 , l2 ), gb1 ∧b22 , N 1 , (lk1 , l2 )) and ((l1 , lj2 ), gb2 ∧b11 , N 2 , (l1 , ll2 )) l l are elements of the set of transitions T c for all locations l2 ∈ L2 and l1 ∈ L1 . Let Bo1 (l1 ) be the set of the constraints bn of all guards gbn such that there exists ln ∈ L1 with (l1 , gbn , N, ln ) ∈ T 1 for any N ∈ P(XS1 ). The constraint b1l1 denotes ∧bi ∈Bo1 (l1 ) ¬bi . The new guard constraints b1 ∧ b2l2 and b2 ∧ b1l1 are defined by: b1 ∧ b2l2 (M, v c ) = b1 (M ∩ X 1 , v c |1 ) ∧ b2l2 (M ∩ X 2 , v c |2 ) b2 ∧ b1l1 (M, v c ) = b2 (M ∩ X 2 , v c |2 ) ∧ b1l1 (M ∩ X 1 , v c |1 ). With the valuation v c |2 : X 2 × R → R which is defined as ∀y ∈ X 2 , n ∈ R : v c |2 (y, n) = v c (y, n). The valuation v c |1 is defined analogously. • The transition ((li1 , lj2 ), gb1 ∧b2 , N 1 ∪ N 2 , (lk1 , ll2 )) is an element of T c with the guard constraint b1 ∧ b2 defined as: b1 ∧ b2 (M, v c ) = b1 (M ∩ X 1 , v c |1 ) ∧ b2 (M ∩ X 2 , v c |2 ). – The set F c consists of flow functions f(lx1 ,l2 ) . At the location (li1 , lj2 ) the equa- i j tion f(lx1 ,l2 ) = flx1 + flx2 holds. i j i j In the following table guards for one specific example based on the above example are given for both the new and the old definition. Old Notation New Notation g1 ({x ≤ 10}, {event1}, {event2}) (gb1 , {event2}) g2 ({x ≤ 10, y > 3}, {event3}, {event4}) (gb2 , {event4}) g1c g1 (gb1 ∧b2 , {event2}) l3 g2c g2 (gb2 ∧b2 , {event4}) l2 g3c ({x ≤ 10, y > 3}, {event1, event3}, {event2, event4}) (gb1 ∧b2 , {event2, event4}) g4c g1 (gb1 , {event2}) g5c g2 (gb2 , {event4}) Antonia Reißner, Matthias Werner Here the constraints are defined as follows: b1 ({x, event1}, v) = (v(x, v(t)) ≤ 10) ∧ v(event1, v(t)), b2 ({x, y, event3}, v) = (v(x, v(t)) ≤ 10) ∧ (v(y, v(t)) > 3) ∧ v(event3, v(t)). Hence the resulting guard functions are: (b1 ∧ b2l3 )({x, y, event1, event3}, v) =b1 ({x, event1}, v) ∧ b2l3 ({x, y, event3}, v) =(v(x, v(t)) ≤ 10) ∧ v(event1, v(t)) ∧ ¬((v(x, v(t)) ≤ 10) ∧ (v(y, v(t)) > 3) ∧ v(event3, v(t))) =(v(x, v(t)) ≤ 10) ∧ v(event1, v(t)) ∧ ((v(x, v(t)) > 10) ∨ (v(y, v(t)) ≤ 3) ∨ ¬v(event3, v(t))) =((v(x, v(t)) ≤ 10) ∧ v(event1, v(t))) ∧ ((v(x, v(t)) > 10)) ∨ ((v(x, v(t)) ≤ 10) ∧ v(event1, v(t))) ∧ ((v(y, v(t)) ≤ 3) ∨ ¬v(event3, v(t))) =0 ∨ ((v(x, v(t)) ≤ 10) ∧ v(event1, v(t))) ∧ ((v(y, v(t)) ≤ 3) ∨ ¬v(event3, v(t))) =((v(x, v(t)) ≤ 10) ∧ v(event1, v(t))) ∧ ((v(y, v(t)) ≤ 3) ∨ ¬v(event3, v(t))) (b1l1 ∧ b2 )({x, y, event1, event3}, v) =b1l1 ({x, event1}, v) ∧ b2 ({x, y, event3}, v) =¬((v(x, v(t)) ≤ 10) ∧ v(event1, v(t))) ∧ ((v(x, v(t)) ≤ 10) ∧ (v(y, v(t)) > 3) ∧ v(event3, v(t))) =((v(x, v(t)) < 10) ∨ ¬v(event1, v(t))) ∧ ((v(x, v(t)) > 10) ∧ (v(y, v(t)) ≤ 3) ∧ v(event3, v(t))) =(v(x, v(t)) < 10) ∧ ((v(x, v(t)) > 10) ∧ (v(y, v(t)) ≤ 3) ∧ v(event3, v(t))) ∨ ¬v(event1, v(t)) ∧ ((v(x, v(t)) > 10) ∧ (v(y, v(t)) ≤ 3) ∧ v(event3, v(t))) =0 ∨ ¬v(event1, v(t)) ∧ ((v(x, v(t)) > 10) ∧ (v(y, v(t)) ≤ 3) ∧ v(event3, v(t))) =¬v(event1, v(t)) ∧ ((v(x, v(t)) > 10) ∧ (v(y, v(t)) ≤ 3) ∧ v(event3, v(t))) (b1 ∧ b2 )({x, y, event1, event3}, v) =b1 ({x, event1}, v) ∧ b2 ({x, y, event3}, v) =(v(x, v(t)) ≤ 10) ∧ v(event1, v(t)) ∧ ((v(x, v(t)) ≤ 10) ∧ (v(y, v(t)) > 3) ∧ v(event3, v(t))) =(v(x, v(t)) ≤ 10) ∧ v(event1, v(t)) ∧ (v(y, v(t)) > 3) ∧ v(event3, v(t))) Depending on the active events only one of these three guards can be active by construction. Therefore no non-determinism is introduced. 2.3 Discussion Besides solving the issues mentioned in the first part of this section, the redefi- nition has some further advantages. A New Definition of Composition of LTIHA In the new definition the underlying graph structure of the composed au- tomaton - expressed as locations and transitions - is independent of the respec- tive guards. The composition of the new automata with regard to the locations and transitions is equivalent to the strong graph product. This graph product is already known to be commutative up to an isomorphism and associative [5]. Furthermore by definition of functions as guards, more conditions to change the location of an automaton can be expressed. Consider the inactivity of an event as a condition. This can not be implemented in the original automata. Some conditions can be modeled in a more compact way using the new introduced guard functions. For example to express that one of two guards is active, multiple transitions or guards were necessary in the former version. Whereas now only one function is necessary. Besides that the original LTIHA only allowed transitions with disjoint input and output event sets. For the new definition this constraint is not necessary. The introduction of a variable subset XE allows to design dependencies on values which are not manipulated by the automaton itself. With these variables the automaton can interact besides synchronization with other automata or other systems which are not designed as LTIHA. 3 Properties of the composition The general idea of the composition operator is to enable the construction of the whole system by composing small automata. The composition of two automata should behave equivalent to the two automata running parallel while interacting using shared variables. From a formal perspective running parallel can only be considered as commutative, hence the operator should have the same property. Since there should be no difference in which order the components are build and composed together, it is needed that the composition is associative as well as commutative. The importance of the composition operator to be commutative and associa- tive was already stated in [7]. If these properties would not hold the composition operator could not be used in the above described way. In the following the automata H 1 , H 2 and H 3 are defined as: H 1 = (L1 , X 1 , W 1 , B 1 , T 1 , F 1 ) H 2 = (L2 , X 2 , W 2 , B 2 , T 2 , F 2 ) H 3 = (L3 , X 3 , W 3 , B 3 , T 3 , F 3 ). 3.1 Commutative Theorem 1. The composition operator is commutative up to an isomorphism. This means if F = H 1 || H 2 = (LF , X F , W F , B F , T F , F F ) Antonia Reißner, Matthias Werner and G = H 2 || H 1 = (LG , X G , W G , B G , T G , F G ) then there exists a bijective map φ : LF → LG such that ∀l1 , l2 ∈ LF : (l1 , g, N, l2 ) ∈ T F if and only if (φ(l1 ), g, N, φ(l2 )) ∈ T G . Besides that X F = X G , W F = W G B F = B G and F F = F G holds. Proof. LF ∼ = LG Let φ be a map φ : (l1 , l2 ) 7→ (l2 , l1 ) with l1 ∈ L1 , l2 ∈ L2 then the location (l1 , l2 ) is an element of L1 ×L2 = LF and (l2 , l1 ) an element of L2 ×L1 = LG . Therefore φ is a map φ : LF → LG . This map is injective and LF and LG have by construction the same number of elements so φ is a bijection. X F = X G The sets X F and X G are equal due to the commutative nature of the set union. By the same argument the internal and synchronization variables are equal in both automata. Consider the set of external variables of the automata H F . This set is by construction equal to 1 2 (XE ∪ XE ) \ XIF = (XE 1 2 ∪ XE ) \ XIG . This equals the set of external variables of H G . F G W =W Consider an element of the set W F : ( v 1 (x, tvF ) x ∈ X 1 v F (x, tvF ) = v 2 (x, tvF ) otherwise and an element of the set W G : ( G v 2 (x, tvG ) x ∈ X 2 v (x, tvG ) = v 1 (x, tvG ) otherwise. It can be observed that the only difference between these valuations is for variables in X 1 ∩ X 2 . By definition of the composition operator v 1 and v 2 have to be equal for all variables in the set X 1 ∩ X 2 . So there is no difference between these functions. Hence every function in W F is also an element of W G and every function in W G is also an element of W F . Therefore the sets have to be equal. B F = B G It was already shown that X F = X G and W F = W G so it follows that B F = B G holds by definition. Since the constraint sets are equal, the guard sets are equal as well. TF ∼= T G Let la = (l1 , l2 ) and lb = (l3 , l4 ) be locations in the automaton F . The transition (la , gb , N, lb ) ∈ T F exists in F if and only if : 1) (l1 , gb1 , N 1 , l3 ) ∈ T 1 , (l2 , gb2 , N 2 , l4 ) ∈ T 2 , b = b1 ∧ b2 and N = N 1 ∪ N 2 or 2) (l1 , gb1 , N 1 , l3 ) ∈ T 1 , l2 = l4 , b = b1 ∧ b2l2 and N = N 1 or 3) (l2 , gb2 , N 2 , l4 ) ∈ T 2 , l1 = l3 , b = b2 ∧ b1l1 and N = N 2 A New Definition of Composition of LTIHA The transition (φ(la ), gb , N, φ(lb )) = ((l2 , l1 ), gb , N, (l4 , l3 )) ∈ T G exists in the automaton G if and only if: a) (l2 , gb2 , N 2 , l4 ) ∈ T 2 , (l1 , gb1 , N 1 , l3 ) ∈ T 1 , b = b2 ∧ b1 and N = N 2 ∪ N 1 or b) (l2 , gb2 , N 2 , l4 ) ∈ T 2 , l1 = l3 , b = b2 ∧ b1l1 and N = N 2 or c) (l1 , gb1 , N 1 , l3 ) ∈ T 1 , l2 = l4 , b = b1 ∧ b2l2 and N = N 1 It can be observed that the condition 1) and a) as well as 2) and c) as well as 3) and b) are equivalent. In these three cases the guards and the sets of activated synchronization variables are equal as well. So the automata F and G have the same underlying graph structure except for an isomorphism. F F = F G Follows trivially by the commutativity of addition. 3.2 Associative Theorem 2. The composition operator is associative, this means that H 1 ||(H 2 || H 3 ) = (H 1 || H 2 ) || H 3 holds for all linear time-invariant hybrid automata H 1 , H 2 and H 3 . Proof. Two automata F = H 1 ||(H 2 || H 3 ) = (LF , X F , W F , B F , T F , F F ) and G = (H 1 || H 2 ) || H 3 = (LG , X G , W G , B G , T G , F G ) are equal if and only if (LF , X F , W F , B F , T F , F F ) = (LG , X G , W G , B G , T G , F G ) holds. For shortness of notation the variable set of an automaton (H 2 || H 3 ) is addressed by X 2,3 a valuation by v 2,3 and a guard constraint by b2,3 . For an automaton H 1 || H 2 this is defined analogously. LF = LG It holds that LF = L1 × (L2 × L3 ) = L1 × L2 × L3 = L1 × (L2 × L3 ) = LG . X F = X G By definition it holds that X F = X 1 ∪ (X 2 ∪ X 3 ). Because the set union is associative this is equal to (X 1 ∪ X 2 ) ∪ X 3 = X G . The same holds for the internal and the synchronization variables. The set of external variables in F is equal to 2,3 F XE 1 = (XE ∪ XE ) \ XIF = (XE 1 2 ∪ (XE 3 ∪ XE \ XI2,3 )) \ XIF . By construction XI2,3 ⊆ XIF so it holds that F 1 2 3 XE = (XE ∪ XE ∪ XE ) \ XIF . Antonia Reißner, Matthias Werner The set of external variables in G is equal to 1,2 G XE = (XE 3 ∪ XE ) \ XIG = ((XE 1 2 ∪ XE \ XI1,2 ) ∪ XE 3 ) \ XIG . By construction XI1,2 ⊆ XIG so it holds that G 1 2 3 XE = (XE ∪ XE ∪ XE ) \ XIG = XE F . W F = W G A valuation in W F has the form  1 1 v (x, tvF ) x ∈ X ( 1 1  F v (x, tvF ) x∈X v (x, tvF ) = = v 2 (x, tvF ) x ∈ X 2 v 2,3 (x, tvF ) otherwise   3 v (x, tvF ) otherwise and in W G the form  1 1 v (x, tvG ) x ∈ X ( 1,2 1,2  v (x, tvG ) x ∈ X v G (x, tvG ) = = v 2 (x, tvG ) x ∈ X 1,2 \ X 1 v 3 (x, tvG ) otherwise   3 v (x, tvG ) otherwise. Hence they denote the same function. So each function that is in W F is also in W G and each function that is in W G is also in W F . Therefore the equality W F = W G holds. B F = B G It was already shown that X F = X G and W F = W G so this follows by definition. The set of constraints are equal so the set of guards are equal in both automata as well. T F = T G The automata F = H 1 ||(H 2 || H 3 ) and G = (H 1 || H 2 ) || H 3 have the same underlying edge structure since the strong graph product is known to be associative. It has to be shown that those edges have the same guard and produce the same events in both automata. Since the logical and as well as the set union are known to be associative it is clear that most of the edges have the same guard constraint and set the same variables to one if taken. It remains to show that the edge between (l1 , l2 , l3 ) and (l4 , l5 , l6 ) with l2 = l5 and l3 = l6 have the same guard in both automata. A New Definition of Composition of LTIHA Consider the constraint of the guard mapping to 1 of this edge in F = H 1 ||(H 2 || H 3 ): b (1) = b1 ∧ b2,3 (l2 ,l3 ) (2) = b1 ∧bi ∈Bo2,3 (l2 ,l3 ) ¬bi (3) = b1 ∧ ∧b2 ∈Bo2 (l2 ) ∧b3 ∈Bo3 (l3 ) (¬(b2 ∧ b3 ) ∧ ¬(b2l2 ∧ b3 ) ∧ ¬(b2 ∧ b3l3 )) (4) = b1 ∧ ∧b2 ∈Bo2 (l2 ) ∧b3 ∈Bo3 (l3 ) ((¬b2 ∨ ¬b3 ) ∧ (¬b2l2 ∨ ¬b3 ) ∧ (¬b2 ∨ ¬b3l3 )) (5) = b1 ∧ ∧b2 ∈Bo2 (l2 ) ∧b3 ∈Bo3 (l3 ) ((¬b2 ∨ ¬b3 ) ∧ (¬ ∧b2 ∈Bo2 (l2 ) ¬b2 ∨ ¬b3 )∧ (6) (¬b2 ∨ ¬ ∧b3 ∈Bo3 (l3 ) ¬b3 )) = b1 ∧ ∧b2 ∈Bo2 (l2 ) ∧b3 ∈Bo3 (l3 ) ((¬b2 ∨ ¬b3 ) ∧ (∨b2 ∈Bo2 (l2 ) b2 ∨ ¬b3 ) (7) ∧ (¬b2 ∨ ∨b3 ∈Bo3 (l3 ) b3 )) = b1 ∧ (∧b2 ∈Bo2 (l2 ) ∧b3 ∈Bo3 (l3 ) (¬b2 ∨ ¬b3 )) (8) ∧ (∧b3 ∈Bo3 (l3 ) (∨b2 ∈Bo2 (l2 ) b2 ∨ ¬b3 )) (9) ∧ (∧b2 ∈Bo2 (l2 ) (¬b2 ∨ ∨b3 ∈Bo3 (l3 ) b3 )) (10) From line 9 follows that if ∀ba ∈ Bo2 (l2 ) : ba = 0 then ∀b3 ∈ Bo3 (l3 ) it holds that b3 = 0. Line 10 indicatates that if ∀b3 ∈ Bo (l3 ) : b3 = 0 then it follows that ∀b2 ∈ Bo (l2 ) : b2 = 0 holds. Consider now the case that there exists at least one bi ∈ Bo2 (l2 ) with bi = 1 then from line 8 it is concluded that ∀b3 ∈ Bo (l3 ) : b3 equals to 0. But by the observation from line 9 it follows ∀ba ∈ Bo2 (l2 ) : ba equals to 0. This is a contradiction to the existence of a bi ∈ Bo2 (l2 ) with bi = 1. For a bj ∈ Bo3 (l3 ) with bj = 1 it follows analogously. In conclusion b can only be true if ∀ba ∈ Bo2 (l2 ) : ba = 0 and ∀b3 ∈ Bo3 (l3 ) : b3 = 0 and b1 = 1 holds. So b can be written as: b = b1 ∧ (∧b2 ∈Bo (l2 ) ¬b2 ) ∧ (∧b3 ∈Bo (l3 ) ¬b3 ) = b1 ∧ b2l2 ∧ b3l3 . Consider the constraint of the guard mapping to 1 of the same edge in G = (H 1 || H 2 ) || H 3 : b =(b1 ∧ b2l2 ) ∧ b3l3 So the same transition has the same guard constraint in both automata. The following table gives an overview over the guard constraints and set of synchronization variables of each transition in both automata. Antonia Reißner, Matthias Werner automaton F automaton G b N b N (l1 , l2 , l3 ) tob1 ∧ (b2 ∧ b3 ) N 1 ∪ (N 2 ∪ N 3 ) (b1 ∧ b2 ) ∧ b3 (N 1 ∪ N 2 ) ∪ N 3 (l4 , l5 , l6 ) l2 = l5 b1 (∧b2l2 ∧ b3 ) N1 ∪ N3 (b1 ∧ b2l2 ) ∧ b3 N1 ∪ N3 l3 = l6 b1 (∧b2 ∧ b3l3 ) N1 ∪ N2 (b1 ∧ b2 ) ∧ b3l3 N1 ∪ N2 l1 = l4 b1l1 ∧ (b2 ∧ b3 ) N2 ∪ N3 (b1l1 ∧ b2 ) ∧ b3 N2 ∪ N3 l1 = l4 and b1l1 ∧ (b2l2 ∧ b3 ) N3 ? : (b1l1 ∧ b2l2 ) ∧ b3 N3 l2 = l5 l1 = l4 and b1l1 ∧ (b2 ∧ b3l3 ) N2 (b1l1 ∧ b2 ) ∧ b3l3 N2 l3 = l6 l2 = l5 and ? : b1 ∧ (b2l2 ∧ b3l3 ) N1 (b1 ∧ b2l2 ) ∧ b3l3 N1 l3 = l6 A ? signifies that the entry follows by the above discussion. Any other entry follows by construction. F F = F G Follows trivially because addition is associative. 4 Conclusion and Future Work Initially we showed some issues of the original LTIHA and the composition op- erator definition. These issues were then solved by changing the respective defi- nitions. By these changes the expressiveness of LTIHA has been expanded. Beyond that the new composition operator was proven to be commutative and associa- tive, which are both necessary conditions for the operator to behave as wanted. Neither of these properties were shown for the original version. After these issues are solved future work will focus on the properties of the redefined composition operator. It will be researched which properties the composition of two automata has if these automata were known to have a zeno execution. For this analysis first the zeno definition of [8] will be adjusted to fit the redefinition of LTIHA. One step further is the analysis of reachability. It will be analyzed if reach- ability is decidable for LTIHA and if reachability results of small automata can be used to analyze the composition of these automata. References 1. Akhundov, Jafar and Tröger, Peter and Werner, Matthias: Superposition Principle in Composable Hybrid Automata. Fundamenta Informaticae 157(4), 321–339(2018) 2. Akhundov, Jafar and Reißner, Michael and Werner, Matthias: Using Hybrid Au- tomata for Early Spacecraft Design Evaluation. Proceedings of the 26th Inter- national Workshop on Concurrency, Specification and Programming. Warsaw, Poland(2017) A New Definition of Composition of LTIHA 3. Doyen, Laurent and Frehse, Goran and Pappas, George J. and Platzer, André: Verification of hybrid systems. Handbook of Model Checking, 1047–1110(2018) 4. André, Étienne: What’s decidable about parametric timed automata? International Journal on Software Tools for Technology Transfer 21(2) 203–219(2019) 5. Harary, Frank and Wilcox, Gordon W.: Boolean operations on graphs. IMathematica Scandinavica 41–51(1967) 6. Roehm, Hendrik and Oehlerking, Jens and Woehrle, Matthias and Althoff, Matthias: Reachset conformance testing of hybrid automata. Proceedings of the 19th Interna- tional Conference on Hybrid Systems: Computation and Control 277–286(2016) 7. Van der Schaft, A.J. and Schumacher, Johannes Maria: Compositionality issues in discrete, continuous, and hybrid systems. International Journal of Robust and Nonlinear Control: IFAC-Affiliated Journal 11(5) 417–434(2001) 8. Lygeros, John and Tomlin, Claire and Sastry, Shankar: Hybrid systems: modeling, analysis and control. (1999) 9. Akhundov, Jafar and Reißner, Michael and Werner, Matthias: Compositional Ex- pressiveness of Hybrid Models. CS&P on Proceedings, (2018)