Thomas Gazagnaire

Shaofa Yang

Lo

H Lou T,

Blaise Genest

P S Thiagarajan

Causal Message Sequence Charts

Keywords: Scenario languages, partial orders, distributed systems, modeling

Properties of scenario languages (Message Sequence Charts, Live Sequence

Charts, UML's sequence diagrams) have been widely studied in the last decade. Scenario languages embed the expressive power of Mazurkiewicz traces, and consequently, several problems such as model checking are undecidable for these languages. Despite their expressive p o wer, most of scenario languages can only model nitely generated behaviors that can be described as the concatenation of patterns from a nite set. However, non-nitely generated behaviors such as sliding windows frequently occur in asynchronous distributed systems. Several extensions of Message Sequence Charts have been proposed to capture non-nitely generated behaviors, but these variants embed the expressive p o wer of automata communicating via unbounded channels (and thus of Turing Machines), making their analysis even more intractable. We propose a new extension of Message Sequence Charts that can model non-nitely generated MSC languages without embedding the expressive power of communicating automata, and study its properties.

Message Sequence Charts Causaux R sum : Les propri t s des langages de sc narios (Message Sequence Charts, Live Sequence Charts, ou diagrammes de s quences d'UML) ont t largement tudi es ces dix derni res ann es. Les langages de sc narios ayant la puissance d'expression des traces de Mazurkiewicz, de nombreux probl mes pratiques, comme le model-checking, sont ind cidables pour ces langages. De plus, malgr leur puissance d'expression lev e, la plupart des langages de sc narios ne permet de g n rer que des comportements niment engendr s, qui ne peuvent tre exprim s que comme des concat nations s quentielles de comportements choisis dans un ensemble ni de motifs. Cependant, on rencontre couramment des comportements non-niment engendr s lorsque l'on cherche mod liser des syst mes distribu s et asynchrones, ce qui est le cas du m canisme de fen tres glissantes du protocole TCP. Plusieurs extensions des Message Sequence Charts ont t propos es pour rem dier ce probl me, mais ces variantes donnent aux sc narios la puissance d'expression des automates communicants canaux de communication non-born s (et par cons quent des Machines de Turing), rendant l'analyse de ces langages encore plus di cile. Ce rapport propose une extension des Message Sequence Charts qui permet de d nir des comportements non niment engendr s sans pour autant donner aux sc narios la puissance des automates communicants, et tudie ses propri t s.

Mots-cl : scenarios, ordres partiels, syst mes distribu s, mod lisation 1 Introduction Scenario languages have met a considerable interest in the last decade. The enthusiasm of the research and engineering community for this kind of notation can be explained by t wo major characteristics of these languages.

Firstly, from the engineering point of view, scenario languages have a simple and appealing graphical representation. The graphical notation depicts clearly the interaction among processes with only a few concepts: processes, messages, internal actions. Figure 1 shows an example of a simple protocol described with High-level Message Sequence Charts (or HMSCs): two processes p and q exchange messages m and n, and then terminate their interaction with a message o. After sending m, process p systematically performs an internal action a. Scenario Secondly, from the research c o m m unity p o i n t of view, scenario languages are well formalized: up to some variation, scenario languages can be de ned as nite state automata over an alphabet of labeled partial orders. The HMSC of Figure 1 can be seen as an automaton labeled by MSCs M1 and M2. These automata can be considered as generators of (usually in nite) families of labeled partial orders and have an interesting expressive power. Furthermore, they are a true concurrency model, and as a consequence, one can expect to solve some problems more e ciently with scenario languages than with an equivalent i n terleaved model. In this report, we will only consider High-level Message Sequence Charts (or HMSCs for short), which are automata over an alphabet of Message Sequence Charts (MSCs), a particular kind of labeled partial orders that are closed for communication (i.e each message sent in a MSC M is also received in M). However, most of results on HMSCs can be easily adapted to other classical scenario languages (Live Sequence charts 12], UML's sequence diagrams 21], ...). Figure 1: A simple distributed protocol described with 2 MSCs and a HMSC However, classical scenario languages also have some major drawbacks. First, it has been shown that HMSCs have, at least, the expressive p o wer of semi-traces 20] and Mazurkiewicz INRIA traces 19]. These results indicate that most of usual problems related to speci cation languages are undecidable for scenario languages. For instance, if we consider two HMSCs H 1 and H 2 , and call F 1 and F 2 the sets of partial orders generated by H 1 and H 2 one can not decide whether H 1 and H 2 de ne a common behavior (i.e. F 1 \F 2 = ). One can not either model-check an HMSC against a property expressed in a temporal logic such a s C T L . T h a t could have m e a n t that scenario are unusable, at least as a speci cation language, because they are not amenable to veri cation.

To tackle this rst drawback, several subclasses of scenario languages have been identi ed: regular High-level MSCs 3], for which the set of all linearizations form a regular language, globally cooperative M S C s 1 9 , 8], for which the common behavior problem described above becomes decidable. Recently, 14] has shown that diagnosis ( nding a complete execution of a model from a partial observation) is decidable for HMSCs.

The second drawback of classical scenario languages is the following: when we consider the set of MSCs generated by a HMSC, these MSC languages are unsurprisingly nitely generated, i.e all MSCs in the language can be de ned as the sequential composition of MSCs chosen from a nite set of MSCs 18]. However, most protocols used nowadays exhibit behaviors that are not nitely generated, for example, sliding windows scenarios: a protocol may involve a sequence of questions and answers from a process A to a process B. A does not have to wait for the answer to a question before sending up to n several other new questions. The value n is then called the size of the sliding window. Behaviors of this kind of protocols often gure messages from A to B and messages from B to A crossing over the network. They may even resemble an in nite braid as in the example of Figure 2, where a message from A to B systematically crosses at least one message from B to A, and conversely. Clearly, a set of behaviors containing such braids of arbitrary sizes can not be de ned by concatenation of elements chosen from a nite set of nite MSCs.

To t a c kle that second drawback, an immediate solution is to extend scenario languages by allowing a partition of message emissions and receptions in MSCs and match emissions and receptions at the time of composition. This solution was proposed in 11], and is called Compositional Message Sequence Charts (or CMSCs for short). However, CMSCs have t h e expressive p o wer of communicating automata (which are known to be as powerful as Turing Machines 5]). Consequently, several problems that are decidable for HMSCs become undecidable for CMSCs. For instance, if we consider a HMSC H, it is trivial to know if there exists an MSC generated by H that contains a given message m. This trivial property becomes undecidable for CMSCs. In order to resolve simultaneously decidability and expressiveness drawbacks, several classes of CMSCs 17, 4 , 1 1 ], sometimes called realizable or safe CMSC, were de ned to ensure decidability 1 0 ]. Safe CMSCs generate only 9-bounded MSCs, i.e. behaviors that have at least one linearization where communication channels do not exceed a certain bound B. This paper proposes another approach to extend HMSC expressiveness while keeping the formalism tractable. It consists in a generalization of the sequential composition mechanisms that allows some commutation among composed MSCs. The resulting generalized model is called causal HMSCs. It is uncomparable with safe CMSCs, the main reason being that FIFO c a n n o t b e ensured in such scenarios. It also implies that the main method used to solve decidability for safe CMSCs -the Kuske's alphabet to encode the problem into traces -cannot be applied since the n-th message sent on a channel is not necessarily the n-th message received on that channel. Instead, we generalize the method of 9] based on atoms, i.e. parts of MSCs that can not be obtained as a concatenation of smaller parts.

