Thomas Gazagnaire
email: thomas.gazagnaire@citrix.com

Blaise Genest
email: blaise.genest@irisa.fr

Loïc Hélouët
email: loic.helouet@irisa.fr

P S Thiagarajan

Shaofa Yang
email: yangsf@comp.nus.edu.sg

Causal Message Sequence Charts

. The high expressive power of MSCs renders many basic problems concerning these languages undecidable. However, several of these problems are decidable for languages that possess a behavioral property called "existentially bounded". Unfortunately , collections of scenarios outside this class are frequently exhibited by systems such as sliding window protocols. We propose here an extension of MSCs called causal Message Sequence Charts and a natural mechanism for defining languages of causal MSCs called causal HMSCs (CaHMSCs). These languages preserve decidable properties without requiring existential bounds. Further, they can model collections of scenarios generated by sliding window protocols. We establish here the basic theory of CaHMSCs as well as the expressive power and complexity of decision procedures for various subclasses of CaHMSCs. We also illustrate the modeling power of our formalism with the help of a realistic example based on the TCP sliding window feature.

Introduction

Scenario languages based on Message Sequence Charts (MSCs) have met considerable interest in the last decade. The attractiveness of this notation derives from two of its major characteristics. Firstly, MSCs have a simple and appealing graphical representation based on just a few concepts: processes, messages and internal actions. Secondly, from a mathematical standpoint, scenario languages admit an elegant formalization: they can be defined as languages generated by finite-state automata over an alphabet of MSCs. These automata are usually called High-level Message Sequence Charts (HMSCs) [START_REF]Message Sequence Chart (MSC)[END_REF].

An MSC is a restricted kind of labelled partial order and an HMSC is a generator of a set of MSCs, that is, a language of MSCs. For example, the MSC M shown in Figure 2 is a member of the MSC language generated by the HMSC of Figure 1 while the MSC N shown in Figure 2 is not. HMSCs are very expressive and hence a number of basic problems associated with them cannot be solved effectively. For instance, it is undecidable whether two HMSCs generate the same collection of MSCs [START_REF] Muscholl | Deciding Properties for Message Sequence Charts[END_REF] or whether an HMSC generates a regular MSC language; an MSC language is regular if the collection of all the linearizations of all the MSCs in the language is a regular string language in the usual sense. Consequently, subclasses of HMSCs have been identified [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF][START_REF] Alur | Model checking of Message sequence Charts[END_REF][START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF] and studied.

On the other hand, a basic limitation of HMSCs is that their MSC languages are finitely generated. More precisely, each MSC in the language can be defined as the sequential composition of elements chosen from a fixed finite set of MSCs [START_REF] Morin | Recognizable sets of Message Sequence Charts[END_REF]. However, the behaviors of many protocols constitute MSC languages that are not finitely generated. This occurs for example with scenarios generated by the alternating bit protocol. Such protocols can induce a collection of braids like N in Figure 2 which cannot be finitely generated.

One way to handle this is to work with the so called safe compositional HMSCs in which message emissions and receptions are decoupled in individual MSCs but matched up at the time of composition, so as to yield an MSC. Compositional HMSCs are however notationally awkward and do not possess the visual appeal of HMSCs. Furthermore the general class of compositional HMSC languages embeds the full expressive power of communicating automata [START_REF] Brand | On Communicating Finite State Machines[END_REF] and consequently inherits all their undecidability results. This paper proposes a new approach to increase the modeling power of HMSCs in a tractable manner. We first extend the notion of an MSC to a causal MSC in which the events belonging to each lifeline (process), instead of being linearly ordered, are allowed to be partially ordered. To gain modelling power, we do not impose any serious restrictions on the nature of this partial order. However, we assume a suitable Mazurkiewicz trace alphabet [START_REF] Diekert | The Book of Traces[END_REF] for each lifeline and use this to define a composition operation for causal MSCs. This leads to the notion of causal HMSCs.

A property called existential boundedness [START_REF] Genest | A Kleene Theorem and Model Checking for a Class of Communicating Automata[END_REF] leads to a powerful proof technique for establishing decidability results for HMSCs. Informally, this property states that there is a uniform upper bound K such that for every MSC in the language there exists an execution along which -from start to finish-all FIFO channels remain K-bounded. On the other hand, when all executions of all MSCs in a language can occur within a fixed upper bound K on channels, the corresponding property is called universally bounded. A causal HMSC (i.e. the MSC language associated with a causal HMSC) is a priori not existentially bounded. Hence the proof method cited above can not be used to obtain the desired decidablity results. Instead, we need to generalize the methods of [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF] and of [START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF] in a non-trivial way.

Our fist major result is to formulate natural -and decidable-structural conditions and to show that causal HMSCs satisfying these conditions generate MSC languages that are regular. Our second major result is that the inclusion problem for causal HMSCs (i.e. given two causal HMSCs, whether the MSC language defined by the first one is included in the MSC langauge of the other) is decidable for causal HMSCs using the same Mazurkiewicz trace alphabets, provided at least one of them has the structural property known as globallycooperative. Furthermore, we prove that the restriction that the two causal HMSCs have identical Mazurkiewicz trace alphabets associated with them is necessary. These results constitute a non-trivial extension for causal HMSCs of comparable results on HMSCs [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF][START_REF] Alur | Model checking of Message sequence Charts[END_REF][START_REF] Henriksen | A Theory of Regular MSC Languages[END_REF] and [START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF]. In addition, we identify the property called "window-bounded" which appears to be an important ingredient of the "braid"-like MSC languages generated by many protocols. Basically, this property bounds the number of messages a process p can send to a process q before having received an acknowledgement to the earliest message. We show it is decidable if a causal HMSC generates a window-bounded MSC language. Finally, we compare the expressive power of languages based on causal HMSCs with other known HMSC-based language and give a detailed example based on the TCP protocol to illustrate the modeling potential of causal HMSCs.

This paper is an extended version of the work presented in [START_REF] Gazagnaire | Causal Message Sequence Charts[END_REF] and contains several important changes and improvements. Specifically, the definition of sregularity for causal HMSCs has been weakened. As a result, causal HMSCs which were not s-regular according to [START_REF] Gazagnaire | Causal Message Sequence Charts[END_REF] -and in fact not even globallycoperative-are deemed to be s-regular under the weakened definition. We have also included here complete proofs and have added a detailed example.

In the next section we introduce causal MSCs and causal HMSCs. We also define the means for associating an ordinary MSC language with a causal HMSC. In the subsequent section we develop the basic theory of causal HMSCs. To this end, we identify the subclasses of s-regular (syntactically regular) and globally-cooperative causal HMSCs and develop our decidability results. In section 4, we identify the "window-bounded" property, and show that one can decide if a causal HMSC generates a window-bounded MSC language. In section 5 we compare the expressive power of languages based on causal HMSCs with other known HMSC-based language classes. Finally, in section 6, we give a detailed example based on the TCP protocol to illustrate the modeling potential of causal HMSCs.

MSCs, causal MSCs and causal HMSCs

Through the rest of the paper, we fix a finite nonempty set P of process names with |P| > 1. For convenience, we let p, q range over P and drop the subscript p ∈ P when there is no confusion. We also fix finite nonempty sets Msg, Act of message types and internal action names respectively. We define the alphabets Σ ! = {p!q(m) | p, q ∈ P, p = q, m ∈ Msg}, Σ ? = {p?q(m) | p, q ∈ P, p = q, m ∈ Msg}, and Σ act = {p(a) | p ∈ P, a ∈ Act}. The letter p!q(m) means the sending of a message with content m from p to q; p?q(m) the reception of a message of content m at p from q; and p(a) the execution of an internal action a by process p. Let Σ = Σ ! ∪Σ ? ∪Σ act . We define the location of a letter α in Σ, denoted loc(α), by loc(p!q(m)) = p = loc(p?q(m)) = loc(p(a)). For each process p in P, we set Σ p = {α ∈ Σ | loc(α) = p}.

Definition 1 A causal MSC over (P, Σ) is a structure B = (E, λ, {⊑ p }, ≪),
where E is a finite nonempty set of events, λ : E → Σ is a labelling function, and the following conditions hold:

• For each process p, ⊑ p ⊆ E p × E p is a partial order, where E p = {e ∈ E | λ(e) ∈ Σ p }. We let ⊑ p ⊆ E p × E p denote the least relation such that ⊑ p is the reflexive and transitive closure of ⊑ p ( ⊑ p is the Hasse diagram of ⊑ p ). • ≪ ⊆ E ! × E ? is a bijection, where E ! = {e ∈ E | λ(e) ∈ Σ ! } and E ? = {e ∈ E | λ(e) ∈ Σ ? }.
For each e ≪ e ′ , λ(e) = p!q(m) iff λ(e ′ ) = q?p(m).

• The transitive closure ≤ of the relation p∈P ⊑ p ∪ ≪ is a partial order.

For each p, the relation ⊑ p dictates the "causal" order in which events of E p may be executed. The relation ≪ identifies pairs of message-emission and message-reception events. We say that the causal MSC B is weak-FIFO iff for any e ≪ f , e ′ ≪ f ′ such that λ(e) = λ(e ′ ) = p!q(m ′ ) (and thus λ(f ) = λ(f ′ ) = q?p(m)), we have either e ⊑ p e ′ and f ⊑ q f ′ ; or e ′ ⊑ p e and f ′ ⊑ q f . In weak-FIFO2 scenarios, messages of the same content between two given processes cannot overtake. Note however that messages of different kind between two processes can overtake. Note that we do not demand a priori that a causal MSC must be weak FIFO. Testing (weak) fifoness of a causal MSC of size b can be done in at most O( b 2 8 -b 4 ), by considering all pairs of messages in the MSC.

Let B = (E, λ, {⊑ p }, ≪) be a causal MSC. We shall write |B| for |E| and refer to |B| as the size of B. A linearization of B is a word a 1 a 2 . . . a ℓ over Σ such that E = {e 1 , . . . , e ℓ } with λ(e i ) = a i for each i; and e i ≤ e j implies i ≤ j for any i, j. We let Lin(B) denote the set of linearizations of B. Clearly, Lin(B) is nonempty. We set Alph(B) = {λ(e) | e ∈ E}, and Alph p (B) = Alph(B) ∩ Σ p for each p.

The leftmost part of Figure 3 depicts a causal MSC M . In this diagram, we enclose events of each process p in a vertical box and show the partial order ⊑ p in the standard way. In case ⊑ p is a total order, we place events of p along a verti-cal line with the minimum events at the top and omit the box. In particular, in M , the two events on p are not ordered (i.e. ⊑ p is empty) and ⊑ q is a total order. Members of ≪ are indicated by horizontal or downward-sloping arrows labelled with the transmitted message. Both words p!q(Q).q!p(A).q?p(Q).p?q(A) and q!p(A).p?q(A).p!q(Q).q?p(Q) are linearizations of M .

