In the existing abundance of di erent hybrid automata formalisms concurrent composition is seldom considered or requires additional semantics which is not always de ned. This work considers three common reasons of problems with hybrid automata composition: contradicting resets in the discrete transitions, global time reference with contradicting initial conditions and redundant non-determinism for ring time. An overview is provided of the existing formalisms and the attempts to solve these particular problems. A reduced hybrid automata formalism, called linear time-invariant hybrid automata, is introduced. It avoids all those problems and yet provides a powerful modeling tool with practical applications. Also, a short discussion is provided for the problem of Zeno behavior and what conditions are demanded for a model to ful ll so that Zeno behavior would not arise during composition.
Introduction Hybrid systems modeling has various applications in model-driven design and veri cation of embedded and reactive systems. It has been a topic of intensive research in the past 20 years [MMP91]. Their hallmark is the combination of discrete and continuous behavior. Most hybrid systems include computational components which operate in discrete steps and physical components with continuous behavior over time. Typical examples are aerospace systems, robotic systems, or process control systems. Since most of these systems are too complex to design and build as a whole, they are decomposed into subsystems and components with reduced complexity and simpler behavior. This process can, of course, be recursively repeated until complexity is manageable. In order for this process to be supported on the modeling level, it is necessary that the applied formalism allows for (de)compositionThe process of decomposition has been historically used in the control systems engineering applications [Nis11]. An important property which is often used to simplify design and analysis is the superposition1 principle which is mathematically de ned as: 1 also called linearity
Since their introduction, hybrid automata formalisms have been emerging with restricted properties to simplify analysis and sometimes composition [AD94] [Hen96] [LSV03] [Abr12]. Examples of subsets of hybrid automata are timed automata [AD94], linear hybrid automata [Hen96], rectangular hybrid automata [HKPV98], hybrid I/O automata [LSV03], etc. Several de nitions of the general hybrid automata exist as well, each with slight deviations in the underlying semantics.
A handful of frameworks leave some of the semantics unspeci ed which makes it di cult for the designer to apply them - separately or compositionally [Hen96] [Ras05] [Abr12] [LLL09]. An example is a general structural de nition of HA where each location has an invariant and several outgoing transitions with respective guards [Hen96] [Ras05] [LLL09] [Abr12]. The problem arises when the invariant is violated thus forcing the automaton to switch its location to another one but no guarding condition of the outgoing transitions is enabled. It remains unspeci ed what happens to the model in such a situation. Another example is the passage of time in several parallel composed automata with synchronising labeled transitions [Abr12]. Since the event (action) semantics is not always speci ed fully and consistently, i.e. are events bu ered or ignored, or what is the global time reference for two composed automata, it is unclear whether one synchronising edge should wait for another one with the same label in the second automaton. There are formalisms which allow for such "waiting" which enables to model physical systems where objects are oating in space waiting for some other event to occur.
Thorough comparison of the existing HA formalisms has lead to the conclusion that three common reasons of problems for hybrid automata composition exist:
2. global time reference with contradicting initial conditions and 3. redundant non-determinism for ring time.
For the practical application of composable control systems a formalism is needed which has none of the aformentioned problems and ful lls the property of superposition of continuous functions.
The contribution of this work lies in the introduction of a new formalism for modeling hybrid systems with a fully speci ed timing, ring, event and composition semantics and ful lling the property of superposition motivated by the applicability from the control systems engineering. Our approach is driven by the motivating example of a dedicated domain speci c language for the veri cation of a space mission at the early design phases where superposition is a critical issue [ASGW16], [ATW15], [STF+13].
The article starts with an overview of the existing hybrid automata formalisms which experience and/or partially solve the composition problems. The general de nition of the utilized hybrid automata variation is given in Section 3. The text continues with a detailed discussion of composition semantics and the arising problems. Section 4 shows how the LTI-HA solve these problems. The paper is concluded by a discussion of further work and possible applications of the formalism. 2
State of the Art In the existing abundance of di erent hybrid automata formalisms concurrent composition is seldom considered in full depth or requires additional semantics which is not always de ned [Ras05] [LLL09] [Abr12]. In the general setting, HA experience all of the three mentioned problems [Hen96] [Ras05] [Abr12] [LLL09] [Alu15]. In [Abr12], an overview is provided of the existing hybrid automata formalisms with rising complexity, starting from labeled transition systems, timed automata and ending with the general hybrid and rectangular automata. That work provides a conceptualized structural view on the hybrid systems. All three types of problems occur in the generalized HA and at least partially in the other formalisms. Furthemore, many formalisms su er from incompleteness of semantics de nition [Hen96] [Ras05] [LLL09] [Abr12].
Hybrid I/O automata (HIOA) were introduced by Lynch et al. rst in 1996 [LSVW96] but have been modi ed several times since [LSV03]. The de nition of hybrid I/O automata is unique in the sence that it eliminates a handful of problems by de ning the hybrid automata by the notion of hybrid traces. Hybrid I/O automata have been demonstrated to be both composable and receptive2. However, HIOA are too restrictive for some of the control applications where explicit notion of superposition is important. For example, HIOA are required to have disjunct output trajectories [LSV03, p.131,p.141] which excludes the possibility of superposition.
Superposition of the ow functions of hybrid automata has been exploited in the linear hybrid automata, however, the introduced formalisms still have at least one of the semantic problems listed in the problem statement [Hen96] [Pap98]. 3 3.1
Linear Time-Invariant Hybrid Automata (LTI-HA) Before the linear time-invariant hybrid automata are de ned, several supporting de nitions are provided.
the assignment to x of a value from its domain D: V (x) : x 7! D(x).
This de nition can be extended to a set of variables:
variable set X is the union of all valuations for all x 2 X of a value from the corresponding domains D(x): V (X) : X 7! V(X ), where V(X) = D(x1) D(x2) ::: D(xn) is the set of all possible valuations. 2 Not experiencing Zeno behavior, even under the composition.
(L,V)(t) consisting of two time-dependent components: the discrete state (L) and the continuous state (V).
De nition 4 (LTI-HA). A linear time-invariant hybrid automaton H is a tuple (L; T ; X ; SI ; SO; E ; A; G; F ; I), where: { L = (L1; : : : ; Ln) is a set of discrete locations also called modes; { T L L is a (not necessarily complete) multiset transition relation; { X is a set of continuous state variables. To each x 2 X , a value from D(x) Rm [ fdcg can be assigned where m 1 but is nite and dc is a special term for unspeci ed ("don't care") value; { SI and SO are two disjunct sets of input and output events, respectively, which de ne the automaton's event signature; { E : T 7! P(P(SI )) and A : T 7! P(SO) are assignments of the interface events SI ; SO to the transitions of the automaton; { G : T V(X ) P(SO) P(P(SI )) 7! ftrue, falseg is a guard function. For all transitions , G( ; V(X ); A( ); E ( )) = g (V(X ); A( ); E ( )) is called the guard (function) of ; { For any location L and for all variables from X there exists an ordinary linear di erential equation F (fL(x; t)) = g(x; t); x 2 X ; t 2 R 0 with g(x; t) : X R 0 7! Rm describing the change of the corresponding variable, where fL(x; t) : X R 0 7! V (X ) is called a ow function, F (fL) is a linear operator P0(t)f L(k) + P1(t)f L(k 1) + ::: + Pk(t)fL with f L(l) = ddl ftlL and Pi(t) : R 7! R being any functions. The set of all ow functions in a given location describe how the valuations of continuous state variables change over time in that location; { I is the initial state of the system (LI ; VI ), where LI 2 L is the initial active mode and VI = VI (X ) is the initial valuation of all the variables in X .
In contrast, the general de nition of hybrid automata usually also includes additional constructs such as location invariants, variable resets along the transitions, ow functions are uncostrained and events that are labels with a simple synchronisation semantics.
De nition 5 (Time Semantics). Evaluation of ow functions is based only on the duration of time interval spent in the corresponding location. In each active location, time elapses at the same rate. Transitions are timeless.
Global time reference can be implemented by taking any xed reference time value which is progressing along with the automata execution. At any time, exactly one location is active, beginning with the LI . Automaton's state changes either with time with respect to the ow functions of the corresponding locations or the discrete transitions, starting in the initial state I.
location L, the valuation of continuous variables V (X ) changes according the location's ow function fL. If no explicit ow function is given for some variables from X their rate of change is assumed to be 0 at the given location. If at some time point a guard g of an outgoing transition (Lc; Ld) evaluates to true, Ld becomes the new active location without delay and all events e 2 A( ) occur. If more than one guard of an outgoing transition evaluates to true, one of the transitions is chosen non-deterministically.
one-to-all semantics, that is, every output event is broadcasted. The input events have a one-to-one semantics and are therefore only generated by a single other automaton. Each input event has to be de ned and speci ed.
De nition 8 (Event Structure Semantics). The input events for a transition form a set E ( ) 2 P2(SI ) where P2(SI ) is a power set of a power set over the set of input events, that is complex events can be formed by coupling the (elementary) input events in the following way: for the transition to become enabled, at least one of the (complex) events S 2 P2(SI ) in the set E ( ) has to occur. Occurrence of such an event implies that all participating events s 2 S have occurred (simultaneously).
occurrences are not bu ered.
There are two possibilities to describe interval events : by two events, one for the start es and one for the completion ef , respectively, or by setting global variables values. Problem with modeling by just events arises when they are not caught thus leading to either o sets in the interval perceptions or overly complex conditions for well-de nedness and composability. Overlapping intervals are easily modeled by global variables with constant values. 3.2
tem (TTS) is a tuple ( ; 0; S; !) where is a (possibly in nite) state space with 0 being the initial state and S is a ( nite) set of labels. Transition relation is de ned as ! S [ R 0 .
De nition 11 (Trace Semantics of a Hybrid Automaton). Trace semantics of a hybrid automaton H = (L; T ; X ; SI ; SO; E ; A; G; F ; I) is de ned as a transition system where: { the (possibly in nite) state space is the set of pairs (l; Vl(X )); where Vl(X ) is in the range of possible valuations in l, de ned by fl { initial state is I { and the transitions "!" are either: discrete: 8T 2 T 9(li; Vi(X )) ! (lj ; Vi(X )); 2 P(S); li; lj 2 L or continuous: 9 2 R 0; being the time point when the location is left, 9(li; Vi(X )) ! (li; Vj (X )) ^ fli is di erentiable on [0; ] and the following conditions hold: 1. fli (0) = Vi(X ), 2. fli ( ) = Vj (X ),and 3. fli [0; ] is closed under subintervals.
Thus, a trace of a hybrid automaton is a nite sequence alternating between continuous evolutions with nite durations and discrete transitions: = s0 0s1 1; :::; n 1sn; where si are the states in TTS, i are the transitions (discrete or continuous) between them and s0 = I. Duration of a trace d( ) is de ned as the sum of all durations along that trace. Since a HA can be non-deterministic, many di erent traces are possible. Generating a control sequence of external events C (S; t), where S SI and t is a time point with respect to the global time reference, is not part of the model but a task for an external solver. 3.3
De nition 12 (Composability). Two LTI hybrid automata H ; H2 are called 1 composable, H1 f H2, i 8x 2 X 1 \ X 2 : VI1(x) = VI2(x), where dc = is always true for all values of .
De nition 13 (Composition). Given two composable hybrid automata H1 and H2, the composition H1 H2 provides a new hybrid automaton Hc = (Lc; T c; X c; SIc; SOc; E c; Ac; Gc; F c; Ic) where 1. Lc = L1 L2 = f(L11; L21); : : : ; (L11; L2n2 ); (L12; L21); : : : ; (L1n1 ; L2n2 )g 2. T=cf=Lc1f1t; L=c12(;L:ic:j:;;LLckc1ln)j1t; 2:: :L;cLcn1Ln2cg;(;Li1; L1k) 2 T 1 _ (Lj2; Ll2) 2 T 2g 3. X c = X 1 [ X 2, 4. SIc = (SI1 [ SI )nSOnSO
2 1 2 56.. 8SOc == (S(LOi[;LSjO); (Lk; Ll)) 2 T , where (Li; Lj ) 2 T 1 and (Lk; Ll) 2 T 2: 1 2 8e 2 S1 \ S2 6= ;: (a) e 2 S j S 2 E 1((Li; Lj )) ^ e 2 A2((Lk; Ll)) )
8E 2 E 1((Li; Lj )) : E c( ) := E c( ) [ fEneg (b) e 2 S j S 2 E 1((Li; Lj )) ^ e 2= A2((Lk; Ll)) )
T c := T cn (c) else E c( ) = E 1( ) [ E 2( )
The same process is repeated with the inverted indexes 1 and 2. 7. 8 2 T : Ac( ) = fe j = (Licj ; Lckl)^ ((e 2 A1(Li1; L1k) ^ j = l) _ (e 2 A2(Lj2; Ll2) ^ i = k)_ (e 2 (A1(Li1; L1k) [ A2(Lj2; Ll2))))g 9. 8Lij 2 Lc: fLij = fLi + fLj 10. Ic = (Lic1i2 ; VI1 [ VI2) 8. Gc = fg(Licj;Lckl) = g(1Li1;L1k)j(Licj ; Lckl) 2 T ^ j = lg\
c fg(Licj;Lckl) = g(Lj2;Ll2)j(Licj ; Lckl) 2 T ^ i = kg
c 2 Properties from semantics de nitions 5-9 remain preserved.
Properties 1 and 2 de ne the new location set which is now a cartesian product of two initial location sets, and the transition in a new location set exists if there was at least one transition in the corresponding locations of initial automata H1 and H2. The variable set is de ned as a union set. All variables with the same names are to be considered global and can be adjusted in a composed manner (property 9). Properties 4-7 describe how the input and output events of the automata are composed. Since the input events have the one-to-one semantics, if one of the two composed automata H1 and H2 has an output event which is the input event for the second automata this event can be cancelled out in the input set of the resulting composed automaton. This, however, does not apply for the output events because of their one-to-all semantics. Properties 6-8 de ne how the input and output events and the guards are assigned to their corresponding transitions in the initial automata. For assignment of input interfaces to the new transitions four possibilities are distinguished: an edge waiting for an event in one automaton is combined with the generating edge of the other automaton, a waiting edge with non-generating edge, non-waiting with the generating edge and non-waiting with non-generating edges. In the rst case, the generated event is removed from all the complex events of the input assignment. In the second case, the transition will never be taken since a waiting edge is waiting for an event which is not generated and not bu ered. For the remaining two combinations it is safe to just unite the input assignments. Mildly speaking, G builds a cut set of enabling valuations in two composed transitions and a union of the input and output events, respectively. Property 9 follows trivially from the linearity property of the superpositioned di erential equations. Since H1 and H2 are composable it is safe to apply property 10. 4 4.1
Semantics of Composition of Hybrid Automata
In the general setting, hybrid automata are de ned as follows [Hen96, p.2] [Ras05, p.4] [LLL09] [Abr12]: De nition 14. A hybrid automaton consists of: { A set of continuous variables X; { A nite directed multigraph (V; E) representing the discrete modes and the transitions between them; { Initial conditions describe how the continuous variables are reset after a timeless discrete transition has been taken; { Invariants are the predicates assigned to the discrete locations and must hold in the respective location when it is active; { Flow conditions describe how the variables in X change continuously with time; { Guard conditions which are the predicates over the values of variables of X and are the enabling conditions for a transition to be taken; { Events which are assigned to the transitions of the automaton. Transitions with with the same labels in di erent automatas must synchronise.
There are some extensions and small di erences between the de nitions which both solve some problems and introduce others. For instance, in [Abr12] it is proposed that discrete transitions in concurrent automata are interleaved, and synchronisation is enhanced with special -transitions for the automaton which is waiting on the synchronising edge. It is immediately clear that this extension solves the problem of race conditions of the resets with non-determinism for the case when, e.g. two transitions with di erent labels re simultaneously with the following resets: x = y + 1 and y = x + 1. However, introducing -transitions allows for modeling of a satellite in the orbit which, while waiting for some maneuver comand from an operations control center, suddenly freezes dead in its orbit since -transitions are also timeless. Furthermore, it does not solve a problem of possible Zeno behavior when time is prevented from passing. A trivial example is given in Fig. 1. If the automata start in states A and C with x = 0; y = 0, then after 10 time units, the system will converge and generate an in nite amount of discrete events. The execution trace would be (A ! B) ) (C ! D) ) (B ! A) ) (D ! C) ) ::: start start
A y 10 y_ = 1
C x 20 x_ = 1 x := 100 y := 15 x := 250
B x
200 x_ = 1
D y 10 y_ = 1 In the general setting, usually no assumption is made3 about the type of di erential equations governing the continuous change of the state variables. If those are not time invariant, it leaves the question open as to how the ow functions are overlapped during parallel composition. Another important drawback 3 An exception would be [LLL09] is the lack of speci cation of the semantics in the case when a state invariant is violated prior to enabling of any outgoing transition [HKPV98] [Ras05] [LLL09] [Abr12]. Several other formalisms based on the general hybrid automata have been presented [Hen96] [Ras05] [LLL09] [Abr12].
An overview of the three possible problems mentioned earlier occurring in the HA formalisms is provided in table (1). Timed automata, being the simplest form of the HA, avoid most of the problems of composition, as well as lack expressivity to describe complex hybrid phenomena [LLL09] [Cas05]. Linear hybrid automata have support for superposition but still have the invariants and resets, and, hence, the implied problems that could arise. Rectangular automata, just as the general automata, experience all of the three problems and also increase the complexity by introducing randomness and uncertainties [Hen96] [HKPV98].
Hybrid I/O automata solve all of the mentioned problems of composition but have explicitly eliminated the possibility for superposition of trajectories for the continuous variables [LSV03, p.131,p.141]. Since composition is the cornerstone of the new formalism that is introduced in this paper, the absence of each of the three undesirable prooerties Pi can be only guaranteed if and only if LTI hybrid automata as a formalism ful ll the following two conditions: 1. the property Pi cannot exist in a single automaton; 2. the Pi-freeness is preserved and Pi not induced by composition, where P1
R, P2
IC and P3
Theorem 1. No contradicting resets are possible in the LTI hybrid automata. Proof 1. Discrete transition resets are not a part of the LTI de nition 4. Furthermore, since there is no composition taking place, no contradictions are possible.
The proof follows trivially. 2. The proof of preservation also follows trivially from the de nition 13 of composition, since no rule introduces discrete resets. The only discrete jumps of the variable values are possible due to Dirac impulses which do not violate the superposition and time-invariance property.tu Theorem 2. No global time reference exists with the contradicting initial conditions in the LTI hybrid automata.
Proof 1. As per de nition 5, time ow is identical for all discrete states, hence time invariance. De nition 4 implies that the ow functions are also linear. Since every variable can only be assigned with value once in the initial state, no contradictions are possible. 2. Proving that this statement is preserved and not induced by composition is equivalent to proving that if two automata are composed with each other the induced automaton is also composable with some other third automaton, since non-contradicting initial conditions are the necessary and su cient condition for composability.
We assume that automata H1; H2 and H3 are pairwise composable. Without loss of generality, rules 3 and 10 of the composition de nition 13 are applied 1 2 to automatas H ; H :
Theorem 2
H1 f H2; H2 f H3; H1 f H3
(H1 H2) f H3 After applying rule 13.11, VI12 = VI1 [ VI2. Thus, set VI12 can be divided to ftrhormee Vsu1bsetIs, elements only from VII1\,eVlIe3m6=en;tsanodnlVyI2fr\omVI3V6=I2 ;a.nTdheelne,mferonmts
I \ V 2. Let us assume that V 1 the initial assumption and the de nition 12, 8x 2 X 8x 2 X 1 \ X 3 : V 1(x) = V 3(x) ^ 2 \ X 3 : V 2(x) = V 3(x)
8x 2 X 1 \ X
2 \ X 3 : V 1(x) = V 2(x) = V 3(x) Linearity and time-invariance are preserved with respect to superposition [Nis11]. Since all of the ow functions in the LTI-HA are linear and timeinvariant, the same applies for the composed automata after applying rules 1 and 9 of de nition 13. tu Theorem 3. Execution of LTI-HA never stalls due to the contradicting invariants and guard conditions.
Proof 1. Invariants are absent in the de nition of the LTI-HA 4. Hence, it is not possible for the behavior of the model to be unspeci ed due to a violated invariant with no guards enabled. 2. The rule for guards in the composition de nition, 13.8, combines several guards of the initial automata. If the guards are contradicting each other, transition is omitted altogether. No invariants are created and the ring enforcement (de nition 6) is preserved. tu 5
Discussion Although some of the common problems mentioned in the introduction of this work have been eliminated in the LTI-HA, others may remain which cannot be completely excluded for hybrid systems or are implied by the semantics of the modeled system itself. It is therefore useful to determine a set of properties, which, combined, will introduce a notion of well-de nedness of the model. A wellde ned model would guarantee correct behavior with respect to the property of interest, that is, model would behave without experiencing unexpected or unwanted behavior. One of such properties is divergence of time. If a model is Zeno-free, time never converges, i.e. it is impossible to nd a subsequence of the model execution trace which includes an in nite amount of events in a nite time. This notion has been extended by Lynch et al. in [LSV03] with the case where a trajectory of a continuous variable is never asymptotic.
Introduction of such a notion into the LTI-HA formalism would allow for automatic checking if a model can or cannot end in a Zeno executionOne possible condition for guaranteeing Zeno-freeness would be the absence of closed transition loops of length 1 consisting of only transient modes, i.e. modes for which at least one outgoing transition is enabled when the mode is entered. If there exists such a cycle, then the model will be executed, following the transition semantics 6, endlessly without the progress of time. 6
Conclusion We presented a formalism that allows the semantic description of linear control systems based on hybrid automata. Several problems of composition of other formalisms have been demonstrated with a comparative analysis to our method.
As next steps, we intend to derive the necessary and su cient conditions for non-Zenoness of the LTI-HA models and demonstrate that this property is preserved by composition. Furthermore, the problem of analysis of liveness and reachability and the implementation of a corresponding tool support will follow.
Appendix: A Modelling and Composition Example To further motivate the use of composable hybrid automata as introduced in this work, a small practical example for satellite functionality is discussed in this Appendix.
In the early conceptual study phase of development, a satellite downlink module which sends gathered information back to Earth can be modelled as having only two distinct states: Sending, when a ground station is visible and there is data to send, or Not Sending, when either no ground station is available or no data is there to be sent (or both). In the Sending state the rate of change of available data and sent data is the same with opposite signs, whereas in the Not Sending state both parameters remain constant (Fig. 2).
8dataavailable > 0; 8clkduration mod d 6= 0:
G((Not Sending, Sending); (dataavailable; clkduration); ;; f;g) = true start
Not Sending da_tasent = 0 da_taavailable = 0
Sending da_tasent = da_taavailable =
The automaton representing ground station availability is presented in Fig. 3. Here, as well, the system has only two states, since a ground station is either available or not. For now, we ignore irregularities of this otherwise periodic process, such as orbit perturbations and communication faults - they can be integrated into the model by taking the worst, shortest possible availability period. Ground station visibility is modelled by two running clocks, one for the period and one for the duration. Once the period time is up, ground station becomes visible for the possible duration time which is measured by the second clock, clkduration. When the clock reaches its maximum value, the automaton switches its discrete state back to the "Not Visible" mode. Since there are no resets in the LTI-HA formalism, it is not possible to reset the clocks. Hence, modular arithmetic is applied. When either of the transitions is taken in the ground station automaton, an output event is generated, one for the start of the visibility period, and one for the end, so that other concurrent automatas could synchronise their transitions with this periodic interval. However, it is also possible to model communication by using the global values of the two clocks of the ground station automaton. This approach is used in the Fig. 2 - it is easy to see that whenever the value of the clock clkduration is not zero modulo the interval duration, the ground station automaton is in its visible state, so the transition from "Not Sending" to "Sending" modes remains enabled. However, when the value is zero modulo interval duration and the downlink module is active, or there is no data to be sent, it should switch back to the "Not Sending mode".
8clkperiod mod (P d) == 0:
G((Not Visible, Visible); (dataavailable);fgs visibility startg,f;g) = true start
Not Visible cl_kperiod = 1
Visible cl_kduration = 1 8clkduration mod d == 0:
G((Visible, Not Visible); (dataavailable), fgs visibility endg,f;g) = true
It is assumed that initial states for the initial automata are ("Not Sending", fdatasent = 0; dataavailable = Cg) and ("Not Visible", fclkperiod = 0; clkduration = 0g). Obviously, both are composable, since the cut set of their initial valuations does not have contradictions. The composed automaton is built by applying composition rules 1-10 and its control graph is depicted in Fig. 4: 1. Lc = ( ('Not Sending', 'Not Visible'), ('Not Sending', 'Visible'), ('Sending', 'Not Visible'), ('Sending', 'Visible') ) = ( nsnv, nsv, snv, sv ) 2. T c = f ((nsnv, nsv), (nsnv, snv), (nsnv, sv), (snv, nsv), (snv, nsv), (snv, sv), (snv, nsnv), (snv, nsnv), (nsv, sv), (nsv, snv), (nsv, nsnv), (sv, nsv),(sv, nsv), (sv, nsnv), (sv, nsnv), (sv, snv))g 3. X c = fdataavailable; datasent; clkperiod; clkdurationg [ fclkperiod; clkdurationg = fdataavailable; datasent; clkperiod; clkdurationg, 4. SIc = ; [ ; = ; 5. SOc = ;[fgs visibility start, gs visibility endg = fgs visibility start, gs visibility endg 6. It is clear that for all the cases when only one of the states in a pair changes, transitions remain unchanged from the corresponding initial automaton. The output events of the corresponding edges are: { (nsnv, nsv): f gs visibility start g; { (nsnv, snv): ;; { (nsnv, sv): f gs visibility start g; { (snv, nsv): f gs visibility start g; { (snv, nsv): f gs visibility start g; { (snv, sv): f gs visibility start g; { (snv, nsnv): ;; { (snv, nsnv): ;; { (nsv, sv): ;; { (nsv, snv): f gs visibility end g; { (nsv, nsnv): f gs visibility end g; { (sv, nsv): ;; { (sv, nsv): ;; { (sv, nsnv): f gs visibility end g; { (sv, nsnv): f gs visibility end g; { (sv, snv): f gs visibility end g. 7. Since the set of input events is empty, f;g is assigned as input events to the all of the transitions. 8. The guards of the resulting transitions are: { (sv, nsv): g((8clkduration mod d == 0); ;; f;g) = true this transition will never be taken since the automaton cannot stop sending available data while the ground station is available; { (sv, nsnv): g((8dataavailable 0; 8clkduration mod d == 0); f gs visibility end g; f;g) = true { (sv, nsnv): g((8clkduration mod d == 0); f gs visibility end g; f;g) =
true { (sv, snv): g((8clkduration mod d == 0); f gs visibility end g, f;g) = true; this transition will be immediately followed by the (snv, nsnv), since the guard is also ful lled 9. The ow functions of the resulting automaton are: { nsnv: da_tasent = 0; da_taavailable = 0; cl_kperiod = 1; cl_kduration = 0 { nsv: da_tasent = 0; da_taavailable = 0; cl_kperiod = 0; cl_kduration = 1 { snv: da_tasent = ; da_taavailable = ; cl_kperiod = 1; cl_kduration = 0 { sv: da_tasent = ; da_taavailable = ; cl_kperiod = 0; cl_kduration = 1 10. Initial state of the composed automaton is given as:
Ic = (nsnv; fdatasent = 0; dataavailable = Cg [ fclkperiod = 0; clkduration = 0g) = (nsnv; fdatasent = 0; dataavailable = C; clkperiod = 0; clkduration = 0g) nsnv nsv snv Fig. 4: The resulting control graph for the composed automaton. Labels are omitted for simplicity. Since snv-state is transient, it is coloured.