This new model is de ned in section 2. The following sections study properties of causal HMSCs: section 3 shows the existence of a decidable subclass of causal HMSCs called tight causal HMSCs, where the linearizations of the orders generated form regular languages. Section 4 shows the existence of a decidable subclass called globally-cooperative Causal HMSCs, where the emptiness of the intersection of two sets of orders is decidable. Section 5 shows the existence of a decidable subclass called bounded window causal HMSCs where each message of a generated order is crossed by a bounded number of messages. Section 6 is a case study. A part of the TCP protocol that can not be modeled with HMSCs is designed with causal HMSCs. Section 7 concludes this work.

INRIA 2 Causal MSCs and Causal HMSCs

Through the rest of the paper, we x a nite nonempty s e t P of process names where jPj > 1, a nite nonempty set Msg of message names, Act a nite nonempty set of internal action names. We de ne the alphabets ! = fp!q(m) j p q 2 P p 6 = q m2 Msgg, ? = fp?q(m) j p q 2 P p 6 = q m2 Msgg, a n d act = fp(a) j p 2 P a 2 Actg. The letter p!q(m) means the sending of message m from p to q p?q(m) the reception of message m at p from q a n d p(a) the execution of internal action a by process p. Set = ! ? act . We de ne 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, w e s e t p = f 2 j loc( ) = pg. De nition 1 A causal MSC over (P ) is a structure B = ( E fv p g p2P ) where E is a nite nonempty set. Members of E are c alled events. : E ! is a labeling function. This labeling function allows for a partition of E into three subsets, E ! = ;1 ( ! ),E ? = ;1 ( ? ) and E act = ;1 ( act ) For each process p in P, v p E p E p is a partial order on E p , w h e r e E p = fe 2 E j loc( (e)) = pg.

E ! E ? identi es message emission-reception pairs. Thus, satis es the following conditions:

For each e 2 E ! , there is at most one e 0 2 E ? such that (e e 0 ) 2 . For each e 2 E ? , t h e r e is at most one e 0 2 E ! such that (e 0 e ) 2 .

For each (e e 0 ) 2 , i f (e) = p!q(m), t h e n (e 0 ) = q?p(m). Let B = ( E fv p g p2P ) be a causal MSC as above. For convenience, we will often drop the subscript p 2 P and let p range over P. We will also write B interchangeably as (E fv p g ), where E E is the transitive closure of ; S p2P v p . We d e n e Alph(B) = f (e) j e 2 Eg. For each p in P, w e s e t Alph p (B) = Alph(B) \ p . Moreover, we de ne the communication graph of B, denoted by CG B , to be the directed graph (Q ), where Q = fp 2 P j E p 6 = g and Q Q is given by: (p q) 2 i \ (E p E q ) 6 = . A linearization of B is a sequence a 1 a 2 : : : a `in `, where `= jEj, such that the elements of E c a n b e l i s t e d a s e 1 , e 2 , : : : , e `with (e i ) = a i for each i a n d e i e j implies i j for any i j. We l e t Lin(B) denote the set of linearizations of B.

As for MSCs, causal MSCs can be represented graphically. In MSCs, each process is represented as a v ertical line (also called lifeline), that symbolizes time elapsing from top to bottom. Along a lifeline, events are totally ordered. For causal MSCs, we w i l l k eep the same representation, except that we will represent e a c h process as a labeled partial order (instead of a labeled total order). Figure 3 depicts a causal MSC M 1 . In M 1 , e v ents located on process p or on process q are unordered. This is symbolized by t wo b o xes attached to instance names p and q, containing two unordered events, respectively e 1 and e 2 for process p, a n d f 1 and f 2 for process q. The linearizations de ned by this causal MSC are: p!q(m):q?p(m):p!q(n):q?p(n) p!q(m):p!q(n):q?p(m):q?p(n) p!q(m):p!q(n):q?p(n):q?p(m) p!q(n):p!q(m):q?p(n):q?p(m) p!q(n):p!q(m):q?p(m):q?p(n) p!q(n):q?p(n):p!q(m):q?p(m) ) is a causal MSC B 0 = (E 0 0 fv 0 p g 0 0 ) such that E 0 = E, 0 = , for each p, v 0 p is a superset of v p , and 0 = . Consequently, 0 is a superset of .

If each v 0 p i s a t o t a l o r der, then we call B 0 a visual extension of B. For the causal MSC B, we will denote by Vis(B) the set of all its visual extensions.

Visual extensions of causal MSCs are MSCs, usually called basic Message Sequence Charts in the literature. The initial idea of visual ordering comes from 2], that notices that depending on the interpretation of an MSC, for example when a lifeline describes a physical entity i n a n e t work, imposing an ordering on message receptions is not possible. Hence, 2] distinguishes two orderings on MSCs: a visual order, 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.

INRIA

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. For example, for the causal MSC B of Figure 4 in any visual extension V = ( fe 1 e 2 f 1 f 2 g fv p v q g ) 2 V i s (B) we can not have e 2 v p e 1 and f 1 v q f 2 at the same time. Even with the possibility to de ne partial orders on each process, Causal MSCs still de ne nite behaviors. We hence have to de ne composition operators that allow for the de nition of unbounded behaviors. For each process p in P, we x a concurrent alphabet ( p I p ), where I p is an independence relation over the alphabet of actions p , i . de nitions of Mazurkiewicz traces, for each trace alphabet ( p I p ), w e de ne the associated trace equivalence p over ? p to be the least equivalence relation such that, for any u v in ? p and a b in p , a I p b implies uabv p ubav. We let u] p (or simply u]) d e n o t e t h e equivalence class containing u, with respect to p . We c a n n o w de ne the composition of two causal MSCs.

De nition 3 Let B = (E fv p g ) and B 0 = (E 0 0 fv 0 p g 0 ) be causal MSCs. We de ne the concatenation of B with B 0 , denoted by B B 0 , to be the causal MSC B 00 = (E 00 00 fv 00 p g 00 ) where E 00 is the disjoint union of E and E 0 . 00 (e) = (e) for e 2 E and 00 (e) = 0 (e) for e 2 E 0 . For each process p in P, v 00 p is the transitive closure of v p S v 0 p S f(e e 0 ) 2 E p E 0 p j (e) D p 0 (e 0 )g.

00 = 0 .
Clearly is a well-de ned and associative operation. We can note that composition of causal MSCs is more general than the usual composition of traces de ned as u]: v] = uv], a s concurrency on processes in each causal MSC need not be compatible with the independence relations fI p g p2P . Hence we can de ne a causal MSC such that e 1 v p e 2 and (e 1 )I p (e 2 ).

So, for a causal MSC B we can not in general nd a word u such t h a t Lin(B) = u].

Note also that if B B 0 are MSCs and D p = p p for every p 2 P , then B B 0 is equivalent to the usual weak sequential composition of B with B 0 (denoted B B 0 ). We recall that the usual weak sequential composition preserves the ordering in B and B 0 , and impose an ordering between events of B and B 0 located on the same process. For more information on weak sequencing, and more generally on the semantics of Message Sequence Charts, the interested reader is referred to 22].

As for MSCs, causal MSCs are not expressive enough to de ne an interesting language. Hence, causal MSCs must be equipped with the usual operations met in process algebras, to allow c hoices, iterations, etc. As for HMSCs, this will be done using an automaton over an alphabet of causal MSCs, called causal High-level MSC.