An MSC B = (E, λ, {⊑ p }, ≪) is defined in the same way as a causal MSC except that every ⊑ p is required to be a total order. In an MSC B, the relation ⊑ p must be interpreted as the visually observed order of events in one sequential execution of p. In Figure 3, Vis(M ) consists of MSCs M 1, M 2. The initial idea of visual ordering comes from [START_REF] Alur | An analyzer for Message Sequence Charts[END_REF], that notices that depending on the interpretation of an MSC, for example when a lifeline describes a physical entity in a network, imposing an ordering on message receptions is not possible. Hence, [START_REF] Alur | An analyzer for Message Sequence Charts[END_REF] distinguishes two orderings on MSCs: a visual order (that is the usual order used for MSCs), that comes from the relative order of events along an instance line, and a causal order, that is weaker, and does not impose any ordering among consecutive receptions.

Let B ′ = (E ′ , λ ′ , {⊑ ′ p }, ≪ ′ ) be a causal MSC. Then we say the MSC B is a visual extension of B ′ if E ′ = E, λ ′ = λ, ⊑ ′ p ⊆ ⊑ p and ≪ ′ = ≪. We let Vis(B ′ ) denote the set of visual extensions of B ′ .
Note that the set of visual extensions of a causal MSC B is not necessarily the union of instance per instance linearizations, as an extension of a causal MSC must remain a MSC, ie. the relation among the events has to remain a partial order. Consider for example, the causal MSC B of Figure 4, and its visual extensions in Figure 5: in any visual extension V = ({e 1 , e 2 , f 1 , f 2 }, λ, {⊑ p , ⊑ q }, ≪) ∈ V is(B) we cannot have e 2 ⊑ p e 1 and f 1 ⊑ q f 2 at the same time.

We next define a concatenation operation for causal MSCs. Unlike for usual MSCs, events of a same process need not be dependent. To express whether there should be a dependency or not, for each process p in P, we fix a concurrent alphabet (Mazurkiewicz trace alphabet [START_REF] Diekert | The Book of Traces[END_REF]) (Σ p , I p ) for each process p ∈ P, where I p ⊆ Σ p × Σ p is a symmetric and irreflexive relation called the independence relation over the alphabet of actions Σ p . We denote the dependence relation (Σ p × Σ p ) -I p by D p . These relations are fixed for the rest of the paper (unless explicitly stated otherwise). Following the usual definitions of Mazurkiewicz traces, for each (Σ p , I p ), the associated trace equivalence re- A causal MSC B is said to respect the trace alphabets {(Σ p , I p )} p∈P iff ⊑ p respects (Σ p , I p ) for every p. In order to gain modelling power, we have allowed each ⊑ p to be any partial order, not necessarily respecting (Σ p , I p ).

We shall now define the concatenation operation of causal MSCs using the trace alphabets {(Σ p , I p )} p∈P .

Definition 2 Let B = (E, λ, {⊑ p }, ≪) and B ′ = (E ′ , λ ′ , {⊑ ′ p }, ≪ ′ ) be causal MSCs. We define the concatenation of B with B ′ , denoted by B ⊚ B ′ , as the causal MSC B ′′ = (E ′′ , λ ′′ , {⊑ ′′ p }, ≪ ′′ ) where:

• E ′′ is the disjoint union of E and E ′ . λ ′′ is given by: λ ′′ (e) = λ(e) if e ∈ E, λ ′′ (e) = λ ′ (e) if e ∈ E and ≪ ′′ = ≪ ∪ ≪ ′ . • For each p, ⊑ ′′ p is the transitive closure of

⊑ p ⊑ ′ p {(e, e ′ ) ∈ E p × E ′ p | λ(e) D p λ ′ (e ′ )}
Clearly, ⊚ is a well-defined and associative operation. Note that in case B and B ′ are MSCs and D p = Σ p × Σ p for every p, then the result of B ⊚ B ′ is the asynchronous concatenation (also called weak sequential composition) of B with B ′ [START_REF] Reniers | Message Sequence Chart: Syntax and Semantics[END_REF], which we denote by B • B ′ . Note that when B 1 and B 2 are weak FIFO causal MSCs, then their concatenation is also weak FIFO. This property comes from the irreflexive nature of the independence relations. This remark also holds for the concatenation of MSCs. We also remark that the concatenation of causal MSCs is different from the concatenation of traces. The concatenation of trace [u] p with [v] p is the trace [uv] p . However, a causal MSC B needs not respect {(Σ p , I p )} p∈P . Consequently, for a process p, the projection of Lin(B) on Alph p (B) is not necessarily a trace. Figure 6 shows an example of sequential composition of two causal MSCs B 1 and B 2 , with the dependency relations D p and D q being the commutative and reflexive closure of p!q(m), p!q(n) , p!q(n), p?q(u) and q?p(n), q!p(v) respectively. Note that although the dependence relation D p contains the pair p!q(m), p!q(n) , sendings of messages m and n by process p in B 1 can be unordered, and remain unordered after composition. An usual way to extend the composition mechanism is to use an automaton labelled by basic scenarios, to produce scenario languages. These automata are called High-level Message Sequence Charts (or HMSCs for short) [START_REF] Rudolph | Tutorial On Message Sequence Charts[END_REF][START_REF] Reniers | High-level Message Sequence Charts[END_REF] when MSCs are concatenated, and a similar construct exists for compositional Message Sequence Charts [START_REF] Gunter | Compositional Message Sequence Charts[END_REF][START_REF] Genest | A Kleene Theorem and Model Checking for a Class of Communicating Automata[END_REF][START_REF] Darondeau | Products of message sequence charts[END_REF]. We can now define causal HMSCs. Recall that we have fixed a set P of process names and a family {(Σ p , I p )} p∈P of Mazurkiewicz trace alphabets.

Definition 3 A causal HMSC over (P, {(Σ p , I p )} p∈P ) is a structure H = (N, N in , B, -→, N fi )
where N is a finite nonempty set of nodes, N in ⊆ N the set of initial nodes, B a finite nonempty set of causal MSCs, -→ ⊆ N × B × N the transition relation, and N fi ⊆ N the set of final nodes.

A path in the causal HMSC H is a sequence ρ = n 0 B 1 -→ n 1 B 2 -→ • • • B ℓ -→ n ℓ . If n 0 = n ℓ , then we say ρ is a cycle. The path ρ is accepting iff n 0 ∈ N in and n ℓ ∈ N fi . The causal MSC generated by ρ, denoted ⊚(ρ), is B 1 ⊚ B 2 ⊚ • • • ⊚ B ℓ .
We let cMSC (H) denote the set of causal MSCs generated by accepting paths of H. We also set Vis(H) = {Vis(M ) | M ∈ cMSC (H)} and Lin(H) = {Lin(M ) | M ∈ cMSC (H)}. Obviously, Lin(H) is also equal to {Lin(M ) | M ∈ Vis(H)}. We shall refer to cMSC (H), Vis(H), Lin(H), respectively, as the causal language, visual language and linearization language of H.

An HMSC H = (N, N in , B, -→, N fi ) is defined in the same way as a causal HMSC except that B is a finite set of MSCs, and that the concatenation operation used to produce MSC languages is the weak sequential composition 2. One basic limitation of HMSCs is that their visual languages are finitely generated. In contrast, the visual language of a causal HMSC is not necessarily finitely generated. Consider for instance the HMSC H in Figure 1, and the independence relations given by: I p = {((p!q(Q), p?q(A)), (p?q(A), p!q(Q)))} and I q = ∅. M 1 and M 2 can be seen as causal MSCs, and H as a causal HMSC over (P = {p, q}, {(Σ p , I p )(Σ q , I q )}). Clearly, Vis(H) is not finitely generated, as it contains infinitely many MSCs similar to N of Figure 2. Throughout the paper, we will use the following standardized graphical convention to depict (causal) HMSCs: nodes are represented by circles, initial nodes are nodes connected to a downward pointing triangle, final nodes are nodes connected to an upward pointing triangle, and a transition t = (n, B, n ′ ) is represented by an arrow decorated by a rectangle containing the (causal) MSC B.

3 Regularity and Language Inclusion for causal HMSCs

Semantics for causal HMSCs

As things stand, a causal HMSC H defines three syntactically different languages, namely its linearization language Lin(H), its visual (MSC) language Vis(H) and its causal MSC language cMSC (H). The next proposition shows that they are also semantically different in general. It also identifies the restrictions under which they match semantically.

Proposition 1 Let H, H ′ be two causal HMSCs over the same family of trace alphabets {(Σ p , I p )} p∈P . Consider the following six hypotheses:

(i) cMSC (H) = cMSC (H ′ ) (i)' cMSC (H) ∩ cMSC (H ′ ) = ∅ (ii) Vis(H) = Vis(H ′ ) (ii)' Vis(H) ∩ Vis(H ′ ) = ∅ (iii) Lin(H) = Lin(H ′ ) (iii)' Lin(H) ∩ Lin(H ′ ) = ∅
Then we have: Proof :

• (i) ⇒ (ii), (i) ′ ⇒ (ii) ′ , (ii) ⇒ (iii) and (ii) ′ ⇒ (iii) ′ but
• The implications (i) =⇒ (ii) and (ii) =⇒ (iii) follow from the definitions. However, as shown in Figure 7,

Vis(G 1 ) = Vis(H 1 ) but cMSC (G 1 ) = cMSC (H 1 ). And Lin(G 2 ) = Lin(H 2 ) but Vis(G 2 ) = Vis(H 2 ).
⇔ (iii) and (ii) ′ ⇔ (iii) ′ .
For most purposes, the relevant semantics for a causal HMSC seems to be its visual language. However in the following we focus first in section 3.2 on the linearization language properties of causal HMSCs. Then, we focus in section 3.3 on the causal language properties. Using the above proposition 1, it is then straightforward to translate these properties to the visual language of causal HMSCs, when the right hypothesis apply.

Regular sets of linearizations

It is undecidable in general whether an HMSC has a regular linearization language [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF]. In the literature, a subclass of HMSCs called regular [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF] (or bounded [START_REF] Alur | Model checking of Message sequence Charts[END_REF]) HMSCs, has been identified. In this paper, to avoid overloading "regular", we shall refer to this syntactic property as "s-regular". The importance of this property lies in the fact that linearization language of every s-regular HMSC is regular. Furthermore, one can effectively decide whether an HMSC is s-regular. Our goal is to extend these results to causal HMSCs.

The key notion of characterizing s-regular HMSCs is that of the communication graph of an MSC. The communication graph captures intuitively the structure of information exchanges among processes in an MSC. Given an MSC M , its communication graph is a directed graph that has processes of M as vertices, and contains an edge from p to q if p sends a message to q somewhere in M . Given an HMSC H, we shall say that M is a cycle-MSC of H if there is a cycle in H such that M is obtained by concatenating the MSCs encountered along this cycle. H is said to be s-regular iff the communication graph of every cycle-MSC of H is strongly connected. H is said to be globallycooperative [START_REF] Morin | Recognizable sets of Message Sequence Charts[END_REF] in case the communication graph of every cycle MSC of H is connected.

We can define a similar notion for causal MSCs. As processes do not necessarily impose an ordering on events, it is natural to focus on the associated Mazurkiewicz alphabet. Thus the communication graph is defined w.r.t the dependency relations {D p } p∈P used for the concatenation while the dependencies among letters of the same process are disregarded.

Definition 4 Let B = (E, λ, {⊑ p }, ≪) be a causal MSC. The communication graph of B is denoted by CG B , and is the directed graph (Q, ), where Q = λ(E) and ⊆ Q × Q is given by: (x, y) ∈ iff

