Athanase Papadopoulos
email: athanase.papadopoulos@math.unistra.fr

Lixin Liu

Daniele Alessandrini
email: daniele.alessandrini@gmail.com

Weixu Su

The behaviour of Fenchel-Nielsen distance under a change of pants decomposition

Keywords: AMS Mathematics Subject Classification: 32G15, 30F30, 30F60 Teichmüller space, Fenchel-Nielsen coordinates, Fenchel-Nielsen metric

come   L'archive ouverte pluridisciplinaire

Introduction

This paper is in the lineage of the papers [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF], [START_REF] Alessandrini | On various Teichmüller spaces of a surface of infinite topological type[END_REF], [START_REF] Alessandrini | On local comparison between various metrics on Teichmüller spaces[END_REF] and [START_REF] Liu | Some metrics on Teichmüller spaces of surfaces of infinite type[END_REF], in which we studied and compared various metrics on Teichmüller spaces of surfaces of finite or of infinite topological type. The first important thing to know in that respect is that some definitions that are equivalent to each other in the Teichmüller theory of surfaces of finite type are no more equivalent in the setting of surfaces of infinite type. Indeed, there are Teichmüller spaces that are associated to a surface of infinite type that are distinct (in the set-theoretic sense) and that would be equal if the same definitions were made in the case of a surface of finite type. Furtermore, each such space associated to a surface of finite or of infinite type carries a natural Date: April 30, 2011. 1 distance function, and it is an interesting problem to study the relations between the various spaces, their distance functions and their topologies.

It is necessary to have different names to the various spaces that arise, and we briefly recall the terminology.

We use the name quasi-conformal Teichmüller space for the "classical" Teichmüller space defined using quasi-conformal mappings and equipped with its Teichmüller metric.

In the paper [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF], we introduced the Fenchel-Nielsen Teichmüller space, a certain space of equivalence classes of complex structures on a surface, equipped with a distance, called the Fenchel-Nielsen distance, defined using Fenchel-Nielsen coordinates. This Teichmüller space and its metric depend on the choice of a pair of pants decomposition of the surface. The Fenchel-Nielsen Teichmüller space was a fundamental tool in our work, because it has explicit coordinates and an explicit distance function, and we used it in the other papers mentioned to describe and understand the other Teichmüller spaces. One of the results obtained was that if the lengths of all the boundary curves of the pair of pants decomposition are bounded above by a uniform constant then there is a set-theoretic equality between the Fenchel-Nielsen Teichmüller space and the quasiconformal Teichmüller space. Furthermore, the identity map between the two Teichmüller spaces, equipped with their respective metrics, is a locally bi-Lipschitz homeomorphism. This gives an explicit description of the global topology and the local metric properties of the quasiconformal Teichmüller space.

In the paper [START_REF] Alessandrini | On local comparison between various metrics on Teichmüller spaces[END_REF], we obtained similar local comparison results between the Fenchel-Nielsen Teichmüller space and the so-called length spectrum Teichmüller space, another deformation space of complex structures, whose definition and metric are based on the comparison of lengths of simple closed curves between surfaces.

In the cases of surfaces of finite type, the various Teichmüller spaces coincide set-theretically, but there are still interesting questions on the local and global comparison of the metrics that are defined on these spaces.

In the present paper, we prove that under a change of the pair of pants decomposition, the identity map between the corresponding Fenchel-Nielsen Teichmüller spaces is not bi-Lipschitz in general. This result holds for surfaces of finite and for those of infinite type. We first prove this result in the case where the surface is a torus with one hole or a sphere with four holes. In this case, the two pair of pants decompositions are obtained from each other by a single elementary move. The proof is based on explicit computations that use formulae obtained by Okai in [START_REF] Okai | Effects of change of pants decompositions on their Fenchel-Nielsen coordinates[END_REF]. We then deduce an analogous result for arbitrary surfaces of finite or of infinite type.

To state the theorems precisely, we now introduce some minimal amount of notation. We refer the reader to Section 2 for more details.

If X 0 is a surface equipped with a complex structure, we denote by T qc (X 0 ) the quasi-conformal Teichmüller space of X 0 , equipped with the quasi-conformal distance d qc , and by T F N,P (X 0 ) the Fenchel-Nielsen Teichmüller space of X 0 with reference to the pair of pants decomposition P, equipped with its associated Fenchel-Nielsen distance d F N,P .

In Section 6 we prove the following:

Theorem 1.1. Let S be an orientable surface which is either of finite topological type of negative Euler characteristic and which is not a pair of pants, or of infinite topological type. Let P be a pair of pants decomposition of S. Then we have the following:

(1) There exists another pair of pants decomposition P ′ such that for every base complex structure X 0 on S we have T F N,P (X 0 ) = T F N,P ′ (X 0 ) as sets, but the identity map between the two spaces equipped with their Fenchel-Nielsen distances d F N,P and d F N,P ′ respectively is not Lipschitz. (2) For every base complex structure X 0 on S, consider the space T = T qc (X 0 )∩ T F N,P (X 0 ). Then the identity map from (T, d F N,P ) to (T, d qc ) is not Lipschitz. (3) If S is of infinite topological type, there exists a base complex structure X 0 on S and another pair of pants decomposition P ′ such that if T is the space T qc (X 0 ) ∩ T F N,P (X 0 ), then the identity map from (T, d F N,P ) to (T, d F N,P ′ ) is not continuous. ( 4) If S is of infinite topological type, there exists a base complex structure X 0 on S such that if T is the space T qc (X 0 ) ∩ T F N,P (X 0 ), then the identity map from (T, d F N,P ) to (T, d qc ) is not continuous.

From this result, we can see that the local comparison results we obtained in the papers [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF] and [START_REF] Alessandrini | On local comparison between various metrics on Teichmüller spaces[END_REF] are optimal in the sense that they cannot be extended to global comparison results, since the global metric geometry of the Fenchel-Nielsen distance depends on the choice of the pair of pants decomposition.

The Fenchel-Nielsen metric

In this section, we recall a few facts from our previous papers, which will help making the present paper self-contained.

Let S be an orientable connected surface of finite or of infinite topological type, that can have punctures and/or compact boundary components. The complex structures that we consider on S are such that each boundary component has a regular neighborhood that is bi-holomorphically equivalent to a bounded cylinder and each puncture has a neighborhood that is bi-holomorphically equivalent to a punctured disc.

We start by reviewing the definition of the Fenchel-Nielsen metric on the Teichmüller space T(S) of S. The definition depends on the choice of a pair of pants decomposition of S.

A pair of pants decomposition P = {C i i = 1, 2, . . .} of S is a decomposition into generalized pairs of pants glued along their boundary components, where a generalized pair of pants is a sphere with three holes, a hole being either a point removed (leaving a puncture on the pair of pants) or an open disc removed (leaving a boundary component on the pair of pants). The curves C i in the above definition are the closed curves on S (including the boundary components) that define the decomposition. It is well-known that every surface of finite topological type with negative Euler characteristic admits a pair of pants decomposition. It also follows from the classification of surfaces of infinite type that every such surface admits a pair of pants decomposition [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF].

To every complex structure on S we can associate a hyperbolic metric, called the intrinsic metric, which was defined by Bers in [START_REF] Bers | Nielsen extension of Riemann surfaces[END_REF]. This metric is conformally equivalent to the given complex structure, and every boundary curve is a geodesic for that metric. The definition of the intrinsic metric is recalled in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF]. In the sequel, when we talk about geometric objects (geodesics, length, angles, etc.) associated to a complex structure on S, it is understood that these are associated to the intrinsic metric on S. A pair of pants decomposition P = {C i } of the surface S equipped with its intrinsic metric is said to be geodesic if each C i is a geodesic closed curve in S with respect to this metric. In [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF] we proved that every topological pair of pants decomposition of S is homotopic to a unique geodesic pair of pants decomposition. (Note that this is not true for general hyperbolic metrics on S. For example, the Poincaré metric of S may not satisfy this property if this metric is different from the intrinsic metric, and this may happen; we discussed this fact in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF].) Given a closed curve C on the surface S, we make the convention that we shall call also C the unique geodesic representative of this closed curve with reference to the intrinsic metric.

Given a complex structure X on S and a geodesic pair of pants decomposition P = {C i } of this surface, then for any closed geodesic C i ∈ P there is a welldefined length parameter l X (C i ), which is the length of this closed geodesic, and a twist parameter τ X (C i ), which is defined only if C i is not the homotopy class of a boundary component of S. The quantity τ X (C i ) is a measure of the relative twist amount along the geodesic C i between the two generalized hyperbolic pair of pants (which might be the same) having this geodesic in common. In this paper, the value τ X (C i ) is a signed distance-parameter, that is, it represents an amount of twisting in terms of a distance measured along the curve, as opposed to an angle of twisting parameter (whose absolute value would vary by 2π after a complete Dehn twist).

For any complex structure X on S, its Fenchel-Nielsen parameter relative to P is a collection of pairs

((l X (C i ), τ X (C i ))) i=1,2,...
where it is understood that if C i is a boundary geodesic, then it has no associated twist parameter, and instead of a pair (l X (C i ), τ X (C i )), we have a single parameter l X (C i ).

Given two complex structures X and X ′ on S, their Fenchel-Nielsen distance (with respect to P) is defined as

(1) d F N (X, X ′ ) = sup i=1,2,... max log l X (C i ) l X ′ (C i ) , |τ X (C i ) -τ X ′ (C i )| ,
again with the convention that if C i is a boundary component of S and therefore has no associated twist parameter, we consider only the first factor. If S is a surface of finite topological type, then d F N (X, X ′ ) is always finite, and the function d F N defines a distance on the Teichmüller space of S, which we will denote simply by T(S). If, instead, S is of infinite topological type, d F N (X, X ′ ) can assume the value infinity. In this case we fix a base complex structure X 0 on S, and we define the Fenchel-Nielsen Teichmüller space of X 0 as the set of homotopy classes of complex structures X on S such that d F N (X 0 , X) is finite. We denote this space by T F N (X 0 ). The function d F N is a distance function in the usual sense on this space, and it makes it isometric to the sequence space ℓ ∞ .

When it is important to stress on the dependence on a given pair of pants decomposition P, we shall denote the Teichmüller space by T F N,P (X 0 ) (this dependence of the space on P may happen only for surfaces of infinite type), and the Fenchel-Nielsen distance by d F N,P (the distance function depends on P also for a surface of finite type).

If a pair of pants decomposition P is obtained from another pair of pants decomposition P ′ by a finite number of elementary moves (represented in Figures 1 and2 below), then for any basepoint X 0 we have the set-theoretic equality T F N,P (X 0 ) = T F N,P ′ (X 0 ).

In the last section of this paper we will prove that for every surface S, there exist two pair of pants decompositions P, P ′ such that for every base complex structure X 0 , the Fenchel-Nielsen Teichmüller spaces are the same (that is, we have a settheoretical equality T F N,P (X 0 ) = T F N,P ′ (X 0 )), but the identity map between the two spaces is not Lipschitz with reference to the two Fenchel-Nielsen distances d F N,P and d F N,P ′ .

The effect of an elementary move on the torus with one hole

In this section, the surface S = S 1,1 is a torus with one hole, where the hole can be either a boundary component or a puncture. A pair of pants decomposition of S is determined by a unique simple closed curve on S which is not homotopic to a point or to the hole.