De nition 4 A causal High-level MSC ( causal HMSC for short) is a structure H = (N N in B N ;!) where:

N is a nite nonempty set. Members of N are c alled nodes. N in N is the set of initial nodes.

B is a nite nonempty set of causal MSCs.

N N is the set of nal nodes.

INRIA ;! N B N is the transition relation. Let H = ( N N in B ;! N ) be a causal HMSC. A path in H is a sequence = n 0 B1 ;! n 1 B2
;! n 2 n `;1 B ;! n `. We refer to n 0 as the starting node and to n `as the ending node of path . The path is accepting i n 0 2 N in and n `2 N . A cycle in H is a path whose starting and ending nodes are equal. The causal MSC generated by , denoted by ( ), is B 1 B 2 B `. A causal MSC B is said to be generated by H i B is generated by an accepting path of H. We l e t cMSC (H) denote the set of causal MSCs generated by H. Similarly, w e w i l l d e n o t e b y Vis(H) and Lin(H) the set of visual extensions and linearizations of all causal MSCs in cMSC (H). We can here immediately remark that Lin(H) = fLin(v) j v 2 Vis(H)g, i.e. the set of linearizations generated by H is the set of linearizations generated by its visual extensions. Finally, note that we do not require any ordering among receptions of messages, even for messages of the same kind. Hence, messages exchanged between two processes in the same direction are not necessarily delivered at the same speed and can cross each o t h e r . This is a major di erence with compositional MSCs, where it is crucial to have a FIFO ordering among messages of the same type.

De nition 5 A MSC language L is nitely generated 18] i there exists a nite set of MSCs X such that any MSC B in L can be de ned as the weak sequential composition of elements of X, i.e. B = B 1 B 2 B t for some B 1 : : : B t in X.

By de nition, High-level Message Sequence Charts de ne nitely generated MSC languages. Note however that all nitely generated MSC languages are not HMSC languages:

B n 1 :B n 2 is nitely generated but is not an HMSC language. For a causal HMSC H, Vis(H) is not necessarily nitely generated. Consider for instance the causal HMSC H of Figure 6, with the following dependence relation D = f(p!q(m) p !q(m)) (p?q(n) p ?q(n))g. The language of visual extensions of H contains braids interleaving messages m and n an arbitrary number of times, such a s t h e one represented on the right p a r t o f the gure. Clearly, the MSC language Vis(H) is not nitely generated.

Let us compare the expressive powers of the di erent scenario models. Firstly, it is obvious that causal HMSCs embed the expressive p o wer of HMSCs: if we c hoose as de nition of the dependency relation the set of all pairs of events located on similar processes (8p 2 P D p = p p ), then the set of visual extensions generated by a causal HMSC with such dependency relation is the set of MSCs generated by a HMSC.

Second, causal HMSCs and CMSCs are uncomparable. Consider, for example the safe CMSC of Figure 7. In CMSCs, a messages need not be complete in the alphabet labeling the partial order automaton. Pending emissions and receptions are associated during concatenation to form messages, and the language generated by a CMSC is the set of MSCs obtained this way. To pair message emissions and receptions, the i th emission of a message of type m is associated to the i th reception of the same type of message. Hence, two occurrences of a given message type can not overtake. The CMSC depicted in the left part of Figure 7 de nes a set of executions where an arbitrary number of occurrences of message m cross a single RR n 6301

p q m n m m n n p q M p q M' m n Figure 6: An example of Causal HMSC H, w i t h D = f(p!q(m) p !q(m)) (p?q(n) p ?q(n))g,
and a behavior in V i s (H) occurrence of message n. This set of behaviors can not be represented as a causal HMSC: to allow executions where message n crosses an arbitrary number of occurrences of message m, causal MSCs should allow c o m m utations between m and n, and hence would also de ne behaviors where m is sent arbitrarily often before n. The causal HMSC depicted on the right of the gure de nes a superset of these executions. Conversely, executions generated by a CMSC need to respect the FIFO ordering among messages of the same kind, which i s not required in causal HMSCs. Hence Causal MSCs and CMSCs are uncomparable. Note also that causal HMSCs allow to answer some questions that are undecidable for Communicating automata (or equivalently CMSCs): let us consider a message m from a process p to a process q. Let us try to answer the following question: is there a MSC generated by H where message m is sent and received? If H = ( N N in B ;! N f i ) is a HMSC or a causal HMSC, answering this question is trivial, and just consists in checking whether there exists an MSC or a causal MSC in B that contains the message m. For communicating automata, this question is known to be undecidable 11].

Linearization Languages of Causal HMSCs

An embedding of Mazurkiewicz traces into HMSCs is described in 20, 1 9 ]. Following basic results in Mazurkiewicz trace theory 7], this embedding means that it is undecidable to determine whether the linearization language of a given HMSC is regular. In 3, 19], a subclass of HMSCs, called bounded HMSCs, was identi ed such that the linearization language of every bounded HMSC is regular. As already mentioned, causal HMSCs embed I={ ( q!p(n), q?p(m)) } the expressive p o wer of HMSCs. Thus, due to 3, 1 9 ] it is undecidable to test whether the linearization language of a given causal HMSC is regular. We show hereafter a su cient condition for a causal HMSC to have a regular linearization language.

We recall the notion of connectedness from Mazurkiewicz trace theory [START_REF] Dalal | Connection management in transport protocols[END_REF]). Let p 2 P . We s a y ; p is D p -connected i the (undirected) graph (; D p \(; ;)) is connected. Now we s a y the causal MSC B is tight i its communication graph CG B is strongly connected and moreover for every p 2 P , Alph p (B) is D p -connected. If however the communication graph CG B is weakly connected and moreover for every p 2 P , Alph p (B) is D p -connected, then we will say that B is weakly tight.

Let H = ( N N in B N ;!) be a causal HMSC. We say t h a t H is tight i for every cycle in H, t h e causal MSC ( ) is tight. Equivalently, H is tight i f o r e v ery strongly connected subgraph G of H such that fB 1 : : : B `g is the set of causal MSCs appearing in G, B 1 : : : B `is tight. Note that tightness of B 1 : : : B `does not depend on the order in which B 1 : : : B `are listed.

Following these de nitions, we c a n n o w establish the main result of this section:

Theorem 1 Let H = (N N in B N ;!) be a tight causal HMSC. Then Lin(H) is a regular subset of ? i.e. we can build an automaton over such that it recognizes Lin(H).

Notice that a weakly thight (causal) HMSC may not be bounded, hence Lin(H) may n o t be regular. For instance, consider a causal HMSC H that iterates a single message, i.e. H is a loop labeled by a MSC that contains a message (a b), with a = p!q and b = q?p. Lin(H) is a Dyck or parenthesis language, which i s w ell known not to be regular. Surprisingly, w e do not need Lin(H) to be regular to be able to model check HMSCs, as shown in 9] and also in the next section.

The result for (non causal) tight HMSC was proved by 16] using an encoding into connected traces and building an automaton which recognizes such connected traces. In our case, nding such embedding into Mazurkiewicz traces seems impossible due to the non Fifoness. Thus, we adapt the proof of regularity of trace closures of loop-connected automata from [START_REF] Dalal | Connection management in transport protocols[END_REF][START_REF] Morin | Recognizable sets of message sequence charts[END_REF].

The rest of this section is now d e v oted to the proof of Theorem 1. We x a t i g h t causal HMSC H as in the theorem, and show t h a t w e can build a nite state automaton A H over which accepts Lin(H).

First, we establish some technical results.

Proposition 1 Let = 1 : : : 2 : : : j j be a path of H, where for each i = 1 : : : j j, the

subpath i = n i 0 Bi 1 ;! n i 1 : : : n i `i;1 B i `i
;! n i 0 is a cycle (these cycles need not be c ontiguous).

Suppose further that the sets b B i = fB i 1 : : : B i `ig, i = 1 : : : j j, are equal. Let e be an event in ( 1 ) and e 0 an event in ( j j ). Let ( ) = ( E fv p g

). Then we have e e 0 .