• x = p!q(m) and y = q?p(m) for some p, q ∈ P and m ∈ Msg, or • xD p y. The example of figure 8 shows the communication graph for the causal MSC B 1 ⊚ B 2 in Figure 6. For instance, there are arrows between q?p(n) and q!p(v) since q?p(n) D q q!p(v). However, there is no arrow between q?p(m) and q?p(n), even though some events of B 1 ⊚ B 2 labeled by q?p(m) and q?p(n) are dependent. Note that for a pair of causal MSCs B, B ′ , the communication graph CG B⊚B ′ = (Q, ) can be computed from the communication graphs

CG B = (Q B , B ) and CG B ′ = (Q B ′ , B ′ ) as follows: Q = Q B ∪ Q B ′ and = B ∪ B ′ ∪ Q 2 ∩ p∈P D p . Hence, for a fixed set of independence rela- tions, if a causal MSC B is obtained by sequential composition, that is B = B 1 ⊚B 2 ⊚• • •⊚B k , then the communication graph of B does not depend on the respective ordering of B 1 , • • • B k , nor on the number of occurrences of each B i .
Hence, for any permutation f on 1..k and any

B ′ = B f (1) ⊚ B f (2) ⊚ • • • ⊚ B f (k) , we have that CG B = CG B ′ .
In the sequel, we will say that the causal MSC B is tight iff its communication graph CG B is weakly connected. We say that B is rigid iff its communication graph is strongly connected. We will focus here on rigidity and study the notion of tightness in section 3.3.

Definition 5 Let H = (N, N in , B, N fi , -→) be a causal HMSC. We say that H is s-regular (resp. globally-cooperative) iff for every cycle ρ in H, the causal MSC ⊚(ρ) is rigid (resp. tight).

It is easy to see that the simple protocol modeled by the causal HMSC of Figure 9 is regular, since the only elementary cycle is labeled by two local events a, b, one message from p to q and one message from q to p. The communication graph associated to this elementary cycle is strongly connected. Note that the visual language of this causal HMSC is not finitely generated, as messages m and n can cross between two occurrences of a and b.

There can be infinitely many cycles in H, hence Definition 5 does not give automatically an algorithm to check whether a causal HMSC is s-regular or globally-cooperative. However, we can use the following equivalent definition to obtain an algorithm: H is s-regular (resp. globally-cooperative) iff for every strongly connected subgraph G of H with {B 1 , . . . , B ℓ } being the set of causal MSCs appearing in G, we have B 1 ⊚ . . . ⊚ B ℓ is rigid (resp. tight). As already discussed, the rigidity of B 1 ⊚ . . . ⊚ B ℓ does not depend on the order in which B 1 , . . . , B ℓ are listed. This leads to a co-NP-complete algorithm to test whether a causal HMSC is s-regular.

Theorem 1 Let H = (N, N in , B, -→, N fi ) be a causal HMSC. Testing whether H is s-regular (respectively globally-cooperative) can be done in time O((|N | 2 + |Σ| 2 ) • 2 |B| )
. Furthermore these problems are co-NP complete.

Proof : We use the ideas in the proofs of [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF][START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF], improving the deterministic complexity implied by the proof in [START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF], which was exponential in the number of transitions of the HMSC (there is at least one transition per label (else we can delete the useless labels)).

We first guess a subset The hardness part follows directly from the co-NP hardness result in [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF].

X = {B 1 , • • • B k } ⊆ B of
As already mentioned, any HMSC can be seen as a causal HMSC where the independence relation of each process is empty. That is, checking whether such causal HMSC are globally-cooperative or s-regular is equivalent to checking global cooperativeness or regularity of the HMSC. These problems being co-NP complete, we get the co-NP hardness.

Theorem 2 Let H = (N, N in , B, N fi , -→) be a s-regular causal HMSC. Then Lin(H) is a regular subset of Σ ⋆ , i.e. we can build an automaton A H over Σ that recognizes Lin(H). Furthermore, the number of states of

A H is at most in |N | 2 • 2 |Σ| • (Σ + 1) K•M • 2 f (K•M ) K , where K = |N | • |Σ| • 2 |B| , M = max{|B| | B ∈ B} (recall that |B| denotes the size of the causal MSC B)nd the function f is given by f (n) = 1 4 n 2 + 3 2 n + O(log 2 n).
In [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF], the regularity of linearization languages of s-regular HMSC was proved by using an encoding into connected traces and building a finite state automaton which recognizes such connected traces. In our case, finding such embedding into Mazurkiewicz traces seems impossible due to the fact that causal MSCs need not be FIFO. Instead, we shall use techniques from the proof of regularity of trace closures of loop-connected automata from [START_REF] Diekert | The Book of Traces[END_REF][START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF].

The rest of this subsection is devoted to the proof of Theorem 2. We fix a s-regular causal HMSC H as in the theorem, and show the construction of the finite state automaton A H over Σ which accepts Lin(H).

First, we establish some technical results.

Lemma 1 Let ρ = θ 1 . . . θ 2 . . . θ |Σ| be a path of H, where for each i = 1 . . . |Σ|,

the subpath θ i = n i,0 B i,1 -→ n i,1 . . . n i,ℓ i -1 B i,ℓ i -→ n i,
0 is a cycle (these cycles need not be contiguous). Suppose further that the sets B i = {B i,1 , . . . , B i,ℓ i }, i = 1, . . . , |Σ|, are equal. Let e be an event in ⊚(θ 1 ) and e ′ an event in ⊚(θ |Σ| ). Let ⊚(ρ) = (E, λ, {⊑ p }, ≪). Then we have e ≤ e ′ .

Proof :

First of all notice that when (σ, σ ′ ) is an edge of CG B , then for every causal MSC B ′ , in the causal MSC B ⊚ B ′ , every event e of B such that λ(e) = σ precedes all events e ′ of B ′ such that λ(e ′ ) = σ ′ . Indeed, if σ and σ ′ belong to the same Σ p , then (σ, σ ′ ) is an edge of CG B if and only if σD p σ ′ , and we necessarily have e ≤ e ′ in B ⊚ B ′ . Similarly, if σ and σ ′ label events located on different processes, then σ is of the form p!q(m) and σ ′ of the form q?p(m). Hence, there exists an event e ′′ of B such that e ≪ e ′′ and λ(e ′′ ) = σ ′ . As the dependence relations are reflexive, we also have e ′′ ≤ e ′ . Similarly, for two

cycles θ i ,θ i+1 of ρ, if (σ, σ ′ ) is an edge of CG B i,1 ⊚•••⊚B i,l i , then all events in ⊚(θ i ) labelled by σ precede events of ⊚(θ i+1 ) labelled by σ ′ . As H is rigid, CG B i,1 ⊚•••B i,l i is strongly connected, and contains a path (σ 1 , σ 2 ) • • • (σ k-1 , σ k ) of length at most |Σ| from σ 1 = λ(e) to σ k = λ(e ′
), and we can find one event e i , i ∈ 1..|Σ| for each cycle such that λ(e i ) = σ i and e

= e 1 ≤ e 2 ≤ • • • ≤ e |Σ| = e ′ . Let ρ = n 0 B 1 -→ • • • B ℓ -→ n ℓ be a path in H, where B i = (E i , λ i , {⊑ i p }, ≪ i ) for i = 1, . . . , ℓ. Let ⊚(ρ) = (E, λ, {⊑ p }, ≪, ≤). A configuration of ρ is a ≤-closed subset of E. Let C be a configuration of ρ. A C-subpath of ρ is a maximal subpath ̺ = n u B u+1 -→ . . . B u ′ -→ n u ′ , such that C ∩ E i = ∅ for each i = u, . . . , u ′ . For such a C-subpath ̺, we define its C-residue to be the set (E u+1 ∪ E u+2 ∪ • • • ∪ E u ′ ) -C. Figure 10 illustrates these notions for a path ρ = n 0 B 1 -→ n 1 B 2 -→ n 2 B 3 -→ n 3 B 4 -→ n 4 B 5 -→ n 5 B 6 -→ n 6 B 7 -→ n 7 .
Each causal MSC is represented by a rectangle. Events in the configuration C are indicated by small filled circles, events not in C but the C-residues are indicated by small blank circles, and events that are not in C nor in its residues are indicated by blank squares. Note that the configuration contains only events from B 1 , B 3 , B 4 and B 5 . The two C-subpaths identified on Figure 10 are the sequences of transitions

ρ 1 = n 0 B 1 -→ n 1 and ρ 2 = n 2 B 3 -→ n 3 B 4 -→ n 4 B 5
-→ n 5 that provide the events appearing in C. One can also notice from this example that C-subpaths do not depend on the length of a the considered path, and that the suffix of each path that does not contain an event in C can be ignored. Lemma 2 Let ρ be a path in H and C be a configuration of ρ. Then, (i) The number of C-subpaths of ρ is at most

K subpath = |N | • |Σ| • 2 |B| . (ii) Let ̺ be a C-subpath of ρ. Then the number of events in the C-residue of ̺ is at most K residue = |N | • |Σ| • 2 |B| • max{|B| | B ∈ B}.
Proof :

(i) Suppose the contrary. Let K = |Σ| • 2 |B| . We can find K + 1 C-subpaths whose ending nodes are equal. Let the indices of these K +1 ending nodes be i 1 < i 2 < . . . < i K+1 . For h = 1, . . . , K, let θ h be the subpath of ρ from n i h to n i h+1 ; and let B h be the set of causal MSCs appearing in θ h . Hence we can find

θ j 1 , θ j 2 , . . ., θ j |Σ| , j 1 < j 2 < . . . < j |Σ| , such that B j 1 = B j 2 = . . . = B j |Σ| .
Pick an event e from ⊚(θ j 1 ) with e / ∈ C. Such an e exists, since, for example, none of the events in the first causal MSC appearing in θ j 1 is in C. Pick an event e ′ from ⊚(θ j |Σ| ) with e ′ ∈ C. Applying Lemma 1 yields that e < e ′ . This leads to a contradiction, since We are now ready to define the finite state automaton A H = (S, S in , Σ, S fi , ⇒) which accepts Lin(H). As usual, S will be the set of states, S in ⊆ S the initial states, =⇒ ⊆ S × Σ × S the transition relation, and S fi ⊆ S the final states. Fix K subpath , K residue to be the constants defined in Lemma 2. If B = (E, λ, {⊑ p }, ≪) is a causal MSC and E ′ a subset of E, then we define the restriction of B to E ′ to be the causal MSC

C is ≤-closed. (ii) Let ̺ = n i B i+1 -→ . . . B i ′ -→ n i ′ . Let E j = E j -C for j = i + 1, . . . , i ′ .
B ′ = (E ′ , λ ′ , {⊑ ′ p }, ≪ ′ ) as follows. As expected, λ ′ is the restriction of λ to E ′ ; for each p, ⊑ ′ p is the restriction of ⊑ p to (E ′ ∩ E p ) × (E ′ ∩ E p ); and ≪ ′ is the restriction of ≪ to E ′ .
Intuitively, for a word σ in Σ ⋆ , A H guesses an accepting path ρ of H and checks whether σ is in Lin(⊚(ρ)). After reading a prefix σ ′ of σ, A H memorizes a sequence of subpaths from which σ ′ was "linearized" (i.e the C-subpath of a path ρ such that C is a configuration reached after reading σ ′ and ⊚(ρ) contains C). With Lemma 2, it will become clear later that at any time, we should remember at most K subpath such subpaths. Moreover, for each subpath, we need to know only a bounded amount of information, which will be stored in a data structure called "segment".