We consider two distinct pair of pants decomposition {α} and {α ′ } of S defined by two essential simple closed curves α and α ′ satisfying i(α, α ′ ) = 1, as represented in Figure 1. Let X be a complex structure on S, equipped with its intrinsic hyperbolic metric. At the hole, X can have geodesic boundary, and in this case we denote by l 0 its length, or it can have a cusp, and in this case we write l 0 = 0. We denote by (l, τ ) the length and twist parameters of the curve α, for the decomposition {α}, and by (l ′ , τ ′ ) the length and twist parameters of the curve α ′ , for the decomposition {α ′ }. We need a formula relating these values. This was done by Okai ([8]) in the case where the hole is a boundary component, but we also need similar formulae for the case of a cusp. In the following proposition we obtain this with a continuity argument. In these formulae, the case where l 0 = 0 means that at the hole the surface has a cusp. Proposition 3.1. With the above notation we have, for all l 0 ≥ 0, cosh(l ′ /2) = sinh -1 (l/2) cosh(τ /2) cosh(l) + cosh(l 0 /2) 2

1/2 cosh(τ ′ /2) = cosh(l/2) cosh 2 (τ /2)(cosh(l) + cosh(l 0 /2)) -2 sinh 2 (l/2) 1/2 cosh 2 (τ /2)(cosh 2 (l/2) + cosh 2 (l 0 /2)) + sinh 2 (l/2) cosh(l 0 /2) 1/2 .
Proof. When l 0 > 0, these formulae are proved in [START_REF] Okai | Effects of change of pants decompositions on their Fenchel-Nielsen coordinates[END_REF]. To see that they also hold when l 0 = 0 (the case of a cusp) we use the shear coordinates relative to an ideal triangulation. We recall that in the case of a torus with one hole equipped with a complex structure (and the corresponding intrinsic metric), an ideal triangulation has three edges, say a, b, c, and associated to every edge there is a real number, called the shear parameter. Thus, we have three numbers, s a , s b , s c . The boundary length l 0 can be read from the shear coordinates: [START_REF] Thurston | Three-dimensional geometry and topology[END_REF]Prop. 3.4.21]), and the cusp corresponds to the case where s a + s b + s c = 0. Here we need the property that the parameters l, |τ |, l ′ , |τ ′ | can also be written as continuous functions of the shear coordinates. To see this one can show that for every element γ of the fundamental group of the surface, the coefficients of the matrix corresponding to γ in the holonomy representation can be written as continuous functions of the shear coordinates. The length of the corresponding closed geodesic in the surface is a continuous function of the trace of this matrix, hence all simple closed curve lengths are continuous functions of the shear coordinates. For the twist parameters, we note that their absolute values can be written as a continuous function of the lengths of some simple closed curves.

l 0 = |s a + s b + s c | (see
To show that the above formulae are valid for l 0 = 0, we just need to note that both the left hand side and the right hand side of the equations are continuous functions of the shear coordinates. It is known that shear coordinates extend to the case of surfaces with cusps (see [START_REF] Thurston | Three-dimensional geometry and topology[END_REF]Chapter 3]), see also [START_REF] Papadopoulos | Shift coordinates, stretch lines and polyhedral structures for Teichmüller space[END_REF]). Then as these functions are equal when l 0 > 0, i.e. when s a + s b + s c = 0, and as this subset is dense in the space of shear coordinates, these functions are equal everywhere, that is, including the case where l 0 = 0.

For simplicity, we choose a complex structure X on the torus with one hole such that its intrinsic metric has the property that the two closed geodesics in the homotopy classes of α and α ′ meet perpendicularly. To see that such a choice is possible, we can start with an arbitrary complex structure on S (equipped with its intrinsic metric) and we cut this surface along the closed geodesic α; in this way α ′ is cut into an essential geodesic arc, which is homotopic to a unique geodesic arc β that is perpendicular to the two boundary components of Y \ {α} that arise from cutting the surface along α. Then we glue back the two components in such a way that in the resulting surface the two endpoints of β match. We obtain a complex structure with the desired property. Such a complex structure corresponds to the case τ = 0 in the notation of Okai [START_REF] Okai | Effects of change of pants decompositions on their Fenchel-Nielsen coordinates[END_REF].

Performing a Fenchel-Nielsen twist of magnitude t along α, we obtain from X a new complex structure X t that has Fenchel-Nielsen coordinates denoted by (l, τ t ) in the coordinate system associated to {α} and (l ′ t , τ ′ t ) in the coordinate system associated to {α ′ }. The coordinates of the complex structure X that we have chosen are (l, 0) and (l ′ , 0) in the bases {α} and {α ′ } respectively. Since X t is obtained by a time-t twist along the curve α, we have τ t = t for all t.

We need to estimate l ′ t and τ ′ t . By the formula for length in Proposition 3.1, we have cosh(l ′ /2) = sinh -1 (l/2) cosh(l) + cosh(l 0 /2) 2

1/2 and cosh(l ′ t /2) = sinh -1 (l/2) cosh(t/2) cosh(l) + cosh(l 0 /2) 2 1/2
. Thus, we have

cosh(t/2) = cosh(l ′ t /2) cosh(l ′ /2) = e l ′ t /2-l ′ /2 + e -l ′ t /2-l ′ /2
1 + e -l ′ .

Using the fact that x ≤ e x , we obtain

0 ≤ l ′ t /2 -l ′ /2 ≤ e l ′ t /2-l ′ /2 ≤ cosh(t/2)(1 + e -l ′ ) which implies 0 < l ′ t /2 ≤ l ′ /2 + cosh(t/2)(1 + e -l ′ ).
As a result, and using l ′ t ≥ l ′ (which follows from our hypothesis that α and α ′ meet perpendicularly for t = 0), we have

0 ≤ log l ′ t l ′ ≤ log l ′ /2 + cosh(t/2)(1 + e -l ′ ) l ′ /2 = log 1 + 2 cosh(t/2)(1 + e -l ′ ) l ′ ≤ 2 cosh(t/2)(1 + e -l ′ ) l ′ .
Now we estimate the twist parameter, using the formula for the twist in Proposition 3.1. For the purpose of the computations, we use the following notation:

A = cosh 2 (l/2) cosh 2 (t/2) (cosh(l) + cosh(l 0 /2)) -2 sinh 2 (l/2)
and B = cosh 2 (t/2) cosh 2 (l/2) + cosh(l 0 /2) + sinh 2 (l/2) cosh(l 0 /2). The quantities A and B are functions of t and l, and we have

cosh 2 (τ ′ t /2) = A B .
We shall focus on the case where l is small and t, l 0 are bounded. Consider the second order expansions near l = 0.

cosh 2 (l/2) = 1 + l 2 /4 + O(l 4 ), cosh(l) = 1 + l 2 /2 + O(l 4 ), sinh 2 (l/2) = l 2 /4 + O(l 4
). Then we have

A = 1 + l 2 /4 + O(l 4 ) × × cosh 2 (t/2) 1 + l 2 /2 + O(l 4 ) + cosh(l 0 /2) -l 2 /4 + O(l 4 ) = cosh 2 (t/2) (1 + cosh(l 0 /2)) + 3 cosh 2 (t/2) -2 + cosh 2 (t/2) cosh(l 0 /2) l 2 4 + O(l 4 )
and

B = cosh 2 (t/2) 1 + l 2 /4 + O(l 4 ) + cosh(l 0 /2) + l 2 /4 + O(l 4 ) cosh(l 0 /2) = cosh 2 (t/2) (1 + cosh(l 0 /2)) + cosh 2 (t/2) + cosh(l 0 /2) l 2 4 + O(l 4 ).
This gives

A -B = 2 cosh 2 (t/2) -2 + cosh 2 (t/2) cosh(l 0 /2) -cosh(l 0 /2) l 2 4 + O(l 4 ) = 1 4 (2 + cosh(l 0 /2)) sinh 2 (t/2)l 2 + O(l 4 ).
Note that the term O(l 4 ) in the previous formula depends on l 0 and |t| only via continuous functions of l 0 , |t|. In particular, there exists an ǫ > 0 such that for l < ǫ we have A -B ≤ Cl 2 where C is a constant that depends only on ǫ and the upper bound of l 0 , |t|.

Note that A ≥ B > 1. From this and the properties of the logarithm function we obtain log cosh 2 (τ ′ t /2) = log

A B = log A -log B ≤ A -B.
Thus, we have log cosh 2 (τ ′ t /2) ≤ Cl 2 . From the continuity of the cosh function, if |τ ′ t | is bounded, then there is a constant K that depends only on the upper bound for

|τ ′ t | such that |τ ′ t | ≤ K log cosh(τ ′ t /2). Therefore, |τ ′ t | ≤ M l
where M is a constant that depends only on the upper bound of l, l 0 , |t|.

We record the above results for the length and twist parameters in the following proposition.

Proposition 3.2. Let X be a complex structure on S 1,1 with the following properties:

(1) X has either geodesic boundary of length l 0 , or a cusp (and in the latter case we write l 0 = 0); (2) there exist a pair of perpendicular simple closed geodesics α, α ′ on X with i(α, α ′ ) = 1. Let X t be the complex structure obtained from X by performing a Fenchel-Nielsen twist of magnitude t along α. Let (l, τ t ) and (l ′ t , τ ′ t ) be the Fenchel-Nielsen coordinates of X t in the coordinate systems associated to {α} and {α ′ } respectively. (Note that l ′ 0 = l ′ .) Assume l 0 and |t| are bounded above by some constant L > 0. Then there exist constants M and ǫ 0 > 0, both depending only on L, such that for all l ≤ ǫ 0 , we have

(2) log l ′ t l ′ ≤ 2 cosh(t/2)(1 + e -l ′ ) l ′ ≤ 4 cosh(t/2) | log l| and |τ ′ t | ≤ M l.
Note that the second inequality in (2) follows from one version of the Collar Lemma, which says that there exists ǫ > 0 such that for l ≤ ǫ 0 , we have l ′ ≥ | log l|.

The effect of an elementary move on the sphere with four holes

In this section, the surface S = S 0,4 is the sphere with four holes, where each hole can be either a boundary component or a cusp. We equip S with two pair of pants decompositions {α}, {α ′ }, defined by two essential simple closed geodesics satisfying i(α, α ′ ) = 2.

