We read with great interest the article by Heff ernan and colleagues reporting an association between persistent lymphopaenia and increasin g mortality in trauma patients [1]. We would like to provide some additional data obtained in a similar cohort of patients.

In parallel with a study recently published in Critical Care in which mHLA-DR expression was assessed [2], we evaluated the CD4 + lymphocyte count and the percentage of CD4 + CD25 + regulatory T cells in trauma patients. Sixty-fi ve patients were included (mean ± standard deviation): age 41 ± 18 years, Simplifi ed Acute Physiology Score II 45 ± 16, and Injury Severity Score 38 ± 10. Of these patients, 21 developed sepsis (mainly pneumoniamedian delay 4 days) and two died of septic shock. Importantly, 3 days after trauma the patients presented with signifi cant CD4 + lymphocyte alterations: a signifi cantly decreased CD4 + T-cell count and an increased regulatory T-cell percen tage (versus control values, P <0.0001; Table 1). Interestingly, we ob served a trend toward lower CD4 + T-cell values in patients presenting with secondary infections versus non-infected individuals (343 cells/μl vs. 454 cells/μl, respectively).

Our results reinforce the observations made by Heff ernan and colleagues [1]. We confi rm here that trauma patients exhibit CD4 + T-cell loss with a relative increase in regulatory T-cell values -both parameters associated with unfavourable outcomes after septic shock [3]. Collectively, these data suggest that, in addition to monocyte anergy [2], lymphocyte alterations should be taken into account in the monitoring of trauma patients.

Lymphocyte subset counts and phen otyping deserve to be investigated in large cohorts of trauma patients to minutely delineate association with specifi c clinical outcomes. Regulatory T cells (% of CD4 + lymphocytes) 9.1 ± 2.5 9.6 ± 2.9 8.9 ± 2.3 6.5 ± 1.5 mHLA-DR (antibodies/cell) 8,897 ± 5,762 6,834 ± 4,268 9,927 ± 6,169 >15,000 a

  References1. Heff ernan DS, Monaghan SF, Thakkar RK, Machan JT, Cioffi WG, Ayala A:

	L E T T E R
	CD4 + T-lymphocyte alterations in trauma patients
	Aurélie Gouel-Chéron 1,2 , Fabienne Venet 2,3 , Bernard Allaouchiche 1,2 and Guillaume Monneret* 2,3
	See related research by Heff ernan et al., http://ccforum.com/content/16/1/R12
	Failure to normalize lymphopenia following trauma is associated with
	increased mortality, independent of the leukocytosis pattern. Crit Care
	2012, 16:R12.
	2. Cheron A, Floccard B, Allaouchiche B, Guignant C, Poitevin F, Malcus C,
	Crozon J, Faure A, Guillaume C, Marcotte G, Vulliez A, Monneuse O, Monneret
	G: Lack of recovery in monocyte human leukocyte antigen-DR expression
	is independently associated with the development of sepsis after major
	trauma. Crit Care 2010, 14:R208.
	3. Venet F, Chung CS, Kherouf H, Geeraert A, Malcus C, Poitevin F, Bohé J,
	Lepape A, Ayala A, Monneret G: Increased circulating regulatory T cells
	(CD4 + CD25 + CD127 -) contribute to lymphocyte anergy in septic shock
	patients. Intensive Care Med 2009, 35:678-686.
	4. Docke WD, Hofl ich C, Davis KA, Rottgers K, Meisel C, Kiefer P, Weber SU,
	Hedwig-Geissing M, Kreuzfelder E, Tschentscher P, Nebe T, Engel A, Monneret
	G, Spittler A, Schmolke K, Reinke P, Volk HD, Kunz D: Monitoring temporary
	immunodepression by fl ow cytometric measurement of monocytic HLA-
	DR expression: a multicenter standardized study. Clin Chem 2005,
	51:2341-2347.
	© 2010 BioMed Central Ltd

*Correspondence: guillaume.monneret@chu-lyon.fr 3 Hospices Civils de Lyon, Hôpital Edouard Herriot, Laboratoire d'Immunologie, Place d' Arsonval, 69437 Lyon, France Full list of author information is available at the end of the article doi:10.1186/cc11376 Cite this article as: Gouel-Chéron A, et al.: CD4 + T-lymphocyte alterations in trauma patients. Critical Care 2012, 16:432.

Table 1 . Trauma patients' immunological characteristics

 1

		Overall population	Septic	Nonseptic	Healthy volunteers
	Parameter	(n = 65)	(n = 21)	(n = 44)	(n = 50)
	CD4 + lymphocytes (cells/μl)	463 ± 274	377 ± 157	500 ± 319	881 ± 261

Abbreviations

mHLA-DR, monocytic Human Leukocyte Antigen DR.

Competing interests

The authors declare that they have no competing interests.


Erwan Mahe

Christophe Gaston

Pascale Le Gall

Equivalence of Denotational and Operational Semantics for Interaction Languages

Keywords: interactions, sequence diagrams, distributed & concurrent systems, formal language, denotational semantics, operational semantics

Message Sequence Charts (MSC) and Sequence Diagrams (SD) are graphical models representing the behaviours of distributed and concurrent systems via the scheduling of discrete emission and reception events. So as to exploit them in formal methods, a mathematical semantics is required. In the literature, different kinds of semantics are proposed: denotational semantics, well suited to reason about algebraic properties and operational semantics, well suited to establish verification algorithms. We define an algebraic language to specify so-called interactions, similar to the MSC and SD models. It is equipped with a denotational semantics associating sets of traces (sequences of observed events) to interactions. We then define a structural operational semantics in the style of process algebras and prove the equivalence of the two semantics.

Introduction

Modelling asynchronous communications between concurrent processes is possible under a variety of formalisms, such as process algebras [START_REF] Rensink | Weak sequential composition in process algebras[END_REF], Petri Nets [START_REF] Haddad | Dynamic recursive petri nets[END_REF], series-parallel languages [START_REF] Lodaya | Series-parallel languages and the boundedwidth property[END_REF], distributed automata [START_REF] Akshay | Distributed timed automata with independently evolving clocks[END_REF], or formalisms derived from Message Sequence Charts (MSC) [START_REF] Mauw | Operational semantics for msc'96[END_REF]. MSCs are graphical models representing information exchanges between sub-systems. Various offshoots of MSCs, including UML Sequence Diagrams (UML-SD) [START_REF]OMG: Unified Modeling Language v2[END_REF], have been proposed and we call languages from that family "Interaction Languages" (IL). Interactions are interesting due to their graphical nature and ease of understanding. IL make it possible to describe scenarios using intuitions that are very easy to share: a) a vertical line per sub-system, called a lifeline, which from top to bottom describes the succession of events as perceived by the sub-system, b) exchanges of messages inducing causality relations between the lifelines, c) high-level operators such as parallel composition to structure simple scenarios.