A causal MSC B = (E, λ, {⊑ p }, ≪) is of size lower than K if |E| ≤ K. A segment is a tuple (n, Γ, W, n ′ ), where n, n ′ ∈ N , Γ is a nonempty subset of Σ, and W is either a non-empty causal MSC of size lower than K residue , or the special symbol ⊥. The state set S of A H is the collection of finite sequences θ 1 θ 2 . . . θ ℓ , 0 ≤ ℓ ≤ K subpath , where each θ i is a segment. Intuitively, a segment (n, Γ, W, n ′ ) keeps track of a subpath ̺ of H which starts at n and ends at n ′ . Γ is the collection of letters of events in ⊚(̺) that have been "linearized". Finally, W is the restriction of ⊚(̺) to the set of events in ⊚(̺) that are not yet linearized. In case all events in ⊚(̺) have been linearized, we set W = ⊥. For convenience, we extend the operator ⊚ by: W ⊚ ⊥ = ⊥ ⊚ W = W for any causal MSC W ; and ⊥ ⊚ ⊥ = ⊥.

We define A H = (S, S in , Σ, S fi , =⇒) as follows:

• As mentioned above, S is the collection of finite sequence of at most K subpath segments. • The initial state set is S in = {ε}, where ε is the null sequence.

• A state is final iff it consists of a single segment θ = (n, Γ, ⊥, n ′ ) such that n ∈ N in and n ′ ∈ N fi (and Γ is any nonempty subset of Σ). • The transition relation =⇒ of A H is the least set satisfying the following conditions.

-Condition (i):

Suppose n B -→ n ′ where B = (E, λ, {⊑ p }, ≪, ≤). Let e be a minimal event in B (with respect to ≤) and let a = λ(e). Let θ = (n, Γ, W, n ′ ) where

Γ = {a}. Let R = E -{e}. If R is nonempty, then W is the restriction of B to R; otherwise we set W = ⊥. Suppose s = θ 1 . . . θ k θ k+1 . . . θ ℓ is a state in S where θ i = (n i , Γ i , W i , n ′ i ) for each i. Suppose further that, e is a minimal event in W 1 ⊚ W 2 ⊚ . . . ⊚ W k ⊚ W . • ("create a new segment") Let ŝ = θ 1 . . . θ k θθ k+1 . . . θ ℓ . If ŝ is in S, then s a =⇒ ŝ.
In particular, for the initial state ε, we have ε a =⇒ θ. • ("add to the beginning of a segment") Suppose

n ′ = n k+1 . Let θ = (n, Γ ∪ Γ k+1 , W , n ′ k+1 ), where W = W ⊚ W k+1 . Let ŝ = θ 1 . . . θ k θθ k+2 . . . θ ℓ . If ŝ is in S, then s a =⇒ ŝ. • ("append to the end of a segment") Suppose n = n ′ k . Let θ = (n k , Γ k ∪ Γ, W , n ′ ), where W = W k ⊚ W . Let ŝ = θ 1 . . . θ k-1 θθ k+1 . . . θ ℓ . If ŝ is in S, then s a =⇒ ŝ. • ("glue two segments") Suppose n = n ′ k and n ′ = n k+1 . Let θ = (n k , Γ k ∪Γ∪ Γ k+1 , W , n ′ k+1 ), where W = W k ⊚W ⊚W k+1 . Let ŝ be θ 1 . . . θ k-1 θθ k+2 . . . θ ℓ . If ŝ is in S, then s a =⇒ ŝ. -Condition (ii): Suppose s = θ 1 . . . θ k θ k+1 . . . θ ℓ is a state in S where θ i = (n i , Γ i , W i , n ′ i ) for i = 1, 2, . . . , ℓ. Suppose W k = ⊥. Let W k = (R k , η k , {⊑ k p }, ≪ k , ≤ k
) and e a minimal event in W k . Suppose further that e is a minimal event in

W 1 ⊚ W 2 ⊚ . . . ⊚ W k . Let θ = (n k , Γ k ∪ {a}, W , n ′ k )
, where W is defined as follows. Let R = R k -{e}. If R is nonempty, then W is the restriction of W to R; otherwise, set W = ⊥. Let ŝ = θ 1 . . . θ k-1 θθ k+1 . . . θ ℓ . Then we have s a =⇒ ŝ, where a = η k (e). (Note that ŝ is guaranteed to be in S.)

We have now completed the construction of A H . It remains to show that A H recognizes Lin(H).

Lemma 3 Let σ ∈ Σ ⋆ . Then σ is accepted by A H iff σ is in Lin(H). Proof : Let σ = a 1 a 2 . . . a k . Suppose σ is in Lin(H). Let ρ = n 0 B 1 -→ . . . B ℓ
-→ n ℓ be an accepting path in H such that σ is a linearization of ⊚(ρ). Hence we may suppose that ⊚(ρ) = (E, λ, {⊑ p }, ≪, ≤) where E = {e 1 , e 2 , . . . , e k } and λ(e i ) = a i for i = 1, . . . , k. And e i ≤ e j implies i ≤ j for any i, j in {1, . . . , k}. Consider the configurations C i = {e 1 , e 2 , . . . , e i } for i = 1, . . . , k. For each C i , we can associate a state s i in A H as follows. Consider a fixed C i . Let ρ = . . . ̺ 1 . . . ̺ 2 . . . ̺ h . . . where ̺ 1 , ̺ 2 , . . ., ̺ h are the C i -subpaths of ρ. Then we set s i = θ 1 . . . θ h where θ j = (n j , Γ j , W j , n ′ j ) with n j being the starting node of ̺ j , and Γ j the collection of all λ(e) for all events e that are in both ⊚(̺ j ) and C i . Let R j be the C i -residue of ̺ j . If R j is nonempty, W j is the causal MSC (R j , η j , {⊑ j p }, ≪ j , ≤ j ) where η j is the restriction of λ to R j ; ⊑ j p is the restriction of ⊑ p to those events in R j that belong to process p, for each p; and ≪ j the restriction of ≪ to R j . If R j is empty, then set W j = ⊥. Finally, n ′ j is the ending node of ̺ j . Now it is routine (though tedious) to verify that ε

a 1 =⇒ s 1 . . . s k-1 a k
=⇒ s k is an accepting run of A H . Conversely, given an accepting run of A H over σ, it is straightforward to build a corresponding accepting path of H.

With Lemma 3, we establish Theorem 2. As for complexity, the number of states in A H is at most (N seg ) K subpath , where N seg is the maximal number of segments. Now,

N seg is |N | 2 • 2 |Σ| • N res ,
where N res is the possible number of residues. Recall that a residue is of size at most K residue . According to Kleitman & Rotschild [START_REF] Kleitman | Asymptotic enumeration of partial orders on a finite set[END_REF], the number of partial orders of size k is in 2

f (k) where f (k) = 1 4 k 2 + 3 2 k + O(log 2 (k)). It follows that the number of |Σ|-labeled posets of size k is in 2 f (k) • |Σ| k .
All residues of size up to k can be encoded as a labeled poset of size k with useless events, labelled by a specific label ♯. Hence the number of residues N res is lower than 2 f (K residue ) • (|Σ| + 1) K residue . Combining the above calculations then establishes the bound in theorem 2 on the number of states of A H .

Inclusion and Intersection of causal HMSC Languages

It is known that problems of inclusion, equality and non-emptiness of the intersection of the MSC languages associated with HMSCs are all undecidable [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF]. Clearly, these undecidability results also apply to the causal languages of causal HMSCs. As in the case of HMSCs, theses problems are decidable for s-regular causal HMSCs since their linearization languages are regular.

It is natural to ask whether we can still obtain positive results for these problems beyond the subclass of s-regular causal HMSCs. In the setting of HMSCs, one can show that for all K ≥ 0, the set of K-bounded linearizations of any globally-cooperative HMSC is regular. Moreover, for a suitable choice of K, the set of K-bounded linearizations is sufficient for effective verification [START_REF] Genest | A Kleene Theorem and Model Checking for a Class of Communicating Automata[END_REF]. Unfortunately, this result uses Kuske's encoding [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF] into traces that is based on the existence of an (existential) bound on communication channels. Consequently, this technique does not apply to globally-cooperative causal HMSCs, as the visual language of a causal HMSC needs not be existentially bounded. For instance, consider the causal HMSC H of Figure 11. It is globallycooperative and its visual language contains MSCs shown in the right part of Figure 11: in order to receive the first message from p to r, the message from p to q and the message from q to r have to be sent and received. Hence every message from p to r has to be sent before receiving the first message from p to r, which means that H is not existentially bounded.

Fig. 11. A globally-cooperative causal HMSC that is not existentially bounded

We shall instead adapt the notion of atoms [START_REF] Ahuja | A Basic Unit of Computation in Distributed Sytems[END_REF][START_REF] Hélouët | Decomposition of Message Sequence Charts[END_REF] and the techniques from [START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF].

Definition 6 A causal MSC B is a basic part (w.r.t. the trace alphabets {(Σ p , I p )} p∈P ) if there do not exist causal MSCs B 1 , B 2 such that B = B 1 ⊚B 2 .
Note that we require that the set of events of a causal MSC is not empty. Now for a causal MSC B, we define a decomposition of B to be a sequence For the converse, let us suppose that there exists a decomposition

B 1 • • • B ℓ of basic parts such that B = B 1 ⊚ • • • ⊚ B ℓ .
B = W 1 ⊚ W 2 ⊚ • • • ⊚ W q such that W 1 . . . W q / ∈ [B 1 . . . B k ].
It means that there exists a permutation φ and an index i with

W j = B φ(j) for all j < i, B φ(1) • • • B φ(k) ∈ [B 1 . . . B k ], and W ′ = W i ∩ B φ(i) = ∅ and W ′′ = W i \ B φ(i) = ∅.
It suffices now to prove that W ′ and W ′′ are causal MSCs and that W i = W ′ ⊚ W ′′ to get a contradiction with the fact that W i is a basic part. By definition, the restriction of ≪ W i to W ′ is still a bijection (a send in W ′ matches a receive in W ′ ). It implies that the restriction of ≪ W i to W ′′ is a bijection too. Both W ′ and W ′′ are thus causal MSCs. The fact that W i = W ′ ⊚ W ′′ comes from the definition of ⊚ and from the fact that W ′ ⊆ B φ(i) and