Let X be a complex structure on S equipped with its intrinsic metric. Near each of the four holes, X can have a geodesic boundary, or a cusp. We denote by l 1 , l 2 , l 3 , l 4 the lengths of the boundary components (as before with the convention that l i is zero if the corresponding hole is a cusp); see Figure 2. We denote by l, τ the length and twist parameter respectively of the curve α, for the decomposition {α}, and by l ′ , τ ′ the length and twist parameter respectively of the curve α ′ , for the decomposition {α ′ }. We need a formula relating these values. Like in the case of the torus with one hole, Okai wrote such formulae in [START_REF] Okai | Effects of change of pants decompositions on their Fenchel-Nielsen coordinates[END_REF] in the case where all the holes are boundary components, and we need to see that the formulae also hold in the case where some of the holes are cusps. In the following proposition we deduce this by a continuity argument, as we did in the previous section for the case of the one-holed torus. Proposition 4.1. With the above notation we have cosh(l ′ /2) = sinh -2 (l/2){cosh(l 1 /2) cosh(l 2 /2) + cosh(l 3 /2) cosh(l 4 /2)

+ cosh(l/2) [cosh(l 1 /2) cosh(l 3 /2) + cosh(l 2 /2) cosh(l 4 /2)] + cosh(τ )[cosh 2 (l/2) +2 cosh(l 1 /2) cosh(l 4 /2) cosh(l/2) + cosh 2 (l 1 /2) + cosh 2 (l 4 /2) -1] 1/2 [cosh 2 (l/2) +2 cosh(l 2 /2) cosh(l 3 /2) cosh(l/2) + cosh 2 (l 2 /2) + cosh 2 (l 3 /2) -1] 1/2 } and cosh(τ ′ ) = {cosh 2 (l 1 /2) + cosh 2 (l 2 /2) + 2 cosh(l 1 /2) cosh(l 2 /2) cosh(l ′ /2) + sinh 2 (l ′ /2)} -1/2 {cosh 2 (l 3 /2) + cosh 2 (l 4 /2) + 2 cosh(l 3 /2) cosh(l 4 /2) cosh(l ′ /2) + sinh 2 (l ′ /2)} -1/2 {sinh 2 (l ′ /2) cosh(l/2)-cosh(l 1 /2) cosh(l 4 /2)-cosh(l 2 /2) cosh(l 3 /2) -cosh(l ′ /2)[cosh(l 1 /2) cosh(l 3 /2) + cosh(l 2 /2) cosh(l 4 /2)]}
Proof. When all the boundary lengths are positive (l 1 , l 2 , l 3 , l 4 > 0) these formulae are proved in [START_REF] Okai | Effects of change of pants decompositions on their Fenchel-Nielsen coordinates[END_REF]. To see that they also hold when some l i is zero, we proceed as in the proof of Proposition 3.1. We fix an ideal triangulation, now having 6 edges, so we have 6 shear coordinates. For i = 1 . . . 4 the length l i can be expressed as the absolute value of the sum of the shear coordinates relative to the edges adjacent to the hole involved (see [START_REF] Thurston | Three-dimensional geometry and topology[END_REF]Prop. 3.4.21]), and the cusp corresponds to the case where this sum is zero. With exactly the same argument as in Proposition 3.1 we can see that the parameters l, |τ |, l ′ , |τ ′ | can be written as continuous functions of the shear coordinates. Hence both the left hand side and the right hand side of the equations are continuous functions of the shear coordinates. As these functions are equal when l 1 , l 2 , l 3 , l 4 > 0, and as this subset is dense in the space of shear coordinates, the functions are equal everywhere, including on the set where the values l i are zero.

Like in the case of the torus with one hole, we choose X such that α and α ′ intersect perpendicularly, in order to simplify the computations. Performing a Fenchel-Nielsen twist of magnitude t along α, we obtain from X a new complex structure X t and we denote its Fenchel-Nielsen coordinates (l, τ t ) in the coordinate system associated to {α} and (l ′ t , τ ′ t ) in the coordinate system associated to {α ′ }. As before we have τ t = t. Then we also have the following proposition. Proposition 4.2. Let X be a complex structure on S 0,4 with the following properties:

(1) every hole of X is a geodesic boundary component or a cusp, with lengths denoted by l 1 , l 2 , l 3 , l 4 (with the convention that l i is zero if the corresponding hole is a cusp); ( 2) there exist a pair of perpendicular simple closed geodesics α, α ′ on X with i(α, α ′ ) = 2. Let X t be the complex structure obtained from X by performing a Fenchel-Nielsen twist of magnitude t along α. Let (l, τ t ) and (l ′ t , τ ′ t ) be the Fenchel-Nielsen coordinates of X t in the coordinate systems associated to {α} and {α ′ } respectively. (Note that l ′ 0 = l ′ .) Then, if l 1 , l 2 , l 3 , l 4 and |t| are bounded from above by some constant L, there exist constants K, M, ǫ 0 > 0, all of them depending only on L, such that for l ≤ ǫ 0 we have

(3) log l ′ t l ′ ≤ K(1 + e -l ′ ) l ′ ≤ 2K | log l| . and |τ ′ t | ≤ M l.
Proof. We note as in the case studied before that the second inequality in (3) follows from the Collar Lemma.

To prove the proposition, we use the formulae in Proposition 4.1. Setting

A = cosh(l 1 /2) cosh(l 2 /2) + cosh(l 3 /2) cosh(l 4 /2) + cosh(l/2) [cosh(l 1 /2) cosh(l 3 /2) + cosh(l 2 /2) cosh(l 4 /2)]
and

B = [cosh 2 (l/2)+2 cosh(l 1 /2) cosh(l 4 /2) cosh(l/2)+cosh 2 (l 1 /2)+cosh 2 (l 4 /2)-1] 1/2
[cosh 2 (l/2) + 2 cosh(l 2 /2) cosh(l 3 /2) cosh(l/2) + cosh 2 (l 2 /2) + cosh 2 (l 3 /2) -1] 1/2 , the formula for the length parameter l ′ becomes cosh(l ′ t /2) = sinh -2 (l/2) (A + cosh(t)B) . For t = 0, this formula becomes cosh(l ′ /2) = sinh -2 (l/2) (A + B) .

Thus, we have cosh(l ′ t /2) cosh(l ′ /2) = (A + cosh(t)B) (A + B) ≤ K,
where K is a constant that depends only on L. Using the same estimates as in Section 3, we obtain

log l ′ t l ′ ≤ 2K(1 + e -l ′ ) l ′ .
Now we estimate the twist τ ′ t . We assume that the twist is positive, to avoid taking absolute values. The formula in Proposition 4.1 gives

(4) cosh(τ ′ t ) = E F ,
where

E = sinh 2 (l ′ t /2) cosh(l/2) -cosh(l 1 /2) cosh(l 4 /2) -cosh(l 2 /2) cosh(l 3 /2) -cosh(l ′ t /2)[cosh(l 1 /2) cosh(l 3 /2) + cosh(l 2 /2) cosh(l 4 /2)] F = {cosh 2 (l 1 /2) + cosh 2 (l 2 /2) + 2 cosh(l 1 /2) cosh(l 2 /2) cosh(l ′ t /2) + sinh 2 (l ′ t /2)} 1/2 {cosh 2 (l 3 /2) + cosh 2 (l 4 /2) + 2 cosh(l 3 /2) cosh(l 4 /2) cosh(l ′ t /2) + sinh 2 (l ′ t /2)} 1/2 .
Note that E > F for all t = 0. Let E 1 = E/ sinh 2 (l ′ t /2), and F 1 = F/ sinh 2 (l ′ t /2). As l → 0, we have l ′ → ∞, and E 1 , F 1 → 1. As a result, we can assume that l is sufficiently small, so that E 1 and F 1 are not less than 1/2. Then log cosh(τ ′ t ) = log

E F = log E 1 F 1 ≤ 2(E 1 -F 1 ).
(We used the fact that log x -log y ≤ 2(x -y) for 1 2 ≤ x ≤ y.) Now we need to estimate E 1 -F 1 . To do this, note that by the first formula of Proposition 3.1, we have cosh(l ′ t /2) ≥ 8 sinh -2 (l/2).

Using the fact that sinh 2 (x) = cosh 2 (x) -1 we conclude that if l is small, there exists a constant C depending only on ǫ 0 such that

sinh(l ′ t /2) ≥ C l 2 .
First we estimate E 1 -cosh(l/2):

|E 1 -cosh(l/2)| = | -cosh(l 1 /2) cosh(l 4 /2) -cosh(l 2 /2) cosh(l 3 /2) sinh 2 (l ′ t /2) - cosh(l ′ t /2)[cosh(l 1 /2) cosh(l 3 /2) + cosh(l 2 /2) cosh(l 4 /2)] sinh 2 (l ′ t /2) | ≤ Hl 2
where H is a constant depending only on L and ǫ 0 .

Then we estimate F 1 -1:

|F 1 -1| = |{1 + cosh 2 (l 1 /2) + cosh 2 (l 2 /2) + 2 cosh(l 1 /2) cosh(l 2 /2) cosh(l ′ t /2) sinh 2 (l ′ t /2) } 1/2 {1 + cosh 2 (l 3 /2) + cosh 2 (l 4 /2) + 2 cosh(l 3 /2) cosh(l 4 /2) cosh(l ′ t /2) sinh 2 (l ′ t /2) } 1/2 -1| = |(1 + Rl 2 + O(l 4 ))(1 + Rl 2 + O(l 4 )) -1| ≤ 2Sl 2
where R and S are constants depending only on L and ǫ 0 . Then, finally:

|E 1 -F 1 | ≤ |E 1 -cosh(l/2)| + |F 1 -1| + | cosh(l/2) -1| ≤ Hl 2 + SL 2 + l 2 2 + 0(l 4 ). Now if |τ ′ t | is small, then there is a constant K such that (τ ′ t ) 2 ≤ K log cosh(τ ′ t ). (We use the formula log cosh x = x 2 /2 + O(x 4 ).) Therefore, |τ ′ t | ≤ M l.
This proves Proposition 4.2.

Comparing Fenchel-Nielsen distances

We reformulate Proposition 3.2 and Proposition 4.2 in the following.

Proposition 5.1. Let X be a complex structure on S 1,1 or S 0,4 that satisfies the assumptions in Proposition 3.2 or Proposition 4.2 respectively. Assume that |t|, l 0 (in the case where S = S 1,1 ) and l 1 , l 2 , l 3 , l 4 (in the case where S = S 0,4 ) are bounded above by some constant L. Then there exist constants K, M and ǫ 0 > 0, all depending only on L such that for l ≤ ǫ 0 , we have

log l ′ t l ′ ≤ K | log l| and |τ ′ t | ≤ M l.
For S = S 1,1 or S 0,4 , let d F N1 and d F N2 denote the Fenchel-Nielsen coordinates on T(S) associated to {α} and {α ′ } respectively. As above, for any complex structure X on S, we denote by X t the complex structure obtained by the time-t Fenchel-Nielsen twist of X along α. We have the following: Proposition 5.2. Suppose that S is either the torus with one hole S 1,1 or the sphere with four holes S 0,4 , with α and α ′ being homotopy classes of closed curves in S satisfying i(α, α ′ ) = 1 in the case S = S 1,1 and i(α, α ′ ) = 2 in the case S = S 0,4 . Then, there exist a sequence of points X n ∈ T(S) such that

d F N1 (X n , X t n ) = |t|, while lim i→∞ d F N2 (X n , X t n ) = 0.
Proof. Let X n , n = 1, 2, . . . be a sequence of complex structures on S satisfying the following properties:

(1) for any n = 1, 2, . . . the geodesics in the classes of α and α ′ intersect perpendicularly;

(2) the hyperbolic length l Xn (α) = ǫ n tends to 0 as n → ∞;

(3) the hyperbolic length of the holes of the torus with one hole S 1,1 or of the sphere with four holes S 0,4 is bounded by some fixed constant L.

It is clear that d F N1 (X n , X t n ) = |t|. By Proposition 5.1, we have

0 ≤ log l ′ t l ′ ≤ K | log ǫ n | , and
|τ ′ t | ≤ M ǫ n . As a result, d F N2 (X n , X t n ) = max{| log l ′ t l ′ |, |τ ′ t |} → 0, as ǫ n → 0.
We conclude with the following Corollary 5.3. With the notation of Proposition 5.2, the identity map between the metrics d F N1 and d F N2 is not Lipschitz. More precisely, there does not exist any constant C satisfying d F N1 (x, y) ≤ Cd F N2 (x, y) for all x and y in T(S).

General surfaces

The aim of this section is to prove Theorem 1.1, which is the analogue of Corollary 5.3 for an arbitrary surface S of finite or infinite type.