Proof: We consider two cases.

Case (i): loc( (e)) = loc( (e 0 )).

INRIA

Let p = loc( (e)). Let us recall that H is tight, thus Alph p ( ( 1 )) = : : : = Alph p ( ( K ))

is D p -connected. Consequently, w e can nd a set of events fe j g j=1 ::: t , where t j p j ; 2, each e j is in ( j+1 ), and such that (e) D p (e 1 ) D p : : : D p (e t ) D p (e 0 ). Thus e e 1 : : : e t e 0 .

Case (ii): loc( (e)) 6 = loc( (e 0 )). Let p 1 p 2 : : : p t be a path from loc( (e)) to loc( (e 0 )) in the communication graph of ( ), where p 1 = loc( (e)), p t = loc( (e 0 )). In view of the arguments in Case (i), it is easy to see that we can pick e v ents e i f i in ( ui ), i = 1 : : : t ;1, where for each i, u i = j p1 j + j p2 j + : : : + j pi j, loc(e i ) = p i , loc(f i ) = p i+1 and e i f i .

Thus e e 1 f 1 e 2 f 2 : : : e t;1 f t;1 e 0 . Let = n 0 B1

;! B ;! n `be a path in H, where B i = ( E i i fv i p g i ) for i = 1 : : :

. Let ( ) = ( E fv p g

). A con guration of is a -closed subset of E. Let C be a con guration of . A C-subpath of is a maximal subpath % = n u Bu+1 ;! : : : B u 0 ;! n u 0 , such that C \ E i 6 = for each i = u : : : u 0 . For such a C-subpath %, w e de ne its C-residue to be the set (E u+1 E u+2 E u 0 ) ; C. Lemma 1 Let be a p ath in H and C be a c on guration of . Then, (i) The number of C-subpaths of is at most K subpath = jNj j j 2 jBj .

(ii) Let % be a C-subpath of . Then the number of events in the C-residue of % is at most K residue = jNj j j 2 jBj maxfjBj j B 2 B g , w h e r e jBj denotes the number of events in the causal MSC B.

Proof:

RR n 6301 (i) Suppose the contrary. Let K = j j 2 jBj . We can nd 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 , l e t h be the subpath of from n i h to n i h+1 and let b B h bethesetof causal MSCs appearing in h . Hence we can nd j1 , j2 , : : : , j j j , j 1 < j 2 < : : : < j j j , such that b B j1 = b B j2 = : : : = b B j j j . Pick a n e v ent e from ( j1 ) with e = 2 C. Such a n e exists, since, for example, none of the events in the rst causal MSC appearing in j1 is in C. Pick a n e v ent e 0 from ( j j j ) with e 0 2 C. Applying Proposition 1 yields that e < e 0 . This leads to a contradiction, since C is -closed.

(ii) Let % = n i Bi+1

;! : : : B i 0 ;! n i 0 . Let b E j = E j ;C for j = i+ 1 : : : i 0 . By similar arguments as in (i), it is easy to show that among b E i+1 , : : : , b E i 0 , a t m o s t jNj j j 2 jBj of them are nonempty. The claim then follows.

We are now ready to de ne the nite state automaton A H = ( S S in S =)) 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 S the nal states. Fix K subpath , K residue to be the constants de ned in Lemma 1. If B = ( E fv p g ) is a causal MSC and E 0 a subset of E, then we de ne the restriction of B to E 0 to be the causal MSC B 0 = ( E 0 0 fv 0 p g 0 ) as follows. As expected, 0 is the restriction of to E 0 for each p, v 0 p is the restriction of v p to (E 0 \ E p ) (E 0 \ E p ) a n d 0 is the restriction of to E 0 . Intuitively, for a word in ? , A H guesses an accepting path of H and checks whether is in Lin( ( )). After reading a pre x 0 of , A H memorizes a sequence of subpaths from which 0 was linearized (i.e the C-subpath of a path such t h a t C is a con guration reached after playing 0 and ( ) contains C). With Lemma 1, it will become clear later t h a t a t a n y time, we should rememberatmostK 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 i = ( E i fv p g ) is K-bounded if jEj K. A segment is a tuple (n ; W n 0 ), where n n 0 2 N, ; is a nonempty subset of , a n d W is either a non-empty K residue -bounded causal MSC, or the special symbol ?. The state set S of A H is the collection of nite sequences 1 2 : : : `, 0 ` K subpath , where each i is a segment. Intuitively, a segment (n ; W n 0 ) keeps track of a subpath % of H which starts at n and ends at n 0 . ; 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 de ne A H = ( S S in S =)) as follows:

As mentioned above, S is the collection of nite sequence of at most K subpath segments.

The initial state set is S in = f"g, where " is the null sequence.

INRIA

A state is nal i it consists of a single segment = ( n ; ? n 0 ) such that n 2 N in and n 0 2 N (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 0 where B = (E fv p g

). Let e be a minimal event in B

(with respect to ) and let a = (e). Let = (n ; W n 0 ) where ; = fag. Let R = E ; f eg. 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 0 i ) for each i. Suppose, for every e 0 2 E with e e 0 , it is the case that (e 0 ) I p for any 2 p \ ( S k+1 i `;i ), where p = loc(e 0 ). ( create a new segment ) Let ŝ = 1 : : : k k+1 : : : `. If ŝ is in S, t h e n s a =) ŝ.

In particular, for the initial state ", w e h a ve " a =) .

( add to the beginning of a segment ) Suppose n 0 = n k+1 . Let ^ = (n ;

Condition (ii):

Suppose s = 1 : : : k k+1 : : : `is a state in S where i = (n i ; i W i n 0 i ) for i = 1 2 : : : . Suppose W k 6 = ?. Let W k = ( R k k fv k p g k k ). Let e be a minimal event in W k and a = k (e). Suppose, for every e 0 2 R k with e e 0 , it is the case that k (e 0 ) I p for any 2 p \ ( S k+1 i `;i ), where p = loc(e 0 ). Let ^ = (n k ; k f ag c W n 0 k ), where c W is as follows:

Let b R = R k ; f eg. If b R is nonempty, then c
W is the restriction of W to b R otherwise c W = ?. Let ŝ = 1 : : : k;1 ^ k+1 : : :

`.

Then we h a ve s a =) ŝ. (Note that ŝ is guaranteed to be in S.)

We h a ve n o w completed the construction of A H . It remains to prove the following lemma to complete the proof of theorem 1:

Lemma 2 Let 2 ? . Then is accepted b y A H i is in Lin(H).