So as to use interactions in formal methods, they have to be fitted with formal semantics. A major hurdle in defining those lies in the treatment of weak sequencing. Weak sequencing allows events taking place on different lifelines to occur in any order while strictly ordering those that take place on the same lifeline. The survey [START_REF] Micskei | The many meanings of uml 2 sequence diagrams: a survey[END_REF] provides an overview of solutions found in the literature.

The most direct ones consist in defining semantics by translation: interactions are translated into models of other formalisms provided with formal semantics. Typical examples are Petri Nets [START_REF] Eichner | Compositional semantics for uml 2.0 sequence diagrams using petri nets[END_REF], automata [START_REF] Knapp | Model checking of uml 2.0 interactions[END_REF] or process algebra [START_REF] Jacobs | On a process algebraic representation of sequence diagrams[END_REF]. The main advantage of such approaches is that those formalisms are equipped with tools such as Model-Checker or Model-Based Testing tools. However, a notable drawback is that the target formalisms are defined on concepts (states, transitions, places...) that are quite different from the ones handled in ILs. Then it is difficult to know whether or not the objects resulting from the translation preserve the meaning associated to the original interaction. For example, in [START_REF] Jacobs | On a process algebraic representation of sequence diagrams[END_REF], the authors propose to translate UML-SD into Communicating Sequential Processes (CSP) [START_REF] Hoare | Communicating Sequential Processes[END_REF]. UML-SD operators such as weak sequencing are encoded in a non-trivial manner, using sequence, parallel composition etc. as CSP does not introduce any similar operator, and as the translation is not presented exhaustively, it is not clear if the asynchronous nature of executions of UML-SD is fully reflected. Other approaches treat IL by equipping them with direct mathematical semantics, either denotational or operational. Denotational semantics either rely on partial order sets [START_REF] Störrle | Semantics of interactions in uml 2.0[END_REF][START_REF] Mahe | Revisiting semantics of interactions for trace validity analysis[END_REF] or on algebraic operators [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF]. Operational semantics [START_REF] Mauw | Operational semantics for msc'96[END_REF] are given in the form of production rules similar to process algebra. Denotational semantics, based on sets of accepted execution traces, are close to intuition. They are well adapted to reason on and prove various properties about interactions. Operational semantics are closer to executable semantics and are well suited to prove the correctness of algorithms realizing formal analysis.

In this paper we set the basis of a framework to deal with interactions via two kinds of semantics (denotational and operational). While in [START_REF] Mahe | Revisiting semantics of interactions for trace validity analysis[END_REF][START_REF] Mahe | A smallstep approach to multi-trace checking against interactions[END_REF] we formulated semantics for interactions by identifying the positions of communication actions using the Dewey notation, we now abstract away positions, to define a denotational semantics in an algebraic style as in [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF] and an operational semantics in the style of Plotkin. Those new formulations enables us to prove the equivalence of the semantics (with an automated Coq proof available in [START_REF] Mahe | Coq proof for the equivalence of the semantics[END_REF]). To our knowledge, there are no similar equivalence results in the literature. In particular, in [START_REF] Mahe | Revisiting semantics of interactions for trace validity analysis[END_REF], there were only some tooled experiments hinting towards their equivalence. Our IL extends the one in [START_REF] Mahe | Revisiting semantics of interactions for trace validity analysis[END_REF] with additional loop mechanisms. Our denotational semantics can be seen as an extension of the one in [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF] with repetition operators in the form of variants of the algebraic Kleene closure. We define a structural operational semantics in the fashion of process algebras [START_REF] Baeten | Process algebra with explicit termination[END_REF]. It adopts some of the ideas introduced in [START_REF] Mauw | Operational semantics for msc'96[END_REF][START_REF] Reniers | Message sequence chart : syntax and semantics[END_REF] but is closer to usual structural operational semantics than the one in [START_REF] Mauw | Operational semantics for msc'96[END_REF][START_REF] Reniers | Message sequence chart : syntax and semantics[END_REF] which includes maps between sent and received messages or negative application rule conditions. This paper is organized as follows: Section 2 introduces the concepts of interactions and traces. Section 3 presents the syntax of our IL and defines a trace semantics in denotational-style. In Section 4 a structural operational semantics is defined in the style of process calculi and we demonstrate its equivalence to the former in Section 5. Finally, in Sections 6 and 7 we discuss some related works and we conclude. A formalisation using Coq of the main demonstrations is available in [START_REF] Mahe | Coq proof for the equivalence of the semantics[END_REF].

Basic interactions & intuition of their meaning

Interactions describe the behavior of distributed and concurrent systems based on their internal and external communications. They are defined over a signature Ω = (L, M ) where L is a set of lifelines and M is a set of messages.

Preliminaries

The executions of systems are characterized by sequences of events called communication actions (actions for short) which are of two kinds: either the emission of a message m ∈ M from a lifeline l ∈ L, denoted by l!m, or the reception of m ∈ M by l ∈ L, denoted by l?m. A Ω denotes the set of actions over Ω. For any such action a, θ(a) denotes the lifeline on which a occurs.

Sequences of actions, called traces, are words in A * Ω , with "." denoting the concatenation operation and being the empty trace. We denote by T Ω = A * Ω the set of traces. Thus, for any two traces t 1 and t 2 , t 1 .t 2 is the trace composed of the sequence of actions of t 1 followed by the sequence of actions of t 2 . We introduce operators to compose (sets of) traces, modeling different notions of scheduling: the strict sequencing (;), the interleaving (||) and the weak sequencing ( × × ).

The set t 1 ; t 2 of strict sequencing of traces t 1 and t 2 is defined as {t 1 .t 2 }. By choosing ";" for denoting the extension of "." to sets of traces, we adopt the same notation as in [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF] for the strict sequencing operator.

Interleaving allows elements of distinct traces to be reordered w.r.t. one another while preserving the order that is specific to each trace. The set t 1 ||t 2 of interleavings of traces t 1 and t 2 is defined by:

||t 2 = {t 2 } t 1 || = {t 1 } (a 1 .t 1 )||(a 2 .t 2 ) = {a 1 .t | t ∈ t 1 ||(a 2 .t 2 )} ∪ {a 2 .t | t ∈ (a 1 .t 1 )||t 2 }
By contrast, weak sequencing only allows such permutations when actions do not occur on the same lifeline. We define a predicate t × × l meaning that the trace t contains an action on the lifeline l (we say t has conflicts w.r.t. l):

× × l = ⊥ and (a.t) × × l = (θ(a) = l) ∨ (t × × l)
By overloading × × , the set t 1 × × t 2 of weak sequencing of t 1 and t 2 is defined by:

× × t 2 = {t 2 } t 1 × × = {t 1 } (a 1 .t 1 ) × × (a 2 .t 2 ) = {a 1 .t | t ∈ t 1 × × (a 2 .t 2 )} ∪ {a 2 .t | t ∈ (a 1 .t 1 ) × × t 2 , ¬(a 1 .t 1 × × θ(a 2 ))}
When defining t 1 × × t 2 , the order of the actions in each trace is preserved and actions in t 2 can only precede those in t 1 that do not occur on the same lifeline. This explains the two subsets constituting (a 1 .t 1 ) × × (a 2 .t 2 ): the first one contains all traces whose first action is a 1 and tail belongs to t 1 × × (a 2 .t 2 ) and the second one is empty if lifeline of a 2 occurs in a 1 .t 1 (i.e. ¬(a 1 .t 1 × × θ(a 2 ))), and contains all traces whose first action is a 2 and tail belongs to (a 1 .t 1 ) × × t 2 otherwise.

The previous binary operators (";", " × × " and "||") defined on traces are canonically extended to sets of traces as follows: with ∈ {; , × × , ||}, T 1 T 2 is the union of all the sets t 1 t 2 with t 1 ∈ T 1 and t 2 ∈ T 2 . The use of the strict sequencing (";"), weak sequencing (" × × ") and interleaving ("||") operators will be illustrated with Fig. 1 in Section 2.2.

Basic interactions

An example of interaction is given in the left of Fig. 1. Lifelines l 1 , l 2 and l 3 are drawn as vertical lines. Emission and reception actions are drawn as horizontal arrows carrying the transmitted messages m 1 , m 2 , m 3 and m 4 and which respectively exit the emitting lifeline or point towards the receiving lifeline. When a direct emission-reception causality occurs, we draw both actions as a single arrow from the emitter towards the receiver. The top to bottom direction relates to time passing. An action (arrow) drawn above another one generally occurs beforehand. This scheduling of actions corresponds to the weak sequencing operator. By contrast, strict sequencing may be used to enforce precedence relations between actions occurring on different lifelines. These two scheduling operators will be respectively denoted by the keywords seq and strict. Other keywords (alt, par, loop) will be also used for denoting other scheduling mechanisms. In Fig. 1, the arrow carrying m 1 and specifying its passing between l 1 and l 3 is modelled by the interaction strict(l 1 !m 1 , l 3 ?m 1 ). Using the strict operator here obliges l 3 ?m 1 to occur after l 1 !m 1 , which reflects the causality of the passing of message m 1 between l 1 and l 3 . The fact that this arrow stands above that carrying m 2 can be modelled using the weak sequencing operator: seq(strict(l 1 !m 1 , l 3 ?m 1 ), strict(l 1 !m 2 , l 2 ?m 2 )). Using seq here instead of strict allows for instance l 2 ?m 2 to occur before l 3 ?m 1 even though the latter is drawn above. However l 1 !m 2 cannot occur before l 1 !m 1 because they both occur on l 1 . Note that, in contrast to strict, the seq operator has no graphical representation in diagrams, as it corresponds to the default scheduling operator.

Parallel and alternative compositions can also be used. On Fig. 1, the passing of m 3 and the emission of m 4 are scheduled using parallel composition. In the diagram representation this corresponds to the box labelled with "par", modelled by the term par(strict(l 1 !m 3 , l 2 ?m 3 ), l 1 !m 4 ). Actions scheduled with par can occur in any order w.r.t. one another. Here, l 1 !m 4 can occur before l 1 !m 3 , after l 2 ?m 3 or in between those two actions. Alternative composition is an exclusive non-deterministic choice between behaviors. Like par, alt is drawn as a box labelled with "alt". The global term describing the left of Fig. 1 is given by: alt(seq(strict(l1!m1, l3?m1), strict(l1!m2, l2?m2)), par(strict(l1!m3, l2?m3), l1!m4))

Repetition operators on sets of traces

Scheduling operators define compositions of traces obtained from enabling or forbidding the reordering of actions according to some scheduling policy. All three are associative (in addition, || is commutative) and admit { } as a neutral element. We define (Kleene) closures of those operators to specify repetitions3 : Definition 1 (Kleene closures). For any ∈ {; , × × , ||} and any T ∈ P(T Ω ), the Kleene closure T * of T is defined by: T * = j∈N T j with T 0 = { } and T j = T T (j-1) for j > 0. The three Kleene closures ; * , × × * and || * are respectively called, strict, weak and interleaving Kleene closures. Within the K-closure T * we can find traces obtained from the repetition (using as a scheduler) of any number of traces of T . In the example from Fig. 2 we consider a set T containing two traces

l1!m1.l2!m2, l2?m1 × × * =                , l1!m1.l2!m2, l2?m1, l1!m1.l2!m2.l1!m1.l2!m2, l1!m1.l1!m1.l2!m2.l2!m2, l1!m1.l2!m2.l2?m1, l2?m1.l2?m1, l2?m1.l1!m1.l2!m2, l1!m1.l2?m1.l2!m2, • • •               
l 1 !m 1 .l 2 !m 2 and l 2 ?m 1 . The first 3 powersets of T (i.e. T × × 0 ∪ T × × 1 ∪ T × × 2 ) are displayed, the rest of the weak K-closure of T (i.e. T × × * ) is represented by the • • • .
We have the property T T * = T * , analogous to the one defining replication !P (i.e. !P = P |!P ) in the family of process calculi (e.g. see [START_REF] Parrow | An introduction to the π-calculus[END_REF]), expressing an unbounded number of copies of P along the parallel composition "|". For ∈ {; , × × , ||} whenever a.t ∈ T 1 T 2 (with a and t any action and trace and T 1 and T 2 any sets of traces), it may be so that action a is taken from a trace a.t that belongs to either T 1 or T 2 . Definition 2 introduces restricted versions of the scheduling operators so as to impose action a to be taken from T 1 .