The idea is to start with an arbitrary pair of pants decomposition P = {C i } of S, to take in it an embedded subsurface of type S 1,1 or S 0,4 with boundary curves belonging to the system {C i }, and to modify the pair of pants decomposition P into a pair of pants decomposition P ′ by an elementary move α → α ′ performed inside this subsurface, according to the scheme used in Sections 3 and 4.

There is one complication in doing this. Even though in the new pair of pants decomposition P ′ the length parameters of all the non-modified curves for the complex structure X t obtained by twisting along the curve α is the same in the systems P and P ′ , the situation is not the same for the twist parameters. Performing the Fenchel-Nielsen twist along the curve α does not modify the twist parameters of the closed curves in the system P that are different from α, but in the system P ′ , the twist parameters of the curves that are on the boundary of the subsurface S 1,1 or S 0,4 do not remain constant. This is the main question that we deal with now.

Let X be a complex structure on S equipped with a geodesic pair of pants decomposition P, and let α ∈ P be a closed geodesic in the interior of X.

The closed geodesic α is either in the interior of a torus with one hole or of a sphere with four holes that is defined by the pair of pants decomposition P. We denote such a one-holed torus or a four-holed sphere by Y .

Let P ′ be the pair of pants decomposition of X obtained from P by an elementary move on α, replacing this curve with a curve α ′ which is contained in Y and which has minimal intersection number with α. We take a sequence X i of complex structures on S satisfying l Xi (α) → 0. By the collar lemma, we then have l Xi (α ′ ) → ∞.

We assume that the curve α is adjacent to two distinct pairs of pants in the decomposition P. The other case can be dealt with in the same way. We shall use the notation of Figure 3.

By Proposition 5.1, t ′ → 0 as l X (α) → 0. As a result, |τ ′ X t (C 1 ) -τ ′ X (C 1 )| → 0 as l X (α) → 0.
The case where the length of β is increased under the twist along α ′ can be dealt with by the same argument. Now we are ready to prove the various statements of Theorem 1.1. Let us summarize the setting. S is an orientable surface which is either of infinite topological type or of finite topological type with negative Euler characteristic and which is not homeomorphic to a pair of pants. Let P be a pair of pants decomposition of S. Let α ∈ P be a curve which is not a boundary component of S, and consider the pair of pants decomposition P ′ obtained from P by an elementary move about α. We denote by α ′ the curve replacing α in P ′ . Let Y be the one-holed torus or four-holed sphere containing α in its interior. If X is a complex structure on S, and t a real number, we denote by X t the structure obtained by a time-t Fenchel-Nielsen twist of X along α. Theorem 6.2. For every base complex structure X 0 on S we have T F N,P (X 0 ) = T F N,P ′ (X 0 ) as sets, but the identity map between these two spaces is not Lipschitz with respect to the metrics d F N,P and d F N,P ′ respectively. More precisely, there exists a sequence of points X n ∈ T F N,P (X 0 ) such that

d F N,P (X n , X t n ) = |t|, while lim n→∞ d F N,P ′ (X n , X t n ) = 0.
Proof. Let X n , n = 1, 2, . . . be a sequence of complex structures on S satisfying the following properties:

(1) for any n = 1, 2, . . . the geodesics in the classes of α and α ′ intersect perpendicularly; (2) the hyperbolic length l Xn (α) = ǫ n tends to 0 as n → ∞;

(3) the hyperbolic length of the boundary curves of the pairs of pants containing α and α ′ is bounded by some fixed constant L. It is clear that d F N,P (X n , X t n ) = |t|. By Proposition 5.1, there exists a constant K such that for all n

| log l X t n (α ′ ) l Xn (α ′ ) | ≤ K | log ǫ n | and |τ ′ X t n (α ′ ) -τ ′ Xn (α ′ )| ≤ Kǫ n . It follows from Lemma 6.1 that for each C j ∈ P ′ \ {α}, lim n→∞ sup Cj ∈P ′ \{α} |τ ′ X t n (C j ) -τ ′ Xn (C j )| = 0.
As a result, lim

n→∞ d F N,P ′ (X n , X t n ) = 0.
Theorem 6.3. For every base complex structure X 0 on S, consider the space T = T qc (X 0 ) ∩ T F N,P ′ (X 0 ). Then the identity map from (T, d F N,P ′ ) to (T, d qc ) is not Lipschitz. More precisely, there exists a sequence of points X n ∈ T and a constant C > 0 such that

d qc (X n , X t n ) ≥ C|t|, while lim n→∞ d F N,P ′ (X n , X t n ) = 0.
Proof. We use the same sequence as in the previous theorem. We claim that there exists a constant C, depending only on the constants L and |t|, and such that d qc (X n , X t n ) ≥ Cd F N,P (X n , X t n ) = C|t|. This essentially follows from Theorem 7.6 in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF], but some special care is needed because, in the form that theorem is stated, one of the hypotheses is not satisfied: that the surfaces X n are upper bounded, i.e. that there exists a constant M such that for every curve C ∈ P we have l X0 (C) ≤ M . This is not satisfied in general. The point is that here we are performing the twist on surfaces X n along the single curve α (while in Theorem 7.6 in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF] we allowed a multi-twist around many curves), so we only need to check that the lengths of the curves of the pairs of pants containing α are bounded by a constant. This is true in this case, because we are assuming that the lengths are bounded above by L. To apply the theorem we also need to check that the lengths d qc (X n , X t n ) are bounded above by a constant that depends only on L and |t|. This is given by Lemma 8.3 in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF], again by paying attention to the fact that, even if the surfaces are not upper bounded, we are twisting only around α, and the lengths of the boundary curves of the pairs of pants containing α are bounded by L. Now assume that S is an orientable surface of infinite topological type and let P be a pair of pants decomposition of S. We choose a sequence of curves α i ∈ P such that the one-holed tori or four-holed spheres Y i containing α i in their interior are all disjoint. We also consider another pair of pants decomposition P ′ , obtained from P by performing elementary moves about all the curves α i . For every i, let α ′ i be the curve replacing α i in P ′ . Finally, we choose a base complex structure X 0 on S satisfying the following:

(1) l X0 (α i ) → 0 as i → ∞;

(2) for all i the geodesics in the classes of α i and α ′ i intersect perpendicularly; (3) the lengths of all the curves of the decomposition P are bounded above by some global constant M . For a real number t, we denote by X i the surface obtained by a time-t Fenchel-Nielsen twist of X 0 along α i .

We have the following: Theorem 6.4. If T is the space T qc (X 0 ) ∩ T F N,P (X 0 ), then the identity map from (T, d F N,P ′ ) to (T, d F N,P ) is not continuous. More precisely, using the above notation, the surfaces X i are in T , and they satisfy d F N,P (X 0 , X i ) = |t|, while lim i→∞ d F N,P ′ (X 0 , X i ) = 0.

Proof. Assume that l X0 (α i ) = ǫ i → 0. It is clear that d F N,P (X 0 , X i ) = |t|. Applying Proposition 5.1, we have

| log l Xi (α ′ i ) l X0 (α ′ i ) | ≤ K | log ǫ i | , and |τ ′ Xi (α ′ i ) -τ ′ X0 (α ′ i )| ≤ Kǫ i ,
where K is a constant depending on M . It follows from Lemma 6.1 that for each

C j ∈ P ′ \ {α i }, lim i→∞ sup Cj∈P ′ \{αi} |τ ′ Xi (C j ) -τ ′ X0 (C j )| = 0.
As a result, lim i→∞ d F N,P ′ (X 0 , X i ) = 0. Theorem 6.5. If T is the space T qc (X 0 ) ∩ T F N,P ′ (X 0 ), then the identity map from (T, d F N,P ′ ) to (T, d qc ) is not continuous. More precisely, the surfaces X i defined above are in T , and there exists a constant C > 0 such that d qc (X 0 , X i ) ≥ C|t|, while lim i→∞ d F N,P ′ (X 0 , X i ) = 0.

Proof. As before, we claim that there exists a constant C, depending only on the constant M and on |t|, such that d qc (X i , X t i ) ≥ Cd F N,P (X i , X t i ) = C|t|. This follows from Theorem 7.6 in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF]. This time all the hypotheses of that theorem are satisfied, and we only need to check that d qc (X i , X t i ) is bounded by something that depends only on L and |t|. This is given by Lemma 8.3 in [START_REF] Alessandrini | On Fenchel-Nielsen coordinates on Teichmüller spaces of surfaces of infinite type[END_REF].

Figure 1 .

 1 Figure 1. The two curves α and α ′ intersect at one point. An elementary move replaces one of these curves by the other one.

Figure 2 .

 2 Figure 2. An elementary move on the sphere with four holes replaces one of the interior curves drawn by the other one.

  Figure 3.

NSFC grant No. 10871211.

We shall apply Proposition 4.2, and for this we assume that X is a complex structure such that l X (α) is sufficiently small. Let X t be as before the time-t twist of X along α. Then, d F N (X, X t ) = |t|.

To estimate the distance d F N ′ (X, X t ), first apply Proposition 5.1:

However, the equality τ ′ X t (β) = τ ′ X (β) is not necessarily true. Indeed, let C 1 , . . . , C 4 be the boundary components of the sphere with four holes that is the union of the two pairs of pants of P that contain α (notation of Figure 3). In the Fenchel-Nielsen coordinates of P ′ , the length of α ′ is changed under the twist along α, and for each j = 1, . . . , 4, τ ′ X t (C j ) may be not be equal to τ ′ X (C j ). However, we have the following:

For the proof, we take i = 1.

Choose a simple closed curve β as in Figure 3, contained in the 4-holed sphere that is the union of the pair of pants with boundary curves α ′ , C 1 , C 2 and the other pair of pants adjacent to C 1 , such that β satisfies i(C 1 , β) = 2 and is disjoint from any other curve in P \ {C 1 }, as in Figure 3.

We may assume that the angles at the intersection points of C 1 with β satisfy cos θ ≥ 1 2 . To achieve this we can choose a sufficiently large integer N , and replace β with its image under an N -order positive Dehn twist along C 1 .

We now apply the first variational formula of Wolpert [START_REF] Wolpert | On the symplectic geometry of deformations of a hyperbolic surface[END_REF]. For s > 0, we denote by l s (β) the hyperbolic length of β under the twist of amount s along C 1 . Denoting the intersection angles of C 1 with β by θ 1,s and θ 2,s , we have dl s (β) ds = cos θ 1,s + cos θ 2,s .

By the mean value theorem, for each s > 0, there exists a ξ ∈ [0, s], such that

Since cos θ j,s , j = 1, 2 are strictly increasing functions of s (Proposition 3.5 of Kerckhoff [START_REF] Kerckhoff | The Nielsen realization problem[END_REF]), we have

by assumption. Combining ( 5) and ( 6), we have [START_REF] Minsky | Extremal length estimates and product regions in Teichmüller space[END_REF] l s (β) -l 0 (β) ≥ s.

We show that |τ ′ X t (C 1 )-τ ′ X (C 1 )| → 0 as l X (α) → 0. Note that l X (C 1 ) = l X t (C 1 ) and β also intersects α ′ .

Suppose first that the length of β is decreased by an amount of x t > 0 under the twist of distance t

Then this length should be increased by the same amount x t under the action of the twist along C 1 . Note that x t ≤ 2|t ′ |.

Applying the inequality (7), we have


Vojtěch Řehák

Petr Slovák

Jan Strejček

‡ Loïc Hélouët

