Linear time-invariant hybrid automata (LTI-HA) have been introduced to model space missions in early design phases. One of LTIHA's main objectives was therefore to allow a composition of (sub) models. In this paper, we evaluate the expressiveness of the composition in LTI-HA. To compare their expressiveness with the existing hybrid automata formalisms, this work proposes a formal notion of compositional expressiveness. In contrast to the more traditional proofs using simulation relations or bisimilarity to compare single models or their respective behavioral expressiveness or equivalence, compositional expressiveness relies on the complexity of the models and the composition operators enabling the engineer to invest less e ort in the modeling process. The following text provides a comparative study of the LTI-HA and several other hybrid formalisms, such as linear hybrid automata and the hybrid I/O automata, with respect to their compositional expressiveness. Speci cally, adequacy of their application is discussed based on the case study in space mission feasibility veri cation.
Most of the real systems consist of a set of subsystems brought together e.g. by physical aspects or function. A compositional approach to modeling and analysis of such a system relies exclusively on the models of the subsystems, without any holistic information about the composed system, an approach that was rst formalized by Gottlob Frege in 1923 [FP93] [Fre05].
For describing space systems during early design phases, a hybrid formalism was proposed in [ATW16] [ASGW16] [ATW15] - Linear Time-Invariant Hybrid Automata (LTI-HA). The adequacy of LTI-HA was demonstrated in [ARW17] by providing an operational semantics for the space mission domain-speci c language proposed by Schaus et. al [STF+13]. LTI-HA address the issue of combining continuous dynamics of di erent discrete states by applying the superposition principle in the composition operator which is extensively applied in the classical control theory as well as the theory of hybrid systems [LA14].
While expressiveness is usually considered from the point of view of behavioral comparison of two formalisms on a meta level, comparison of expressiveness from the compositional point of view lacks the deserved attention [Cas05] [BCH+13] [SA06]. Although many extensions for compositional semantics exist for hybrid formalisms, only few of them are discussed in terms of expressiveness of models [SY96] [Sif99] [BS00]. Although not desirable, this is an understandable state of a airs since compositional expressiveness of a modeling method is rather a question of taste and usability.
The contribution of the following paper lies in the introduction of the notion of compositional expressiveness and its application for comparison of LTI-HA with other hybrid automata (HA) formalisms, such as linear hybrid automata and hybrid I/O automata. The formal considerations in this work are supported by an use-case based comparison of expressive power of the LTI-HA.
The remaining paper is structured as follows: the next section discusses some of the related work, followed by several supporting de nitions in section 3. Section 4 is the core of this paper. First, two motivational examples are provided from the application domain of early spacecraft modeling. Then, several formal metrics are introduced to support the formal de nition of the compositional expressiveness which is immediately applied to the LTI-HA formalism with respect to hybrid I/O automata (HIOA) and linear as well as rectangular HA (LHA and RHA, respectively). The paper is nalized with a discussion of behavioral expressiveness of LTI-HA models and some concluding remarks. 2
Related Work As such, LTI-HA are closely related to the switched, piecewise a ne and complementarity systems [LA14]. In [GT04], a class of piecewise a ne automata with superposition support is brie y introduced to be immediately applied for modeling biological protein regulatory networks. However, as discussed in [ATW16] and [ATW18], support for invariants and discrete resets could be problematic for the composition. The composition operator has also not been formally introduced for this promising formalism [GT04].
The general framework for timed compositional modeling formalism - timed automata with deadlines where invariants of the classical timed automata are replaced with the notion of deadlines - taken by Sifakis and Yovine [SY96] was extended to hybrid systems in [BS00] by Bornot and Sifakis. They discuss the possible compositional semantics of actions for hybrid systems. It is also assumed that compatible automata operate on disjunct state spaces [BS00].
Van der Shaft and Schumacher [SS01] investigate compositionality from the point of view of dynamic systems and discuss some important properties of the composition operator such as commutativity and associativity. 3
De nitions The following de nitions capture the essential terms necessary for the later discussions [ATW18].
De nition 1 (LTI-HA). A linear time-invariant hybrid automaton H is a tuple (L; X ; SI ; SO; T ; F ), where: { L = fL1; : : : ; Lng is a set of discrete locations (or modes); { X is a set of continuous real-valued variables, called state variables. Time in this context refers to a designated variable t 2 X . { SI and SO are two disjoint sets of input and output events, respectively, which de ne the event signature of the automaton; { T L 2C(X ) 2SI 2SO L is a guarded (not necessarily complete) transition relation, where denotes a Cartesian product and C(X ) is a set of all possible constraints over X . The guard is thus a triple (C; E ; A) with a set of constraints C 2 2C(X ) a set of input events E 2 2SI and a set of output events A 2 2SO . The locations along with the transitions (with possible loops) constitute the control graph representing the structure of the given hybrid automaton; { The change of any x 2 X , except for the time reference t, at any time point is described by the ow function fL of the currently active location describing the continuous change of system state xi(t) = fxi;L(t): We are restricting the ow functions only to those which are valid solutions for ordinary linear time-invariant di erential equations of some order k 1. This restriction guarantees that ow functions ful ll the superposition property. Therefore, for two simultaneously active locations L1 and L2 of two concurrent hybrid automata the resulting rate of change of a global continuous variable xi is de ned as xi(t) = fxi;L1 (t) + fxi;L2 (t). Let F denote the set of ow functions for every location in L and t_ = 1 for all L 2 L.
De nition 2 (Initial con guration). I is the initial state/con guration of the system (t0) = (LI ; VI ), where LI 2 L is the initial active mode, VI : X 7! R is the initial valuation of all the variables in X and VI (t) = t0. De nition 3 (Composition operator). Any two LTI-HA H1 and H2 for cwohmicphathibolledsh8ybxri2d Xau1to\mXa2ta:, VthI1e(xp)ar=alVleIl2(cxo)maproesictaiollnedHc1ojmjHp2atpibroled.uGceisvean ntwewo hybrid automaton Hc = (Lc; X c; SIc; SOc; T c; F c) with the initial con guration Ic, where the components are de ned as follows: 1. Lc = L1 L2 = f(L11; L21); : : : ; (L1n1 ; L2n2 )g =
fLc11; Lc12; : : : ; Lc1n2 ; : : : ; Lcn1n2 g 2. X c = X 1 [ X 2 3. SIc = (SI1nSO2) [ (SI2nSO1) 4. SOc = SO [ SO
1 2 5. 8 transitions (Lix; Cx; E x; Ax; Lkx); (Ljy; Cy; E y; Ay; Lly): ((ba)) i9iff((LE(ixEj y;\C\SxOAy[x=C=;y:;EE8yxL\[2S(OxLE)yyn:aAn9d(x()L(;SAixOy;xL\[);EACxyx=;;LE;kx)l;))A2x;T(cL,kx; L)) 2 T c, or ((E x \ SOy = ;) and (E y \ SOx = ;)) where either x = 1; y = 2, or vice versa. 6. 8fxk;Li (t) 2 F 1; fxk;Lj (t) 2 F 2: fxk;Lij (t) = fxk;Li (t) + fxk;Lj (t) 7. IC = (LcI1I2 ; VI1 [ VI2) The operator is not de ned for not compatible LTI-HA. 4
Compositional Expressiveness The following section provides two motivational examples: one informally discusses a use case when set-based directional event semantics is more expressive than any semantics based on a singleton labels, and the second shows how superposition principle allows a modeling engineer to apply the divide and conquer approach more e ectively and therefore reduces modeling e ort. 4.1
... ...
i k H1 ...
...
E1 : fag A1 : fg ...
j l H2
E2 : fg A2 : fag fc 10g ... ... ...
m n H3
E3 :3f:af;gbg A fx > 10g ... ... ...
o p H4
E4 : fg Afd4 : fbg 5g ... ... Consider the interaction patterns between the four transitions in the four LTI-HA depicted in Figure 1. The automata are representing, from left to right: a downlink module of a satellite moving on a Low Earth Orbit(LEO), primary ground station A, synchronization module and the secondary ground station B. Without loss of generality, we are only considering the parts of the automata representing interactions with one another and not the speci cs of their dynamics. Synchronization events a and b represent availability of the ground stations A and B, respectively. Synchronization module is responsible for synchronizing the clocks of the satellite, a procedure carried out only when both ground stations are available. This is done to eliminate possible synchronization faults (see, for example, [DHSS95] or [LMS86]).
It is clear that transitions j ! l and o ! p can be taken independently, while the transitions i ! k and m ! n cannot. The transition m ! n can only be taken simultaneously with the both enabled transitions j ! l and o ! p. The transition i ! k will only be synchronized with the transition j ! l. The paths of non-zero length from l to j and p to o are represented with thick dotted arrows. If the locations j and o can simultaneously be active with valuations fc 10; d < 5g and fc 10; d 5g, then, obviously, transitions j ! l and o ! p are not always taken synchronously.
For HIOA or structured HIOA (SHIOA [MLL06] [Mit07]) to model this system, a relabling procedure consisting of two modi cations may be performed: rst, both ground stations have to be modeled as a single automaton; second, the transition with two events being simultaneous, a new event has to be introduced, e = fa; bg which would synchronize with the m ! n transition. The same holds for the timed automata if the continous dynamics could be modeled with only clock variables [BY04].
Set-based undirectional hybrid automata formalism like [RTP96] may be suitable for modeling the system described in Figure 1. However, the composition operator in [RTP96] only considers synchronous actions in case when there is a non-empty intersection between them. Let us assume that the transitions i ! k, m ! n and o ! p are labeled with i!k = fag, m!n = fa; bg and o!p = fbg, respectively. The above interaction is indeed preserved. However, if we rst compose H1 with H4 and only then with H3, the information about possible simultaneity of events a and b is lost. Since composition operator in [RTP96, p.7] only considers the labeled dependencies between transitions pairwise, transition with m!n = fa; bg will never be enabled. However, merging m ! n rst with either i ! k or o ! p solves the problem. Hence, composition operator in [RTP96, p.7] is not associative. Our composition operation is both associative and supports event directions making them more intuitional.
Obviously, not set-based undirectional based are less expressive than the last two discussed methods. This clearly demonstrates the advantage of the directional set-based event synchronization: directionality makes events more intuitional while assigning more than one label to a transition, more complex communication patterns are possible. 4.2
As a second example, consider the two automata from [ATW18] in Figure 2.
NotdscS===encsdding (fd 0; c > CRITICALg; f gs visible g, f a g) dcs===Secncc12d1(i(t(nttg tt)t))
(fd = 0g; fg;f b g ) (fg; f gs not visible g,f c g ) Off s = s d = d c = c (fc > CRITICALg;f event visible g,f d g ) ( f g(,ffdevenLtI MnoItTgv,fisgib,fleegg,f)f g )
On d = sc3=(ts t) c = c4(t t) In the early conceptual phase of development, the satellite downlink module which sends gathered information back to Earth is modeled 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 there is no data 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.
The valuable data which is sent back to Earth comes from a camera which can rotate and x on the events of interest. Hence, depending on whether an event is visible or not, the camera can also be in two states: On and O . The data can only be written if there is enough free storage, therefore the constant LIMIT represents the maximum data that can be stored at any instance. The constant CRITICAL stands for the lowest level of battery charge needed for any of the components to start.
The continuous variables s; d; c stand for the amount of data sent, the data still stored on the satellites storage unit and the battery charge, respectively. c1c4 are some prede ned constants. The downlink component can only be activated when a ground station is visible which is represented by the gs visible event.
Since LTI-HA explicitly support the superposition principle for ow functions, output trajectories do not need to be exclusive. This allows to combine e ects of both automata on the same continuous variable, in this case all three of them: s; d; c by the composition operator [ATW18].
(S)HIOA explicitly forbid superposition of the output trajectories [LSV03, p.131,p.141] [Mit07, p.35]. That is, for any formalism without support for superposition to model a system where some of the components have overlapping continuous output trajectories, it is necessary to model all of those components as a single automaton with the cartesian product of all of the corresponding locations.
Other hybrid automata formalisms follow either the same strategy as (S)HIOA or imply an agreement of ow conditions between the locations [ATW18]. Thus, they would also require an engineer to explicitly specify all of the possible combinations of ows thus eliminating the advantages of compositional analysis altogether. 4.3
Transitions Given m LTI hybrid automata H1; :::; Hm, we de ne a synchronization function sync: T[ 7! 2T[ that maps the transition i to the set of all transitions which synchronize with it: sync( i) = 8f jj i = j ; i 6= jg for non-directional event semantics >>><>>>>>f jj i \ Lj = j \ Li 6= ;; i 6= jg f(RoLHrHAsAet[-[RbAaaCss0He5dH]n9[Po3n]V-[9dN4iOr]e[ScHtYieo9nn30a]0l[]H,evHeenAn0t0[]As,ebm1a2n])tics (LHA [RTP96]) >>f jj a; i = e; j ; i 6= jg for directional event semantics >>> (HIOA [LSV03], TA [BY04]) > j >>f jA i \ E j = SOi \ E j 6= ;; i 6= jg for set-based event semantics : (LTI-HA [ATW18]) where T[ = Si=1::m T i with T i from Hi, i is the label on the transition i in the automaton H , e; i ; a; i are the input and output labels on the i transition in the automaton Hi. i is a set of labels assigned to transition i respectively. Li is the set of labels of the LHA i [RTP96]. i is any transition out of T[. Without loss of generality, we assume that for the directional event semantics, there is always only a single automaton generating every consumable event [ATW18] [LSV03].
The function rsync : T[ 7! 2T[ maps the set of all transitions i to the set of all transitions which generate the necessary inputs for the transition at hand: rsync( i) = 8same as sync( i) for non-directional event semantics >>><>>>>>same as sync( i) f(RoLHrHAsAet[-[RbAaaCss0He5dH]n9[Po3n]V-[9dN4iOr]e[ScHtYieo9nn30a]0l[]H,evHeenAn0t0[]As,ebm1a2n])tics (LHA [RTP96]) >>f jj e; i = a; j ; i 6= jg for directional event semantics >>> (HIOA, TA) > j >>f jE i \ A j = E i \ SOj 6= ;; i 6= jg for set-based event semantics : (LTI-HA)
Therefore, rsync de nes a di erent set of values in the cases of directional event semantics. Table 1 provides a comparative study of compositional properties de ned below for HA depending on the types of event semantics: directional or non-directional, set-based or singular (singleton).
jsync( i)j provides the number of transitions from other automata with whom the given transition may synchronize. For the directed event semantics, output events are usually observable by any other automata [LSV03] [ATW18]. Obviously, for all the formalisms, this number is greater equal than zero.
The jrsync( i)j-row represents the number of transitions having as outputs the inputs of i. Since the inverse function is de ned in the same way as the original for the undirectional event semantics, no change is observed here.
8j : jf j j j 2 rsync( i); E j \ A j E j \ Higj is the number of transitions which possibly generate the necessary input for the given transition but do not have all the events generated by the automaton containing them. This is a critical condition to be ful lled during composition, if there is a single producer for each event. It is guaranteed by the condition 5b for the composition operator of LTIHA and the condition (3) for the event synchronization in [RTP96, p.7].
jfsjs rsync( i); 8 j ; k 2 s : j = k; @s0 rsync( i) with l 2 s0; 9 j 2 s : j = lgj is the number of hybrid automata generating the necessary events for a given transition. In the case of singular directional event semantics it is only possible to synchronize with a single producer of an event for the HIOA [LSV03] [Mit07]. Timed automata in the UPPAAL [BLP+96] allow for several generators of a single event. This row is emphasized since this is a case of an increased expressiveness of set-based labeling formalisms in contrast to singular labeling mechanisms.
max (jsjs rsync( i); 8 j ; k 2 s : j = k; @s0 rsync( i) with l 2 s0; 9 j 2 s : j = lgj) represents the maximum number of transitions generating the necessary events for the given transition, per automaton. For all the cases, the number of those transitions can be non-zero, however, for the cases of set-based labelings, the events should be exactly those which lie in the intersection set of the whole automaton and the given transition i, since synchronization (and structural merging during composition) only occur pairwise in the existing formalisms.
The following row is another case where set-based approaches have a de nite advantage with respect to singular cases: it represents the number of possible transitions from other automata which can consume subsets of the given event label. Obviously, no such thing exists for singular cases, and only those having strictly the same labeling will be able to sychronize.
Properties
Examples
Event Non-directional Semantics Singular Set-based [ACHH93] [NOSY93] [RTP96] [Hen00]
Singular De nition 4 (Event Dependency of Guards). Two guards - g1 = (C1; E1; A1) from H1; g2 = (C2; E2; A2) from H2 - are said to be event-dependent i E1 \ A2 6= ; _ E2 \ A1 6= ;. The guard g1 is said to be event-dependent on the second automaton i E1 \ SO2 6= ;.
Event (in)dependency of guards consequently implies event-(in)dependency of the corresponding transitions. It is clear from the constraint SI \ SO = ; that those two guards cannot be in the same automaton.
of guards G of size k 2 has a cycle of event dependencies if there is a sequence of these guards (g0; :::; gk 1), such that 8i; 0 i < k : Ai \ E(i+1)mod k 6= ;.
Clearly, circular event dependencies are only possible for the directional cases. The last row shows wether the formalism has an explicit support for stutter transitions. HIOA have eliminated them in the later rede nitions to avoid compositionality issues [LSV03]. LTI-HA do not have implicit stutter transitions. However, they can be explicitly de ned, as provided in the Table 1. These transitions, however, are always enabled and will be taken immediately when their start-location is entered. They also pose a danger of introducing time locks (time convergence), should there be a cycle containing only stutter transitions.
The relabling procedure discussed in the rst example of this section, can be formalized as follows: 8 i from Hi where jE i j > 1 : 8Hj with SOj \ E i 6= ; : jj j H The labeled event set E i will be then renamed to a single letter in the composed automaton. Although we do not account here for the cascading dependencies of the events, it should be clear that in the worst case all of the automata Hj ; j = 1::m will have to be combined with each other by the user. E.g. consider the scenario where one LTI-HA consumes all of the events generated by other LTI-HA over a single transition. Furthermore, for any set of event labels A, all of the possible subset of those events can be consumed by a di erent automaton. That is, for every possible set from 2A, a new transition has to be introduced in the automaton containing a transition labeled with A. (1) Locations As discussed in the second example of this section, the modeling engineer has to account for all of the possible combinations of continuous ows which could become exponential in the minimum number of states of the HA, if for all jLij holds jLij 2. That is, for 10 LTI-HA with three states per automaton, 310 locations would be required to model in any formalism not supporting superposition: i.e. (S)HIOA, LHA, RHA, HA, etc.
Formally, in the worst case for a set of m LTI hybrid automata H1; :::; Hm: if 9X
XU ;XU =
X i where 8x 2 X; 8Lij : x_ Lij 6= 0 (2) then L =
[ i=1::m m i=1
m Li; jLj = Y
i jL j i=1 where L is the total set of the composed locations.
De nition of Compositional Expressiveness Considering the above metrics, we can now de ne the notion of compositional expressiveness for hybrid automata. It amounts to the information a modeling engineer uses to describe the system components before the composed system is built. Clearly, since the composition operator has exponential run-time and produces a structure with an exponential number of nodes, it is desirable to shift the modeling complexity into the "pre-composition phase" since the modeling e ort is then linear in the number of nodes and edges.
We rely on the number of edges (T ) as well as the number of vertices (L) needed to describe a system S. We assume that for both formalisms under comparison, a minimal representation can be achieved, and that there is some behavioral equivalence satis ed for models of S in the respective formalisms (e.g. bisimilarity).
compositionally more expressive than a modeling formalism B (A c B) if, for describing a system S (or a family of systems): for a minimal representations of S in A, HA(S), and B, HB(S), respectively. Proposition 1. For a family of systems where the the condition from the equation (2) holds or 9 i from T[ with jE i j > 1, linear time-invariant hybrid automata are compositionally more expressive than HIOA.
Proof. The proof follows from the discussions and metrics from the this section. 5
Discussion This paper has introduced an initial approach at formalizing the notion of compositional expressiveness in terms of events labeling and continuous ow combinations. It has been directly applied to demonstrate the superior compositional expressiveness of LTI-HA with respect to HIOA.
Timing of transitions was never considered in this work, as well as the modal extensions of guards [SY96, p.5]. In the extended version of this work, we plan to include timeliness of events as well as the modalities for combining the guards which are assigned to the transitions into the notion of compositional expressiveness. We also intend to adopt the notion of HA comparability of Lynch et. al. [LSV03] and put the LTI-HA in the context of other formalisms in terms of behavioral expressiveness.
Associativity is an important property for composition of discrete event systems in general and hybrid automata in particular [SS01] [CL10]. Proving it for LTI-HA is not trivial due to the complex event semantics and remains as a future challenge.
The relabling procedure discussed in section 4 can potentially be extended to a full algorithm which would transform a system of LTI-HA into a system of HIOA which is a powerful modeling method with tool support [Fre05]. This algorithm would also require a behavioral expressiveness relation established between the two formalisms which we also intend as a future work. A formal meta-language that could be used to de ne simulation relations could be the extension theorem [BS00] [SY96] or timed transition systems [Cas05] [BCH+13].