Definition 2 (Restricted scheduling operators). For any ∈ {; , × × , ||}, we define the operator such that for any sets of traces T 1 and T 2 we have:

T 1 T 2 = { t ∈ T 1 T 2 | (t = a.t ) ⇒ (∃ t 1 ∈ T Ω , s.t. (a.t 1 ∈ T 1 ) ∧ (t ∈ {t 1 } T 2 )) }
As an example, given T 1 = {l 1 !m.l 1 ?m} and T 2 = {l 2 !m}, we have:

T 1 × × T 2 =    l 1 !m.l 1 ?m.l 2 !m, l 1 !m.l 2 !m.l 1 ?m, l 2 !m.l 1 !m.l 1 ?m    and T 1 × × T 2 = l 1 !m.l 1 ?m.l 2 !m, l 1 !m.l 2 !m.l 1 ?m
We now define Head-First closures (abbr. HF-closure) of scheduling operators.

Definition 3 (Head-first closures). For any ∈ {; , × × , ||}, we define the Head-First closure of as * i.e. the Kleene closure of the restricted operator.

In the following we will show that HF-closure and K-closure are equivalent for ; and || but that this is not the case for × × . Lemma 1. For any ∈ {; , ||}, T ∈ P(T Ω ), t in T Ω and a ∈ A Ω we have:

(a.t ∈ T * ) ⇒ (∃ t ∈ T Ω s.t. (a.t ∈ T ) ∧ (t ∈ {t } T * ))
Proof. By induction on j given a.t ∈ T j . For ||, we use its commutativity. Let us detail a counter example showing that the weak K-closure × × * and the weak HF-closure

× × * are not equivalent. Given T = {l 1 !m 1 .l 2 ?m 1 , l 2 !m 2 }, let us consider the powerset T × × 2 of T . By definition, {l 2 !m 2 } × × {l 1 !m 1 .l 2 ?m 1 } ⊂ T × × 2 .
Here we can choose to take l 1 !m 1 as a first action and therefore t =

l 1 !m 1 .l 2 !m 2 .l 2 ?m 1 ∈ T × × 2 . However, t ∈ T × × T = T × × 2
and more generally, for any j smaller or greater that 2, t ∈ T × × j . Hence, T × × * ⊆ T × × * .

Syntax & denotational semantics

As noted earlier in Section 2.2, interactions terms are defined inductively. Basic building blocks include the empty interaction ∅ which specifies the empty behavior (observation of no action) and any atomic action a of A Ω , which specifies the single-element trace a. More complex behavior can then be specified inductively using the binary constructors strict, seq, par and alt and the unary constructors loop S (strict loop), loop H (head loop up to × × ), loop W (weak loop) and loop P (parallel loop).

Definition 4 (Interaction Language). We denote by I Ω the set of terms inductively defined by the set of operation symbols F = F 0 ∪ F 1 ∪ F 2 s.t.:

symbols or arity 0 (constants) are F 0 = {∅} ∪ A Ω symbols of arity 1 are F 1 = {loop S , loop H , loop W , loop P } symbols of arity 2 are F 2 = {strict, seq, par, alt}

In Definition 4 we define our Interaction Language (IL) as a set of terms I Ω inductively defined from the set of symbols F with arity in N. The set P(T Ω ) of sets of traces admits the structure of a F-algebra using operators introduced in section 2. The denotational semantics of interactions is then defined in Definition 5 using the initial homomorphism associated to this F-algebra.

Definition 5 (Denotational semantics). A = (P(T Ω ), {f A | f ∈ F}) is the F-algebra defined by the following interpretations of the operation symbols in F:

∅ A = { } a A = {a} strict A = ; seq A = × × par A = || alt A = ∪ loop A S = ; * loop A H = × × * loop A W = × × * loop A P = || *
The denotational semantics σ d of I Ω is the unique F-homomorphism σ d : I Ω → P(T Ω ) between the free term F-algebra 4 T F and A.

The semantics of constants ∅ and a ∈ A Ω are sets containing a single element being respectively { } and {a}. The strict, seq, par and alt symbols are respectively associated to the ;, × × , || and union ∪ operators on sets of traces. The use of the strict sequencing (";"), weak sequencing (" × × ") and interleaving ("||") operators is illustrated on the right of Fig. 1 so as to compute the semantics of the interaction example given on the left of Fig. 1. For instance, from the second line to the third line, using distinct colours to better visualise the differences between scheduling operators, weak sequencing {l 1 !m 1 .l 3 ?m 1 } × × {l 1 !m 2 .l 2 ?m 2 } allows l 1 !m 2 to be reordered before l 3 ?m 1 but not before l 1 !m 1 while interleaving {l 1 !m 3 .l 2 ?m 3 }||{l 1 !m 4 } allows l 1 !m 4 to be placed anywhere w.r.t. l 1 !m 3 and l 2 ?m 3 . The resulting set of traces is given on the bottom right.

From a system designer perspective, using loop S , loop H , loop W or loop P is motivated by different goals:

-With loop S (i), each instance of a repeatable behavior must be executed entirely before any other can start. We can use loop S to specify some critical repeatable behavior of which there can only exist one instance at a time. -With loop P (i), all existing instances can be executed concurrently w.r.t. one another, and, at any given moment, new instances can be created. loop P can therefore be used to specify protocols in which any number of new sessions can be created and run in parallel.

A structural operational semantics

Now we present our structural operational semantics. It relies on the definition (by structural induction) of two predicates: "i ↓" (the termination predicate) indicates that the interaction i accepts the empty trace and "i a -→ i " (the execution relation) indicates that traces a.t such that t is accepted by i are accepted by i. The relation → allows the determination, for any interaction i, of which actions a can be immediately executed, and, of potential follow-up interactions i which express continuations t of traces a.t accepted by i. Defining an execution relation → is a staple of process calculus [START_REF] Baeten | Process algebra with explicit termination[END_REF]. We will pay particular attention to the weak sequencing operator in Section 4.2 before defining → in Section 4.3.

Termination

By reasoning on the structure of an interaction term i, we can determine whether or not the empty trace belongs to its semantics. When this holds, we say that i terminates and use the notation i ↓ as in [START_REF] Baeten | Process algebra with explicit termination[END_REF][START_REF] Mauw | Operational semantics for msc'96[END_REF].