ECEASST Decidable Race Condition and Open Coregions in HMSC

Keywords: HMSC, race condition, trace-race condition, open coregions

Message Sequence Charts (MSCs) is a visual formalism for the description of communication behaviour of distributed systems. An MSC specifies relations between communication events with partial orders. A situation when two visually ordered events may occur in any order during an execution of an MSC is called a race and is usually considered as a design error. While there is a quadratic time algorithm detecting races in a finite communication behaviours called Basic Message Sequence Charts (BMSCs), the race detection problem is undecidable for High-level Message Sequence Charts (HMSCs), an MSC formalism describing potentially infinite sets of potentially unbounded behaviours. To improve this negative situation for HMSCs, we introduce two new notions: a new concept of race called trace-race and an extension of the HMSC formalism with open coregions, i.e. coregions that can extend over more than one BMSC. We present three arguments showing benefits of our notions over the standard notions of race and HMSC. First, every trace-race-free HMSC is also race-free. Second, every race-free HMSC can be equivalently expressed as a trace-race-free HMSC with open coregions. Last, the trace-race detection problem for HMSC with open coregions is decidable and PSPACE-complete. Finally, the proposed extension of coregions allows to represent in a visual fashion whether an arbitrary number of racing events in the usual MSC formalism are concurrent or not.

Introduction

Message Sequence Chart (MSC) [START_REF]ITU Telecommunication Standardization Sector -Study group 17[END_REF] is a popular visual formalism for specification of distributed systems behaviours (e.g. communication protocols or multi-process systems). Its simplicity and intuitiveness come from the fact that MSC describes only exchange of messages between system components, while other aspects of the system (e.g. content of the messages, computation steps) are abstracted away. Even such an incomplete model can indicate serious errors in the designed system. This paper focuses on a common error called race condition.

MSCs are based on composition of simple chronograms called Basic Message Sequence Charts (BMSCs). A BMSC consists of a finite number of processes and events. Processes are represented by vertical lines, and all events executed by some process are located on its lifeline and ordered from top to bottom. Messages are represented by an arrow from a sending event to a receiving event. Total orderings of events on lifelines and messages form a visual order <, which provides graphically information on the respective ordering of events. However, the visual order can not always be enforced by the architecture of the modelled system. In addition to the visual order, there exists a causal order ≪, that is weaker than <. Intuitively, events e, f are in causal order e ≪ f , if the BMSC enforces that e always precedes f . There are several definitions of causal order depending on the settings of the modelled system and semantics of the model. For example, if one process sends two messages to another process, the corresponding receive events are causally ordered if and only if the considered message transport protocol has the FIFO property: two messages sent from one process to another are always received in the same order.

In this paper, we assume that every process has one unbounded buffer for all incoming messages and that the message transport protocol satisfies the FIFO property.

A BMSC contains a race condition (or simply race) [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF] if there are two visually ordered events that are not causally ordered (i.e. they can actually occur in an arbitrary order). For example, Figure 1 depicts that the process q receives a message from r followed by a message from p. As processes and communication in BMSCs are always asynchronous, the messages can be also received in the opposite order as shown in Figure 2. In both figures, the two receive events are in race as they are ordered visually but not causally. Races in BMSC description should be considered as a design error, as they exhibit discrepancies between the intended ordering designed in a BMSC, and the ordering that a real implementation of this BMSC would enforce. Races in a BMSC can be detected in quadratic time [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF].

While a BMSC describes only a single and finite communication scenario, its extension called High-level Message Sequence Chart (HMSC) [START_REF] Rudolph | Tutorial on Message Sequence Charts[END_REF][START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF] can describe more complex interactions, with iterations and alternatives between several scenarios. An HMSC is a finite state transition system where each state is labelled by a BMSC or a reference to another HMSC. In the sequel, we will only consider HMSCs labelled by BMSCs. Each run (i.e. a path starting in the initial state and ending in a final state) of an HMSC can be understood as a single BMSC, which is a concatenation of the BMSCs labelling the states along the run. Hence, an HMSC represents a potentially infinite set of BMSCs of unbounded size.

The definition of race was extended to HMSCs in [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF]. Roughly speaking, an HMSC H has a race if some BMSC represented by H contains a race and H does not represent any BMSC where the two racing events are defined with the opposite visual order. Unfortunately, the problem whether a given HMSC contains a race is undecidable [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF][START_REF]ITU Telecommunication Standardization Sector -Study group 17[END_REF].

In this paper, we propose an alternative definition of race for HMSCs called trace-race. Intuitively, an HMSC has a trace-race if some BMSC represented by H contains a race. Clearly, ECEASST every trace-race-free HMSC is also race-free but not vice versa. To improve the expressive power of trace-race-free HMSCs, we extend the HMSC formalism with open coregions. A coregion is a standard part of the MSC formalism that allows some events on the same process in a BMSC to be visually unordered. In particular, coregions can be used to visually order only causally related events (hence making concurrency a visual property). While this application of coregions can remove all races in BMSCs, it is not sufficient for removing all races in HMSCs. An open coregion is basically a coregion spread over several BMSCs. We present a transformation of an arbitrary race-free HMSC into an equivalent trace-race-free HMSC with open coregions, where equivalence means that the two HMSCs have the same linearizations. Finally, we show that the problem whether a given HMSC with open coregions contains a trace-race is decidable and PSPACE-complete. In fact, our algorithm is polynomial for HMSCs with fixed number of processes and gates. For definitions of gates and linearizations see Sections 2 and 3, respectively.

The rest of the paper is organized as follows. Section 2 recalls the definitions of BMSCs, HMSCs, and race condition for BMSCs. The race and trace-race conditions for HMSCs are defined and compared in Section 3. Section 4 is devoted to the translation of race-free HMSCs into equivalent trace-race-free HMSCs. The decidability and complexity of the trace-race detection problem is discussed in Section 5. Section 6 briefly summarizes benefits of the presented notions. Due to the space limitations, we present only crucial lemmata and theorems accompanied by explanations of basic ideas. Proofs with all technical details can be found in [START_REF] Řehák | Decidable Race Condition for HMSC[END_REF].

Preliminaries

The following definitions omit some features of MSCs given by the ITU standard [START_REF]ITU Telecommunication Standardization Sector -Study group 17[END_REF], e.g. atomic actions, labelling of messages with names, timers etc. However, these restrictions are quite common, and our results can be extended to MSCs with atomic actions and message labelling using the technique of [START_REF] Darondeau | Products of Message Sequence Charts[END_REF].

BMSCs with (open) coregions, gates, and general ordering

The basic concepts of BMSCs are described in Section 1. In the visual representation of a BMSC, processes are depicted as vertical lines and messages are represented by arrows between these lines. Events located on the same process line are visually ordered from top to bottom. A process line may contain segments called coregions delimiting subsets of events. Events in a coregion are a priori not in visual order, but they can be visually ordered using a general ordering relation. (this relation need not be a partial order). Coregions are visually represented by rectangles and general ordering by dashed arrows between pairs of ordered events (see Figure 3).

In existing MSC formalisms, coregions are limited to finite set of events located in a single BMSC. We extend the definition of BMSCs with open coregions and gates. These features allow coregions of arbitrary size, spread over several concatenated BMSCs. Gates enable events of different BMSCs to be generally ordered within the final joined coregion. Similar ideas for connecting orders using gates or predicates was already proposed for instance in [START_REF] Pratt | Modeling concurrency with partial orders[END_REF][START_REF] Gazagnaire | Event Correlation with Boxed Pomsets[END_REF].

A coregion can be open on top (top-open coregion), on bottom (bottom-open coregion)

, or open on both sides. All processes use a common gate name space G. For each process p, we define the sets of top gates p.G = {p.g | g ∈ G} and bottom gates p.G = {p.g | g ∈ G} located on process p. Given a BMSC with a set of processes P, we set P.G = p∈P p.G and P.G = p∈P p.G to be the sets of all top and bottom gates in this BMSC, respectively. We also extend the general ordering to range over both events and gates within an open coregion.

Definition 1 Let G be a finite gate name space. A BMSC over G is a tuple M = (P, E S , E R , P, {< p } p∈P , M, C, {≺ C } C∈C ) where

• P is a finite set of processes.

• E S , E R are disjoint finite sets of send and receive events, respectively. We set E = E S ∪ E R .

• P : E → P is a mapping that associates each event with a process.

• < p is a total order on all events on a process p.

• M ⊆ (E S × E R
) is a bijective mapping, relating every send with a unique receive. We assume that a process cannot send a message to itself, i.e. P(e) = P( f ) whenever (e, f ) ∈ M. For any (e, f ) ∈ M, we use M(e) to denote the receive event f , and M -1 ( f ) to denote the send event e. • C is a finite set of pairwise disjoint coregions, where a coregion C ∈ C is a consistent nonempty subset of events and gates of a single process p, i.e.

-/ 0 = C ⊆ P -1 (p) ∪ p.G ∪ p.G for some p ∈ P -if e < p d < p f and e, f ∈ C, then d ∈ C.

Visual order, causal order and race in BMSCs

Every BMSC induces two preorders on events: visual < and causal ≪ ordering. The visual order represents the order of events directly described by the BMSC. Loosely speaking, < is the reflexive and transitive closure of total orders < p of events on each process, excluding the order of events within each coregion, plus general ordering and the order generated by the FIFO ECEASST property and the fact that every send event precedes the corresponding receive event. The visual order is actually defined over the union of events and gates.

Definition 2 Let M = (P, E S , E R , P, {< p } p∈P , M, C, {≺ C } C∈C ) be a BMSC over G. A visual order < given by M is the least preorder < ⊆ (P.G ∪ E) × (P.G ∪ E) such that

(i) < contains the relation p∈P < p C∈C C ×C ∪ ( C∈C ≺ C ) ∪ M,
(ii) < respects the FIFO property, i.e. for every e, f ∈ E S such that P(e) = P( f ) and P(M(e)) = P(M( f )), it holds that e < f implies M(e) < M( f ).1

One can define a BMSC where < is not a partial order. This situation is clearly a design error and it can be detected by a cycle detection algorithm. In the sequel, we always assume that < is a partial order.

In contrast to the visual order, the causal order captures the partial order of events that has to be respected by all executions as it is enforced by the semantics of the design. Hence, the causal order represents the interpretation of a BMSC relevant to its implementation.

Definition 3 Given a BMSC M = (P, E S , E R , P, {< p } p∈P , M, C, {≺ C } C∈C ) over G, we define a causal order ≪ as the least partial order on E such that e ≪ f , if

• (e, f ) ∈ M , i.e. send and receive events of each message are ordered, or • P(e) = P( f ) and e < f and f ∈ E S , i.e. any send event is delayed until all previous events took place, or • P(e) = P( f ) and ∃e ′ , f ′ ∈ E such that e ′ < f ′ , P(e ′ ) = P( f ′ ), (e ′ , e) ∈ M and ( f ′ , f ) ∈ M , i.e. causal order respects the FIFO property.

Lemma 1 For every BMSC it holds ≪ ⊆ <. Further, for each f ∈ E S it holds e < f ⇐⇒ e ≪ f .

A race is defined as a difference between visual and causal order on events.

Definition 4 If a BMSC contains some events e, f satisfying e < f and e ≪ f , we say that the BMSC contains a race (between events e, f ). Otherwise, the BMSC is called race-free.

Theorem 1 ([AHP96])

The problem whether a given BMSC with n events contains a race is decidable in time O(n 2 ).