W ′′ ⊆ B φ(i+1) • • • B φ(k) .
It is thus easy to compute the (finite) set of basic parts of a causal MSC B, denoted Basic(B), since it suffices to find one of its decomposition. Proof : Let B = (E, λ, {⊑ p }, ≪). We describe the decomposition of B, which is analogous to the technique in [START_REF] Hélouët | Decomposition of Message Sequence Charts[END_REF]. We consider the directed graph (E, ≤ ∪R), where R is the symmetric closure of ≪ ∪ p∈P R ′ p ∪ R ′′ p , with Intuitively, R ′ p denote pairs of events that are ordered in B, but which labels are independent in I p . As this ordering can not be obtained via composition, this ordering should appear in the decomposition of B, that is e and e ′ should belong to the same basic part. Similarly, relation R ′′ p contains pairs of events that are unordered in B, but which labels are dependent.

R ′ p = {(e, e ′ ) ∈ E p × E p | e ⊑ p
For each strongly connected component E ′ of (E, ≤ ∪R), we associate a structure C = (E ′ , λ ′ , {⊑ ′ p }, ≪ ′ ), where λ ′ is the restriction of λ to E ′ , ⊑ ′ p is the restriction of ⊑ ′ p to E ′ , and ≪ ′ is the restriction of ≪ to E ′ . It is easy to see that C is a causal MSC, since each receive needs to be in the same strongly connected component than its associated send (since the relation includes the symmetric closure of ≪). We first prove that C is a basic part. By contradiction, otherwise, we would have C = B 1 ⊚ B 2 , which by definition of ⊚ means that no edge of ≤ ∪R can go from one event of B 2 to one event of B 1 , which contradicts the fact that E ′ is strongly connected.

Let E 1 , . . . , E n be the set of basic parts obtained. We order them such that there is no edge of ≤ ∪R from any event of E j to some event of E i with i < j (it is always possible, else E i , E j would be in the same strongly connected component). It is now clear that B = E 1 ⊚ • • • ⊚ E n , since no event of E j can be before an event of E i , i < j (else there would be an edge of ≤ from E j to E i ). Notice that the decomposition in strongly connected components with Tarjan's Algorithm is in linear time in the number of edges, that is linear in

|B| + p∈P | ⊑ p | ≤ |B| + |B| 2 ,
where |B| is the number of events of B. For comparison, recall that the complexity of decomposing an MSC B in atoms [START_REF] Hélouët | Decomposition of Message Sequence Charts[END_REF] is in O(2|B|) (the immediate successor relation in MSCs is the union of the message pairing relation and the total ordering on instances, that is there are at most 2 immediate successors for a given event).

In view of Proposition 3, we assume through the rest of this section that every transition of a causal HMSC H is labelled by a basic part. This obviously incurs no loss of generality, since we can simply decompose each causal MSC in H into basic parts and decompose any transition of H into a sequence of transitions labeled by these basic parts. Given a causal HMSC H, we let Basic(H) be the set of basic parts labelling transitions of H. Trivially, a causal MSC is uniquely defined by its basic part decomposition. Then instead of the visual language we can use the basic part language of H, denoted by

BP (H) = {B 1 . . . B ℓ ∈ Basic(H) ⋆ | B 1 ⊚ . . . ⊚ B ℓ ∈ cMSC (H)}.
Notice that BP (H) = [BP (H)] by Proposition 2, that is, BP (H) is closed by commutation. We can also view H as a finite state automaton over the alphabet Basic(H), and denote by

L Basic (H) = {B 1 • • • B ℓ ∈ Basic(H) ⋆ | n 0 B 1 -→ n 1 • • • B ℓ
-→ n ℓ is an accepting path of H} its associated (regular) language. We now relate BP (H) and L Basic (H).

Proposition 4 Let H be a causal HMSC. Then BP (H) = [L Basic (H)]. Proof : First, let us take a word w in [L Basic (H)]. Thus w = B 1 . . . B k ∼ B i 1 . . . B i k such that B i 1 . . . B i k ∈ L Basic (H). As L Basic (H) ⊆ BP (H) and B 1 ⊚ . . . ⊚ B k = B i 1 ⊚ . . . ⊚ B i k we conclude that [L Basic (H)] ⊆ BP (H).
Second, let us take a word w in BP (H). Let us note ⊚(w) its corresponding causal MSC, i.e. for w = Assuming we know how to compute the trace closure of the regular language L Basic (H), we can obtain BP (H) with the help of Proposition 4. In general, we cannot effectively compute this language. However if H is globally-cooperative, then [L Basic (H)] is regular and a finite state automaton recognizing [L Basic (H)] can be effectively constructed [START_REF] Diekert | The Book of Traces[END_REF][START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF]. Considering globally-cooperative causal HMSCs as finite state automata over basic parts, we can apply [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF] to obtain the following decidability and complexity results: Theorem 3 Let H, H ′ be causal HMSCs over the same family of trace alphabets {(Σ p , I p )} p∈P . Suppose H ′ is globally-cooperative. Then we can build a finite state automaton

B 1 . . . B k , ⊚(w) = B 1 ⊚ . . . ⊚ B k . Then
A ′ over Basic(H ′ ) such that L Basic (A ′ ) = [L Basic (H ′ )]. Moreover, A ′ has at most 2 O(n•b)
states, where n is the number of nodes in H and b is the number of basic parts in Basic(H). Consequently, the following problems are decidable:

(i) Is cMSC (H) ⊆ cMSC (H ′ )? (ii) Is cMSC (H) ∩ cMSC (H ′ ) = ∅?
Furthermore, the complexity of (i) is PSPACE-complete and that of (ii) is EXPSPACE-complete.

The above theorem shows that we can model-check a causal HMSC against a globally-cooperative causal HMSC specification. Note that we can only apply Theorem 3 to two causal HMSCs over the same family of trace alphabets. If the causal HMSCs H, H ′ in theorem 3 satisfy the additional condition that every causal MSC labeling the transitions of H and H ′ respects {(Σ p , I p )} p∈P , then we can compare the visual languages Vis(H) and Vis(H ′ ), thanks to Proposition 1.

On the other hand, if the independence relations are different, the atoms of H and H ′ are unrelated. Theorem 4 proves that comparing the MSC languages of two globally-cooperative causal HMSCs H, H ′ using different independence relations is actually undecidable. The only way to compare them is then to compare their linearization languages. Consequently, we would need to work with s-regular causal HMSCs.

Theorem 4 Let G, H be globally-cooperative causal HMSCs with respectively families of trace alphabets {(Σ p , I p )} p∈P and {(Σ p , J p )} p∈P , where for each p, I p and J p are allowed to differ. Then it is undecidable to determine whether Vis(G) ∩ Vis(H) = ∅.

Proof : We reduce the PCP problem, which is well known to be undecidable, to the emptiness of the intersection of the visual languages of two (globallycooperative) causal HMSCs, if we do not assume that both causal HMSCs use the same independence relation.

Let J be a finite set and (v i , w i ) i∈J be an instance of PCP, with v i , w i ∈ {a, b} * \ ǫ for all i ∈ J. We will use two causal HMSCs H 1 and H 2 to encode the PCP. The intuition for the reduction is that the causal HMSC H 1 generates sequences of CaMSCs of the form (V i W i ) * , where CaMSCs V i and W i represent respectively the words v i and w i . The causal HMSC H 2 generates sequences of the form (A Ā ∨ B B) * , where the causal MSCs X and X represent an x letter in v and w respectively, with x ∈ {a, b}.

We have three process, P 1 , P 2 and P 3 . The causal MSCs A, B are made of a single message from process P 1 to process P 3 , respectively labeled by a and b. The causal MSCs Ā, B are made of two messages both labeled by the same letter (respectively ā and b). The first message is from process P 1 to P 2 , and the second message is sent after the reception of the first message, from process P 2 to process P 3 . For each pair (v i , w i ) in the PCP instance, we build two causal MSCs V i and W i . If v i is of the form v i = xyz, the causal MSC V i is made of the concatenation of X, Y, Z. Similarly, W i is made of the concatenation X, Ȳ , Z, when w i = xyz. These causal MSCs are depicted in Figure 12. Let us denote by V the labels appearing in V i 's and by W the labels appearing in W i 's. The independence relation I 1 for H 1 states that all events on process P 2 and P 3 commute. On process P 1 , events labeled by a letter of V (namely P 1 !P 3 (a) and P 1 !P 3 (b) commute with events labeled by a letter of W (namely P 1 !P 2 (ā) and P 1 !P 2 ( b). There is no commutation among events labeled by a letter of V , and no commutations among events labeled by a letter of W . In the same way, the independence relation I 2 for H 2 states that no events on process 1 and 2 commute. On process 3, events from v (namely 3?1(a) and 3?1(b) commute with events from w (namely 3?2(ā) and 3?2( b). There is no commutations among events from v, and no commutations among events from w.

It is easy to check that both H 1 and H 2 are globally-cooperative. Indeed, notice first that the letters a and b behave exactly the same. We can then forget about them for global cooperativeness, and draw the communication graph considering only 6 letters P 1 !P 2 , P 2 ?P 1 , P 2 !P 3 , P 3 ?P 1 , P 1 !P 3 , P 3 ?P 1 . Every elementary cycle of H 1 contains a V i and a W i . Since v i , w i are non empty words, every of these 6 letters appear in every loop of H 1 . In particular, we have the undirected relation P 1 !P 2 -P 2 ?P 1 -P 2 !P 3 -P 3 ?P 2 -P 3 ?P 1 -P 1 !P 3 , which proves that the graph is connected. In the same way, every loop of H 2 contains a X X, hence every of the 6 letters appear in every elementary cycle (and loop) of H 2 . This time, the graph is connected, but through another undirected path: P 3 ?P 1 -P 1 !P 3 -P 1 !P 2 -P 2 ?P 1 -P 2 !P 3 -P 3 ?P 2 . Hence, both H 1 and H 2 are globally-cooperative.

Assume that Vis(H 1 ) ∩ Vis(H 2 ) = ∅. Let M ∈ Vis(H 1 ) ∩ Vis(H 2 ). Let v be the projection of M on alphabet P 1 !P 3 (a), P 1 !P 3 (b), and w the projection of M on alphabet P 1 !P 2 (ā), P 1 !P 2 ( b). Now, because M ∈ Vis(H 2 ) and since there is no commutation on process P 1 allowed by I 2 , we get that v = w, confusing P 1 !P 2 (ā) with P 1 !P 3 (a) and P 1 !P 2 ( b) with P 1 !P 3 (b).

Second, because M ∈ Vis(H 1 ), there exists a sequence

i 1 • • • i n ∈ J * with M ∈ V is(V i 1 ⊚ W i 1 ⊚ • • • V in ⊚ W in ).
Since by I 1 , there is no commutation among letters of v, the projection v of M on alphabet P 1 !P 3 (a), P 1 !P 3 (b) is the same as the projection of

V i 1 ⊚ W i 1 ⊚ • • • V in ⊚ W in . That is, v = v i 1 • • • v in (confusing
letter a with P 1 !P 3 (a) and letter b with P 1 !P 3 (b)). In the same way, w = w i 1 • • • w in (confusing letter a with P 1 !P 2 (ā) and letter b with

P 1 !P 2 ( b)). That is v i 1 • • • v in = v = w = w i 1 • • • w in , which proves that it is a solution for the PCP problem. Now, assume that the instance (v i , w i ) i∈I of PCP has a solution v i 1 • • • v in = w i 1 • • • w in = x 1 • • • x m .
Consider the following MSC M . We describe M process by process (which is enough to uniquely define M since all MSCs in V is(H 1 ) and V is(H 2 ) are weak FIFO). On process P 1 , M is of the form P 1 !P 3 (x 1 )P 1 !P 2 ( x1 ) • • • P 1 !P 3 (x m )P 1 !P 2 ( xm ). On process P 2 , M is of the form P 2 ?P 1 ( x1 )P 2 !P 3 ( x1 ) • • • P 2 ?P 1 ( xm )P 2 !P 3 ( xm ). On process 3, M is of the form P 3 ?P 1 (a 1 )P 3 ?P 1 (b 1 )P 3 ?P 1 (c 1 )P 3 ?P 2 ( d1 )P 3 ?P 2 ( ē1 )P 3 ?P 1 ( f1 ) • • • P 3 ?P 1 (a n ) P 3 ?P 1 (b n )P 3 ?P 1 (c n )P 3 ?P 2 ( dn )P 3 ?P 2 ( ēn )P 3 ?P 1 ( fn ), where for all j, v i j = a j b j c j and w i j = d j e j f j . It is easy to see that M ∈ Vis(H 1 ) ∩ Vis(H 2 ), which ends the proof.

Window-bounded causal HMSCs

One of the chief attractions of causal MSCs is that they enable the specification of behaviors containing braids of arbitrary size such as those generated by sliding windows protocols. Very often, sliding windows protocols appear in a situation where two processes p and q exchange bidirectional data. Messages from p to q are of course used to transfer information, but also to acknowledge messages from q to p. If we abstract the type of messages exchanged, these protocols can be seen as a series of query messages from p to q and answer messages from q to p. Implementing a sliding window means that a process may send several queries in advance without needing to wait for an answer to each query before sending the next query. Very often, these mechanisms tolerate losses, i.e. the information sent is stored locally, and can be retransmitted if needed (as in the alternating bit protocol). To avoid memory leaks, the number of messages that can be sent in advance is often bounded by some integer k, that is called the size of the sliding window. Note however that for scenario languages defined using causal HMSCs, such window sizes do not always exist. This is the case for example for the causal HMSC depicted in Figure 1 with independence relations I p = {((p!q(Q), p?q(A)), (p?q(A), p!q(Q)))} and I q = {((q?p(Q), q!p(A)), (q!p(A), q?p(Q))}. The language generated by this causal HMSC contains scenarios where an arbitrary number of messages from p to q can cross an arbitrary number of messages from q to p. A question that naturally arises is to know if the number of messages crossings is bounded by some constant in all the executions of a protocol specified by a causal HMSC. In what follows, we define these crossings, and show that their boundedness is a decidable problem. Definition 7 Let M = (E, λ, {⊑ p }, ≪) be an MSC For a message (e, f ) in M , that is, (e, f ) ∈ ≪, we define the window of (e, f ), denoted W M (e, f ), as the set of messages {e ′ ≪ f ′ | loc(λ(e ′ )) = loc(λ(f )) and loc(λ(f ′ )) = loc(λ(e)) and e ≤ f ′ and e ′ ≤ f }.

We say that a causal HMSC H is K-window-bounded iff for every M ∈ Vis(H) and for every message (e, f ) of M , it is the case that |W M (e, f )| ≤ K. H is said to be window-bounded iff H is K-window-bounded for some K. (the first answer from q to p) is symbolized by the area delimited by dotted lines. It consists of all but the first message Q from p to q. Clearly, the causal HMSC H of Figure 1 is not window-bounded. We now describe an algorithm to effectively check whether a causal HMSC is window bounded. It builds a finite state automaton whose states remember the labels of events that must appear in the future of messages (respectively in the past) in any MSC of Vis(H).

Formally, for a causal MSC B = (E, λ, {⊑ p }, ≪) and (e, f ) ∈≪ a message of B, we define the future and past of (e, f ) in B as follows:

Future B (e, f ) = {a ∈ Σ | ∃x ∈ E, f ≤ x ∧ λ(x) = a} Past B (e, f ) = {a ∈ Σ | ∃x ∈ E, x ≤ e ∧ λ(x) = a}
Notice that for a message m = (e, f ), we always have λ(e) ∈ Past B (m) and λ(f ) ∈ Future B (m). For instance, in Figure 13, Past B (m 1 ) = {p!q(Q), q?p(Q), q!p(A)}.

Intuitively, if a letter of the form p!q(m) is in the future of a message (e, f ) in a causal MSC B, then any occurrence of message m that is appended to B is in the future of (e, f ). Hence, this message can not appear in the window of (e, f ). Note that a symmetric property holds for the past of (e, f ).

Proposition 5 Let B = (E, λ, {⊑ p }, ≪) and B ′ = (E ′ , λ ′ , {⊑ ′ p }, ≪ ′ ) be two causal MSCs, and let m ∈≪ be a message of B. Then we have:

Future B⊚B ′ (m) = Future B (m) ∪ {a ′ ∈ Σ | ∃x, y ∈ E ′ ∃a ∈ Future B (m) s.t. λ(y) = a ′ ∧ x ≤ ′ y ∧ a D loc(a) λ(x)} Past B ′ ⊚B (m) = Past B (m) ∪ {a ′ ∈ Σ | ∃x, y ∈ E ′ ∃a ∈ Future B (m) s.t. λ(y) = a ′ ∧ y ≤ ′ x ∧ a D loc(a) λ(x)} Proof : Follows from definition. Let H = (N, N in , B, -→, N fi ) be a causal HMSC. Consider a path ρ of H with ⊚(ρ) = B 1 ⊚ • • • ⊚ B ℓ and a message m in B 1 . First, the sequence of sets Future B 1 (m), Future B 1 ⊚B 2 (m), . . ., Future B 1 ⊚•••⊚B ℓ (m) is non-decreasing.
Using proposition 5, these sets can be computed on the fly and with a finite number of states. Similar arguments hold for the past sets. Now consider a message (e, f ) in a causal MSC B labelling some transition t of H. With the above observation on Future and Past, we can show that, if there is a bound K (e,f ) such that the window of a message (e, f ) in the causal MSC generated by any path containing t is bounded by K (e,f ) , then K (e,f ) is at most b|N ||Σ| where b = max{|B| | B ∈ B}. Further, we can effectively determine whether such a bound K (e,f ) exists by constructing a finite state transition system whose states memorize the future and past of (e, f ). Thus we have the following: The rest of this subsection is devoted to the proof of Theorem 5. We fix H as in Theorem 5.

Proof : [of Theorem

• • • n 0 → • • • n 1 → • • • n 2 → • • • n |Σ| → • • • , where n 1 = • • • = n |Σ| = n ′ .
Let us denote by E i the label of the prefix

• • • n 0 → • • • n 1 → • • • n 2 → • • • n i of ρ, for i = 0, 1, 2, . . . , |Σ|.
Consider the sequence of sets F i = Future E i (e, f ), i = 0, 1, . . . , |Σ|. Each F i is a subset of Σ and the sequence F 0 , F 1 , . . . , F |Σ| is non-decreasing. Hence, we can find ℓ ≤ |Σ| such that F ℓ = F ℓ+1 . This means that the path ρ ′ , which is computed from path ρ by repeating twice the cycle between n ℓ and n ℓ+1 (n ℓ excluded but n ℓ+1 included), have at least one more message m ′ which crosses m. Thus, we can exhibit a new execution V ′ ∈ Vis(⊚(ρ ′ )) such that (e, f ) is crossed by at least k + 2 messages. As we can iterate this construction, it means that H is not window-bounded.

We next establish Theorem 5(ii). We shall show that for a given message m, one can decide in an efficient way whether there is a window bound, by constructing a finite state transition system that memorizes Future(m) and Past(m).

For a given causal HMSC H = (N, N in , B, N fi , -→) and a message (e, f ) of some causal MSC B ∈ B, we build the following transition system A (e,f ) = (Q, Q in , B, Q fi , δ) that computes the possible futures of (e, f ), where:

• Q = N × 2 Σ
is a set of states, recalling a node in H and a future,

• Q in = {(n, ∅) | n ∈ N in } is the set of initial states, • (n, X) ∈ Q fi if and only if n ∈ N fi . • δ ⊆ Q × B × Q is the least transition relation such that: • (n, ∅), B, (n ′ , ∅) ∈ δ if n B -→ n ′
Thus Theorem 5(ii) follows from Lemma 4. It remains to establish the complexity claim in Theorem 5(ii). The transition system A (e,f ) has at most |N | × 2 |Σ| states, and we have to analyze strongly connected components of A (e,f ) . However, as noticed before, every strongly connected component of A (e,f ) enjoys the property to have a second component which is constant. Hence we need to test the property only for maximal strongly connected components. Indeed, if C is a strongly connected component of A (e,f ) such that q!p(m ′ ) is the label of an event in a causal MSC labeling a transition of C but that is not in Future(C), then we can consider the maximal strongly connected component D of A (e,f ) containing C (it exists since the union of two non disjoint strongly connected components is again a strongly connected component). Since D is a strongly connected component, its second component Future(D) is constant, hence Future(D) = Future(C). Since C ⊆ D, we have that q!p(m ′ ) is a label of an event of D and is not in Future(C) = Future(D).

Using Tarjan's algorithm [START_REF] Tarjan | Depth-first search and linear graph algorithms[END_REF], we can compute in quadratic time the partition of A (e,f ) into maximal strongly connected components (for each set X ⊆ 2 Σ , we partition the subpart of A (e,f ) with a constant second component being X).

Then for each maximal strongly connected component (C, X), it suffices to compute λ(C) and to compare it with X, which is linear in n.

Relationship with Other Scenario Models

We compare here the expressive power of other HMSC-based scenario languages with causal HMSCs. For comparison, we will only consider weak-FIFO scenario languages, that is HMSCs that are labelled by weak FIFO MSCs and causal HMSCs that are labelled by causal MSCs which visual extensions are weak FIFO. Indeed, non weak-FIFO scenarios can be seen as a little degenerate descriptions, as they can be differentiated by their visual languages, but not by their linearization languages. Hence, within this weak-FIFO setting, the comparisons established in this section holds both for visual languages and linearization languages.

The first topic of comparison is causal HMSCs themselves. Indeed, a previous definition [START_REF] Gazagnaire | Causal Message Sequence Charts[END_REF] of s-regular and globally-cooperative causal HMSCs required that for every p ∈ P, and for every B labeling a cycle of a causal HMSC, Alph p (B) was D p -connected. It is not necessary in the definition of this paper: two letters from the same process can be connected through communication via another process, and not directly on the same process. It is important in the following setting.

An important question is the class of Communicating Finite State Machine (CFM for short) corresponding to HMSC languages. It has been shown in [START_REF] Henriksen | A Theory of Regular MSC Languages[END_REF] that s-regular (compositional) HMSCs corresponds to universally bounded CFMs. The natural model to compare causal HMSCs and CFMs could be asynchronous cellular automata with type [START_REF] Bollig | On the Expressiveness of Asynchronous Cellular Automata[END_REF], also called mixed machine in [START_REF] Gazagnaire | Scenario Languages: Using Partial Orders to Model, Verify and Supervize Distributed and Concurrent Systems[END_REF], which allows communication both through Mazurkiewicz traces and messages.

It has been shown in [START_REF] Gazagnaire | Scenario Languages: Using Partial Orders to Model, Verify and Supervize Distributed and Concurrent Systems[END_REF] that using the same s-regular definition as in this paper, universally bounded mixed model and s-regular causal (compositional) HMSCs coincide. It is easy to see that this is not the case with the old definition of [START_REF] Gazagnaire | Causal Message Sequence Charts[END_REF]. Consider the following example: a causal HMSC composed of a single loop labelled by a causal MSC M that contains four unordered messages:m, o from process p to process q, and n, g from process q to process p. The dependence relation D p is defined as the reflexive and symmetric closure of {(p!q(m), p?q(g)); (p?q(n), p!q(o))} and D q = Σ q ×Σ q This example and the communication graph associated to its single loop are represented in Figure 14.

Clearly, this causal HMSC is not s-regular nor even globally-cooperative with the definition of [START_REF] Gazagnaire | Causal Message Sequence Charts[END_REF] (Σ p is not D p -connected), but it is s-regular with the definition of this paper. Also, there is no globally-cooperative causal HMSC in the terms of [START_REF] Gazagnaire | Causal Message Sequence Charts[END_REF] recognizing the same language. Then, we consider HMSCs. Two important strict HMSC subclasses are (i) s-regular (also called regular in [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF] and bounded in [START_REF] Alur | Model checking of Message sequence Charts[END_REF]) HMSCs which ensure that the linearizations form a regular set and (ii) globally-cooperative HMSCs [START_REF] Genest | Infinite-state High-level MSCs: Model-checking and Realizability[END_REF], which ensure that for a suitable choice of K, the set of Kbounded linearizations form a regular representative set. By definition, causal HMSCs, s-regular causal HMSCs and globally-cooperative causal HMSCs extend respectively HMSCs, s-regular HMSCs and globally-cooperative HMSCs.

Figure 11 shows a globally-cooperative causal HMSC which is not in the subclass of s-regular causal HMSCs. Thus, s-regular causal HMSCs form a strict subclass of globally-cooperative causal HMSCs. ) extending ≪ ∪ ≪ ′ , and preserving the FIFO ordering of messages with similar content (actually, in the definition of [START_REF] Gunter | Compositional Message Sequence Charts[END_REF], there is no channel content). We refer here to the definition of [START_REF] Darondeau | Products of message sequence charts[END_REF], where compositional HMSCs generate weak-FIFO MSCs. Note that so far, compositional HMSCs do not allow for non-weak FIFO description, but that a small variant of the language could easily be defined to allow this kind of description (as long as non FIFOness remains inside a node of the CHMSC).

A CHMSC H generates a set of MSCs, denoted Vis(H) by abuse of notation, obtained by concatenation of compositional MSCs along a path of the graph. With this definition, some path of a CHMSC may not generate any correct MSC. Moreover, a path of a CHMSC generates at most one MSC. The class of CHMSC for which each path generates exactly one MSC is called safe CHMSC, still a strict extension over HMSCs. S-regular and globally-cooperative HMSCs have also their strict extensions in terms of safe CHMSCs, namely as s-regular CHMSC and globally-cooperative CHMSCs. Let us now compare causal HMSCs and CHMSCs. It is not hard to build a regular compositional HMSC which MSC language can not be defined with a causal HMSC. An example is a CHMSC H that generates the visual language Vis(H) = {M i | i = 0, 1, . . .}, where each M i consists of an emission of a message m from p to r, then a sequence of i blocks of three messages: a message n from p to q followed by a message o from q to r then a message s from r to p. And at last the reception of message m on r. This MSC language is represented in Figure 15. This visual language can be easily defined with a CHMSC, by separating emission and reception of m and iterating a MSC containing messages n, o, s an arbitrary number of times. Clearly, this Vis(H) is not finitely generated, and it is not either the visual language of a causal HMSC. Assume for contradiction, that there exists a causal HMSC G with Vis(G) = Vis(H). Let k be the number of messages of the biggest causal MSC which labels a transition of G. We know that M k+1 is in Vis(G), hence M k+1 ∈ Vis(⊚(ρ)) for some accepting path ρ of G. Let N 1 , . . . , N ℓ be causal MSCs along ρ, where ℓ ≥ 2 because of the size k. It also means that there exist

N ′ 1 ∈ Vis(N 1 ), . . ., N ′ ℓ ∈ Vis(N ℓ ) such that N ′ 1 • • • • • N ′ m ∈ Vis(G). Thus, N 1 • • • • • N ℓ = M j
for some j, a contradiction since M j is a basic part (i.e. cannot be the concatenation of two MSCs). That is (regular) compositional HMSCs are not included into causal HMSCs. On the other hand, regular causal HMSCs have a regular set of linearizations (Theorem 2). Also by the results in [START_REF] Henriksen | A Theory of Regular MSC Languages[END_REF], it is immediate that the class of visual languages of regular compositional HMSCs captures all the MSC languages that have a regular set of linearizations. Hence the class of regular causal HMSCs is included into the class of regular compositional HMSCs. Last, we already know with Figure 11 that globally-cooperative causal HMSCs are not necessarily existentially bounded, hence they are not included into safe compositional HMSC. The relationships among these scenario models are summarized by Figure 16, where arrows denote strict inclusion of visual languages. Two classes are incomparable if they are not connected by a transitive sequence of arrows. We use the abbreviation sr for s-regular, gc for globally-cooperative, s for safe, damaged, lost, duplicated, or delivered out of order by the Internet communication system. This is achieved by assigning a sequence number to each segment transmitted, and requiring a positive acknowledgment (ack) from the receiving tcp. Actually, the sequence number of ack sent by process p is the sequence number of the next tcp packet that p expects. Figure 18 shows a causal HMSC modeling a bi-directional data transfer, where sequence numbers are abstracted. The last phase of the TCP protocol is connection termination. The connection termination phase uses a four-way handshake. Each side of the connection terminates the session independently. When an endpoint wishes to stop its half of the connection, it transmits a f in packet, which the other end acknowledges with an ack. Therefore, a typical tear-down requires a pair of f in and ack segments from each tcp endpoint. The four-way handshake is modeled on figure 19: an end event is seen on process p when no more tcp packet are sent from p. In MSC f in1, process 1 stops first, and process 2 can continue to send tcp packets, then process 2 stops. In MSC f in12, process 1 and process 2 stops at the same time. In MSC f in2 process 2 initiates the termination of the communication, and then process 1 stops. A connection can be "half-open" when one side has terminated its connection, but not the other. The side that has terminated can no longer send data using this connection, but the other side can. Finally, it is possible for both hosts to send f in simultaneously. In this case, both sides just have to send ack packets to terminate the TCP connection. This can be considered as a 2-way handshake since the f in/ack sequence is done in parallel in both directions.

Automata of Figure 17, Figure 18 and Figure 19 model the 3 phases of TCP protocol. A complete description of the TCP protocol with MSCs can be obtained as a composition of these tree models, just by performing a classical sequential composition of the automata, as shown on Figure 20. So far, we have proposed scenario descriptions of the TCP protocol, and provided the HMSCs describing the typical executions of TCP, but we did not define the commutation relation over events of the protocol that allows for the interleaving of different phases of the protocol. Let us define the local dependency relations D p for process p in rocess1, rocess2}. If we chose the normal weak concatenation, as defined in HMSCs, D p = Σ p × Σ p we obtain a synchronized execution of data transfer phase: every process send only one tcp packet and waits for the corresponding ack packet. Left part of figure 21 describes this kind of execution. This visual order is generated by the causal HMSC on figure 20 with D p = Σ p × Σ p for each process, i.e. the usual weak concatenation of HMSC. Note however that in an implementation of the TCP protocol, data transfer from the two sites can be performed in parallel. Hence, the classical sequential composition of HMSCs does not suffice to model interesting behaviors of TCP. Moreover, processes can send tcp packets without waiting for acknowledgments. Thus, events occurring between p(start) and p(end) can occur in any order in a visual extension, i.e. I p = {p!q(tcp), p?q(ack), p?q(tcp), p!q(ack), p?q(f in)} 2 -{(a, a) ∈ Σ 2 p } for each process p in {P rocess1, P rocess2} and q in {P rocess1, P rocess2} \ {p}. An execution of this causal HMSC is shown on the right part of figure 21.

Note that the causal HMSC we propose in Figure 20 for modeling the TCP protocol is not a regular causal HMSC and its linearization language is not regular: that means this protocol cannot be modeled by classical communicating finite state machines. Furthermore, this model is not window bounded, as an infinite number of ack messages can cross tcp ones. Finally, this causal HMSC H is not globally-cooperative, as the cycle labeled by comm12.comm21 does not have a connected communication graph. However, it is possible [START_REF] Gazagnaire | Scenario Languages: Using Partial Orders to Model, Verify and Supervize Distributed and Concurrent Systems[END_REF] to show that the language of H viewed as an automaton on basic parts is closed by commutation, that is L Basic (H) = [L Basic (H)]. In this case, we can apply directly the second part of Theorem 3 with A ′ equals to H ′ . Consequently, this protocol can be model-checked against any property described by a causal HMSC.

Conclusion

We have defined an extension of HMSC called causal HMSC that allows the definition of braids, such as those appearing in sliding window protocols. We have also identified in this setting, many subclasses of scenarios that were defined for HMSCs which have decidable verification problems. An interesting class that emerges is globally-cooperative causal HMSCs. This class is incomparable with safe compositional HMSCs because the former can generate scenario collections that are not existentially bounded. Yet, decidability results of verification can be obtained for this class.

An interesting open problem is deciding whether the visual language of a causal HMSC is finitely generated. Yet another interesting issue is to consider the class of causal HMSCs whose visual languages are window-bounded. The set of behaviors generated by these causal HMSCs seems to exhibit a kind of regularity that could be exploited. Finally, designing suitable machine models (along the lines of Communicating Finite Automata [START_REF] Brand | On Communicating Finite State Machines[END_REF]) is also an important future line of research.

Fig. 1 .

 1 Fig. 1. An HMSC over two MSCs

Fig. 2 .

 2 Fig. 2. Two MSCs M and N

Fig. 3 .

 3 Fig. 3. A causal MSC M and its visual extensions M 1, M 2.

Fig. 4 .

 4 Fig. 4. An example of causal MSC B: the set of visual extensions of B is not the instance per instance commutative closure of any visual extension of B.

Fig. 5 .

 5 Fig. 5. Visual extensions of the causal MSC B of Figure 4. lation ∼ p over Σ ⋆ p is the least equivalence relation such that, for any u, v in Σ ⋆ p and α, β in Σ p , α I p β implies uαβv ∼ p uβαv. Equivalence classes of ∼ p are called traces. For u in Σ ⋆ p , we let [u] p denote the trace containing u. Let B = (E, λ, {⊑ p }, ≪) be a causal MSC. We say ⊑ p respects the trace alphabet (Σ p , I p ) iff for any e, e ′ ∈ E p , the following hold: (i) λ(e) D p λ(e ′ ) implies e ⊑ p e ′ or e ′ ⊑ p e (ii) e ⊑ p e ′ implies λ(e) D p λ(e ′ )

Fig. 6 .

 6 Fig. 6. Concatenation example.

Fig. 7 .

 7 Fig. 7. Relations between linearizations, visual extensions and causal orders

Fig. 8 .

 8 Fig. 8. Communication graph for causal MSC B 1 ⊚ B 2 of Figure 6.

Fig. 9 .

 9 Fig. 9. A non finitely generated s-regular causal HMSC and its communication graph.

Fig. 10 .

 10 Fig. 10. An example of path, a configuration C, and its C-subpaths.

  For a set B of basic parts, we associate a trace alphabet (B, I B ) (w.r.t. the trace alphabets {(Σ p , I p )} p∈P ) where I B is given by: B I B B ′ iff for every p, for every α ∈ Alph p (B), for everyα ′ ∈ Alph p (B ′ ), it is the case that α I p α ′ . We let ∼ B bethe corresponding trace equivalence relation and denote the trace containing a sequence u = B 1 . . . . .B ℓ in B ⋆ by [u] B (or simply [u]). For a language L ⊆ B ⋆ , we define its trace closure [L] B = u∈L [u] B . We begin by proving that the decomposition of any causal MSC B is unique up to commutation. More precisely, Proposition 2 Let B 1 . . . B k be a decomposition of a causal MSC B. Then the set of decompositions of B is [B 1 . . . B k ]. Proof : It is clear that every word in [B 1 . . . B k ] is a decomposition of B.

Proposition 3

 3 For a given causal MSC B, we can effectively decompose B in time O(|B| 2 ).

  e ′ and λ(e) I p λ(e ′ )} , R ′′ p = {(e, e ′ ) ∈ E p × E p | e ⊑ p e ′ and e ′ ⊑ p e and λ(e) D p λ(e ′ )} .

1 -

 1 this word is generated by an accepting path ρ = n 0 P → n 1 . . .

  l of H such that ⊚(w) = P 1 ⊚. . .⊚P l . By proposition 2, we know that any other decomposition of ⊚(w) belongs to [B 1 . . . B k ], and in particular, the one we choose. Thus we obtain that BP (H) ⊆ [L Basic (H)].

Fig. 12 .

 12 Fig. 12. PCP encoding with two causal HMSCs

Fig. 13 .

 13 Fig. 13. Window of message m 1

Figure 13

 13 Figure 13 illustrates notion of window, where the window of the message m 1(the first answer from q to p) is symbolized by the area delimited by dotted lines. It consists of all but the first message Q from p to q. Clearly, the causal HMSC H of Figure1is not window-bounded. We now describe an algorithm to effectively check whether a causal HMSC is window bounded. It builds a finite state automaton whose states remember the labels of events that must

Theorem 5

 5 Let H = (N, N in , B, -→, N fi ) be a causal HMSC. Then we have:(i) If H is window-bounded, then H is K-window-bounded, where K is at most b • |N | • |Σ|. (ii)Further, we can effectively determine whether H is window-bounded in time O(s • |N | 2 • 2 |Σ| ), where s is the sum of the sizes of causal MSCs in B.

Fig. 14 .

 14 Fig. 14. A s-regular causal HMSC with the communication graph of its cycle

Fig. 15 .

 15 Fig. 15. A regular (but not finitely generated) set of MSCs

Fig. 16 .

 16 Fig. 16. Comparison of Scenario languages

Fig. 18 .

 18 Fig.18. Data transfer between process 1 and process 2.

Fig. 19 .

 19 Fig. 19. The TCP connection termination.

Fig. 20 .

 20 Fig. 20. A (causal) HMSC model of the TCP protocol.

Fig. 21 .

 21 Fig. 21. Two executions of the TCP example, with the HMSC semantics (on the left) and with the causal HMSC semantics (on the right).

  •. HMSCs can then be considered as causal HMSCs labelled with MSCs, and equipped with empty independence relation (for every p ∈ P, I p = ∅). Hence, a path ρ of H generates an MSC by concatenating the MSCs along ρ with operation •. We let Vis(H) denote the set of MSCs generated by accepting paths of H with •, and call Vis(H) the visual language of H. Recall that an MSC language (i.e. a collection of MSCs) L is finitely generated[START_REF] Morin | Recognizable sets of Message Sequence Charts[END_REF] iff there exists a finite set X of MSCs satisfying the condition: for each MSC B in L, there existB 1 , . . . , B ℓ in X such that B = B 1 • • • • • B ℓ .Many protocols exhibit scenario collections that are not finitely generated. For example, sliding window protocols can generate arbitrarily large MSCs repeating the communication behavior shown in MSC N of Figure

  the converses do not hold in general. • If every causal MSC labelling transitions of H and H ′ respects {(Σ p , I p )} p∈P , then (i) ⇔ (ii) and (i) ′ ⇔ (ii) ′ . • If every causal MSC labelling transitions of H and H ′ is weak FIFO, then (ii) ⇔ (iii) and (ii) ′ ⇔ (iii) ′ .

  By similar arguments as in (i), it is easy to show that among E i+1 , . . ., E i ′ , at most |N | • |Σ| • 2 |B| of them are nonempty. The claim then follows.

  5(i)] Suppose that H is not k-window-bounded, wherek = b • |N | • |Σ|. Let B ∈ B be a causal MSC in cMSC (H), and let the pair (e, f ) be a message of B. Let ρ be a path of H, and V ∈ Vis(⊚(ρ)) be an MSC such that the message (e, f ) is crossed by k + 1 messages in V Recall that a causal MSC contains at most b/2 messages. Then, ρ contains at least 2|Σ| occurrences of a node n ′ , such that the label of n ′ contains at least a message m ′ that crosses (e, f ) in V . Without loss of generality, we can consider that n ′ is repeated at least |Σ| times after B in ρ (else we apply a symmetric proof, considering repetitions of B ′ occurring before B). That is, ρ is of the form

  Hence, the overall complexity of the algorithm is in O(|N | 2 • 2 |Σ| ). As, we build the two automata A (e,f ) and A (e,f ) for each occurrence (e, f ) of a message in each causal MSC labeling a transition of H, we obtain a complexity in O(s.|N | 2 .2 |Σ| ), where s is the sum of the sizes of causal MSCs in B.

  Trivially, globally-cooperative causal HMSCs are a strict subclass of causal HMSCs. Figure9displays a sregular causal HMSC whose visual language is not finitely generated. It follows that (s-regular/globally-cooperative) causal HMSCs are strictly more powerful than (s-regular/globally-cooperative) HMSCs.Another extension of HMSCs is compositional HMSCs (or CHMSCs for short), first introduced by[START_REF] Gunter | Compositional Message Sequence Charts[END_REF]. CHMSCs generalize HMSCs by allowing dangling message-sending and message-reception events, i.e. the message pairing relation ≪ in a compositional MSC is only a partial non-surjective mapping contained in E ! × E ? . The concatenation of two compositional MSCs M • M ′ performs the instance-wise concatenation as for MSCs, and computes a new message pairing relation ≪ ′′ defined over (E ! ∪ E ′ ! ) × (E ? ∪ E ′ ?

A different notion called strong FIFO that does not allow overtakings of messages between two given processes of different content is also frequently used in the MSC literature.

• (n, ∅), B, (n ′ , Future B (e, f )) ∈ δ if n B -→ n ′ and (e, f ) belongs to B.

• (n, X), B, (n ′ , X ′ ) ∈ δ, where B = (E, λ, {⊑ p }, ≪, ≤), if n B -→ n ′ , and X ′ = X ∪ {λ(y) | ∃x, y ∈ E, ∃a ∈ X ∧ a D λ(x) ∧ x ≤ y}.

Note that the first rule in the construction of the transition relations of A (e,f ) simply copies the transitions of H. The second rule perform a random choice of a message in a random occurrence of a transition of H labelled by B. This rule is important, as it allows to chose nondeterministically an occurrence (e, f ) of a message after an arbitrary path in the HMSC. The last rule updates the futures or pasts after the choice of a message occurrence. A state q = (n, X) in A (e,f ) represents a possible set X of labels in Future ⊚(ρ) (e, f ) for some path ρ that ends (respectively starts) at node n in H, and contains a message (e, f ). Slightly abusing the notation, we will denote by Future(q) (resp. Past(q)) the set X. Note that in any strongly connected subset

. Hence, we will denote by Future(C) (resp. Past(C)) the set of observed labels on any state of C.

We can also build a finite state transition system A ′ (e,f ) that computes the possible pasts of (e, f ), by a backward search in the causal HMSC H.

We observe the following properties of the finite state automata A (e,f ) and A ′ (e,f ) .

Lemma 4 Let H = (N, N in , B, -→, N fi ) be a causal HMSC. Let B be a causal MSC in B and (e, f ) a message in B with the label of e being p!q(m). Consider the finite state automata A (e,f ) and A ′ (e,f ) as constructed above. Then, H is window-bounded iff both of the following conditions hold:

• There does not exist a strongly connected component C in A (e,f ) and a letter q!p(m ′ ) ∈ Σ such that q!p(m ′ ) is in Alph(B) -Future(C) for some causal MSC B labelling a transition in C. • There does not exist a strongly connected component C in A ′ (e,f ) and a letter q!p(m ′ ) ∈ Σ such that q!p(m ′ ) is in Alph(B)-Past(C) for some causal MSC B labelling a transition in C.

Proof : One direction is straightforward. If any of these strongly connected components exists (either before or after m), then there is an unbounded number of path generating an unbounded number of occurrences of q!p(m ′ ) that are not causally related to m. Hence, for each of these path, there is a visual extension where all m ′ generated by occurrences of the cycle cross m, and the window size of m is not bounded. The other direction is a direct consequence of Theorem 5(i).

CaHMSC for causal HMSCs and CHMSC for compositional HMSCs.

A Detailed Example

We consider the TCP sliding window mechanism to show the usefulness and the expressive power of causal HMSCs.

The Transmission Control Protocol (TCP) is one of the core protocols of Internet. Using TCP, applications on networked hosts can create point-to-point connections to one another, over which they can exchange data in packets. The protocol guarantees reliable and in-order delivery of data from sender to receiver. TCP also distinguishes data for multiple connections by concurrent applications (e.g. Web server and e-mail server) running on the same host.

We first explain the relevant aspects of the TCP protocol [START_REF]DARPA Internet Program Protocol Specification[END_REF]. For reasons of simplicity and readability, we shall abstract away some of the technical aspects of the protocol when constructing a model. The classical TCP is divided into 3 parts:

The first one is connection establishment. The procedure to establish connections uses a synchronize (syn) packet and involves an exchange of three messages. This exchange is called a three-way handshake [START_REF] Dalal | Connection Management in Transport Protocols[END_REF]. Once a connection is established it can be used to carry data in both directions, that is, the connection is "full duplex". This connection phase can be modeled using MSCs, as shown in Figure 17. In this example, MSC Connect12 describes the case when process 1 initiates a connection, and MSC Connect21 the case when process 2 initiates the connection. When a process executes an event labeled by start, it is ready to begin the data transfer phase of TCP. The second phase of the TCP protocol is data transfer. TCP is able to transfer a continuous stream of bytes in each direction between its users by packaging some number of bytes into segments for transmission through the Internet system. TCP uses sequence numbering in order to recover from data that is