Definition 6 (Termination). The predicate ↓⊂ I Ω is such that for any i 1 and i 2 from I Ω , any f ∈ {strict, seq, par} and any k ∈ {S, H, W, P } we have:

∅ ↓ i 1 ↓ alt(i 1 , i 2 ) ↓ i 2 ↓ alt(i 1 , i 2 ) ↓ i 1 ↓ i 2 ↓ f (i 1 , i 2 ) ↓ loop k (i 1 ) ↓
All rules of Definition 6 are evident. The empty interaction ∅ only accepts , and thus terminates. An interaction with a loop at its root terminates because it is possible to repeat zero times its content. As alt(i 1 , i 2 ) specifies a choice, it terminates iff either i 1 or i 2 terminates. An interaction of the form f (i 1 , i 2 ), with f being a scheduling constructor, terminates iff both i 1 and i 2 terminate. The rules are consistent with the denotational semantics:

Lemma 3 (Termination w.r.t. σ d ). For any i ∈ I Ω , (i ↓) ⇔ ( ∈ σ d (i))
Proof. By induction on the term structure of interactions.

In summary, i ↓ means that i may terminate immediately, but because of nondeterminism, depending on the nature of i, i may allow arbitrary long traces.

Dealing with weak-sequencing using evasion & pruning

Weak sequencing only allows interleavings between actions that occur on different lifelines. As a result, within an interaction of the form i = seq(i 1 , i 2 ), some actions that can be executed in i 2 (i.e. such that i 2 a -→ i 2 ) may also be executed in seq(i 1 , i 2 ), i.e. such that seq(i 1 , i 2 ) a -→ i . In other words, given a trace a.t ∈ σ d (i), action a might correspond to an action expressed by i 2 . This is however conditioned by the ability of i 1 to express traces that have no conflict w.r.t. a so that a may be placed in front of what is expressed by i 1 when recomposing a.t.

We define the evasion predicate as a weaker notion than the termination predicate ↓. The evasion predicate "↓ × × " can be described as a form of local termination. For a lifeline l, we say that i evades l, denoted by i ↓ × × l if i accepts at least one trace that does not contain actions occurring on l.

Definition 7 (Evasion). The predicate ↓

× × ⊂ I Ω × L is such that for i 1 and i 2 in I Ω , l ∈ L, a ∈ A Ω , f ∈ {strict, seq, par} and k ∈ {S, H, W, P } we have:

∅ ↓ × × l θ(a) = l a ↓ × × l i 1 ↓ × × l alt(i 1 , i 2 ) ↓ × × l i 2 ↓ × × l alt(i 1 , i 2 ) ↓ × × l i 1 ↓ × × l i 2 ↓ × × l f (i 1 , i 2 ) ↓ × × l loop k (i 1 ) ↓ × × l
The empty interaction ∅ evades any lifeline as contains no action. An interaction reduced to a single action a evades l iff a does not occur on l. As for termination, an interaction with a loop at its root evades any lifeline because it accepts . Choice and scheduling operators are also handled in the same manner as for the termination predicate. Moreover, we consider the collision predicate ↓ × × by considering dual structural rules w.r.t. those defining the evasion predicate ↓ × × so that we have: i

↓ × × l iff ¬(i ↓ × × l)).
Lemma 4 (Evasion w.r.t. σ d ).

For any l ∈ L and i ∈ I Ω ,(i

↓ × × l) ⇔ (∃ t ∈ σ d (i), ¬(t × × l))
Proof. By induction on the term structure of interaction.

Let us remark that, for any i ∈ I Ω , if i ↓ then ∀ l ∈ L, i ↓ × × l. Indeed, has no conflict w.r.t. any l. The opposite does not hold: it suffices to consider i = alt(l 1 !m, l 2 !m) and observe that ∀ l ∈ {l 1 , l 2 }, i ↓ × × l holds while i ↓ does not. The application of the evasion predicate (w.r.t. lifeline l 2 ) is illustrated on Fig. 3. On the right is represented the syntactic structure of an interaction i, and, on the left, the corresponding drawing as a sequence diagram. On the syntax tree, the nodes are decorated with symbols (resp. ) to signify that the subinteraction underneath that node evades (resp. collides with) l 2 . Starting from the leaves we can decorate all nodes and conclude once the root is reached. By taking the right branch of the alternative and by choosing not to instantiate the loop, we can see that i accepts some traces that have no conflict w.r.t. lifeline l 2 (in our case, only the trace l 3 !m 2 .l 1 ?m 2 ). As a result the interaction i verifies i ↓ × × l 2 . On the diagram representation, evasion can be illustrated by drawing a line over l 2 the lifeline of interest. This line can be decomposed into several areas that are colored either in green or in red. The coloration depends on whether the sub-interaction corresponding to the operand evades or collides with l 2 .

Provided that i 1 ↓ × × θ(a), an action a that is executable in i 2 i.e. s.t. i 2 a -→ i 2 is also executable in i = seq(i 1 , i 2 ). However, this is not enough to define a rule seq(i 1 , i 2 ) a -→ i compatible with the semantics σ d . i must specify continuations t s.t. a.t ∈ σ d (i). Continuation traces t are built from traces t 1 ∈ σ d (i 1 ) and t 2 such that ¬(t 1 × × θ(a)) and a.t 2 ∈ σ d (i 2 ). By defining i 1 as the interaction which expresses exactly traces t 1 s.t. ¬(t 1 × × θ(a)) we may produce a rule seq(i 1 , i 2 ) a -→ seq(i 1 , i 2 ). The computation of i 1 is called pruning and is defined as an inductive relation

× × -→ s.t. i × × l - → i indicates that the pruning of i ∈ I Ω w.r.t. l ∈ L yields i ∈ I Ω . Pruning is defined so that σ d (i ) ⊆ σ d (i) is the maximum subset of σ d (i)
that contains no trace conflicting with l (see Lemma 6).

Definition 8 (Pruning). The pruning relation

× × -→ ⊂ I Ω × L × I Ω is s.t.
for any l ∈ L, any f ∈ {strict, seq, par} and any k ∈ {S, H, W, P }:

∅ × × l - → ∅ θ(a) = l a × × l - → a i 1 × × l - → i 1 i 2 × × l - → i 2 f (i 1 , i 2 ) × × l - → f (i 1 , i 2 ) i 1 × × l - → i 1 i 2 × × l - → i 2 alt(i 1 , i 2 ) × × l - → alt(i 1 , i 2 ) i 1 × × l - → i 1 i 2 ↓ × × l alt(i 1 , i 2 ) × × l - → i 1 i 2 × × l - → i 2 i 1 ↓ × × l alt(i 1 , i 2 ) × × l - → i 2 i 1 × × l - → i 1 loop k (i 1 ) × × l - → loop k (i 1 ) i 1 ↓ × × l loop k (i 1 ) × × l - → ∅
Evasion and pruning are intertwined notions. Indeed, as per Lemma 5 evasion is equivalent to the existence and unicity of a pruned interaction.

Lemma 5 (Conditional existence & unicity for pruning).

For any i ∈ I Ω and any l ∈ L, (i

↓ × × l) ⇔ (∃! i ∈ I Ω s.t. i × × l - → i )
Proof. By induction on the term structure of interactions.

Let us comment on the rules defining the pruning relation. We have ∅ × × l -→ ∅ because the semantics of ∅ being { }, there are no conflicts w.r.t. l. Any action a ∈ A Ω is prunable iff θ(a) = l. In such a case, a needs not be eliminated and thus a × × l -→ a. For i = alt(i 1 , i 2 ) to be prunable we must have either or both of

i 1 ↓ × × l or i 2 ↓ × ×
l. If both branches evade l they can be pruned and kept as alternatives in the new interaction term. If only a single one does, we only keep the pruned version of this single branch. For any scheduling constructor f

, if i = f (i 1 , i 2 ), in order to have i ↓ × × l we must have both i 1 ↓ × × l and i 2 ↓ × × l.
In that case the unique interaction i such that i × × l -→ i is defined as the scheduling, using f , of the pruned versions of i 1 and i 2 . For loops i = loop k (i 1 ) with k ∈ {S, H, W, P }, we distinguish two cases: (a) if i 1 ↓ × × l then any execution of i 1 will yield a trace conflicting l and repetitions should be forbidden; (b) if i 1 ↓ × × l repetitions are kept, given that i 1 can be pruned as i 1 × × l -→ i 1 . This being the modification which preserves a maximum amount of traces, we have loop k (i 1 ) × × l -→ loop k (i 1 ). We have seen that the interaction i of Fig. 3 satisfies i ↓ × × l 2 . Therefore Lemma 5 implies the existence of a unique i s.t. i × × l2 -→ i . Fig. 4 illustrates the computation of i . The blue lines represent the modifications in the syntax of i that occur during its pruning into i . On Fig. 3 we decorated sub-interactions of i with whenever they did not evade l 2 . During pruning, those sub-interactions must be eliminated given that the resulting term must not express actions occurring on l 2 . Hence, on Fig. 4, we have crossed in blue the problematic sub-interactions. The root node is an alt. Let us note i = alt(i 1 , i 2 ). On Fig. 3 we have seen that

we have i 1 ↓ × × l 2 and i 2 ↓ × × l 2 . Therefore we have i × × l2 -→ i 2 with i 2 being such that i 2 × × l2 -→ i 2 .
This selection of the right branch of the alt is illustrated on Fig. 4 by the curved arrow which "replaces" the alt by the seq on its bottom right. There remains to determine i 2 s.t. i 2 × × l2 -→ i 2 . At the root of i 2 we have a seq. Let us note i 2 = seq(i A , i B ). As per Fig. 3

we have both i

A ↓ × × l 2 and i B ↓ × × l 2 and therefore i 2 = seq(i A , i B ) such that i A × × l2 -→ i A and i B × × l2 -→ i B .
Underneath i A , no actions occur on l 2 and hence i A = i A . At the root of i B we have a loop S . Let us note i B = loop S (i C ). As per Fig. 3 we have i C ↓ × × l 2 and therefore i B = ∅ which is illustrated on Fig. 4 by the ← ∅ in blue, which "replaces" the loop S by ∅. Finally there remain i = seq(i A , ∅), which is drawn on the right of Fig. 4. Lemma 6 states that given i × × l -→ i , the pruned interaction i exactly specifies all the executions of i that do not involve l.

Lemma 6 (Pruning w.r.t. σ d ). For any l ∈ L and any i and i from I Ω :

(i × × l - → i ) ⇒ (σ d (i ) = {t ∈ σ d (i) | ¬(t × × l)})
Proof. By induction on the term structure of interactions.

Execution relation & operational semantics

A structural operational semantic in the style of Plotkin [START_REF] Plotkin | A structural approach to operational semantics[END_REF] allows determining traces t = a 1 . • • • .a n through the assertion of a succession of predicates of the form i j aj -→ i j+1 representing the evolution of the system. By expressing action a j , the system goes from being modelled by i j to being modelled by i j+1 .

Definition 9 (Execution relation). The execution relation →⊂ I

Ω × A Ω × I Ω is s.t.: a a -→ ∅ i 1 a -→ i 1 alt(i 1 , i 2 ) a -→ i 1 i 2 a -→ i 2 alt(i 1 , i 2 ) a -→ i 2 i 1 a -→ i 1 par(i 1 , i 2 ) a -→ par(i 1 , i 2 ) i 2 a -→ i 2 par(i 1 , i 2 ) a -→ par(i 1 , i 2 ) i 1 a -→ i 1 strict(i 1 , i 2 ) a -→ strict(i 1 , i 2 ) i 2 a -→ i 2 i 1 ↓ strict(i 1 , i 2 ) a -→ i 2 i 1 a -→ i 1 seq(i 1 , i 2 ) a -→ seq(i 1 , i 2 ) i 1 × × θ(a) --→ i 1 i 2 a -→ i 2 seq(i 1 , i 2 ) a -→ seq(i 1 , i 2 ) i 1 a -→ i 1 loop S (i 1 ) a -→ strict(i 1 , loop S (i 1 )) i 1 a -→ i 1 loop H (i 1 ) a -→ seq(i 1 , loop H (i 1 )) i 1 a -→ i 1 loop W (i 1 ) × × θ(a) --→ i loop W (i 1 ) a -→ seq(i , seq(i 1 , loop W (i 1 ))) i 1 a -→ i 1 loop P (i 1 ) a -→ par(i 1 , loop P (i 1 ))
Many of the rules are directly similar to those in use for process algebras. In an interaction reduced to an action a, a may be executed with ∅ as remaining interaction. If within i = alt(i 1 , i 2 ), action a can be executed in either i 1 or i 2 with either i 1 a -→ i 1 or i 2 a -→ i 2 then it may be executed in i and the resulting interaction is either i 1 or i 2 . For i = par(i 1 , i 2 ), if we have either i 1 a -→ i 1 or i 2 a -→ i 2 then a may be executed in i and the resulting interaction naturally is either par(i 1 , i 2 ) or par(i 1 , i 2 ). Executing actions on the left of either a strict or a seq follows the same rule as in the case of a par because no precedence relations are enforced on the left-hand side. However, an action a may be executed on the right of i = strict(i 1 , i 2 ) only if i 1 terminates. Indeed, in that case i 1 may express the empty trace as per Lemma 3 and nothing prevents a to be the first action to be executed. The resulting interaction is then i 2 given that we force i 1 to express . Likewise, within i = seq(i 1 , i 2 ) there is a condition for executing an action a on the right. This condition is that i 1 ↓ × × θ(a), which, as per Lemma 5 is implied by the condition i 1 × × θ(a)