Note that [START_REF] Alur | An Analyzer for Message Sequence Charts[END_REF] deals with BMSCs without any coregions. However, an extension of this theorem to BMSCs with (possibly open) coregions and general ordering is straightforward.

The following lemma says that a BMSC contains a race if and only if it contains a race between two events on the same process.

Lemma 2 A BMSC contains a race if and only if there are two events e, f such that e < f , e ≪ f , and P(e) = P( f ).

HMSCs

An HMSC is a finite directed graph with an initial state and a set of final states, where each state is labelled with a BMSC.

Definition 5 An HMSC is a tuple (S, →, s 0 , S F , L, L ) where

• S is a finite set of states, s 0 ∈ S is an initial state, S F ⊆ S is a set of final states, • →⊆ S × S is a transition relation,
• L is a finite set of BMSCs over a common gate name space, • L(s) : S → L is a mapping assigning to each state a BMSC.

A sequence of states

σ = s 1 s 2 • • • s k is a path, if (s i , s i+1 ) ∈→ for every 1 ≤ i < k. A path is a run if s 1 = s 0 and s k ∈ S F .
To give a semantics of HMSCs, we need to define a concatenation operation on BMSCs. Intuitively, the concatenation of BMSCs M 1 and M 2 is done by gluing the corresponding process lines together with the BMSC M 2 drawn beneath M 1 . If M 1 and M 2 contain bottom-open and top-open coregions on a process p, respectively, then the two coregions are merged and each bottom gate p.g of the upper open coregion is joined with the corresponding top gate p.g of the lower open coregion. Further, whenever an event e of the upper coregion is generally ordered with a joined gate and this joined gate is generally ordered with an event f of the lower coregion, the events e, f become generally ordered in the newly created coregion. The joined gates are then removed. If M 1 contains a bottom-open coregions on a process p that is not in M 2 , then the coregion remains bottom-open. However, if M 1 contains a bottom-open coregion on a process p and M 2 contains the process p without any top-open coregion on it, then the bottom side of the coregion is closed.

Definition 6 Let M i = (P i , E Si , E Ri , P i , {< ip } p∈P , M i , C i , {≺ iC } C∈C i ) for i = 1,
2 be two BMSCs over a common gate name space G and such that the sets E S1 ∪ E R1 and E S2 ∪ E R2 are disjoint (we can always rename events so that the sets become disjoint). The concatenation of M 1 and M 2 is the BMSC

M 1 • M 2 = (P 1 ∪ P 2 , E S1 ∪ E S2 , E R1 ∪ E R2 , P 1 ∪ P 2 , {< p } p∈P , M 1 ∪ M 2 , C, {≺ C } C∈C ) where < p =        < 1p if p ∈ P 1 P 2 < 2p if p ∈ P 2 P 1 transitive closure of < 1p ∪ < 2p ∪ (P -1 1 (p) × P -1 2 (p)) if p ∈ P 1 ∩ P 2
and C contains all coregions C of the following five kinds: Note that if visual orders of M 1 and M 2 are partial orders, then the visual order of M 1 • M 2 is also a partial order. Figures 4 and5 provide an example of two BMSCs and their concatenation.

1. C ∈ C 1 and C is not bottom-open or C is on a process p ∈ P 1 P 2 . We set ≺ C =≺ 1C . 2. C ∈ C 2 and C is not top-open or C is on a process p ∈ P 2 P 1 . We set ≺ C =≺ 2C . 3. C = C 1 p.G for some C 1 ∈ C 1 such that p.G ⊆ C 1 and p.G ∩ C 2 = / 0 for all C 2 ∈ C 2 , i.
M 1 • M 2 4. C = C 2 p.G for some C 2 ∈ C 2 such that p.G ⊆ C 2 and p.G ∩ C 1 = / 0 for all C 1 ∈ C 1 , i.e. C corresponds to a coregion of C 2 that is top-open but there is no matching bottom- open coregion in C 1 . We set ≺ C =≺ 2C 2 ∩ (C ×C). 5. C = (C 1 p.G) ∪ (C 2 p.G) for some C 1 ∈ C 1 and C 2 ∈ C 2 satisfying p.G ⊆ C 1 and p.G ⊆ C 2 , i.e. C
Each path s 1 s 2 • • • s k of an HMSC represents a single BMSC given by concatenation of the BMSCs assigned to s 1 , s 2 , . . . , s k , i.e. a path

σ = s 1 s 2 • • • s k represents the BMSC L(σ ) = L(s 1 ) • L(s 2 ) • . . . • L(s k ).
Hence, an HMSC represents a set of BMSCs corresponding to its runs. As an HMSC may contain a cycle, the represented set of BMSCs can be infinite and there is no bound on the size (i.e. number of events) of such BMSCs.

Race conditions in HMSCs

First we explain the idea of race conditions for a set of BMSCs. Let us consider a system where two processes p and r send a message to a third process q, that receives them in arbitrary order. This behaviour can be specified (even without any coregion) by two BMSCs depicted in Figures 1 and2. Even if both BMSCs contain a race, the specification given by this pair of BMSCs should be considered as race-free because both permutations of the two receive events on process q allowed by causal ordering are included in the specification.

The race condition for a set of BMSCs can formulated very simply using the following terminology. An execution induced by a BMSC M is a totally ordered set (E, ⊂), where E is the set of events of M and ⊂ is a linear extension of the causal order ≪ given by M. We say that such an execution (E, ⊂) corresponds to a BMSC M ′ if M ′ has the same set of events and ⊂ is a linear extension of the visual order < of M ′ . Definition 7 We say that a set of BMSCs contains a race if there exists an execution induced by some BMSC of the set and not corresponding to any BMSC of the set.

The race condition for HMSCs introduced in [MP99] follows the same principle. Unfortunately, we cannot directly say that an HMSC contains a race if it represents a set of BMSCs containing a race. The problem is that the BMSCs represented by the HMSC are constructed with the concatenation operation during which events can be renamed. Therefore, the events are replaced by labels keeping the information about sending and receiving processes. Further, the linearly ordered executions are replaced by words called linearizations.

Definition 8 Let M = (P, E S , E R , P, {< p } p∈P , M, C, {≺ C } C∈C ) be a BMSC. We define an auxiliary function label : E → {p!q, p?q | p, q ∈ P} such that label(e) = p!q if e ∈ E S , p = P(e), and q = P(M(e)) p?q if e ∈ E R , p = P(e), and q = P(M -1 (e)).

A linearization of M w.r.t. a partial order ❁∈ {<, ≪} is a word label(e 1 )label(e 2 )

• • • label(e n ) such that E = {e 1 , e 2 , • • • , e n
} and e i ❁ e j implies i < j. Moreover, we define Lin ❁ (M) to be the set of all linearizations of M w.r.t. ❁. Finally, we define linearizations of an HMSC H w.r.t. ❁∈ {<, ≪} to be the set

Lin ❁ (H) = σ is a run of H Lin ❁ (L(σ )).
Intuitively, Lin ≪ (M) represents all executions induced by M, while Lin < (M) represents all executions corresponding to M.

Definition 9 ([MP99]) An HMSC H contains a race if Lin < (H) = Lin ≪ (H).
This definition of race has several drawbacks. First of all, the problem whether an HMSC contains a race is undecidable even if we restrict the problem to HMSCs without coregions [START_REF] Muscholl | Message Sequence Graphs and Decision Problems on Mazurkiewicz Traces[END_REF][START_REF] Muscholl | Analyzing Message Sequence Charts[END_REF]. Further, as soon as we consider HMSCs with coregions, this notion of race does not tally with the definition of race for BMSCs. For example, the BMSC drawn in Figure 3 contains a race as the messages from q to r can be sent in arbitrary order while the receive events r 1 , r 2 are visually ordered. If we look at this BMSC as an HMSC with only one state, then there is no race with respect to Definition 9 as both events r 1 , r 2 are represented in linearizations by the same label r?q and therefore the information about their order is lost.

A simple definition of a trace-race follows.

Definition 10 An HMSC H contains a trace-race if there is a run σ of H such that the BMSC L(σ ) contains a race.

If an HMSC H contains no trace-race, then each of its runs σ represents a race-free BMSC L(σ ). As visual and causal orders of a race-free BMSC coincide, we get that Lin < (L(σ )) = Lin ≪ (L(σ )). Hence, every trace-race-free HMSC is also race-free. The inverse implication does not hold. For example, the race-free HMSC of Figure 6 has a trace-race (the HMSC describes the system discussed at the beginning of this section). As the definition of trace-race does not replace events by labels, trace-race tallies with the definition of race for BMSCs, i.e. a BMSC has a race if and only if it has a trace-race when seen as a single state HMSC.

It is commonly agreed that designers should avoid races in HMSCs. We provide an intuitive explanation why we think that designers should actually avoid trace-races as well. Let H be a race-free HMSC with a trace-race. As H has a trace-race, there has to be a run σ such that L(σ ) induces an execution not corresponding to L(σ ). As H is race-free, this execution corresponds to some BMSC L(σ ′ ), where σ ′ = σ is another run of H.2 Lemma 1 implies that all executions corresponding to a run are also induced by the run. Hence, the execution is in fact induced by (at least) two different runs of the HMSC. This is a potential source of errors as an implementation of this kind of description tends to violate the "write things once" programming principle. Moreover, trace-race-free HMSCs are usually more compact and their use may encourage a cleaner way for designing systems. For example, compare the trace-race-free system depicted on Figure 7, which models the same behaviour as the race-free HMSC of Figure 6.

Transformation of HMSCs into trace-race-free HMSCs

We present a transformation of an arbitrary HMSC H into a trace-race-free HMSC H ′ . The transformation modifies only BMSCs in the states of H. The modified BMSCs have the same processes, events, and causal orders as the original BMSCs, but they induce different visual orders. As the structure of H ′ remains the same, it has the same set of runs as H. The HMSC is changed in such a way that both visual and causal orders of the BMSC corresponding to a run σ in H ′ are the same as the causal order of the BMSC corresponding to σ in H. Hence, Lin < (H ′ ) = Lin ≪ (H ′ ) = Lin ≪ (H) and H ′ is trace-race-free. Moreover, if H was race-free (i.e. Lin < (H) = Lin ≪ (H)), then Lin < (H) = Lin ≪ (H) = Lin < (H ′ ) = Lin ≪ (H ′ ) and we say that H and H ′ are equivalent. The transformation of the original HMSC H proceeds in two steps.

Step 1 We modify each BMSC M in a state of H such that each process is covered with a coregion open on both sides, while BMSCs represented by the resulting HMSC remain the same as those represented by H: the same events on the same processes with the same visual and causal orders. We use general orderings and two fresh gate names pre, suc to induct the same visual (and hence also causal) orders. The definition of concatenation implies that, on a process p, all events of BMSCs preceding M in some run of H are visually ordered before all events of M (except those in a top-open coregion). This relation is preserved using the gate p.pre. Similarly, all events of M (except those in a bottom-open coregion) are visually ordered before all events of BMSCs succeeding M in some run of H. This relation is preserved using the gate p.suc.

More precisely, the general ordering ≺ C ′ of a coregion C ′ open on both sides and covering a process p is defined as the least relation satisfying the following conditions (where G ′ = G ∪ {pre, suc} and < refers to the original visual order of M):