Proof: Let = a 1 a 2 : : : a k . Suppose is in Lin(H). Let = n 0 B1 ;! : : : B ; ! n `be an accepting path in H such that is a linearization of ( ). Hence we may suppose that ( ) = (E fv p g

) where E = fe 1 e 2 : : : e k g and (e i ) = a i for i = 1 : : : k . And e i e j implies i j for any i j in f1 : : : k g. Consider the con gurations C i = fe 1 e 2 : : : e i g for i = 1 : : : k . For each C i , w e can associate a state s i in A H as follows.

Consider a xed 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 0 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 betheC i -residue of % j . If R j is nonempty, W j is the causal MSC (R j j fv j p g j j ) where j is the restriction of to R j v j p is the restriction of v p to those events in R j that belong to process p, for each p a n d j the restriction of to R j . If R j is empty, t h e n s e t W j = ?. Finally, n 0 j is the ending node of % j . Now it is routine (though tedious) to verify that " a1 =) 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.

We have t h e n shown that tightness allows the construction of an automaton A H that recognizes all linearizations of H.

As for complexity, it is easy to see that the number of states of A H is at most jNj 2 2 j j 2 jNj j j 2 jBj m jNj j j 2 jBj , w h e r e m = maxfjBj j B 2 B g .

Inclusion and Intersection of Causal HMSCs

As already mentioned, due to the embedding of Mazurkiewicz traces into Message Sequence Charts, we can not decide whether the intersection of two MSC languages generated by HMSCs is empty or not, or if a MSC language is included in an other one. Fortunately, for a subclass of HMSCS called globally-cooperative HMSCs, and which captures in particular bounded HMSCs, this problem becomes decidable 9]. This section shows that a similar class exists for Causal HMSCs. This class of globally cooperative causal HMSCs heavily depends on how causal MSCs generated by the order automaton can be decomposed into elementary parts. Such decomposition into atomic MSCs was proposed for MSCs in 1, 1 3 ]. As for MSC, we c a n i n troduce a notion of decomposition into basic parts for causal MSCs. Basic parts are units of composition, they will be useful to nd a canonical representation of any causal MSC.

For a Causal MSC B a decomposition is a sequence o f b asic parts B 1 :B 2 : : : B k such that B = B 1 B 2 : : : B k .

Slightly extending the independence relation I p de ned in section 2, we will say that two sets A and B are independent, denoted by A I p B if for all a i in A and b i in B, INRIA a i I p b i . Similarly, we will say that two basic parts B 1 and B 2 are independent, denoted by B 1 k B 2 , if their labels are instance-wise mutually independent, i.e. for all process p in P, Alph p (B 1 )I p Alph p (B 2 ). Note that whenever B 1 k B 2 , w e h a ve B 1 B 2 = B 2 B 1 . This property allows us to de ne an associated trace e quivalence as the least congruence over B ?

Basic , where B Basic is a given collection of basic parts, such that 8a b 2 B Basic , a k b =) ab ba. Thus, we can consider trace u] over basic parts as the equivalence class of any w ord of basic parts u 2 B ? Basic .

Moreover, given a causal HMSC H, we will denote by B Basic (H) the nite set of basic parts occurring in the decomposition of all causal MSCs which label transitions of H. We a l s o de ne H Basic as a new causal HMSC in which w e replace each transition (n src B n dst ) by nodes and transitions (n src B 1 n 1 ) : : : (n k;1 B k n dst ) where B 1 : : : B k is a decomposition of B, a n d (n i ) i2f1::kg are fresh states. L(H Basic ) B ?

Basic(H) is the language over B Basic (H) generated by H Basic , i . e . a w ord w = B 1 :B 2 : : : : B k belongs to L(H Basic ) if and only if there exists an accepting path = n 0 B1

;! n 1 : : : B k ;! n k in H Basic . Finally, we will denote by BP(H) = fB 1 : : : B k 2 B ?

Basic(H) j B 1 : : : B k 2 cMSC (H)g the language of basic parts generated by H. We c a n n o w consider the trace language generated by a causal HMSC H. We will identify a subclass of causal HMSCs, called globally-cooperative causal HMSCs, for which e a c h o f i t s memberH corresponds to a connected rational trace language over the basic part alphabet

B Basic (H).

A brute force solution to nd a decomposition of a causal MSC B = ( E f p g p2P ) is to check for all possible partitions of E, whether the reconstruction of the decomposition is exactly B. The following proposition shows that decomposition construction can be brought back to the detection of strongly connected components in a directed graph de ned over events of E. This construction is analogous to the technique in 13], and can be performed in O(jEj 2 ).

Proposition 2 Let us note p the cover relation of v p , i.e. e p e 0 i e v p e 0 and no e i is such that e v p e i v p e 0 . These two problems are e quivalent:

1. B = ( E v p ) can be d e composed into B 1 : : : B k , w h e r e B i = ( E i i v i p i ) is a basic part.

2. The graph G B = ( E R ) has fE Bi g i2 1::k] as strongly connected c omponents and 8i < j E Bj E Bi \ R = . A p air of events (e e 0 ) 2 E belongs to R if and only if: they are l o cally related i n B, i.e. 9p 2 P j e p e 0 , or they are r eception and emission of the same message, i.e. e e 0 or, e 0 e or they are not compatible with local independency relation, i.e. 9p 2 P j e 0 p e and (e)I p (e 0 ), or they are not compatible with local dependency relation, i.e. 9p 2 P j e 0 6 v p e, e 6 v p e 0 , a n d (e)D p (e 0 ).

Proof: Let us note R ;1 = f(e e 0 ) j (e 0 e ) 2 Rg, R Ip = f(e 0 e ) 2 E E j e p e 0 ^ (e)I p (e 0 )g and R Dp = f(e e 0 ) 2 E E j e 6 v p e 0 ^e0 6 v p e ^ (e)D p (e 0 )g. Thus, we c a n rewrite R as R = ;1 ( p R Ip R Dp ) p2P .

First, let us take t wo causal MSCs X 1 = ( E 1 1 v 1 p 1 ) and X 2 = ( E 2 2 v 2 p 2 ) and consider the causal MSC X = X 1 X 2 . We can remark that we h a ve R Ip \ (E 2 E 1 ) = and R Dp \ (E 2 E 1 ) = . Thus, R \ (E 2 E 1 ) = , and consequently E X is not a strongly connected component.

Second, let us prove t h a t if E X is not a strongly connected component of G B then X is not a basic part of B. If E X is not strongly connected component, that means that we can decompose it into n strongly components E 1 : : : E n , w i t h n > 1. We can then extend R to these subsets (E i E j ) 2 R if 9e i 2 E i e j 2 E j such that (e i e j ) 2 R. We can be more precise: (E i E j ) 2 R i 9e i 2 E i e j 2 E j such that (e i e j ) 2 RnR ;1 . Indeed, if (e i e j ) is in R ;1 then E i is strongly connected to E j which is not the case as they are distinct sets. Moreover, as and R Dp are re exive, and R Ip \ (R Dp R ;1 Dp ) = , R Ip \ (

;1 ) = , p \(R Dp R ;1 Dp ) = and R Ip ;1 p , w e h a ve RnR ;1 = p2P ( p nR ;1 Ip ) = f(e e 0 ) j 9 p 2 P e p e 0 ^ (e)D p (e 0 )g. Thus, (E i E j ) 2 R i for all e i 2 E i , e j 2 E j , e i p e j ) (e i )D p (e j ). Finally, we deduce from the later the following result : R \ ( p2P p ) \ (E i E j ) = f(e i e j ) 2 E i E j j (e i )D p (e j )g, which means that X Ei X Ej = X Ei Ej (X E is the causal MSC resulting of the projection of causal MSC X to events of E). To conclude the proof, we have t o consider a linearization E i1 : : : E in of the n strongly components, and then the composition X Ei 1 X Ei 2 ::: Ei n which is equals to X, which mean that X is not a basic part.

This proposition gives us an algorithm to compute a possible decomposition of a causal MSC B: we rst compute the strongly connected components B 1 : : : B k of the graph de ned above, and then nd a linearization B i1 : : : : B ik , that is chosen according to the respective dependencies among basic parts in B. We n o w p r o ve that all decomposition of the initial causal MSC are equivalent u p -t o p e r m utations allowed by jj. Proposition 3 Let B be a c ausal MSC, and B 1 : : : : : B k be a p ossible decomposition of B.

Then any other decomposition of B belongs to B 1 : : : B k ].

Proof: Let us suppose that there exists a wo r d o f b a s i c p a r t s W = w 1 :w 2 : : : w q such that B = w 1 w 2 : : : w q but W 6 2 B 1 : : : B k ]. We know that fB1 : : : B k g is the nest partition w.r.t. relation R de ned in proposition 2. That is, fw 1 w q g = fB1 : : : B k g. Hence, we c a n nd a mapping f : fw 1 w q g ; ! f B1 : : : B k g that associates an isomorphic basic part of fB1 : : : B k g to each w i . Furthermore, two isomorphic basic parts are necessarily ordered. If W 6 2 B 1 : : : B k ], then there are two basic parts of W, w i w j such that w i precedes w j in W, and for any mapping f, f(w j ) precedes f(w i ) in B 1 : : : B k and f(w j ) and f(w i ) do not commute in B 1 : : : B k . This can only happen if there exists two e v ents e 2 f(w j ) and e 0 2 f(w i ) such that loc(e) = loc(e 0 ) and e e 0 in B. Hence, we can not have w i jjw j nor w i w j in W. Contradiction.

INRIA

We are now ready to prove the main result of this section. The following theorem shows that a causal HMSC de nes a rational (Mazurkiewicz) trace language over basic parts.

Theorem 2 Let H be a c ausal HMSC, and let L] be the closure o f w o r ds of L B ? Proof: First, let us take a w ord w in L(H Basic ]. Thus w = B 1 : : : B k B i1 : : : B i k such that B i1 : : : B i k 2 L (H Basic ). As L(H Basic ) BP(H) and B 1 : : : B k = B i1 : : : B i k we conclude that L(H Basic )] BP(H).

Second, let us take a w ord w in BP(H). Let us note B w its corresponding causal MSC, i.e. for w = P 1 : : : P k , B w = P 1 : : : P k . Then this word is generated by an accepting path = n 0 B1

;! n 1 : : : B l ;! n l of H such that w = B 1 : : : B l and B i can be decomposed into P ji : : : P ji+1;1 , for i in f1 : : : l ; 1g and B l can be decomposed into P j l : : : P k , where 1 = j 1 < : : : j l < k . By proposition 3, we k n o w t h a t a n y other decomposition of B i belongs to P ji : : : P ji+1;1 ], and in particular, the one we c h o o s e t o b u i l d H Basic . As u] v] = uv],

we can conclude to obtain BP(H) L(H Basic )].

We h a ve s h o wn in section 3 that the class of bounded HMSCs had an equivalent c l a s s with similar properties in Causal HMSCs. We now introduce a useful subclass of causal HMSCs, called globally cooperative causal HMSCs, that is the causal HMSC pendant o f t h e class of globally cooperative HMSCs. De nition 7 A c ausal MSC B is connected if the alphabet of its basic parts (fB 1 : : : B k g, is a connected alphabet (w.r.t. the independence relation k). A causal HMSC is globallycooperative, if for each cycle = n B1 ;! n 1 B2

;! : : : B k ;! n , the causal MSC ( ) is connected.

Corollary 1 Let H and H 0 be two causal HMSC. If H 0 is globally-cooperative, then we can build an automaton A 0 such that L(A 0 ) = L(H 0 Basic )] with jA 0 j = O(2 jH 0 jjBBasic(H 0 )j ).

Thus:

H H 0 is PSPACE-complete.
H \ H 0 = is EXPSPACE-complete. Proof: Using Theorem 2 we k n o w that we can embed basic parts automata into rational traces. Moreover, the basic parts automaton H Basic obtained from a globally-cooperative causal HMSC H is still globally cooperative. Thus, globally-cooperative causal HMSCs can beembedded into connected rational traces.

Then, using 7] or 19], we k n o w that inclusion and intersection are decidable with the associated complexity results of 19].

Finally, for any languages L and L 0 , testing whether L] L 0 ] is equivalent t o t e s t i n g if L L 0 ]. Thus, only H 0 has to be globally-cooperative. The same result holds for intersection, as L] \ L 0 ] = if and only if L \ L 0 ] = .

This corollary can be used to perform model-checking of causal HMSCs against a globallycooperative causal HMSC speci cation. Hence, as we cannot use complementation for causal HMSC languages, we will consider two di erent kinds of model-checking: positive modelchecking, i.e. 'Does the model H have the properties S ?' which corresponds to testing whether cMSC (H) cMSC(S) or not, and negative m o d e l -c hecking, i.e. 'Does the model H perform some bad behaviors S ?', which corresponds to test wether cMSC(H)\cMSC (S) 6 = or not.

Bounded-window Causal HMSCs

Recall that the main objective of causal MSCs is to allow the de nition of behaviors containing braids of arbitrary size such as those generated by sliding windows protocols. Clearly, Causal HMSCs are more powerful than HMSCs: they allow for the de nition of behaviors that contain those braids (see for instance the examples of Figures 2 and6), while HMSCs do not. 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 series of questions (messages from p to q) and answers (messages from q to p). Implementing a sliding window means that a process may send several questions in advance without need to wait for an answer to each question before INRIA sending the next one. Very often, these mechanisms tolerate losses, i.e. the information sent is stored locally, and can be retransmitted if needed.

Of course, to avoid memory leaks, the number of messages that can be sent i n a d v ance is bounded by s o m e i n teger k, that is called the size of the sliding window. Note however that the causal HMSC of Figure 6 also de nes visual extensions that have the form of the behavior represented in Figure 9. In these executions, a message of type n may cross an unbounded number of occurrences of a message of type m. A question that naturally arises is to know if in all the executions of protocol designed with causal HMSCs, the number of messages crossings is naturally bounded by some constant. In the sequel, we c haracterize these crossings, and show that their boundedness is a decidable problem.

De nition 8 Let B = ( E fv p g

) be a visual extension of a causal MSC, i.e. B is a MSC. A message occurrence m is a couple (e m f m ) such that (e m ) = p!q(m), (f m ) = q?p(m) and e m f m . The crossing window, or simply window, of the message occurrence m is the set W M ( m) = f(e 0 f 0 ) 2 j loc(e 0 ) = q ^loc(f 0 ) = p ^e f 0 ^e0 fg.

The MSC B on the example of gure 10 illustrates the de nition of crossing windows.

Each message appears exactly once, so for simplicity w e will denote message occurrences by m n o p t u and v. The elements that will appear in the window of message p = ( e f) are message occurrences from P to Q which emissions are located in the set of predecessors of f, and which receptions are located in the set of successors of e. Thus, we h a ve W B (p) = fn og. Moreover, W B (u) = fvg. In the example of Figure 10 windows are symbolized by areas delimited by dotted lines. Now, the question that arises is whether the window o f a n y message occurrence is bounded, for any MSC generated by a causal HMSC H.

De nition 9 Let H = (N N in B N ;!) be a causal HMSC. H is window bounded if and only if there exists an integer n such that 8M = ( E fv p g p2P ) 2 Vis(H) 8 m 2 we have jW M ( m)j n.

In the sequel, we show t h a t knowing whether a causal HMSC is window bounded is a decidable problem. It can be solved by construction of an automaton that recalls events labels that must appear in the future of messages (respectively in the past) in any visual extension of C M S C (H). Let B = ( E fv p g ) be a causal MSC, and let m = ( e f) be a given message occurrence. We can de ne the two following sets: Future B ( m) = fa 2 j 9 x 2 E f x ^ (x) = ag Past B ( m) = fa 2 j 9 x 2 E x e ^ (x) = ag Clearly, messages which emission appears in Future B ( m) or which reception appears in Past B ( m) do not belong to the window of m. On the example of Figure 10, we have for example Future B (n) = fQ?P(n Let m = (e f) be an occurrence of message m. Then Future B ( m) = fQ?P(m)g, and Future B B 0 ( m) = fQ?P(m) Q!R(o) R?Q(o)g. For a given message occurrence m = ( e f) from a process p to a process q and a given MSC B, i f q!p(m 0 ) appears in Future B (m), then for any B 0 , all occurrences of message m 0 in M 0 do not belong to W B B 0 ( m). A similar property holds for labels that belong to the past of message occurrence m. More intuitively, a state q = (n X) in A m represents a possible set X f labels in Future ( ) ( m) for some path that ends at node n in H, and contains an occurrence of message m. Slightly abusing the notation, we will denote by Future(q) the set X.

) Q?P(o) Q!R(v) R?Q(v) Q?R(t) Q?R(u)g P Q R m n o p Wp t u v Wu
The second rule in the transition relation (resp. 0 ) is important, as it allows to chose nondeterministically an occurrence m of a message, and to start memorizing the labels appearing in its future (resp. in its past). Note that in any strongly connected subset C = fq 1 : : : q k g of A m (respectively A 0 m ), Future(q 1 ) = Future(q 2 ) = = Future(q k ) (resp. Past(q 1 ) = Past(q 2 ) = = Past(q k )). Hence, we will denote by Future(C) (resp. Past(C)) the set of observed labels on any state of C. To complete the proof, we need the following lemma.

Lemma 3 Let H be a c ausal HMSC over an alphabet of causal MSCs B. Let m be a message from process p to process q in a causal MSC B 2 B , and let A m and A 0 m be the two automata as de ned a b ove. Then, W m (H) is bounded i b oth of the following holds:

C, s t r ongly connected c omponent of A m such that q!p(m 0 ) is the label of an event in a c ausal MSC labeling a transition of C but is not in Future(C), a n d C, strongly connected c omponent of A 0 m such that q?p(m 0 ) is the label of an event in a c ausal MSC labeling a transition of C and is not in Past(C).

Proof: One direction is straightforward. If any o f these strongly connected components exists (either before or after m, the chosen occurrence of m ), then there is an unbounded number of path generating an unbounded number of occurrences of q!p(m 0 ) that are not causally related to m. Hence, for each of these path, there is a visual extension where all m 0 generated by occurrences of the cycle cross m, a n d W m (H) is not bounded. Now, let us prove the other direction. Let us suppose that for all k, there exists a V V i s (H), s u c h that fW v ( m) j v 2 V g is not of k-bounded windows size for a message occurrence m contained in a causal MSC B, and let be a p a t h of H labeled by v 2 V .

Then there is necessarily a causal MSC B 0 that contains a message occurrence m 0 that can be repeated k=ntimes along and which m crosses. Then B 0 is repeated at least k=(2n) times either before or after the occurrence of B.

Let k > 2n (j j + 1 ) , then B 0 is repeated at least j j + 1 times let say after B, that is = 1 (q 1 B q 2 ) 2 , where 2 = 2 0 (q 2 0 B q 3 1) 2 1 (q 2 1 B q 3 2) : : : (q 2 j j+1 B q 3 (j j+2) 2 (j j+2) . Hence q 2 i ;! q 2 i+1 is a loop of H, that is it forms a strongly connected component. Moreover, the j j + 1 sets Future(q 1 q 2 i )( m) are strictly increasing subsets of , hence we have some i for which Future(q 1 q 2 i )( m) = Future(q 1 q 2 i+1 )( m). There will hence be a strongly connected component C of A m which corresponds to this choice of m and of q 2 i ;! q 2 i+1 . Moreover, q!p(m 0 ) 6 2 Future q1 q2 i+1 ( m).

Thus, q!p(m 0 ) is not in Future C ( m). The proof when B 0 is played often before B is symmetric.

The automaton A m has at most n 2 j j nodes, and we h a ve to analyze strongly connected components of A m . However, as noticed before, every strongly connected component o f A m T. Gazagnaire, S. Yang, L. H lou t, B. Genest, P.S. Thiagarajan enjoys the property t o h a ve a second component w h i c h 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 m such that q!p(m 0 ) is the label of an event in a causal MSC labeling a transition of C b u t t h a t i s n o t i n Future(C), then we can consider the maximal strongly connected component D of A m containing C (it exists since the union of two non disjoint strongly connected components is again a strongly connected component). Since D it is a strongly connected component, its second component Future(D) is constant, hence Future(D) = Future(C). Since C D, w e h a ve that q!p(m 0 ) is a label of an event o f D and is not in Future(C) = Future(D). Using Tarjan's algorithm 24], we can compute in quadratic time the partition of A m into maximal strongly connected components (for each s e t X 2 , w e partition the subpart of A m with a constant second component b e i n g X). Then for each maximal strongly connected component (C X), it su ces to compute (C) and to compare it with X, which is linear in n. Hence, the overall complexity of the algorithm is in O(n 2 :2 j j+1 ).

Let us consider again the example of Figure 6. The automaton A m associated to the window of message m is represented in Figure 12. One can notice that the causal HMSC of Figure 6 is kind of duplicated by A m . This is due to the fact that we can decide to start observing a window after any occurrence of message m. n 0 fp!q(m)g Figure 12: The automaton A for W m from the example of Figure 6 Corollary 2 Let H be a c ausal HMSC , and m be a message of H, then if the window size of m is bounded, it is lower than 2n(j j + 1 ) .

Case-study: the TCP protocol

We propose a case study to show the usefulness and the expressive p o wer of Causal HMSCs. The Transmission Control Protocol (TCP) is one of the core protocols of Internet. Using INRIA 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 inorder 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 quote bellow some fragments of RFC793 23], the reference document about TCP protocol, to explain what a TCP scenario is. For reasons of simplicity and readability, w e abstracted some technical issues in our model. A classical TCP scenario is divided into 3 parts:

The rst 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 6 ]. 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 13. In this example, we use the standard notation 15]. The initial node of our automaton is depicted by a p o i n t-down triangle, and the end node by a p o i n t-up triangle. The labeling of the automaton's transitions by M S C s s h a l l be clear from the drawings. In the example of Figure 13, the MSC on the left describes the case when process 1 initiates a connection, and the MSC on the right 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 p a c kaging some number of bytes into segments for transmission through the internet system. TCP uses sequence numbering in order to recover from data that is 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 a c knowledgment ( ack) f r o m 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 14 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 i n packet, which the other end acknowledges with an ack. Therefore, a typical tear-down requires a pair of f i n and ack segments from each tcp endpoint. The four-way handshake is modeled on gure 15 : an end event i s s e e n on process p when no more tcp packet are sent f r o m p. In the the MSC at the left of the gure, process 1 stops rst, and process 2 can continue to send tcp packets, then process 2 stops. In the middle of the gure, process 1 INRIA and process 2 stops in the same time. In the MSC at the right of the gure, process 2 stops rst, then process 1. 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 i n simultaneously. In this case, both sides just have t o s e n d ack packets to terminate the TCP connection. This can be considered as a 2-way handshake since the fin=ack sequence is done in parallel in both directions. Automata of Figure 13, Figure 14 and Figure 15 model the 3 phases of TCP protocol. Data exchange from process 2 to process 1 can be easily obtained from the MSC of Figure 14 by exchanging the roles of process 1 and process 2 in the model. 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. To facilitate the understanding, we w i l l o n l y s h o w a simpli ed view of the complete protocol in Figure 16. In this model, we only consider lossless connections and forget the simultaneous disconnections.

So far, we h a ve proposed scenario descriptions of the TCP protocol, and provided the HMSCs describing the typical executions of TCP, b u t we did not de ne the commutation relation over events of the protocol that allows for the interleaving of di erent phases of the protocol. Let us de ne the local dependency relations D p for process p in f1 2g. If we Figure 16: A automaton which models TCP protocol with lossless channels and without bounds of sliding window size.

INRIA chose the normal weak concatenation, as de ned in HMSCs, i.e. D p = p p , w e o b t a i n a synchronized execution of data transfer phase: every process send only one tcp packet and waits for the corresponding ack packet. Left part of gure 17 describes this kind of execution. This visual order is generated by the Causal HMSC on gure 16 with D p = p p , 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 su ce 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 = fp!q(tcp) p ?q(ack) p ?q(tcp) p !q(ack) p ?q(f i n )g 2 =f(a a) 2 g. An execution of such a causal HMSC is shown on the right part of gure 17. Note that the causal HMSC model of TCP is not tight, and that the language of its linearizations of the protocol is not regular. This model is no more window bounded, as an in nite numberofack messages can cross tcp ones.

Conclusion

We h a ve de ned an extension of HMSC called Causal HMSC that allows the de nition of braids, such as those appearing in so-called sliding windows protocols. This new scenario language does not embed the expressive p o wer of communicating automata. Hence several problems remain decidable, and many classes of scenarios that were de ned for HMSCs nd their equivalent in Causal HMSCs. Moreover, these new classes are incomparable with their correspondent classes in Compositional HMSC models, mainly because CMSCs assume a FIFO semantics -to the contrary of our approach t h a t makes no speci c assumptions on message delivery policy.

Furthermore, Causal HMSCs raise several interesting issues. For example, deciding whether a set of visual extensions is nitely generated is still an open problem. Another interesting issue is to consider the class of causal HMSCs that have bounded crossing windows for all their messages. The set of behaviors generated by this kind of causal HM-SCs seem to exhibit some kind of regularity that could be exploited using graph grammars techniques.

  languages have b e e n i n tegrated into UML 21], and have b e c o m e de facto a standard notation.

Figure 2 :

 2 Figure 2: An in nite braid

Figure 3 :

 3 Figure 3: An example of causal MSC M 1 . Events are not totally ordered on each processes.

Figure 4 :Figure 5 :

 45 Figure 4: An example of causal MSC B: the set of visual extensions of B is not the instance per instance commutative c l o s u r e o f a n y visual extension of B.

  irre exive relation. We denote the dependence relation ( p p ) ; I p by D p . For convenience, we a l s o d e n e I

Figure 7 :

 7 Figure 7: Comparing CMSCs and Causal HMSCs

Figure 8 :

 8 Figure 8: Events in C-subpaths are indicated by small lled circles. Events in C-residues are indicated by small blank circles.

  ; k+1 c W n 0 k+1 ), where c 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 0 k . Let ^ = ( n k ; k ; c W n 0 ), where c W = W k W. Let ŝ = 1 : : : k;1 ^ k+1 : : : `. If ŝ is in S, t h e n s a =) ŝ. ( glue two segments ) Suppose n = n 0 k and n 0 = n k+1 . Let ^ = (n k ; k ; ; k+1 c W n 0 k+1 ), where c W = W k W W k+1 . Let ŝ = 1 : : : k;1 ^ k+2 : : : `. If ŝ is in S, then s a =) ŝ.

De nition 6 A

 6 causal MSC B is a basic part (w.r.t. a dependency relation D) if it can not be d e composed into two (non-empty) causal MSCs B 1 and B 2 such that B = B 1 B 2 .

  Basic(H) by the independence r elation k. Then BP(H) = L(H Basic )].

Figure 9 :

 9 Figure 9: An unbounded window generated by protocol of Figure 6

Figure 10 :

 10 Figure 10: a M S C B and two w i n d o ws: W p and W u denote the set of messages that cross p and u.

Figure 11 :

 11 Figure 11: Construction of Future B B 0 ( m)

Figure 13 :

 13 Figure 13: Connection establishment b e t ween process 1 and process 2.

  proposes two w ays to model this data transfer phase with MSCs. The MSC on the left of the Figure models lossless channels.The MSC in the right of the gure models a two state protocol which is able to handle packets losses during the data exchange: in the rst state we execute the normal behavior, and when a loss occurs the protocol passes in a second state where tcp packets that were not acknowledged are resent u n til the corresponding ack is received. The left part of the gure corresponds to lossless channels.

Figure 14 :

 14 Figure 14: 2 di erent w ays to model data transfer between process 1 and process 2.

Figure 15 :

 15 Figure 15: The TCP connection termination.

Figure 17 :

 17 Figure 17: Two executions of the TCP example, with the HMSC semantics (on the left) and with the Causal HMSC semantics (on the right) INRIA

RR n 6301

http://www.inria.fr ISSN 0249-6399

of messages appearing in the window of a message occurrence m in a visual extension of H. We will say that W m (H) is bounded if and only if there exists some k 2 N such that 8B 2 V i s (H) 8 m message occurrence o f B, jW B j k. Theorem 3 Let H be a c ausal HMSC of size n, and let m be a message of H. The boundedness of W m (H) is decidable in time O(n 2 :2 j j+1 ).

Proof:

For a given causal HMSC H = (N N in B N ;!) and a message m, we build the following automaton:

;! n 0 and m belongs to B. ; (n X) B (n 0 X 0 ) 2 , where B = ( E fv p g ), i f n B ;! n 0 , a n d X 6 = , and X 0 = X fa 0 2 j 9 x y 2 E 9a 2 Future B ( m) (y) = a 0 ^x y^a D (x)g.

We also build an automaton that computes Past( m), b y a b a c kward search in the causal HMSC H. More precisely,

;! n and m belongs to B. ; n X) B (n 0 X 0 ) 2 , where B = ( E fv p g ), i f n 0 B ;! n, a n d X 6 = , and X 0 = X f a 0 2 j 9 x y 2 E 9a 2 Past B ( m) (y) = a 0 ^y x ^a D (x)g INRIA