--→ i 1 . Finally, we obtain i a -→ seq(i 1 , i 2 ) given that i 2 a -→ i 2 and that the pruning of i 1 up θ(a) yields i 1 .

Let us look at rules for loop operators loop S , loop H and loop P which look the same, i.e. loop k (i) a -→ f (i , loop k (i)) under the condition i a -→ i and using the notation (k, , f ) ∈ {(S, ; , strict), (H, × × , seq), (P, ||, par)}. and thus the formulation of its rule is self-evident. In the case of loop S and loop P it is the fact that the HF and K-closures of ; and || are equivalent (as per Lemma 2) which enables their respective rules to be formulated in this manner.

Any t ∈ σ d (f (i , loop k (i))) verifies t ∈ {t 1 } σ d (loop k (i)) for a certain t 1 ∈ σ d (i ). If
The rule for loop W allows for the first action to be taken from a later iteration of the loop. Let us consider i = loop W (i 1 ) and a.t ∈ σ d (i). The rule is formulated

such that t ∈ σ d (seq(i , seq(i 1 , i))) with i × × θ(a) --→ i and i 1 a -→ i 1 . Given that i is a loop, it is always prunable (Lemma 5) so there exists i s.t. i × × θ(a) --→ i . The fact that t ∈ σ d (seq(i , seq(i 1 , i))) translates into having t ∈ σ d (i ) × × σ d (i 1 ) × × σ d (i). Then, if a is taken from the first iteration of the loop, then, given that ∈ σ d (i ) (Lemma 6) we have t ∈ { } × × {t 1 } × × σ d (i) with t 1 = a.t 1 ∈ σ d (i 1
). If a is taken from the second iteration of the loop, let us consider t 1 ∈ σ d (i 1 ) the first iteration and t 2 = a.t 2 ∈ σ d (i 1 ) the second one (from which a is taken and hence t 2 ∈ σ d (i 1 )). We have t ∈ {t 1 } × × {t 2 } × × σ d (i) and the condition ¬(t 1 × × θ(a)). This condition implies, as per Lemma 6 that {t 1 } ⊂ σ d (i ). The reasoning is the same when a is taken from later instances. Let us consider a.

t ∈ {t 1 } × × • • • × × {t n-1 } × × {t n } × × σ d (i). We then have {t 1 } × × • • • × × {t n-1 } ⊂ σ d (i ) because i
is either a loop (and therefore absorbing) or ∅ (all the t j are then ). Hence the rule indeed allows a to be taken from any iteration.

The predicates ↓ and → ground the operational semantics σ o given below:

Definition 10 (Operational semantics). σ o :

I Ω → P(T Ω ) is s.t.: i ↓ ∈ σ o (i) t ∈ σ o (i ) i a -→ i a.t ∈ σ o (i)

Illustrative example

On Fig. 5 we illustrate both the operational semantics and an example showcasing the difference between loop H and loop W . Execution trees are drawn with the help of the HIBOU tool described in [START_REF] Mahe | A smallstep approach to multi-trace checking against interactions[END_REF]. We consider repetitions of i = alt(strict(l 1 !m 1 , l 2 ?m 1 ), l 2 !m 2 ). On the first row, we illustrate the construction of a trace accepted by seq(i, i) where i is repeated twice using weak sequencing. Here, the second occurrence of action l 1 !m 1 (at the bottom) is immediately seq(i, i) executable because, with pruning, we can force the choice of the right branch of the first alternative which evades l 1 . At the end, the trace t = l 1 !m 1 .l 2 !m 2 .l 2 ?m 1 is expressed by seq(i, i). Now, if we consider loop H (i), we get what is illustrated on the second row of Fig. 5. We can manage to execute the first action l 1 !m 1 but from that point, the second action of t which is l 2 !m 2 is not executable. Indeed, the presence of l 2 ?m 1 at the top of the diagram prevents it to be executed. As loop H is associated to the weak HF-closure × × * and not to the K-closure × × * , it is therefore expected that t could not be accepted by loop H (i) in this example. However, on the third row of Fig. 5, loop W (i) can recognize t. The addition of the pruned version of the loop allows one to delay the determination of the instance as part of which the initial l 1 !m 1 is executed.

l 1 !m 1 ---→ l 2 !m 2 ---→ l 2 ?m 1 ---→ loopH (i) l 1 !m 1 ---→ loopW (i) l 1 !m 1 ---→ l 2 !m 2 ---→ l 2 ?m 1 ---→
on partial order sets. The extent to which UML-SDs are formalised may vary [START_REF] Micskei | The many meanings of uml 2 sequence diagrams: a survey[END_REF]: some works formalize loops [START_REF] Lu | Required behavior of sequence diagrams: Semantics and conformance[END_REF], others do not [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF], and some only allow finitely many iterations [START_REF] Störrle | Semantics of interactions in uml 2.0[END_REF]. In all cases where there are loops, only one loop operator is proposed and may correspond to either loop H or loop W .