• For every e ∈ (E ∪ p.G), f ∈ (E ∪ p.G), if e < f , then (e, f ) ∈≺ C ′ . • For every e ∈ E, if e is not in a top-open coregion in M, then (p.pre, e) ∈≺ C ′ . • For every e ∈ E, if e is not in a bottom-open coregion in M, then (e, p.suc) ∈≺ C ′ . • p.suc × (E ∪ p.G ′ ) ⊆≺ C ′ . • (E ∪ p.G ′ ) × p.pre ⊆≺ C ′ .
Step 2 We restrict the general orderings to induce visual orders equivalent to the original causal orders. Due to Definition 3, it is sufficient to generally order pairs (e, f ) such that e < f and f ∈ E S (where < refers to the original visual order). Formally, we replace every general ordering ≺ C ′ computed in the previous step with ≺ C ′ ∩ ((P.G ′ ∪ E) × (P.G ′ ∪ E s )).

Trace-race detection problem for HMSCs

This section studies decidability and complexity of the trace-race detection problem, i.e. the problem whether a given HMSC (with open coregions) contains a trace-race. We assume that each state of a given HMSC H = (S, →, s 0 , S F , L, L) appears on some run of H and it is labelled with a race-free BMSC. Recall that H contains a trace-race if and only if there is a run σ such that the BMSC L(σ ) contains a race. There is such a run if and only if there is a path π = s 0 s 1 s 2 . . . s k where L(s 0 . . . s k-1 ) is a race-free BMSC containing an event e and L(s k ) is a race-free BMSC containing an event f such that L(π) contains a race between e and f . Due to Theorem 1, one can easily check whether a given path π = s 0 s 1 s 2 . . . s k meets these conditions. However, it does not solve the trace-race detection problem as there could be infinitely many paths starting in s 0 .

Our detection technique relies on a precise characterization of races appearing in concatenation M 1 • M 2 of two race-free BMSCs. For this, we need two new functions returning sets of joined gates. Intuitively, a joined gate p.g for a concatenation M 1 • M 2 is a reference to a gate that appears as a bottom gate p.g in M 1 and is identified with the corresponding top gate p.g of M 2 during concatenation. We denote by p.G and P.G the sets all joined gates over gate name space G and the process p or all processes P, respectively. In the context of a concatenation M 1 • M 2 , ↓ (e) and ↑ (e) always refer to the values of these functions in the BMSC M i (where i ∈ {1, 2}) originally containing the event e. The characteri-

Figure 3 :

 3 Figure 1: A BMSC containing a race

A

  coregion C containing a top gate is called top-open and it has to contain all top gates p.G and satisfy that if e < p f and f ∈ C then e ∈ C. A coregion C containing a bottom gate is called bottom-open and it has to contain all bottom gates p.G and satisfy that if e < p f and e ∈ C then f ∈ C. A coregion which is both top-open and bottom-open is called just open. • ≺ C is an acyclic relation called general ordering on elements in C such that ≺ C ⊆ (p.G ∪ P -1 (p)) × (p.G ∪ P -1 (p)), where p is the process containing the coregion C. The definition says that a top-open coregion has to contain all top gates. As coregions are pairwise disjoint, there is at most one top-open coregion. Similarly, each BMSC contains at most one bottom-open coregion. Note that we do not impose that coregions contain events. For example, an open coregion covering an inactive process can connect top and bottom gates. In the visual representation, an open coregion is depicted as a rectangle without the side(s) which are open. Gates are represented by small squares on the corresponding missing side of these rectangles. As gates are always depicted in the same order, their names become redundant (and they are often omitted). For example of BMSCs with open coregions see Figure 4. Recall that dashed arrows represent a general ordering.

  e. C corresponds to a coregion of C 1 that is bottom-open but there is no matching topopen coregion in C 2 (note that C is closed on the bottom side). We set ≺ C =≺ 1C 1 ∩ (C ×C).

Figure 4 :

 4 Figure 4: BMSCs M 1 (upper) and M 2 p q r s

Figure 6 :

 6 Figure 6: An race-free HMSC with a trace-race

Definition 11

 11 Given a BMSC M = (P, E S , E R , P, {< p } p∈P , M, C, {≺ C } C∈C ) over gate name space G, we define two functions ↓ (), ↑ () : (E S ∪ E R ) → 2 P.G as ↓ (e) = {p.g ∈ P.G | e < p.g} and ↑ (e) = {p.g ∈ P.G | p.g < e}.

Proc. GT-VMT 2010

The FIFO property is usually not included in the definition of a visual order. However, once we choose the FIFO message passing setting, violating this property should be considered as a design error and it can be easily detected. Hence, we included the property directly in our definition.5 / 12Volume

(2010)

Volume 29 (2010)

In fact, the linearization corresponding to the mentioned execution has to be in Lin < (L(σ ′ )).9 / 12Volume 29 (2010)

Acknowledgements: We would like to thank Philippe Darondeau for an important hint.

Bibliography

supported by Czech Science Foundation (GA ČR), grants No. 201/08/P459 and No. P202/10/1469. † Partially supported by the research centre "Institute for Theoretical Computer Science (ITI)", project No. 1M0545. ‡ Partially supported by Czech Science Foundation (GA ČR), grant No. 201/08/P375, and Ministry of Education of the Czech Republic, project No. MSM0021622419.

/ 12

Volume 29 (2010)

ECEASST zation of races in M 1 • M 2 is formulated in Lemma 3. The lemma assumes that the two race-free BMSCs M 1 , M 2 are in the special form of Section 4, where all events and gates on each process are covered by a coregion open on both sides. Note that every BMSC can be converted to this form by the first step of the transformation presented in the previous section.

Lemma 3 Let M 1 • M 2 be a concatenation of two race-free BMSCs M 1 , M 2 in the special form, e be an event of M 1 , and f be an event of M 2 such that P(e) = P( f ) = p. Then e and f are in race if and only if all the following conditions hold.

The precondition P(e) = P( f ) is not a serious restriction thanks to Lemma 2. The characterization says that to decide whether an event e of M 1 is in race with some event of M 2 , one needs to know only label(e), ↓ (e) and, if e is a receive action, then also ↓ (M -1 (e)). Triples (label(e), ↓ (e), ↓ (M -1 (e))) for receive events e and (label(e), ↓ (e), / 0) for send events e are called footprints of M 1 . Note that the number of footprints for a fixed set of processes P and a gate name space G is bounded by 2

Extending function P to labels as P(p!q) = P(p?q) = p, Lemma 3 can be reformulated as follows:

Lemma 4 Let M 1 and M 2 be two race-free BMSCs in the special form. The concatenation M 1 • M 2 contains a race if and only if there is a receive event f in M 2 and a footprint (l, F, F ′ ) of M 1 such that all the following conditions hold.

Now we return to the observation from the beginning of this section. Let s, s ′ be two states of the HMSC H such that (s, s ′ ) ∈→. If we have the set of footprints of all BMSCs of the form L(π) where π is a path leading from s 0 to s, we are able to decide whether any concatenation L(π) • L(s ′ ) contains a race. Moreover, we can effectively compute the set of footprints of all BMSCs of the form L(π).L(s ′ ).

Hence, with each state s of the HMSC H we associate the set of all footprints of all BMSCs corresponding to paths starting in s 0 and leading to s. These sets of associated footprints can be easily computed using the fixpoint approach. If no race is detected during the computation, then the HMSC is trace-race-free. The precise algorithm, its complexity analysis, and complexity analysis of the trace-race detection problem can be found in [START_REF] Řehák | Decidable Race Condition for HMSC[END_REF].

with open coregions and gates) over a gate name space G, the problem whether H contains a trace-race is decidable in time

, where b is the size of the largest BMSC in L. Hence, the problem is in P if the number of processes and gates is fixed.

Theorem 3 The trace-race detection problem is PSPACE-complete.


E Mueller

M Haim

T Petnehazy

M Acham-Roschitz

Trop

M Trop

An innovative local treatment for staphylococcal scalded skin syndrome

Abstract Staphylococcal scalded skin syndrome (SSSS) is the clinical term used to describe a range of blistering skin disorders induced by the exfoliative toxins of Staphylococcus aureus and prevalently affects neonates, infants and toddlers who lack antibodies to S. aureus toxins. SSSS is a highly contagious disease and is characterised by erythema and fever, followed by the formation of large fragile superficial blisters, which rupture only to leave extensive areas of denuded skin. A diagnosis of SSSS relies on the clinical picture, as well as on histological and microbiological findings. Neonates and young infants are particularly susceptible to a lack of the protective skin barrier, which may cause excessive protein and fluid losses, hypothermia and secondary infection. Due to a complete denudation of skin, the patients also suffer from almost unbearable pain. In our communication, we present an innovative temporary coverage of the denuded skin with Suprathel® (PolyMedics Innovations GmbH, Denkendorf, Germany). Suprathel® relieves pain, prevents heat loss and secondary infection, accelerates wound healing, does not need to be changed and makes daily care easy for the nurses and is well tolerable for the patient.

In 1878, Baron Gottfried Ritter von Rittershain [START_REF] Ritter Von Rittershain | Die exfoliative dermatitis jüngerer Säuglinge[END_REF] described a remarkable type of disease in the newborn and named it "dermatitis exfoliativa", which was, thereinafter, referred to as "Ritter's disease". The aetiology of the disease was not known to him and von Rittershain believed devoutly that dermatitis exfolitiva was not contagious. In 1970, Melish and Glasgow [START_REF] Melish | The staphylococcal scalded-skin syndrome: development of an experimental model[END_REF] discovered the aetiological agent for Ritter's disease to be phage Group 2 coagulase-positive staphylococci and reproduced the skin lesions using cultured supernatant strain TA (phage type 71, Group 2) in a neonatal mouse model. They called this disease entity staphylococcal scalded skin syndrome (SSSS). The clinical term SSSS is used to describe a range of blistering skin disorders induced by the exfoliative toxins (ETs) of Staphylococcus aureus. ETs are spread haematogenously from a localised source and, in the absence of specific antitoxin antibodies, cause widespread epidermal damage. In 2008, Nishifuji et al. [START_REF] Nishifuji | Staphylococcal exfoliative toxins: "molecular scissors" of bacteria that attack the cutaneous defense barrier in mammals[END_REF] described the ETs' action and coined the term "molecular scissors". Virulent strains of the bacteria produce ETs that cause the loss of keratinocyte cell-cell adhesion in the superficial epidermis. The three isoforms of ETs, i.e. ETA, ETB and ETD, are glutamate-specific serine proteases that specifically and efficiently cleave a single peptide bond in the extracellular region of human and mouse desmoglein1 (Dsg1), a desmosomal intercellular adhesion molecule. Staphylococcal exfoliative toxins act as "molecular scissors" to facilitate percutaneous bacterial invasion by cleavage of keratinocyte cell-cell adhesion molecules. ETB-producing S. aureus is the predominant isolate in generalised SSSS and its ETs show species specificity for Dsg1 cleavage. SSSS prevalently affects neonates, infants and toddlers who lack antibodies to S. aureus toxins; only 41% of children aged 2 to 5 years but 91% of adults older than 40 years have antibodies against ETA. SSSS is a highly contagious disease and is characterised by erythema and fever, followed by the formation of large fragile superficial blisters, which rupture to leave extensive areas of denuded skin. In the generalised form, fluid from intact bullae is generally sterile and the infecting strain is usually recovered from distant sites, such as the throat and/or nose. Renal function plays a critical role in determining susceptibility to the generalised form of the disease in neonates and in adults [START_REF] Cribier | Staphylococcal scalded skin syndrome in adults. A clinical review illustrated with a new case[END_REF]. The diagnosis of SSSS relies on the clinical picture as well as on histological and microbiological findings. Histopathologically, SSSS is marked by keratinocyte detachment in the superficial layers of the dermis and intra-epidermal blistering without induced keratinocyte necrosis [START_REF] Nishifuji | Staphylococcal exfoliative toxins: "molecular scissors" of bacteria that attack the cutaneous defense barrier in mammals[END_REF].

