The aim of this paper is to solve some issues of linear timeinvariant hybrid automata as de ned in [9]. First these issues are explained on a small example, before the revised de nitions of linear timeinvariant hybrid automata and their composition operator are presented. Furthermore it is shown that this new composition operator is commutative and associative.
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 veri cation of systems is widely recognized. Since
most modern systems - like embedded systems - have to interact with the
physical 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
approach to model a hybrid system is a hybrid automata. These automata are used
for example in the eld of embedded systems [
To model a system as a hybrid automaton all possible states of the system 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 veri cation. 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 e ort. 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
automata [
Linear time-invariant hybrid automata (LTIHA) and their composition were
rst de ned by Akhundov et al. ([
In the current paper we are discussing drawbacks of the original approach for LTIHA. We suggest an alternative de nition and show some properties of this composition. 2
Linear Time-Invariant Hybrid Automata In the rst part of this section the original approach is analyzed and two main issues are explained. To overcome these issues a new de nition of linear timeinvariant hybrid automata and their composition operator is presented in the second part. In the last part the e ects of changing the de nitions are discussed. 2.1
The original de nition of LTIHA [
A further issue of the former composition operator is discussed using an example. Consider the following automata:1 l1 l3 g1 g2 l2 l4 (l1; l3) g1c (l2; l3) g2c g3c g5c (l1; l4)
g4c (l2; l4)
A guard is de ned by [
To overcome the rst issue described above, we suggest a modi ed 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
First the formal de nition 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 de nition.
De nition 1. A linear time-invariant hybrid automaton is a six tuple
H = (L; X; W; B; T; F ) consisting of: { Set of locations L = fl1; ::; lng { Set X of real valued state variables, decomposable in sets of internal state variables XI , external state variables XE with t 2 XE and synchronization variables XS . The variable t denotes the time of the system. { A set of valuations
W = fv j v : X
R ! R, for t it holds that v(t; r1) = v(t; r2)8r1; r2 2 Rg consisting of functions v which map each variable x 2 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 in uenced by the automaton, but given e.g. from the outside world. The valuations of the synchronization variables s 2 XS have the form: Where Es R denotes the set of discrete time points at which a synchronization event occurs. { 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 gb(M; v) = (1 b evaluates to true
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 2 L, g 2 C and N 2 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 tv, then the valuation is modi ed to:
This holds for all variables s 2 N . The set Es is extended to the set Es [ ftvg { A set of ow functions F = fflx j 8l 2 L 8x 2 XI g containing functions which describe the change of each state variable for each location. These ow functions are solutions to linear ordinary di erential 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.
De nition 2. The state (lj ; v) of a linear time-invariant hybrid automaton consists of the location lj 2 L and the valuation v.
These changes of the linear time-invariant hybrid automata enable a redefinition of the corresponding composition operator. Without the change of the underlying automata the new composition operator would produce an automaton which is not necessarily a LTIHA.
De nition 3. Two automata H1 = (L1; X1; W 1; B1; T 1; F 1) and H2 = (L2; X2; W 2; B2; T 2; F 2) can be composed using the operator jj if 8x 2 X1 \ X2 : v1(x; tv1 ) = v2(x; tv2 ) holds. The resulting automaton Hc = H1 jj H2 equals (Lc; Xc; W c; Bc; T c; F c) with the following properties: { The set of locations Lc equals L1 L2. { The set of variables Xc is equal to X1 [ X2 and can be decomposed in the set of internal variables XIc = X1 I
I [ X2, the set of external variables XEc = XE1 [ XE2 n XIc and the set of synchronization variables XSc = XS1 [ XS2 . { The set W c consists of valuations vc having the form vc(x; tvc ) = (v1(x; tvc ) x 2 X1 v2(x; tvc ) otherwise. { The set of constraints Bc equals the set of all to true or false evaluable constraints over a subset of the set of variables Xc and the valuation vc. The set Cc 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) 2 T 1 and (lj2; gb2 ; N 2; ll2) 2 T 2 be transitions in the corresponding automata.
The transitions ((li1; l2); gb1^bl22 ; N 1; (lk1; l2)) and ((l1; lj2); gb2^bl11 ; N 2; (l1; ll2)) are elements of the set of transitions T c for all locations l2 2 L2 and l1 2 L1. Let Bo1(l1) be the set of the constraints bn of all guards gbn such that there exists ln 2 L1 with (l1; gbn ; N; ln) 2 T 1 for any N 2 P(XS1 ). The constraint bl11 denotes ^bi2Bo1(l1):bi. The new guard constraints b1 ^ bl22 and b2 ^ bl11 are de ned by: b1 ^ bl22 (M; vc) = b1(M \ X1; vcj1) ^ bl22 (M \ X2; vcj2) b2 ^ bl11 (M; vc) = b2(M \ X2; vcj2) ^ bl11 (M \ X1; vcj1):
R ! R which is de ned as 8y 2 X2; n 2 R : vcj2(y; n) = vc(y; n):
b1 ^ b2(M; vc) = b1(M \ X1; vcj1) ^ b2(M \ X2; vcj2): tion f(xli1;lj2) = flx1 + flx2 holds.
i j { The set F c consists of ow functions f(xli1;lj2). At the location (li1; lj2) the equa
In the following table guards for one speci c example based on the above example are given for both the new and the old de nition.
g1 g2 c g1 c g2 10; y > 3g; fevent1; event3g; fevent2; event4g) (gb1^b2 ; fevent2; event4g) g1 (gb1 ; fevent2g) g2 (gb2 ; fevent4g) Here the constraints are de ned as follows: b1(fx; event1g; v) = (v(x; v(t)) 10) ^ v(event1; v(t)); b2(fx; y; event3g; v) = (v(x; v(t))
10) ^ (v(y; v(t)) > 3) ^ v(event3; v(t)): Hence the resulting guard functions are: (b1 ^ bl23 )(fx; y; event1; event3g; v) =b1(fx; event1g; v) ^ bl23 (fx; y; event3g; 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)) =((v(x; v(t))
3) _ :v(event3; v(t))) 10) ^ v(event1; v(t))) ^ ((v(x; v(t)) > 10)) _ ((v(x; v(t)) =0 _ ((v(x; v(t)) =((v(x; v(t)) 10) ^ v(event1; v(t))) ^ ((v(y; v(t))
3) _ :v(event3; v(t))) 10) ^ v(event1; v(t))) ^ ((v(y; v(t)) 3) _ :v(event3; v(t))) 10) ^ v(event1; v(t))) ^ ((v(y; v(t)) 3) _ :v(event3; v(t))) 3) ^ v(event3; v(t))) 3) ^ v(event3; v(t))) 3) ^ v(event3; v(t))) 3) ^ v(event3; v(t))) 10) ^ (v(y; v(t)) > 3) (bl11 ^ b2)(fx; y; event1; event3g; v) =bl11 (fx; event1g; v) ^ b2(fx; y; event3g; 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))
_ :v(event1; v(t)) ^ ((v(x; v(t)) > 10) ^ (v(y; v(t)) =0 _ :v(event1; v(t)) ^ ((v(x; v(t)) > 10) ^ (v(y; v(t)) =:v(event1; v(t)) ^ ((v(x; v(t)) > 10) ^ (v(y; v(t)) (b1 ^ b2)(fx; y; event1; event3g; v) =b1(fx; event1g; v) ^ b2(fx; y; event3g; v) =(v(x; v(t))
10) ^ v(event1; v(t)) ^ ((v(x; v(t)) ^ 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
Besides solving the issues mentioned in the rst part of this section, the rede nition has some further advantages.
In the new de nition the underlying graph structure of the composed
automaton - expressed as locations and transitions - is independent of the
respective 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 [
Furthermore by de nition 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 de nition 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
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 di erence 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
associative was already stated in [
In the following the automata H1, H2 and H3 are de ned as:
H1 = (L1; X1; W 1; B1; T 1; F 1) H2 = (L2; X2; W 2; B2; T 2; F 2)
H3 = (L3; X3; W 3; B3; T 3; F 3): 3.1
Theorem 1. The composition operator is commutative up to an isomorphism. This means if
F = H1 jj H2 = (LF ; XF ; W F ; BF ; T F ; F F ) and
G = H2 jj H1 = (LG; XG; W G; BG; T G; F G) then there exists a bijective map : LF ! LG such that 8l1; l2 2 LF : (l1; g; N; l2) 2 T F if and only if ( (l1); g; N; (l2)) 2 T G. Besides that XF = XG, W F = W G BF = BG and F F = F G holds.
Proof.
LF = LG Let be a map : (l1; l2) 7! (l2; l1) with l1 2 L1; l2 2 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. XF = XG The sets XF and XG 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 HF . This set is by construction equal to
(XE1 [ XE2 ) n XIF = (XE1 [ XE2 ) n XIG:
This equals the set of external variables of HG.
W F = W G Consider an element of the set W F : and an element of the set W G:
It can be observed that the only di erence between these valuations is for variables in X1 \ X2. By de nition of the composition operator v1 and v2 have to be equal for all variables in the set X1 \ X2. So there is no di erence 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.
BF = BG It was already shown that XF = XG and W F = W G so it follows that BF = BG holds by de nition. Since the constraint sets are equal, the guard sets are equal as well.
T F = T G Let la = (l1; l2) and lb = (l3; l4) be locations in the automaton F . The transition (la; gb; N; lb) 2 T F exists in F if and only if : 1) (l1; gb1 ; N 1; l3) 2 T 1, (l2; gb2 ; N 2; l4) 2 T 2,
b = b1 ^ b2 and N = N 1 [ N 2 or 2) (l1; gb1 ; N 1; l3) 2 T 1, l2 = l4,
b = b1 ^ bl22 and N = N 1 or 3) (l2; gb2 ; N 2; l4) 2 T 2, l1 = l3, b = b2 ^ bl11 and N = N 2 The transition ( (la); gb; N; (lb)) = ((l2; l1); gb; N; (l4; l3)) 2 T G exists in the automaton G if and only if: a) (l2; gb2 ; N 2; l4) 2 T 2, (l1; gb1 ; N 1; l3) 2 T 1,
b = b2 ^ b1 and N = N 2 [ N 1 or b) (l2; gb2 ; N 2; l4) 2 T 2, l1 = l3,
b = b2 ^ bl11 and N = N 2 or c) (l1; gb1 ; N 1; l3) 2 T 1, l2 = l4,
b = b1 ^ bl22 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
Theorem 2. The composition operator is associative, this means that
H1 jj(H2 jj H3) = (H1 jj H2) jj H3 holds for all linear time-invariant hybrid automata H1; H2 and H3.
Proof. Two automata and are equal if and only if
F = H1 jj(H2 jj H3) = (LF ; XF ; W F ; BF ; T F ; F F )
G = (H1 jj H2) jj H3 = (LG; XG; W G; BG; T G; F G) (LF ; XF ; W F ; BF ; T F ; F F ) = (LG; XG; W G; BG; T G; F G) holds. For shortness of notation the variable set of an automaton (H2 jj H3) is addressed by X2;3 a valuation by v2;3 and a guard constraint by b2;3. For an automaton H1 jj H2 this is de ned analogously.
LF = LG It holds that LF = L1 (L2 L3) = L1 L2 L3 = L1 (L2 L3) = LG. XF = XG By de nition it holds that XF = X1 [ (X2 [ X3). Because the set union is associative this is equal to (X1 [ X2) [ X3 = XG. The same holds for the internal and the synchronization variables. The set of external variables in F is equal to
XEF = (XE1 [ XE2;3) n XIF = (XE1 [ (XE2 [ XE3 n XI2;3)) n XIF : By construction X2;3
I
XIF so it holds that
XEF = (XE1 [ XE2 [ XE3 ) n XIF : The set of external variables in G is equal to By construction X1;2
I
XIG so it holds that XEG = (XE1;2 [ XE3) n XIG = ((XE1 [ XE2 n XI1;2) [ XE3) n XIG:
XEG = (XE1 [ XE2 [ XE3) n XIG = XEF : W F = W G A valuation in W F has the form and in W G the form
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.
BF = BG It was already shown that XF = XG and W F = W G so this follows by de nition. 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 = H1 jj(H2 jj H3) and G = (H1 jj H2) jj H3 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. Consider the constraint of the guard mapping to 1 of this edge in F = H1 jj(H2 jj H3): b = b1 ^ b(2l;23;l3) = b1 ^bi2Bo2;3(l2;l3) :bi From line 9 follows that if 8ba 2 Bo2(l2) : ba = 0 then 8b3 2 Bo3(l3) it holds that b3 = 0. Line 10 indicatates that if 8b3 2 Bo(l3) : b3 = 0 then it follows that 8b2 2 Bo(l2) : b2 = 0 holds. Consider now the case that there exists at least one bi 2 Bo2(l2) with bi = 1 then from line 8 it is concluded that 8b3 2 Bo(l3) : b3 equals to 0. But by the observation from line 9 it follows 8ba 2 Bo2(l2) : ba equals to 0. This is a contradiction to the existence of a bi 2 Bo2(l2) with bi = 1. For a bj 2 Bo3(l3) with bj = 1 it follows analogously. In conclusion b can only be true if 8ba 2 Bo2(l2) : ba = 0 and 8b3 2 Bo3(l3) : b3 = 0 and b1 = 1 holds. So b can be written as: b = b1 ^ (^b22Bo(l2):b2) ^ (^b32Bo(l3):b3) = b1 ^ bl2 ^ bl33 : 2 Consider the constraint of the guard mapping to 1 of the same edge in G = (H1 jj H2) jj H3: b =(b1 ^ bl22 ) ^ bl3 3 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. (1) (2) (3) (6) (7) (8) (9) (10)
b b1 ^ (b2 ^ b3)