Our denotational semantics is inspired from [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF]. We have completed their definitions dealing with loop operators. [START_REF] Mauw | Operational semantics for msc'96[END_REF] introduces an operational semantics for MSC using a termination predicate and an execution relation. Similarities between [START_REF] Mauw | Operational semantics for msc'96[END_REF] and our work include the use of pruning which, in [START_REF] Mauw | Operational semantics for msc'96[END_REF], relates to a "permission relation". In [START_REF] Mauw | Operational semantics for msc'96[END_REF], loops are not handled and there is no strict constructor: direct causal relations between actions occurring on different lifelines (e.g. emission-reception of a message) are handled by maps, updated during executions. Moreover, rules involve negative conditions such as i a -→ expressing that it is not possible to find an interaction i verifying i a -→ i . This way of doing reduces the set of rules to be considered, but does not give clear access to reasoning about the rule system itself, in particular reasoning about semantics equivalence. In [START_REF] Reniers | Message sequence chart : syntax and semantics[END_REF], a loop construction for weak sequencing composition is considered in addition to the constructions discussed in [START_REF] Mauw | Operational semantics for msc'96[END_REF]. Rules in [START_REF] Reniers | Message sequence chart : syntax and semantics[END_REF] include two rules similar to our rules for loop H and loop W so that the semantics includes the two ways of dealing with composition according to the weak sequencing × × .

Earlier works of ours [START_REF] Mahe | Revisiting semantics of interactions for trace validity analysis[END_REF][START_REF] Mahe | A smallstep approach to multi-trace checking against interactions[END_REF] focused on the static analysis of traces against interactions. We have proposed an algorithmicised semantics allowing us, given an interaction i and an action a, to compute the follow-up interaction i whose traces are licit extensions of a with respect to i. This previous semantics was defined in a functional style by identifying the actions likely to start a trace by means of their position in the interaction term. The use of positions makes the semantics less readable and understandable than a structural operational semantics à la process algebra, and hampers reasoning about the semantics. Novel contributions in this paper w.r.t. [START_REF] Mahe | Revisiting semantics of interactions for trace validity analysis[END_REF][START_REF] Mahe | A smallstep approach to multi-trace checking against interactions[END_REF] consist in the distinction of loop W & loop H , the formulation of a denotational semantics in an algebraic style rather than using precedence relations, the formulation of a structural operational semantics and primarily, a proof of equivalence between both semantics.

Conclusion & further work

In this paper we define an IL including weak and strict sequencing, parallel and alternative composition as well as four distinct loop operators to specify different kinds of repetition. We formulate the semantics of this IL: (1) in denotational-style, making use of composition & algebraic operators and (2) in operational-style by reconstructing accepted traces via the succession of atomic executions. The equivalence of both formulations is proven (Coq proof in [START_REF] Mahe | Coq proof for the equivalence of the semantics[END_REF]). We currently investigate how to enrich our language with some form of value passing i.e. instead of exchanging abstract messages we may interpret them concretely or symbolically with typed data. This last point is notably addressed in some process calculi frameworks [START_REF] Ingólfsdóttir | A symbolic approach to value-passing processes[END_REF].

Fig. 1 :

 1 Fig. 1: Example of a basic interaction & its trace semantics

Fig. 2 :

 2 Fig. 2: Example illustrating the weak Kleene closure

Lemma 2 (

 2 Equivalence of HF & K closures for ; & ||). For any set of traces T , we have T ; * = T ; * and T || * = T || * .Proof. By induction on a member trace t.

Fig. 3 :

 3 Fig. 3: Illustration of the evasion predicate (here w.r.t. lifeline l2)

Fig. 4 :

 4 Fig. 4: Illustration of pruning

Fig. 5 :

 5 Fig. 5: Illustration of the operational semantics & of the counter-example from Sec.2.3

  action a comes from the first iteration of the loop i.e. a.t∈ {a.t 1 } σ d (loop k (i)) ⊂ σ d (i) σ d (loop k (i)), it coincides with using the restricted operator as a scheduler. It turns out that loop H is explicitly associated to

	× × *

For a set E, P(E) is the set of all subsets of E.

The free term F-algebra is defined by interpreting symbols of F as constructors of new terms: for f ∈ F of arity j, for t1, . . . tj ∈ IΩ, f (t1, . . . tj) is interpreted as itself.

Proving the equivalence of both semantics

In the following we prove the equivalence of σ o and σ d . A formalisation of the proofs using Coq is available in [START_REF] Mahe | Coq proof for the equivalence of the semantics[END_REF].

Let us at first prove that for any interaction i we have σ o (i) ⊆ σ d (i). The first step to do so is to characterize the execution relation "→" w.r.t. σ d : Lemma 7 (Property 1 of → w.r.t. σ d ). For any a ∈ A Ω , t ∈ T Ω and i and

Proof. By induction on cases that make i a -→ i possible.

Lemma 7 and Lemma 3 state that the σ d semantics accepts the same two construction rules (that for the empty trace and that for non empty traces of the form a.t) as those that define σ o inductively. As a result any trace that is accepted according to σ o is also be accepted according to σ d :

Proof. By induction on a member trace t.

Let us now prove the reciprocate, i.e. that for any interaction i, σ d (i) ⊆ σ o (i). We provide, with Lemma 8, a second characterization of "→" w.r.t.

Proof. By induction on the term structure of interactions.

Thanks to Lemma 8 and Lemma 3 we conclude with Theorem 2:

Proof. By induction on a member trace t.

We have therefore proven both inclusion and can conclude that the operational semantics σ o is indeed equivalent to the denotational-style semantics σ d .

Related works

Unlike some other works (e.g. [START_REF] Knapp | UML Interactions Meet State Machines -An Institutional Approach[END_REF]), we do not have a dedicated construction for the passing of a message from a lifeline to another. We formulate this in the form strict(a!m, b?m), expressing that the emission of message m on lifeline a precedes its reception on b. In [START_REF] Micskei | The many meanings of uml 2 sequence diagrams: a survey[END_REF] a survey of formal semantics associated to UML-SDs is proposed. It is notable that UML-SDs are described semi-formally in the norm [START_REF]OMG: Unified Modeling Language v2[END_REF]. This allows for a rich language with operators such as assert or negate [START_REF] Harel | Assert and negate revisited: Modal semantics for UML sequence diagrams[END_REF] which are not covered in our IL. However a full formalisation proves difficult, as explained in [START_REF] Micskei | The many meanings of uml 2 sequence diagrams: a survey[END_REF][START_REF] Harel | Assert and negate revisited: Modal semantics for UML sequence diagrams[END_REF]. Most formal approaches rely on translations towards other formalisms [START_REF] Eichner | Compositional semantics for uml 2.0 sequence diagrams using petri nets[END_REF] or consist in denotational semantics [START_REF] Störrle | Semantics of interactions in uml 2.0[END_REF] that are most often based