We report the case of a male infant who had to stay in hospital since birth due to different congenital malformations resulting in major illnesses. The boy was delivered by caesarean section at 36 weeks of gestation because of oligohydramnios. Postpartum, a left lower limb deformity consisting of tibial and distal femoral aplasia, club foot and mirror foot was observed. He had multiple vertebral anomalies at different levels of the spine. Prenatally, he showed renal agenesis of the right kidney and hydronephrosis of the contralateral kidney. At 4 days of age, the patient developed a renal insufficiency with elevated serum creatinine concentration and was taken to surgery for decompression of the obstructed urinary system by percutaneous nephrostomy and insertion of a left nephrostomy tube. Due to the chronic renal insufficiency, he suffered from hypocalcaemia, hyperkalaemia, hyperphosphataemia, secondary hyperparathyroidism and renal anaemia. At 5 days of age, his abdomen had become distended and he began vomiting bilestained fluid. An exploratory laparotomy was performed, which revealed a perforated ascending colon and an ileostomy was fashioned. Due to an interoperatively determined small bowel length of 60-85 cm and the fact that he demonstrated failure to thrive, he was diagnosed with congenital short bowel syndrome. At the age of 5 weeks, the patient again showed features of an acute abdomen and was taken to surgery for re-operation. A resection of part of the small intestine, a resection of part of the large intestine and a reduction of an intussusception were performed. A third laparotomy conducted at the age of 6 weeks showed a stenosis of the rectosigmoid junction. A double-barrel colostomy of the sigmoid colon was performed. At the age of 3 months, he underwent a colostomy reversal to rejoin the colon. Because the patient refused any food, a percutaneous endoscopic gastronomy (PEG) tube was inserted at the age of 11 months. The main problem regarding nursing care was severe diaper dermatitis with ulceration caused by intractable diarrhoea (at least ten stools a day) as a result of the combination of the short bowel syndrome and the renal insufficiency. The diaper dermatitis proved to be intractable to any local treatment. Microbiological analysis of the diaper area (specifically, the anus) repeatedly showed the presence of Escherichia coli, Enterobacter cloacae, Klebsiella pneumoniae and Enterococcus faecalis, as well as S. aureus.

At the age of 14 months, the boy suddenly developed fever, malaise and was more irritable than usual due to the discomfort of his persistent diaper dermatitis-although he was on permanent pain therapy. During routine night time care, a nurse spotted an erythematous rash on the skin of the trunk and facial area. Within only a few hours, the rash spread on the tender and painful skin and small flaccid bullae erupted. The patient was given an antibiotic (Cefuroxim) intravenously, increased parenteral fluid support and was transferred to the children's burns unit. The next morning the patient was taken to the operating room (OR). Under anaesthesia large sheets of epidermal detachment were removed and swabs taken (which remained sterile) (Fig. 1). The total body surface area affected was more than 50%. Mucous membranes and nails were not affected. Nikolsky's sign was positive. On the cleaned, oozing superficial red wounds, Suprathel® (PolyMedics Innovations GmbH, Denkendorf, Germany) was applied; above it, one layer of paraffin and absorbent gauze, secured with an elastic netting (Figs. 2 and3). The next day, the wound check in the OR revealed new lesions all over the body, so that, in the end, 90% total body surface area was affected after 36 hours (Figs. 4 and5). Suprathel® wound dressing was extended to the whole body with the exclusion of the genital region due to the frequent loose stools. Since SSSS is toxin-mediated, the lesions may continue to appear for 24-36 hours after the start of the antibiotic treatment. Any Suprathel® that became dislodged or any new areas of SSSS that developed after the first application were covered with new Suprathel®. With Suprathel® in place, the patient's pain dramatically decreased and the wounds needed no further treatment. Skin biopsy was obtained from the right flank and the histological examinationshowing mid-epidermal cleavage with minimal inflamma- With Suprathel® treatment as a whole-body dressing, the blister formation subsided and complete resolution occurred within five days, without scarring (Figs. 6 and7). The patient was transferred back to the Department of Neonatology after seven days at the paediatric burns unit. The intravenous antibiotic therapy was continued for a total course of 14 days.

Since the aetiology of SSSS has been known and antibiotics have been available, systemic antibiotic therapy has become a standard treatment. In severe cases, intravenous therapy with anti-staphylococcal antibiotics is required. In patients with initial therapeutic failure using conventional antibiotics, one should not forget the possibility of methicillin-resistant S. aureus (MRSA) involvement. Topical antibiotics in generalised SSSS are often not effective, since the focus of infection is usually not known and often distant from the site of blistering. They should also be avoided due to unpredictable absorption through denuded skin. Silver sulfadiazine, which is still used in some burns units, is not recommended for SSSS because of enhanced systemic absorption through denuded skin [START_REF] Murray | Recognition and management of Staphylococcus aureus toxin-mediated disease[END_REF]. Steroids are contraindicated on the basis of both experimental and clinical evidence [START_REF] Ladhani | Clinical, microbial, and biochemical aspects of the exfoliative toxins causing staphylococcal scalded-skin syndrome[END_REF]. In addition to the antibiotic management strategy, about which there is no controversy, there is a vast consensus that patients with Fig. 4 Wound check on the second day: Suprathel® became transparent and adheres well to the wounds Fig. 3 Complete temporary coverage of the denuded skin with Suprathel®, a layer of paraffin and absorbent gauze secured with elastic netting Fig. 2 Suprathel® was applied on the cleaned red wounds Fig. 5 New lesions appeared on day two severe blistering skin diseases are better managed in burns units. Burns units have a number of specialised facilities and a team trained in dealing with all aspects of major burns [START_REF] Sheridan | The burn unit as a resource for the management of acute nonburn conditions in children[END_REF]. Core temperature and room temperature need to be monitored carefully, as thermal dysregulation is common; even though the patient is febrile, peripheral vasodilatation adds to loss of heat and may cause a drop in the core temperature. Despite the burn-like appearance of SSSS, massive fluid resuscitation is not required since the massive burn oedema, which develops after thermal injury, does not appear in SSSS. Pain management and local skin care represent the major challenges in SSSS. The choice of analgesia must be based on the needs of the patient and opiates are preferred. Selecting the proper wound dressing helps to alleviate pain remarkably-but skin care in generalised SSSS is the most divergently discussed topic. Lowney et al. [START_REF] Lowney | The scalded skin syndrome in small children[END_REF] recommend general measures: "the skin must be treated gently and kept clean." Margileth [START_REF] Margileth | Scalded skin syndrome: diagnosis, differential diagnosis, and management of 42 children[END_REF] states:

"Topical therapy includes manual removal of denuded skin, using aseptic technique two or three times daily. Patients with extensive (over 50%) denuded skin might be treated as burn patients using continuous 0.5% silver nitrate compresses for several days." Elias et al. [START_REF] Elias | Staphylococcal scalded skin syndrome. Clinical features, pathogenesis, and recent microbiological and biochemical developments[END_REF] used cool, continuous wet dressings with 0.5% silver nitrate alternating with the application of mafenide acetate or sulfadiazine silver cream. Simpson [START_REF] Simpson | The management of staphylococcal scalded skin syndrome in infants[END_REF] advocates: "The child should be nursed in a warm environment with minimal clothing. An emollient, such as a 50:50 mix of white soft paraffin and liquid paraffin, may be applied to lesions to reduce fluid loss and soothe the area." Patel [START_REF] Patel | Treatment of staphylococcal scalded skin syndrome[END_REF] suggests: "Blisters should be left intact and eroded skin treated with emollients or covered with Vaseline impregnated gauze to maintain skin barrier function, as well as reduce further skin trauma." Blyth et al. [START_REF] Blyth | Severe staphylococcal scalded skin syndrome in children[END_REF] advises: "Sterile dressings are required and these should be applied in theatre initially to minimise the pain involved and to reduce the infection risk. Daily theatre changes of dressings are required until recovery starts."

In our case, the main focus of attention at the burns unit was given to the denuded skin and the subsequent implications of such a large wound area. We used Suprathel® in this patient as a wound cover. Suprathel®, a newly developed wound dressing, is produced from a synthetic copolymer consisting mainly of DL-lactide (>70%), trimethylene carbonate and ε-caprolactone. It represents a synthetic dressing that imitates the properties of natural epithelium and consists of a membrane with 80% porosity. Pore sizes vary between 2 and 50 μm. Its moisture permeability prevents the accumulation of wound fluid, supporting wound healing and re-epithelisation. It is also permeable to oxygen. During the course of reepithelisation, the membrane becomes transparent, allowing the evaluation of the wound bed without manipulation of the wound dressing itself. Suprathel® can be quite simply adapted to any body part and does not hinder the patient's mobilisation and comfort. Mechanical alteration is avoided by the spontaneous attachment due to the adsorption of wound secretion. Suprathel® as a material itself may be costly prima facie (1 cm 2 costs 50 to 60 cents); however, comparing the overall treatment cost to a material which needs daily dressing changes and causes painful discomfort for the patient reveals a reduction of costs overall. We use Suprathel® in children with superficial and deep dermal burns with good results. The clinical studies in burn patients confirmed the promotion of re-epithelisation, minimisation of pain, reduction of patient discomfort and cost-effectiveness [START_REF] Uhlig | Suprathel-an innovative, resorbable skin substitute for the treatment of burn victims[END_REF][START_REF] Schwarze | Suprathel, a new skin substitute, in the management of partial-thickness burn wounds: results of a clinical study[END_REF]. Taking these qualities into account, the wound dressing Suprathel® should be introduced into the field of acute non-burn conditions in children as well, because the local treatment with Supra-thel® in SSSS relieves pain, prevents heat loss and secondary infection, accelerates wound healing, does not Fig. 7 Skin lesions are healed completely on day five Fig. 6 Day five: Suprathel® peels away and can be easily removed with any emollient need to be changed and, hence, makes daily care easy for the nurses and is well tolerated by the patient. This is also the first case report where Suprathel® has been used as a whole-body dressing for local treatment in SSSS.

We browsed the literature for relevant references about where and how to treat skin lesions in patients with generalised SSSS, and frequent recommendations to treat severe cases in burns units were found. Recommendations on how to treat skin lesions differ enormously from very general to very specific. From the published references, the impression emerges that wound handling is usually painful, the dressing procedures may have to be repeated several times a day, recommended cool and wet dressings enhance the danger of hypothermia and when silver dressings have been used, silver absorption is uncontrollable. The handling of the patient is far from easy for the nursing staff and unpleasant and dolorous for the patient. With complete temporary coverage of the denuded skin with Suprathel®, a layer of paraffin and absorbent gauze secured with elastic netting, a whole-body dressing is created. The handling of the patient in question was easier, hypothermia did not occur and the nurses' acceptance of the whole-body dressing was outstanding.

Fig. 1

 1 Fig. 1 Sheets of epidermal detachment on the patient's back and diaper dermatitis as presented at the first admission to the operating room

Eur J Clin Microbiol Infect Dis (2010) 29:893-897

Conflict of interest

The authors indicate that they have no financial relationships to this article to disclose and they do not have any relationship to the manufacturer of the described dressing.