Chris Worman

Boting Yang

On the Tileability of Polygons with Colored Dominoes

Keywords: Domino tiling, Colored domino tiling, Wang tiles, 2-SAT, NP-complete, Orthogonal polygons

We consider questions concerning the tileability of orthogonal polygons with colored dominoes. A colored domino is a rotatable 2 × 1 rectangle that is partitioned into two unit squares, which are called faces, each of which is assigned a color. In a colored domino tiling of an orthogonal polygon P , a set of dominoes completely covers P such that no dominoes overlap and so that adjacent faces have the same color. We demonstrated that for simple orthogonal polygons that can be tiled with colored dominoes, two colors are always sufficient. We also show that for tileable non-simple orthogonal polygons, four colors are always sufficient and sometimes necessary. We describe an O(n) time algorithm for computing a colored domino tiling of a simple orthogonal polygon, if such a tiling exists, where n is the number of dominoes used in the tiling. We also show that deciding whether or not a non-simple orthogonal polygon can be tiled with colored dominoes is NP-complete.

Introduction

We study a computational tiling problem where the tiles model the commonly used domino game piece. We consider tiling orthogonal polygons with so-called colored dominoes, which are rotateable 2 × 1 rectangles that are partitioned into two colored faces. The colors on the domino faces are used to restrict how the dominoes can be positioned: when the faces of two dominoes are positioned next to each other in a tiling, their colors must coincide. Colored dominoes are similar to Wang tiles (1; 13; 9; 20; 4), which are unit squares with colored sides. Wang tiles find application in DNA computing (1; 13) and image processing (7; 11).

Many variants of domino tiling problems have been studied, but most of the results have focused on "colorless" dominoes, which are simply 2 × 1 rotateable rectangles (see, for example, (14; 8; 18; 16; 17; 10; 19)). Results concerning colored domino tilings have only arisen relatively recently (21; 5; 22; 23). In the colored domino tiling problems studied in [START_REF] Worman | Tiling layouts with dominoes[END_REF] and [START_REF] Biedl | The complexity of domino tiling[END_REF], a multiset of dominoes is provided, and in tilings the multiplicity of the dominoes cannot exceed those in the multiset. In [START_REF] Worman | Tiling layouts with dominoes[END_REF], the multiplicity of the provided dominoes equals that of the multiplicity of the dominoes used in the tiling. An algorithm is described for computing colored domino tilings of so-called "paths" or "cycles". This algorithm runs in time linear in the number of dominoes used in the tiling. The authors of (21) also consider a colored domino tiling problem where some dominoes have already been positioned on the polygon, and we are asked to decide if the tiling can be completed. This problem is shown to be NP-complete. In [START_REF] Biedl | The complexity of domino tiling[END_REF], Biedl studies two variants of a domino tiling problem. In the first problem, known as EXACT DOMINO TILING, the multiplicity of dominoes in the provided set is equal to multiplicity of the dominoes used in the tiling. Biedl shows that EXACT DOMINO TILING is NP-complete, even for a very restricted class of polygons known as "caterpillars". It is also shown that EXACT DOMINO TILING remains NP-complete when the dominoes are restricted to three colors. In the second domino tiling problem studied in [START_REF] Biedl | The complexity of domino tiling[END_REF], which is called PARTIAL DOMINO TILING, not all the dominoes are used in the tiling. It is shown that PARTIAL DOMINO TILING is NP-complete, and remains so even for so-called "paths" or "cycles". It is also shown that PARTIAL DOMINO TILING is NP-complete when the dominoes are restricted to three colors. We also note the result by Beauquier et. al. [START_REF] Beauquier | Tiling figures of the plane with two bars[END_REF], which proves the NP-completeness for deciding the tileability of a polygon with holes for non-colored dominoes.

In the problems that we study, the set of dominoes used is not a multiset, and each domino has 2 colors and can be used an unlimited number of times. Thus we are concerned with questions related to the following: "Does there exist a set of colored dominoes that can tile a given orthogonal polygon P ?"

We demonstrate that for simple orthogonal polygons that can be tiled with colored dominoes, two colors are always sufficient. We also show that for tileable non-simple orthogonal polygons, four colors are always sufficient and sometimes necessary. We also describe an O(n) time algorithm for computing a colored domino tiling of a simple orthogonal polygon, where n is the number of dominoes used in the tiling. We also show that deciding whether or not a non-simple orthogonal polygon can be tiled with colored dominoes is NP-complete.

Definitions

A colored domino is a rotatable 2 × 1 rectangle that has been partitioned into two colored unit squares, which we refer to as the faces of the colored domino. A colored domino is deemed a twin if it is monochromatic. Since all dominoes considered herein will be colored, we will often refer to "colored dominoes" simply as "dominoes". All polygons that we consider are orthogonal polygons with integer coordinates. We adopt terminology similar to that found in (21; 5), and refer to such polygons as layout polygons. A polygon is deemed simple if it does not contain holes. We refer to the set of unit squares induced by the integer grid within a layout polygon P as the squares in P , which are denoted by ρ(P ). We deem two squares p, q ∈ ρ(P ) to be adjacent if p shares an edge with q. A tiling is a placement of dominoes from a set D of dominoes onto a layout polygon P such that each square in ρ(P ) is covered by exactly one domino face and adjacent faces of dominoes have the same color. We say that p, q ∈ ρ(P ) are matched under a tiling if p and q are covered by the same domino in the tiling. A tiling of a layout polygon P therefore induces a perfect matching of ρ(P ).

Suppose there exists a colored domino tiling τ of a layout polygon P that uses k colors. We can immediately see that there must also exist a colored domino tiling of P that uses 1 color since we can simply re-color the faces of all the dominoes in τ to be black. This observation is unsatisfying since the colors on the dominoes becomes irrelevant. Since we are interested in tilings that use colored dominoes, we must disallow twin dominoes. Thus we are only concerned with tilings that do not use twin dominoes. Motivated by this restriction, we define D k for k ≥ 2 as follows: D k is the set of Next we introduce the main tools that we use to analyze colored domino tilings. The following concept will be used extensively throughout the remainder of the paper: Definition 2.3 Twin-Forcing Arrangement: Let P be a layout polygon with a perfect matching M of ρ(P ). A twin-forcing arrangement is a set of four squares p, q, r, s ∈ ρ(P ) contained in a 2 × 2 subrectangle of P , such that p and q are adjacent and matched with each other, while r and s are adjacent, but r is not matched with s.

One can easily show that a twin-forcing arrangement is forbidden in layout polygons that are k-tileable for k ≥ 2 since p and q must be covered with a twin domino. Next we introduce the concepts of leaves and corners in layout polygons. Definition 2.4 Leaf: Let L be a 2 × 1 subrectangle of P . Then L is a leaf of P if L contains a square p such that p is adjacent to exactly one square in ρ(P ). Definition 2.5 Corner: Let C be a 2 × 2 subrectangle of P . Then C is a corner of P if C contains a square p such that p is adjacent to only two other squares in ρ(P ).

The following two Lemmas about leaves and corners will be essential to our algorithm, and will also be useful when we obtain lower bounds on the number of colors needed to tile a non-simple layout polygon. Lemma 2.6 Let P be a k-tileable layout polygon for k ≥ 2 that contains a leaf L. In any k-tiling of P there is only one domino that covers L.

Proof: Let L be a leaf from a layout polygon P that contains the squares p and q. W.l.o.g, suppose p is only adjacent to q. In any tiling p is matched to an adjacent square, and since p is only adjacent to q, the domino that covers p must also cover q, as required. ✷ Lemma 2.7 Let P be a k-tileable layout polygon for k ≥ 2 that contains a corner C. In any k-tiling of P there are only two dominoes that covers C.

Proof: Let C be any corner from a layout polygon P . Since C is a 2 × 2 rectangle, it must contain exactly 4 squares. We will refer to these squares as p i , p j , p k , p l , where p i is only adjacent to p j and p k . Since p i is only adjacent to p j and p k , p i must be matched with either p j or p k in a tiling of P . W.l.o.g, we can suppose that p i is matched with p j . If p k is matched with p l then we have our result, so for the sake of contradiction suppose that p k is not matched with p l . Then p i , p j , p k , and p l form a twin-forcing arrangement, which is a contradiction. ✷

A key observation about leaves and corners is their existence in simple layout polygons.

Fig. 1: A non-simple layout polygon that does not contain a leaf or a corner.

Lemma 2.8 If P is a simple layout polygon such that |ρ(P )| ≥ 2, then P contains a leaf or a corner.

Proof: Let p be a square from ρ(P ) that is incident with a convex vertex v of P . Then p is adjacent to at most two other squares from ρ(P ), and p must be adjacent to at least one other square since |ρ(P )| ≥ 2.

If p is only adjacent to one other square from ρ(P ), then p is part of a leaf, and the Lemma follows. So suppose p is adjacent to two other squares, say p i and p j . If p i and p j are both adjacent to a common neighbor that is not p, then p is part of a corner, and the Lemma follows.

So assume that p is the only common neighbor of p i and p j . Thus one vertex of p is a convex vertex of P , and another vertex of p is a concave vertex of P . Now assume there is no leaf or corner. For each convex vertex of P we can associate a unique concave vertex. Let c and r be the number of convex and concave (i.e. reflex) vertices in P , respectively. Then we have that c ≤ r. Since it can easily shown that for any simple orthogonal polygon c > r, we arrive at a contradiction and the Lemma follows. ✷

Notice that Lemma 2.8 only holds for simple layout polygons. Figure 1 illustrates a non-simple layout polygon that does not contain a leaf or a corner.

The next set of definitions provide a connection between graph coloring and colored domino tiling. If P is a layout polygon that has been tiled with colored dominoes, then we refer to the color of the domino face that is covering the square p ∈ ρ(P ) as color(p). Definition 2.9 Color Partition: Let P be a k-tileable layout polygon, and let τ be a k-tiling of P . We define the color partition of P with respect to τ to be a partition P 1 , P 2 , ..., P m of P , such that P i is a maximal connected set of like-colored squares, for i = 1, 2, ..., m.

The following Lemma will be useful when we consider tiling simple layout polygons.

Lemma 2.10 For any k-tileable simple layout polygon P with a k-tiling τ , the color partition P 1 , P 2 , ..., P m implied by τ is such that P i is a simple polygon for each 1 ≤ i ≤ m.

Proof: For the sake of contradiction, suppose P i is not a simple polygon, i.e. suppose that P i contains a hole H. Let u 1 , u 2 , u 3 be three consecutive vertices along the boundary of H such that u 2 is a reflex vertex with respect to P i . Let p 1 , p 2 ∈ ρ(P i ) be such that p 1 has the edge u 1 u 2 , while p 2 has the edge u 2 u 3 . Let p be a square in H such that p has edges u 1 u 2 and u 2 u 3 . Since P is a simple polygon, we know that p ∈ ρ(P ). Then we have color(p) = color(p 1 ) and color(p) = color(p 2 ) by Definition 2.9. Note that for each pair of adjacent squares with different colors, they must be matched in τ . Thus, p is matched with p 1 and p 2 . This contradicts the fact that there is no overlapping dominoes in a k-tiling. ✷ Definition 2.11 Color Partition Graph: Let P 1 , P 2 , ..., P m be the color partition associated with a ktiling τ of a k-tileable layout polygon P . We define the color partition graph to be a graph with vertices v 1 , v 2 , ..., v m . There is an edge (v i , v j ), i = j, in the color partition graph if the partitions P i and P j share an edge on their boundaries.

Notice that if we color the nodes of a color partition graph G according to the colors of the corresponding color partitions, then we have a proper k-coloring of G. Likewise, a k-coloring of G defines a k-tiling of the original polygon. Thus a k-coloring of a color partition graph corresponds exactly to a k-tiling. This is the key observation that is exploited in the following section.

Colored Domino Tilings and Graph Coloring

In this section we obtain tight bounds on the number of colors needed to tile simple and non-simple layout polygons.

Definition 3.1 Chromatic Number of P :

The chromatic number of a layout polygon P , denoted χ(P ), is the minimum number k ≥ 2 for which P is k-tileable.

We begin by describing a simple result that will be useful in obtaining forthcoming results. Lemma 3.2 In any k-tiling of a layout polygon P , each vertex of any square in ρ(P ) is incident with at most 2 different colors.

Proof: Since the Lemma obviously holds for k ≤ 2, suppose k ≥ 3. Suppose that v is a vertex of some square in ρ(P ) which is incident with at least 3 different colors. Let p 1 , p 2 , p 3 ∈ ρ(P ) be three squares which are incident with v and have 3 different colors respectively. Without loss of generality, suppose that p 1 is adjacent to p 2 and p 3 . Note that for each pair of adjacent squares in ρ(P ) with different colors, they must be matched in the k-tiling. Thus, p 1 is matched with p 2 and p 3 . This contradicts the fact that there are no overlapping dominoes in a tiling. ✷ Lemma 3.3 If P is a k-tileable simple layout polygon with a k-tiling τ , for k ≥ 2, then the color partition graph G associated with τ is a tree.

Proof: Since P is a simple layout polygon, it is easy to see that G is connected. Suppose that G has a cycle v 1 v 2 ...v a v 1 , 3 ≤ a ≤ m. Let P ′ be the union of P 1 , P 2 , ..., P a . Now we use Lemma 3.2 to show that there must exist a hole H in P ′ which encloses at least one square. Let x 1 and x 2 be the extreme points on the boundary between P 1 and P 2 (refer to Figure 2(a)). Consider the path v 2 , v 3 , ..., v a , v 1 implied by the cycle in G (see Figure 2(b)). Notice that the parts along this path, i.e. P 2 , P 3 , ..., P a , P 1 , enclose either x 1 or x 2 . Let x i ∈ {x 1 , x 2 } be the point enclosed by this path. Assuming that P ′ does not contain a hole, x i must be incident with at least one square that is not contained in either P 1 or P 2 . We have two cases to consider.

Firstly, it may be the case that x i is incident with two squares s 1 , s 2 ∈ P 1 ∪ P 2 (ex. x 1 from Figure 2(b)). W.l.o.g., suppose s 1 is adjacent to a square from P 1 , while s 2 is adjacent to a square from P 2 If s 1 and s 2 are the same color, then x i is incident with three colors, contradicting Lemma 3.2. If s 1 and s 2 are different colors, then s 1 must be matched with both s 2 and a square from P 1 , which is a contradiction.

Otherwise x i is incident with three squares in P 1 ∪ P 2 (ex. x 2 from Figure 2(b)). In this case x i is incident with three colors since both P 1 and P 2 are maximally connected sets of like-colored squares. This contradicts Lemma 3.2. We conclude that there exists a hole H in P ′ .

By Lemma 2.10, H is not a hole in any of P i , 1 ≤ i ≤ a. Let u 1 , u 2 , u 3 be three consecutive vertices along a path on the boundary of H such that u 2 is a reflex vertex of P ′ . Let p 1 , p 2 ∈ ρ(P ′ ) be such that p 1 has the edge u 1 u 2 , while p 2 has the edge u 2 u 3 . Let p ∈ ρ(P ′ ) be such that p has edges u 1 u 2 and (b) u 2 u 3 . Since P is a simple polygon, we know that p ∈ ρ(P ). Then we have color(p) = color(p 1 ) and color(p) = color(p 2 ). Note that for each pair of adjacent squares with different colors, they must be matched in τ . Thus, p is matched with p 1 and p 2 . This contradicts the fact that there is no overlapping dominoes in a tiling. Since G is connected and contains no cycles, G is a tree. ✷

Since trees are 2-colorable, we have the following:

Theorem 3.4 If P is a k-tileable simple layout polygon for k ≥ 2, then χ(P ) = 2.
The following Corollary, which will be useful when considering an algorithm for tiling simple layout polygons, is implied by the 2-colorability of trees and the proof of Lemma 3.3: Corollary 3.5 Let P be a simple layout polygon. P has a k-tiling with a perfect matching M of ρ(P ) for k ≥ 2 if and only if P has a 2-tiling with a perfect matching M of ρ(P ). Now we turn our attention to non-simple layout polygons, i.e. layout polygons that contain one or more holes.

Lemma 3.6 There exists a (non-simple) layout polygon such that k-tilings can only exist for k ≥ 4.

Proof: We claim that the layout polygon depicted in Figure 3(a) requires at least four colors in any twinfree colored domino tiling. We begin by identifying all the leaves and corners in this layout polygon (see Figure 3(b)). The identification of the leaves and corners forces certain squares to be matched with each other. These forced matchings are shown in Figure 3(c). Now we consider how the leftmost-lowest square in P , which we will call l, is matched (see Figure 4). It is either matched with the neighbor to its right, or l is matched with the neighbor that is above l.

Case(i): First suppose that l is matched with its neighbor to the right. This forces the set of matchings shown in Figure 4 (a). Now consider how the square labelled as p in Figure 4(a) is matched. It cannot be matched with its right neighbor since the domino involved in such a matching would be forced to be a twin. Thus p must be matched with the neighbor that is above p. This forces the matchings in Figure

4(b)

. We can see that such a matching forces two twin dominoes, one of which is indicated in Figure 4(b). Thus l cannot be matched with its right neighbor. Case(ii): Suppose l is matched with the neighbor that is above l. This matching implies other matchings that are shown in Figure 5(a). The corresponding color partition is shown in Figure 5(b). The resulting color partition graph is shown in Figure 5(c). Since K 4 is a subgraph of this graph, at least 4 colors are required in any coloring, as claimed. ✷

If we combine Lemma 3.6 with the fact that any color partition graph of a layout polygon is planar, and is therefore 4-colorable, we obtain the following: Theorem 3.7 Let P be a k-tileable layout polygon for k ≥ 2. Then χ(P ) ≤ 4, and this bound is tight.

(c) l (a) (b)

Tiling Simple Layout Polygons

In this Section we describe an algorithm for the TWINLESS TILING problem for simple layout polygons. We note that our algorithm not only decides whether or not a simple layout polygon is k-tileable for k ≥ 2, it also computes such a tiling if one exists. Our algorithm operates on the following decomposition of the layout polygon.

Definition 4.1 Leaf-Corner Decomposition: A leaf-corner decomposition of a layout polygon P , denoted L(P ), is defined recursively as follows: if P does not contain a leaf or a corner, then L(P ) := ∅.

Otherwise, let X be a leaf or corner of P , and let P 1 , P 2 , ..., P l be the simple layout polygons obtained by removing X from P . Then we define L(P ) := {X} L(P 1 ) L(P 2 ) ... L(P l ).

We pause here to consider an important note concerning the members of a leaf-corner decomposition L(P ). A member of L(P ) is not necessarily a leaf or a corner of P , although each member of L(P ) is a leaf or a corner of some subpolygon of P . For convenience, we will refer to the members of L(P ) as leaves or corners. We can justify this naming convention by observing that Lemma 2.6 and Lemma 2.7 hold for the members of L(P ): Lemma 4.2 Let P be a simple layout polygon that is k-tileable for k ≥ 2, and let L(P ) be a leaf-corner decomposition of P . If L ∈ L(P ) is a 1 × 2 rectangle then in any k-tiling of P for k ≥ 2, there is only one domino that covers L. Furthermore, if C ∈ L(P ) is a 2 × 2 rectangle then in any k-tiling of P , for k ≥ 2, there are only two dominoes that cover C. Let P be a simple layout polygon with |ρ(P )| = 2(d + 1) squares that is k-tileable for k ≥ 2. Let L(P ) be a leaf-corner decomposition of P , and let X be the leaf or corner mentioned in Definition 4.1 that is used to define L(P ). By induction, the Lemma holds for each of the simple layout polygons obtained by removing X from P . Since X is a leaf or a corner of P , Lemma 2.6 or Lemma 2.7 implies the result. ✷

We say that a leaf-corner decomposition L(P ) covers P if and only if the union of all the members in L(P ) is P . Lemma 4.3 Given a simple layout polygon P and a leaf-corner decomposition L(P ), if L(P ) does not cover P then P is not k-tileable for k ≥ 2.

Proof: Let L(P ) be a leaf-corner decomposition of P . Suppose that P is k-tileable even though L(P ) does not cover P . Define P := {P 1 , P 2 , ..., P l } to be the set of simple layout polygons obtained by removing L(P ) from P . By Definition 4.1, we have that each P i ∈ P does not contain a leaf or a corner. It follows from Lemma 2.8 that each P i ∈ P is not k-tileable for k ≥ 2. But since P is k-tileable, and by Lemma 4.2, each P i ∈ P is also k-tileable, and we arrive at a contradiction. ✷

Due to the following result, the main objective of our algorithm is to compute a perfect matching of ρ(P ) that does not contain any twin-forcing arrangements. Lemma 4.4 Let P be a simple layout polygon. P is k-tileable with matching M , for k ≥ 2, if and only if M is a perfect matching of ρ(P ) that does not contain a twin-forcing arrangement. Let P be a simple layout polygon with 2(d + 1) squares. Suppose there exists a perfect matching M of ρ(P ) that does not contain any twin-forcing arrangements. Let p 1 be a square from ρ(P ) that is incident with a convex vertex of P . Let p 2 be the square that p 1 is matched with, and w.l.o.g assume p 2 is below p 1 . Define P 1 , P 2 , ..., P l to be the set of mutually edge disjoint simple layout polygons obtained by removing p 1 and p 2 from P . For the remainder of the proof we will refer to P 1 , P 2 , ..., P l collectively as the components. Define M i to be the matching of P i that is implied by M , for 1 ≤ i ≤ l. Since |ρ(P i )| ≤ 2d, by induction we have that P i is k-tileable with matching M i , for k ≥ 2 and 1 ≤ i ≤ l. Furthermore, by Corollary 3.5, each P i is 2-tileable with matching M i . So let us tile the portion of P that is covered by P 1 , P 2 , ..., P l using the guaranteed 2-tilings that exist for each of these components. To complete the tiling of P , we must cover p 1 and p 2 with a multicolored domino. Now let us consider the squares that may surround p 1 and p 2 (see Figure 6). Notice that not all of p 3 , ..., p 8 are necessarily in P . Also, if p i and p j are in different components, then inverting the colors in p i 's component (i.e. changing white squares to black, and black squares to white) has no effect on the colors in p j 's component.

Cover p 1 and p 2 with a non-twin domino, ensuring that this domino's colors coincide with color(p 3 ) and color(p 4 ) if either or both of p 3 or p 4 are in P . The fact that M does not contain twin-forcing arrangements guarantees that such a non-twin domino exists. If both of p 3 and p 4 are not in P then cover p 1 and p 2 with a non-twin domino according to the color of p 6 . Now suppose color(p 6 ) = color(p 2 ). We can remedy this by inverting the colors in the component that contains p 6 . This inversion does not change color(p 3 ) and color(p 4 ) if p 6 and p 4 are in different components. So suppose p 6 is in the same component as p 4 . We have that p 5 ∈ ρ(P ), otherwise p 5 is a hole, or part of a hole, in P . Since color(p 2 ) = color(p 4 ), we have color(p 6 ) = color(p 4 ). Therefore, the color of p 5 is different to at least one of p 6 or p 4 , and must be matched with that one, but this also causes a twin-forcing arrangement involving p 2 , p 4 , p 5 , and p 6 , which is a contradiction. We conclude that color(p 6 ) = color(p 2 ).

Similarly, we can argue that color(p 8 ) = color(p2), or the color of p 8 can be inverted without changing color(p 6 ), color(p 4 ), and color(p 3 ). Thus P can be k-tiled for k ≥ 2, as required. ✷

Let L be a leaf, and C be a corner, from a leaf-corner decomposition L(P ) of a simple layout polygon P . According to Lemma 4.2, the squares in L must be matched, and the squares contained C may be matched one of two ways, in any k-tiling of P , for k ≥ 2. Suppose we are given a perfect matching of ρ(P ) that is associated with a k-tiling of P for k ≥ 2, and let p be the highest and leftmost square in C. If p is matched with its right neighbor, then we say that C is matched "horizontally", and deem C matched "vertically" otherwise. The key to our algorithm is noticing that the matching of a leaf or a corner may "force" neighboring leaves and corners to be matched a certain way if we are to avoid twin-forcing arrangements. To illustrate this, consider the corners C 1 , C 2 , and C 3 from the leaf-corner decomposition of a layout polygon depicted in Figure 7(a). Suppose the corner C 2 is matched as in Figure 7(b). We can see that C 1 can be matched in either of two ways without causing a twin-forcing arrangement. This is not the case for C 3 . If C 3 is matched "vertically" (see Figure 7(b)) then a twin-forcing arrangements arises. This forces C 3 to be matched "horizontally" as in Figure 7(c). We can generalize these observations in the following Lemma. We say that two members X and Y of a leaf-corner decomposition are adjacent if there exists two squares p, q ∈ ρ(P ), such that p ∈ X, q ∈ Y , and p and q are adjacent. Also, an edge of a leaf or corner x is an edge from the bounding rectangle of x. Lemma 4.5 Let P be a simple layout polygon with a perfect matching M of ρ(P ), and a leaf-corner decomposition L(P ) that covers P . L(P ) satisfies the following rules with respect to M if and only if M does not contain a twinforcing arrangement:

(c) C 1 C 2 C 3 (a) (b)
1. For each edge e of each leaf L ∈ L(P ), there is at most one member of L(P ) that both intersects e and is adjacent to L.

2. If C i , C j ∈ L(P ) are two corners that share an entire edge, then C i and C j are both matched horizontally or they are both matched vertically.

3. If L, C i ∈ L(P ) are a leaf and a corner such that L shares an entire vertical (resp. horizontal) edge with C i , then C i is matched vertically (resp. horizontally).

4. If X, Y ∈ L(P ) are both adjacent to a corner C i ∈ L(P ), such that both X and Y intersect the same vertical (resp. horizontal) edge of C i , then C i is matched horizontally (resp. vertically).

Proof: (⇒) Suppose for the sake of contradiction that M contains a twinforcing arrangement. Let p, q, r, and s be four squares that form a twinforcing arrangement, such that p and q are matched, while r and s are unmatched. Lemma 4.2 implies that since p and q are matched, they are either both contained in the same leaf or both contained in the same corner from L(P ). First suppose p and q are both contained in the leaf L ∈ L(P ). If r and s are contained in different members of L(P ), then rule (1) is violated. So r and s are contained in the same member of L(P ), and since r and s are not matched, they must be contained in a corner. But rule (3) implies that r and s are matched, which is a contradiction. So suppose p and q are both contained in the corner C 1 ∈ L(P ), and w.l.o.g. assume that C 1 is matched vertically. If r and s are both contained in the corner C 2 ∈ L(P ), then by rule (2), C 2 is matched vertically, which implies r and s are matched, which is a contradiction. So r and s must be contained in different members of L(P ). This contradicts rule (4), and hence we conclude that M does not contain any twinforcing arrangements.

(⇐) Suppose for the sake of contradiction that one of rules ( 1)-( 4) is does not hold for L(P ). If rule (1) is violated then there exists two unmatched squares that are each adjacent to a different square in L, and since the squares in L are necessarily matched by Lemma 4.2, a twin-forcing arrangement is formed, which is a contradiction. If rule ( 2), (3), or ( 4) is violated then there is a vertically (resp. horizontally) matched pair of squares next two unmatched squares, and a twin-forcing arrangement is formed, which implies a contradiction. ✷

Now we can describe our algorithm for solving the TWINLESS TILING problem for simple layout polygons. Before considering our algorithm, we make an important note concerning the input to our algorithm. The time taken by algorithms that operate on polygons is typically expressed in terms of the number of vertices that the polygon has. This presents a problem for the TWINLESS TILING problem since we can describe a layout polygon with O(1) vertices that contains an arbitrary number of squares. Although we can deal with this problem in a number of different ways, we adopt the following assumption: the layout polygon P is described by ρ(P ) in the input in the form of an adjacency list of squares and neighbors. Using this assumption, we can access the neighbors of each square in O(1) time since each square has at most four neighbors. Proof: The algorithm begins by constructing a leaf-corner decomposition L(P ) of P . If L(P ) does not cover P then the algorithm halts and reports that P is not k-tileable for k ≥ 2. The correctness of this step of the algorithm is guaranteed by Lemma 4.3.

Then the algorithm uses rules (1)-( 4) of Lemma 4.5 to construct a boolean expression φ, which is an instance of the 2SAT problem. For each corner C i ∈ L(P ) we create two variables h i and v i , which correspond to C i being matched horizontally and vertically, respectively. In order to ensure that exactly one matching of C i is chosen, we add the following clauses to φ: (h i ∨ v i ) and (¬h i ∨ ¬v i ). If rule (1) is violated for any leaf in L(P ), we add the unsatisfiable clause (f alse) to φ. We encode rules (2)-( 4) as clauses by inspecting the neighbors of each leaf and corner in L(P ). If the condition of rule ( 2) is satisfied, then we add the following clauses to φ: (¬h i ∨ h j ), (¬h j ∨ h i ), (¬v i ∨ v j ), and (¬v j ∨ v i ). If the condition of rule (3) is satisfied, we add the following clause to φ: (v i ) (resp. (h i )). For rule (4) we conditionally add the following clause:

(h i ) (resp. (v i )).
By construction, φ is satisfiable if and only if L(P ) conforms to rules (1)-( 4) of Lemma 4.5. Furthermore, a satisfying assignment of φ corresponds exactly to a perfect matching M of ρ(P ), and by Lemma 4.5, M does not contain a twin-forcing arrangement. Thus by Lemma 4.4, φ is satisfiable if and only if P is k-tileable. Thus we can decide if P is k-tileable for k ≥ 2 by solving the 2SAT problem on φ.

To construct a tiling of P , we use Corollary 3.5 to observe that M is a matching of some 2-tiling. We compute the colors of the dominoes in a 2-tiling of P as follows. We color an arbitrary square p ∈ ρ(P ) using the color black. Then we proceed using Depth-First Search (DFS), only visiting those squares that are uncolored. When we visit a square q, we assign a color to q based upon the color of a neighboring square: if a neighbor is colored black, and q is matched with this neighbor, then q is colored white, otherwise q is colored black. Since DFS is used to visit the squares, each square is assigned a color, and we are guaranteed that no twin dominoes arise since M is the matching of a 2-tiling.

L(P ) can be computed in O(|ρ(P )|) time as follows. First we identify all leaves and corners in P by examining each square and its neighbors. Place each of these leaves and corners in a list called T . Notice that some members of T may overlap. Then we iteratively remove leaves and corners from P until T is empty:

1. Remove the next item from T and call it X.

2. If X is still completely contained in P then add X to L(P ).

3. P = P -X.

Tiling Non-Simple Layout Polygons

In this Section we show that the TWINLESS TILING problem is NP-complete for non-simple layout polygons, i.e. layout polygons that contain holes. This problem is in NP since we can "guess" a tiling and verify that this tiling is a k-tiling for k ≥ 2 in non-deterministic polynomial time.

Our reduction is from a boolean satisfiability problem called PLANAR 3,4SAT. Let φ be a boolean expression in conjunctive normal form. We define the inclusion graph of φ, denoted G(φ), to be the graph whose vertices are the variables and clauses of φ. An edge (v i , c j ) exists in G(φ) if and only if the variable v i appears negated or unnegated in clause c j . DECISION: Is φ satisfiable?

The PLANAR 3,4SAT problem is known to be NP-complete (see [START_REF] Jansen | The minimum broadcast time problem for several processor networks[END_REF] and ( 15)). Our reduction will construct a layout polygon P that is k-tileable for k ≥ 2 if and only if φ is satisfiable. To accomplish this, we will use a planar embedding of G(φ) as a template for P . Specifically, we will use a planar orthogonal grid drawing of G(φ), which we denote as D(φ), which has the following properties: (i) Each edge of G(φ) is drawn as a chain of orthogonal line segments, (ii) Each bend in the drawing of an edge lies at an integer valued coordinate, (iii) Each node of G(φ) drawn as a point that is located at an integer valued coordinate, and

(iv) All edges are disjoint except when their endpoints meet at a node.

We maintain the graph theoretic terminology when referring to D(φ). For example, when we say "an edge e in D(φ)" we are referring to the chain of orthogonal line segments that constitute the drawing of the edge e in G(φ). Similarly, when we say "the vertex v in D(φ)" we are referring to the point in the integer plane associated with the vertex v in G(φ).

As already noted, D(φ) will be used as a template for P . So that |ρ(P )| is not too large, we must ensure that the edges in D(φ) are not too long. It is known that each edge in D(φ) has a length in O(n 2 ) if D(φ) occupies O(n 2 ) space, where n is the number of variables in φ. Such a planar orthogonal grid drawing can be computed in O(n) time (see, for example, ( 6)). We note here that as part of our reduction, D(φ) will also be scaled by a constant in order to ensure that P can be constructed correctly. The exact value of this constant will be discussed in what follows.

To construct P , we will overlay various gadgets over the nodes and edges in D(φ). These gadgets, which are layout polygons, will correspond to different aspects of φ. We employ gadgets that represent variables, negation, and clauses. We also make use of a special gadget called a spacer that is used to ensure proper connections between variable gadgets and clause gadgets.

Variable Gadget: A variable gadget represents a particular variable from φ. The tiling of a variable gadget will correspond to the variable being assigned a particular truth value. The variable gadget is depicted in Figure 8(a). Figure 8(b) identifies important aspects of the variable gadget. The terminals of a variable gadget will be used to attach a variable gadget to the appropriate clause gadgets. The center will be used to position a variable gadget on the appropriate node in D(φ). Specifically, if a variable gadget is representing a variable v i , then the variable gadget is positioned in the plane so its center is located at the node associated with v i in D(φ). The value corner is used to "set" the truth value of variable. Specifically, (b) (a) the orientation (i.e. horizontal or vertical) of the matching of the value corner with respect to a k-tiling for k ≥ 2 will determine the truth value of the variable. Figure 9 depicts the two possible ways that a variable gadget can be matched so that a twin-forcing arrangement does not arise. Also, one can see that both of these matchings have a corresponding k-tiling for k ≥ 2. Thus we have the following: Lemma 5.2 In a k-tiling of a variable gadget for k ≥ 2, the value corner of a variable gadget is matched horizontally (resp. vertically) if and only if all squares in the variable gadget are also matched horizontally (resp. vertically).

We use these two possible matchings of a variable gadget to represent the two possible truth values of the variable that the gadget represents. If the variable gadget is matched vertically, then the variable is set to "false", and if the variable gadget is matched horizontally, then the variable is set to "true". Negation Gadget: The "truth" value of a variable gadget will be transmitted to a clause gadget according to the orientation of the tiling of the variable gadget. When a variable appears negated in a clause, we must "flip" this orientation. The gadget that accomplishes this is called the negation gadget and is depicted in Figure 10 Clause Gadget: A clause gadget is used to represent a clause from φ (see Figure 11(a)). Figure 11(b) identifies important aspects of the clause gadget. The terminals in a clause gadget are used to connect a clause gadget to the appropriate variable gadgets. The center of the clause-gadget is used to position a clause gadget on the appropriate vertex in D(φ). Specifically, if a clause gadget is representing a clause c i , then the clause gadget is positioned in the plane so that the center is located at the vertex associated with c i . The clause gadget is then rotated if necessary so that each of the terminals intersect a line segment that is incident with the node associated with c i .

The clause gadget is constructed such that it is k-tileable for k ≥ 2 if and only if at least one of the variable gadgets that is connected to it is tiled horizontally, i.e. set to true. Before considering the details concerning how we connect a variable gadget to a clause gadget, let us consider how we represent satisfiability in a clause gadget. Figures 12(a)-(h) depict all the possible matchings of the clause gadget that do not create twin-forcing arrangements. We can see that no twin dominoes need to be used in the matchings in Figures 12(a)-(g). Notice that in each of these Figures (i.e. (a)-(g)), at least one of the 2 × 2 squares that surround the terminals is matched horizontally, i.e. in the "true" orientation. Now consider Figure 12(h). In this Figure, each of the 2 × 2 squares surrounding the terminals are matched vertically, i.e. in the "false" orientation. Although Figure 12(h) does not contain a twin-forcing arrangement, one can show that there is no k-tiling for k ≥ 2 that uses this matching as follows: Figure 12(i) depicts the matching from Figure 12(h) with ten squares emphasized. These squares must have the same color in any k-tiling for k ≥ 2 that uses this matching. Since two of these squares are matched, a twin domino must be used, and hence the matching depicted in Figure 12(h) cannot be used by any k-tiling for k ≥ 2. The following summarizes these observations: Lemma 5.4 In any k-tiling for k ≥ 2 of a clause gadget, at least one of the 2 × 2 squares that surround the terminals must be tiled horizontally, i.e. in the "true" orientation.

Before describing the final gadget, we consider a partial construction of P using the techniques that have been discussed thus far, and we describe how we connect variable gadgets to clause gadgets. Our example will demonstrate the need for the final gadget.

Suppose we define φ := (v 1 ∨ v 2 ∨ ¬v 3 ) ∧ (¬v 1 ∨ v 2 ∨ v 3 ). Figure 13(a) depicts a sample planar orthogonal grid drawing of G(φ), which we denote as D(φ). variable and clause gadget associated with v 2 and c 1 . Thus certain line segments in D(φ) may be too short to properly position the gadgets. Although not illustrated in Figure 13(b), disjoint line segments in D(φ) may be so close together that two or more gadgets may intersect. We can remedy both of these problems by first scaling D(φ) by a constant a so that the boundary of each gadget is disjoint from D(φ), and so that no gadgets intersects. This scaling should also take into account the possible need for negation gadgets, as well as the final gadget that we have yet to describe. Although we do not give an explicit value for the scaling constant a, we can take a be the sum of the longest side of the orthogonal bounding box for each gadget to ensure that D(φ) is large enough to accommodate the gadgets. Since we are scaling D(φ) by a constant, D(φ) still occupies O(n 2 ) space in the plane.

The last issue we discuss motivates the need for the final gadget. To connect a variable gadget to the appropriate clause gadget(s), we will use a sequence of 2 × 2 groups of squares. Figure 14 illustrates this idea. Notice that the orientation of the matching in any k-tiling for k ≥ 2 is the same throughout the sequence of 2 × 2 squares, even if the sequence contains a bend. This ensures that the proper "truth" value is transmitted from the variable gadget to the clause gadget. These squares are added along the line segments that represent the edge between the variable and the clause in D(φ). Figure 15 depicts a detailed view of the top portion of Figure 13(a). Collections of 2 × 2 groups of squares has been used in an attempt to connect variable gadgets to clause gadgets. This works fine for the connection between v 3 and c 1 , but does not work for the connection between v 1 and c 1 . This is because the distance between the appropriate terminals for the gadgets representing v 1 and c 1 is an odd number. We cannot complete the connection between v 1 to c 1 with a 2 × 1 group of squares since then the truth value cannot be transmitted properly:

Fig. 2 :

 2 Fig. 2: (a) The boundary between P1 and P2. (b) The dashed lines represent the path v2, v3, ..., va, v1.

Fig. 3 :Fig. 4 :

 34 Fig. 3: (a) A layout polygon P . (b) The leaves and corners of P have been lightly shaded. (c) The matchings that are forced by the leaves and corners of P .

Fig. 5 :

 5 Fig. 5: (a) The matchings implied by matching l with the neighbor above l. (b) The color partition implied by the matching. (c) The resulting color partition graph contains a K4.

Proof:

  We induct on |ρ(P )|. The Lemma is trivially true for |ρ(P )| ≤ 4. So assume that the Lemma is true for |ρ(P )| ≤ 2d.

Fig. 6 :

 6 Fig. 6: The squares surrounding the matched squares p1 and p2.

Fig. 7 :

 7 Fig. 7: A matching that forces another matching. (a) Three label corners. (b) Matchings of C2 and C3 that cause of twin-forcing arrangement. (c) A matching of C2 that forces a matching of C3.

Theorem 4 . 6

 46 The TWINLESS TILING problem can be solved in O(|ρ(P )|) time on simple layout polygons, or equivalently, O(n) time, where n is the number of dominoes needed in the tiling.

4 .

 4 Add to T all new leaves and corners that are created by removing X. Notice that Step 2 of this procedure is conditional since some members of T may overlap. This procedure stops after O(|ρ(P )|) steps, and each step can be accomplished in O(1) time. Computing φ can clearly be accomplished in O(|ρ(P )|) time by examining the O(1) neighbors of each leaf and corner from L(P ). Notice that φ has O(|ρ(P )|) clauses. Thus a satisfying assignment of φ can be computed in O(|ρ(P )|) time using the algorithm from (2). Assigning colors to the squares in ρ(P ) uses DFS and hence can be accomplished in O(|ρ(P )|) time. ✷

Definition 5 . 1

 51 PLANAR 3,4SAT INSTANCE: A boolean expression φ in conjunctive normal form such that: (i) Each clause contains exactly 3 literals, (ii) Each variable appears negated or unnegated at most 4 times in φ, and (iii) The inclusion graph G(φ) is planar.

Fig. 8 :

 8 Fig. 8: (a) The variable gadget. (b) The terminals, center, and value corner of a variable gadget.

Fig. 9 :Fig. 10 :

 910 Fig. 9: (a) The variable gadget matched vertically representing "false". (b) The variable gadget matched horizontally representing "true".

  (a).

  Figure 10(b) identifies two important regions of the negation gadget called the input corner and the output corner.

Figure 10

 10 (c) and (d) illustrates the fact that the orientation of the matching associated with a k-tiling for k ≥ 2 of the input corner is always opposite to that of the output corner. Thus we have demonstrated the following:

Fig. 11 :Lemma 5 . 3

 1153 Fig. 11: (a) The clause gadget. (b) The terminals and center of the clause gadget.

Figure 13 Fig. 12 :

 1312 Fig.12: The matchings of the clause gadget that do not contain a twin-forcing arrangement.

Fig. 13 :

 13 Fig. 13: (a) A sample planar orthogonal grid drawing D(φ). (b) The variable and clause gadgets positioned on D(φ).

Fig. 14 :

 14 Fig. 14: (a) An example of a sequence of 2 × 2 groups of squares used to connect a variable gadget to a clause gadget. (b) A sequence of squares transmitting "false". (c) A sequence of squares transmitting "true".

Fig. 15 :

 15 Fig. 15: A detailed view of the top portion of D(φ).

  Extending definition 2.1 slightly, we define a k-tiling to be a tiling that uses dominoes from D k . We study the following tiling decision problem:

	Definition 2.2 TWINLESS TILING:
	INSTANCE: A layout polygon P .

k 2 non-twin dominoes over k colors. Definition 2.1 k-tileable: A layout polygon P is k-tileable if and only if there exists a tiling of P using dominoes from D k . DECISION: Is P k-tileable for k ≥ 2?

Acknowledgements

We would like to thank Therese Biedl for useful comments regarding the results presented in Section 4.

† Research was supported in part by NSERC under Grant 261290-03. 1365-8050

if we simply insert a 2 × 1 group of squares to complete the connection between v 1 and c 1 , then the only truth value that can correctly be transmitted is "false", i.e. the connection between v 1 and c 1 must be tiled vertically. We cannot simply scale D(φ) by a factor of 2 to remedy this problem because we need odd distances between centers of variable gadgets and clauses gadgets. We can however remedy this problem by inserting a spacer gadget, which is depicted in Figure 16(a). Now we show that the spacer gadget is an identity gadget in the sense that the input corner will always be matched with the same orientation as the output corner in any k-tiling for k ≥ 2. Figure 16(b) depicts a set of matchings that clearly must exists in a k-tiling for k ≥ 2. Four squares from the spacer gadget have also been labeled p, q, r, and s. Due to the forced matchings in the spacer gadget, we can observe that p and q (resp. r and s) must have the same color in any k-tiling of the spacer gadget for k ≥ 2. This implies the following: Lemma 5.5 In any k-tiling of a spacer gadget for k ≥ 2, the input and output corners are either both matched horizontally or both vertically. This Lemma is only useful once we notice another important feature of the spacer gadget: the distance between the input and output corners is odd. Thus spacer gadgets can be inserted on line segments in D(φ) when necessary in order to ensure that we can properly connect variable and clause gadgets.

From our construction we can see that P is k-tileable if and only if φ is satisfiable. Thus we have the following: Theorem 5. [START_REF] Biedl | A better heuristic for orthogonal graph drawings[END_REF] The TWINLESS TILING problem is NP-complete for non-simple layout polygons.

Open Problems

We have characterized the so-called chromatic number, denote χ(P ), of layout polygons, which is the minimum number of colors needed in a colored domino tiling. We showed that for each k-tileable simple layout polygon P , χ(P ) = 2, for k ≥ 2. For each k-tileable non-simple layout polygon P , we showed that χ(P ) ≤ 4, for k ≥ 2. We also showed that this bound is tight in the sense that there exists a nonsimple layout polygon P such that χ(P ) = 4. We are interested in characterizing those layout polygons that require at most three colors in any k-tiling for k ≥ 2. Also, we are interested in the computational complexity of tiling such layout polygons.


Thomas Brihaye

Words and bisimulations of dynamical systems

In this paper we study bisimulations on dynamical systems through a given partition. Our aim is to give a new vision of the notion of bisimulation by using words. To achieve this goal, we encode the trajectories of the transition system as words. This method was introduced in our paper "On o-minimal hybrid systems" in order to give a new proof of the existence of a finite bisimulation for o-minimal hybrid systems (as previously proved in a paper by Lafferriere G., Pappas G.J. and Sastry S.). Here we want to provide a systematic study of this method in order to obtain a procedure for building finite bisimulations based on words.

Introduction

More and more real-life systems are automatically controlled. It is of a capital importance to know whether the programs governing these systems are correct. In order to be able to manipulate these real-life systems, various mathematical models have been introduced (timed automata [START_REF] Alur | A theory of timed automata[END_REF], hybrid systems [START_REF] Henzinger | The theory of hybrid automata[END_REF],...) making the study of the abstract systems a wide and interesting domain of research. Unfortunately even the abstract systems are not always that easy to handle, the main problem being their infinite size. One way to solve this problem is to reduce these infinite systems to finite systems in such a way that enough information is preserved. It is known that bisimulations (see [START_REF] Aczel | Non-well-founded sets[END_REF][START_REF] Pappas | Bisimulation of context-free grammars and of pushdown automata[END_REF][START_REF] Henzinger | Hybrid automata with finite bisimulations[END_REF]) are a "reduction" of particular interest since they preserve a lot of interesting properties (reachability problem, model-checking branching logic... [HNSY94, ACH + 95, AHLP00]). That is why we focus our attention on systems admitting a finite bisimulation.

In [START_REF] Brihaye | On o-minimal hybrid systems[END_REF] in order to prove the existence of a finite bisimulation for an extended class of ominimal hybrid systems (i) , we encode the continuous dynamics through words (see also [START_REF] Brihaye | On the expressiveness and decidability of o-minimal hybrid systems[END_REF]). In the previous two papers we limit ourselves to the encoding of o-minimal dynamical systems (i.e. dynamical systems definable in an o-minimal structure; see [vdD98] for a nice overview on o-minimality.). In particular we only had to manipulate finite words. Let us mention that some analogue already appears in the literature (the notion of signature for example in [START_REF] Asarin | On the decidability of the reachability problem for planar differential inclusions[END_REF]). Let us also notice that bisimulations of dynamical systems has been studied independently in [START_REF] Julius | State maps of general behaviors, their lattice structure and bisimulations[END_REF] but in a different framework. They studied dynamical system as defined in [START_REF] Willems | Paradigms and puzzles in the theory of dynamical systems[END_REF].

Our technique was used by Korovina and Vorobjov in order to compute a doubly exponential bound on the size of the coarsest finite bisimulation of pfaffian hybrid systems (see [START_REF] Korovina | Pfaffian hybrid systems[END_REF]). They recently improved their results by reducing the bound to a single exponential and prove that this bound is tight (see [START_REF] Korovina | Upper and lower bounds on sizes of finite bisimulations of Pfaffian hybrid systems[END_REF]).

In this paper, we want to give a systematic study of this encoding technique. In particular we give a Procedure (Bisiω) that aims to build a bisimulation on a dynamical system through a partition. Our hope is that this systematic study will lead to the discovery of some new general classes of dynamical systems (through partition) which admit finite bisimulations. Beyond the fact that dynamical systems are of interest in their own, they are an essential component of hybrid systems. In particular, when strong reset conditions are assumed on the hybrid system, finding finite bisimulations of the hybrid system reduces in finding a finite bisimulation on each location (which is endowed with a dynamical system) w.r.t. the partition induced by the guards, resets and invariant. It is the case for o-minimal hybrid systems, see [START_REF] Lafferriere | O-minimal hybrid systems[END_REF]. Moreover a recent point of view on the theory of hybrid systems allows to see an hybrid system as a dynamical system (see the notion of hybrifold in [START_REF] Simic | Towards a geometric theory of hybrid systems[END_REF]).

The rest of the paper is organized as follows. In section 2, we recall classical definitions and properties of bisimulations on a transition system, we also describe the well-known bisimulation algorithm ([BFH91, [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF][START_REF] Henzinger | The theory of hybrid automata[END_REF]), which is in fact a semi-algorithm. We end this section by defining what we call a dynamical system in this paper. Section 3 is the main section of the paper. We start by explaining how to associate a word with a trajectory; we introduce the notion of dynamical type which allows in some sense to recover the continuous dynamics through the partition. These tools being formalized we introduce a conceptual semi-algorithm called Procedure Bisiω and we prove that this procedure computes a bisimulation. We also describe several variants of our procedure. Finally we discuss in which case Bisiω provides the coarsest bisimulation of a dynamical system through a given partition. In Section 4 we provide an extensive list of examples.

Preliminaries

In this section, we recall some basic definitions and results concerning bisimulations on a transition system (see [START_REF] Aczel | Non-well-founded sets[END_REF][START_REF] Pappas | Bisimulation of context-free grammars and of pushdown automata[END_REF][START_REF] Henzinger | Hybrid automata with finite bisimulations[END_REF] for general references). We also recall the well-known bisimulation algorithm ([BFH91, [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF][START_REF] Henzinger | The theory of hybrid automata[END_REF]). Then we give definition of dynamical systems and associate with them a natural transition system.

Transition systems and bisimulation

Definition 2.1 A transition system T = (Q, Σ, →) consists of a set of states Q (which may be uncountable), Σ a finite alphabet of events, and

→ ⊆ Q × Σ × Q a transition relation. A transition (q 1 , a, q 2 ) ∈ → is denoted by q 1 a -→ q 2 . A transition system is said finite if Q is finite.
If the alphabet of events is reduced to a singleton, Σ = {a}, we will denote the transition system (Q, →) and omit the event a.

a a q 1 q ′ 1 q 2 q ′ 2 T 1 T 2 ∼ ∼ Fig. 1: Forward stable relation a a q 1 q ′ 1 q 2 q ′ 2 T 1 T 2 ∼ ∼ Fig. 2: Backward stable relation
Definition 2.2 Given a transition system T = (Q, Σ, →), a finite path in T is a finite sequence of transitions q 0 q 1 q 2 • • • q n such that for all i = 1, ..., n there exists a i ∈ Σ such that q i-1 ai -→ q i . We denote it as follows:

ρ = q 0 a1 -→ q 1 a2 -→ q 2 • • • an --→ q n .
Definition 2.3 Given two transition systems on the same alphabet of events,

T 1 = (Q 1 , Σ, → 1 ) and T 2 = (Q 2 , Σ, → 2 ), a partial simulation of T 1 by T 2 is a binary relation ∼ ⊆ Q 1 × Q 2 which
satisfies the following condition:

∀q 1 , q ′ 1 ∈ Q 1 , ∀q 2 ∈ Q 2 , ∀a ∈ Σ, q 1 ∼ q 2 and q 1 a -→ 1 q ′ 1 ⇒ ∃q ′ 2 , q ′ 1 ∼ q ′ 2 and q 2 a -→ 2 q ′ 2 (1)
The condition (1) is read T 2 partially simulates T 1 .

Definition 2.4 Given ∼ a partial simulation of T 1 by T 2 , we say that ∼ is a simulation of T 1 by T 2 if, for each q 1 ∈ Q 1 , there exists q 2 ∈ Q 2 such that q 1 ∼ q 2 . Definition 2.5 Given two transition systems on the same alphabet of events,

T 1 = (Q 1 , Σ, → 1 ) and T 2 = (Q 2 , Σ, → 2 ), a bisimulation between T 1 and T 2 is a relation ∼ ⊆ Q 1 × Q 2 such that ∼
is a simulation of T 1 by T 2 and the inverse relation (ii) ∼ -1 is a simulation of T 2 by T 1 . In this case we say that T 1 and T 2 are bisimilar.

Remark 2.6 One could consider a different notion of bisimulation, let us call it back-bisimulation or backward bisimulation (see [START_REF] Henzinger | What's decidable about hybrid automata?[END_REF]). This would come from the notion of partial backwardsimulation defined as partial simulation (Definition 2.3) where the condition (1) is replaced by:

∀q 1 , q ′ 1 ∈ Q 1 , ∀q ′ 2 ∈ Q 2 , ∀a ∈ Σ, q ′ 1 ∼ q ′ 2 and q 1 a -→ 1 q ′ 1 ⇒ ∃q 2 , q 1 ∼ q 2 and q 2 a -→ 2 q ′ 2
We say that a bisimulation is a forward stable relation and that the back-bisimulation is a backward stable relation. The difference between these two notions is illustrated on Figures 1 and2. Definition 2.7 Given a transition system T = (Q, Σ, →), we can look at bisimulations on Q×Q; they are called bisimulations on T .

(ii) If ∼= {(q 1 , q 2 ) ∈ Q 1 × Q 2 | q 1 ∼ q 2 }, then ∼ -1 = {(q 2 , q 1 ) ∈ Q 2 × Q 1 | q 1 ∼ q 2 }.
As already mentioned in the introduction, a motivation for the study of bisimulation is the reachability problem. Let us make this problem more precise: Reachability Problem 2.8 Given T = (Q, Σ, →) a transition system, Init ⊆ Q and F in ⊆ Q two subsets of states, is there a finite path (iii) ρ from Init to F in?

If T = (Q, →
) is a reflexive (iv) transition system then there exists several trivial "partial" bisimulations on T given by ∼ q = {(q, q ′ ) | q ′ ∈ Q} for q ∈ Q. This implies that there exists a bisimulation between T and a one-state system T 0 , where T 0 = (Q 0 , → 0 ) with Q 0 = {q 0 } and → 0 = {(q 0 , q 0 )}. The bisimulation between T and T 0 is given by ∼ 0 = {(q, q 0 ) | q ∈ Q}.

Regarding the reachability problem 2.8, the bisimulations ∼ q and ∼ 0 are completely irrelevant. One can have a bisimulation between a completely disconnected reflexive transition system and a single state system (T 0 ). This gives a motivation for the definition of bisimulation w.r. Definition 2.9 Given T a transition system, P a partition of Q and ∼ ⊆ Q × Q a bisimulation, we say that the bisimulation ∼ respects the partition P if given any p, q ∈ Q such that p ∼ q then p and q belong to the same piece of the partition P. We will speak of bisimulations w.r.t. P.

Definition 2.10 Given T a transition system, P a partition of Q we can define the coarsest bisimulation on T w.r.t. P, it is denoted ∼ P : In the case of bisimulations which are equivalence relations, we can define the notion of quotient of a transition system by such a bisimulation. Definition 2.12 Given a transition system T = (Q, Σ, →) and ∼ a bisimulation on T which is an equivalence relation. We can consider the quotient of T by ∼, denoted by T / ∼ = (Q/ ∼ , Σ, → ∼ ) and defined as follows:

∼ P = {∼ | ∼
• Q/ ∼ = {[q] ∼ | q ∈ Q} where [q] ∼ = {q ′ | q ∼ q ′ } • [q 1 ] ∼ a -→ ∼ [q 2 ] ∼ if and only if there exists q ′ 1 ∈ [q 1 ] ∼ and q ′ 2 ∈ [q 2 ] ∼ such that q ′ 1 a -→ q ′ 2 .
Remark 2.13 Definition 2.12 makes sense even when we consider an equivalence relation ∼ which is not a bisimulation.

(iii) i.e. ρ = q 0 a 1

--→ q 1 a 2 --→ q 2 • • •
an --→ qn with q 0 ∈ Init and qn ∈ F in. (iv) i.e. for all q ∈ Q we have that q → q.

Lemma 2.14 Given T a transition system, ∼ a bisimulation on T which is an equivalence relation, then the graph of the natural map

[•] ∼ : Q → Q/ ∼ is a functional bisimulation from T to its quotient transition system T / ∼ (see [Cau95, Lemma A.1 p. i]).
We end this subsection by making precise the folk result that states that bisimulations preserve the Reachability Problem.

Lemma 2.15 Given T , Init, F in as in the Reachability Problem 2.8, P a partition of Q given by Init ∩ F in, F in \ Init, Init \ F in, Q \ (Init ∪ F in) and ∼ P a bisimulation on T which is an equivalence relation w.r.t. P. There exists a finite path in T from Init to F in if and only if there exists a finite path in T / ∼P from Init/ ∼P to F in/ ∼P .

Let us notice that the same result holds for back-bisimulation.

Bisimulation Algorithm

As already mentioned previously, it is an important question to know whether a given infinite system admits a finite bisimulation. Since, for example, the reachability problem is decidable for a finite system effectively described. Moreover it would be nice to have an automatic procedure to build this finite bisimulation. These facts lead to the introduction of the bisimulation algorithm which appeared in [BFH91, [START_REF] Kanellakis | CCS expressions, finite state processes, and three problems of equivalence[END_REF][START_REF] Henzinger | The theory of hybrid automata[END_REF]. Given a transition system T = (Q, Σ, →) and P 0 a finite partition of Q, the bisimulation algorithm iterates the computation of predecessors (v) of the pieces of the partition, let us recall it: Algorithm 2.16 Initialization: P := P 0 While ∃P, P ′ ∈ P ∃a ∈ Σ such that ∅ = P ∩ Pre a (P ′ ) = P

Set P 1 = P ∩ Pre a (P ′ ) and P 2 = P \ Pre a (P ′ ) Refine P := (P \ {P }) ∪ {P 1 , P 2 } End while Return P

The following are well-known results on the bisimulation algorithm.

Lemma 2.17 Given T a transition system and P 0 a finite partition of Q, the bisimulation algorithm terminates if and only if there exists a finite bisimulation on T w.r.t. P 0 .

Lemma 2.18 If the bisimulation algorithm terminates it provides the coarsest bisimulation on T w.r.t. P 0 .

Dynamics

Definition 2.19 A dynamical system (vi) is a pair (M, γ) where: (v) Given T a transition system and q ∈ Q, the set of a-predecessors of q, denoted Prea(q), is defined by Prea

(q) = {q ′ ∈ Q | q ′ a
-→ q}, and if P ⊆ Q, Prea(P ) = S q∈P Prea(q). (vi) Our definition of dynamical system is an attempt to generalize the continuous dynamics of hybrid systems ( [START_REF] Henzinger | The theory of hybrid automata[END_REF]) with no explicit reference to differential equations. This definition, even if rather close, is different from the one given in [START_REF] Willems | Paradigms and puzzles in the theory of dynamical systems[END_REF]. Deeper investigation on the links between the two definitions would be relevant work.

1

Fig. 3: A finite automaton

• M = M, < is a totally ordered structure,

• γ :

M k1 × M → M k2 is a function.
The function γ is called the dynamics of the dynamical system. More generally, we can consider the case where γ is defined on subsets of M that is γ :

V 1 × V → V 2 with V 1 ⊆ M k1 , V ⊆ M and V 2 ⊆ M k2 .
In the sequel we assume the range of γ is equal to M k2 . Classically, when M is the field of the reals, we see M as the time, M k1 × M as the space-time, M k2 as the (output) space and M k1 as the input space. We keep this terminology in the more general context of a structure M.

In this presentation time and space have the same underlying structure (i.e. M) this comes from our presentation in [START_REF] Brihaye | On o-minimal hybrid systems[END_REF] where we needed the whole dynamical system to be definable in the o-minimal structure M. However we can imagine dynamical system with dynamics γ :

V 1 × V → V 2
where V is a totally ordered set and V 1 , V 3 are defined in completely different structure. This should not affect the results presented in the sequel.

The definition of dynamical system encompasses a lot of different behaviors. Let us give some examples.

Example 2.20 Let M = N, < and the dynamics γ : {0, 1}×{0, 1} → {0, 1} is given by γ(x, t) = (x + t) mod 2. The transition system associated with this dynamical system (see Definition 2.24) is in fact a finite automaton (see Figure 3).

Example 2.21 We can recover the continuous dynamics of the timed automaton (see [START_REF] Alur | A theory of timed automata[END_REF]). In this case, we have that M = R, < and the dynamics γ : R n × [0, +∞[→ R n is defined as follows.

γ(x 1 , ..., x n , t) = (x 1 + t, ..., x n + t)

Example 2.22 Definition 2.19 also allows dynamical systems with non deterministic (vii) behavior. Let us consider (M, γ) where each point of the plane has two possible behaviors: "to go to the right" or "to go up" (see Figure 4 on page 22). More precisely we have that M = R, < and γ : R 3 × R → R 2 is defined as follows.

γ(x 1 , x 2 , p, t) = (x 1 + t, x 2 ) if p 0 (x 1 , x 2 + t) if p < 0 Definition 2.23 If we fix a point x ∈ M k1 , the set Γ x = {γ(x, t) | t ∈ M } ⊆ M k2
is called the trajectory determined by x.

(vii) The non determinism comes in fact from the associated transition system, see Definition 2.24.

We define a transition system associated with the dynamical system, this definition is an adaptation to our context of the classical continuous transition in the case of hybrid system (see [START_REF] Lafferriere | O-minimal hybrid systems[END_REF] for example). Definition 2.24 Given (M, γ) a dynamical system, we define a transition system T γ = (Q, → γ ) associated with the dynamical system by:

• the set Q of states is M k2 ;
• the transition relation y 1 → γ y 2 is given by: ∃x ∈ M k1 , ∃t 1 , t 2 ∈ M, t 1 t 2 and γ(x, t 1 ) = y 1 and γ(x, t 2 ) = y 2 Remark 2.25 Let us notice that T γ is a reflexive transition system.

Remark 2.26 The transition system T γ is in general not transitive. To illustrate this fact, let us consider Example 2.22. Given the three points of the output space y 1 = (0, 0), y 2 = (0, 1) and y 3 = (1, 1), we clearly have that y 1 → γ y 3 since y 1 → γ y 2 and y 2 → γ y 3 . Indeed y 1 = γ(0, 0, -1, 0), y 2 = γ(0, 0, -1, 1) = γ(0, 1, 1, 0) and y 3 = γ(0, 1, 1, 1).

Words and dynamics

Given a dynamical system (M, γ) and P a finite partition of the space M k2 , an interesting question is to know if there exists a finite bisimulation of (M, γ) w.r.t. P. If such a bisimulation exists the bisimulation algorithm 2.16 provides the coarsest one by iterating the computation of the predecessors of the pieces of the partition P. The goal of this section is to give another procedure that computes the coarsest bisimulation on a dynamical system (M, γ) (i.e. a bisimulation on T γ ) w.r.t. a partition P. Our approach is in some sense more global that the bisimulation algorithm. We use the idea introduced in [BMRT04] which consists in encoding the dynamics of (M, γ) through the partition P by words on this partition. Let us first explain how we associate a word with a trajectory.

Encoding trajectories by words

First let us define the notion of word in this general (possibly uncountable) context. This definition is inspired from [START_REF] Bruyère | Automata on linear orderings[END_REF], see also [START_REF] Truss | Infinite permutation groups. II. Subgroups of small index[END_REF][START_REF] Rabinovich | Automata over continuous time[END_REF]. Definition 3.1 Given P a finite set (called the alphabet), M a totally ordered set, a word ω on P is a function from M to P; the word ω is also denoted in a sequence-like notation by (ω i ) i∈M where ω i ∈ P is the image of the element i under the function ω.

We recover the classical finite words or ω-words when the set M is respectively finite or equal to N.

Example 3.2 Let us consider the finite set P = {A, B}. We give three examples of words on P.

1. Given the finite set M 1 = {1, 2, 3, 4} equipped with the natural ordering and the function

ω 1 : M 1 → P such that ω 1 (1) = A, ω 1 (2) = B, ω 1 (3) = A
and ω 1 (4) = B, we recover an example of finite word. In this case ω 1 is classically denoted ABAB.

2. Given the set of natural number M 2 = N equipped with the natural ordering and the function ω 2 : M 2 → P such that ω 2 (n) = A if n is even and ω 2 (n) = B if n is odd, we recover an example of ω-word. In this case ω 2 is classically denoted (AB) ω .

3. Given the set of real number M 3 = R equipped with the natural ordering and the function

ω 3 : M 3 → P such that ω 3 (n) = A if n ∈ Q and ω 2 (n) = B if n ∈ R \ Q, we have a "degenerated" example of word.
We need to introduce basic notions related to words in this general context. For finite words, we adopt the classical notations.

Definition 3.3 Given ω : M → P a word on P, a subword of ω is given by ω s : M ′ → P where M ′ ⊆ M is an arbitrary subset of M considered with the order induced from M . Definition 3.4 Given ω : M → P a word on P, a suffix of ω is a subword of a particular form. A subword ω s : M ′ → P is a suffix if and only if M ′ = {t | t t 0 } or M ′ = {t | t > t 0 } for some t 0 ∈ M . In the same way we can define the notion of prefix. Definition 3.5 Given ω 1 : M 1 → P and ω 2 : M 2 → P two words on P, the concatenation of the words ω 1 and ω 2 is defined by the word ω 1 ω 2 : M 1 ∪M 2 → P where ω 1 ω 2 ↾ M1 = ω 1 and ω 1 ω 2 ↾ M2 = ω 2 and where the order on M 1 ∪M 2 is the order induced from M 1 on M 1 , the order induced from M 2 on M 2 and ∀m

1 ∈ M 1 , ∀m 2 ∈ M 2 we have that m 1 < m 2 in M 1 ∪M 2 .
We are now ready to build words associated with trajectories. Given (M, γ) a dynamical system and P a finite partition of M k2 , given x ∈ M k1 we associate a word with the trajectory Γ x in the following way. We consider the sets {t ∈ M | γ(x, t) ∈ P } for each P ∈ P. This gives a partition of the time M . In order to define a word on P associated with the trajectory determined by x, we need to define the set of intervals F x . F x = I (I is a time interval or a point) and is maximal for the property ∃P ∈ P, ∀t ∈ I, γ(x, t) ∈ P .

For each x, the set F x is totally ordered by the order induced from M . Let us note that the set F x can be equal to M itself. This allows us to define the word on P associated with Γ x denoted ω x . Definition 3.6 Given x ∈ M k1 , the word associated with Γ x is given by the function ω x : F x → P defined by: ω x (I) = P where I ∈ F x is such that ∀t ∈ I γ(x, t) ∈ P.

Let us note that given x ∈ M k1 , there exists a unique word ω x on P associated with the trajectory Γ x . The intuition behind the introduction of F x is the following. We want successive (viii) letters of the words ω x to be different. Definition 3.7 We denote by Ω P the set of words associated with (M, γ) w.r.t. P. We have that Ω P is a set of words on P. (viii) The notion of successive letters is only defined for "well behaving" dynamical systems.

The set Ω P gives in some sense a complete static description of the dynamical system (M, γ) through the partition P. In order to recover the dynamics, we need further information. This is the object of the following subsection.

Dynamical type

Given a point x of the input space M k1 , we have associated with x a trajectory Γ x and a word ω x . If we consider (x, t) a point of the space-time M k1 × M , it corresponds to a point γ(x, t) lying on Γ x . To recover in some sense the position of γ(x, t) on Γ x from ω x , we associate with (x, t) a suffix of the word ω x denoted ω (x,t) . The construction of ω (x,t) is similar to the construction of ω x . We need to introduce the set of intervals

F (x,t) = I ∩ {t ′ | t ′ t} I ∈ F x } .
For each (x, t), the set F (x,t) is totally ordered by the order induced from M . This allows us to define the suffix of the word ω x associated with time t denoted ω (x,t) . Definition 3.8 Given (x, t) ∈ M k1 × M , the suffix of the word ω x associated with time t is given by the function ω (x,t) : F (x,t) → P defined by: ω (x,t) (I) = P where I ∈ F (x,t) is such that ∀t ′ ∈ I γ(x, t ′ ) ∈ P.

Due to the particular form of the suffixes ω (x,t) , it makes sense to define the first letter of ω (x,t) .

Definition 3.9 Given (x, t) ∈ M k1 × M , the first letter of the suffix ω (x,t) is given by ω x (I) where I is the interval of F x such that t ∈ I. We denote the first letter of ω (x,t) by F(ω (x,t) ).

Let us notice that given (x, t) a point of the space-time M k1 × M there is a unique suffix ω (x,t) of ω x associated with (x, t).

Given a point y ∈ M k2 it may have several (x, t) such that γ(x, t) = y and so several suffixes are associated with y. In other words, given y ∈ M k2 , the future of y is non deterministic, and so a single suffix ω (x,t) is not enough to recover the dynamics of the transition system through the partition P. To encode the dynamical behavior of a point y of the output space M k2 through the partition P, we introduce several notions of dynamical type of a point y w.r.t. P. Definition 3.10 Given a dynamical system (M, γ), a finite partition P of M k2 , a point y ∈ M k2 the suffix dynamical type of y w.r.t. P is denoted Suf P (y) and defined by: Suf P (y) = {ω (x,t) | γ(x, t) = y}.

We have that Suf P (y) is a subset of suffixes of words of Ω P . Definition 3.11 Given a dynamical system (M, γ), a finite partition P of M k2 , an integer n ∈ N, a point y ∈ M k2 the n-subword dynamical type of y w.r.t. P is denoted nSub P (y) and defined by:

nSub P (y) ={ω | γ(x, t) = y and ω is a subword of ω (x,t)
and the length of ω, |ω| n and F(ω) = F(ω (x,t) )}. Definition 3.12 Given a dynamical system (M, γ), a finite partition P of M k2 , a point y ∈ M k2 the subword dynamical type of y w.r.t. P is denoted Sub P (y) and defined by: Sub P (y) = n∈N nSub P (y).

We have that nSub P (y) is a subset of Sub P (y) for all n ∈ N. Notations 3.13 If we want to talk about a dynamical type of the point y without specifying if it is a subword, n-subword or suffix dynamical type, we use the notation T P (y).

Our goal is to refine the partition P in order to build a bisimulation w.r.t. P. For this purpose we consider the equivalence relation between points of the output space M k2 "to have same dynamical type w.r.t. P". This equivalence relation induces a new partition of the output space M k2 which refines P. Definition 3.14 We denote by T (P) the refinement of the partition P obtained by considering the equivalence relation ≡ T (P) on M k2 given by: y 1 ≡ T (P) y 2 if and only if T P (y 1 ) = T P (y 2 ).

Notations 3.15 The partition T (P) is respectively denoted Suf (P), nSub (P) and Sub (P) in the case of the suffix, n-subword and subword dynamical type.

Remark 3.16 The nSub (P) partitions are only relevant for n 2. Indeed, 0Sub (P) = M k2 and 1Sub (P) = P. This is why in the sequel of the paper when we talk about n-subword dynamical typen we always assume n 2.

Remark 3.17 Once T (P) is computed (ix) two possibilities can occur. On one hand we can have that P = T (P), in this situation, we have that P is in fact a bisimulation on (M, γ) w.r.t. P (see Theorem 3.27). On the other hand we can have that P = T (P). In this case we can refine T (P) by considering the dynamical types on T (P). We start by building words on T (P) associated with the trajectories Γ x to obtain Ω T (P) and finally we obtain the different kinds of dynamical types w.r.t. T (P). This leads to a third partition T (T (P)) denoted T 2 (P). Again two situations can occur: T (P) = T 2 (P) or T (P) = T 2 (P). This allows us to consider a general procedure that we describe in the following subsection.

Remark 3.18 The readers familiar with the classical bisimulation algorithm (2.16) realised that the partition induced by 2Sub (P) is sufficent in order to compute bisimulation. We investigate the other dynamical types in order to "accelerate" in some sense the construction of the bisimulation, in particular when the bisimulation algorithm does not terminate (see Corollary 3.37 and Example 4.1).

(ix) the meaning of the word "computed" is discussed in Remark 3.20.

Procedure Bisiω

By starting with some initial partition P 0 we have seen how to build a new partition T (P 0 ). We iterate the construction to obtain a sequence of partitions T i (P 0 ) i∈N such that for each i ∈ N we have that the partition T i+1 (P 0 ) = T T i (P 0 ) corresponds to the partition induced by the dynamical types w.r.t. T i (P 0 ). This construction is summarized by the following procedure, we call this procedure Bisiω. Remark 3.20 Procedure Bisiω is merely conceptual. Indeed in general it is far to be computable. One main problem to be settled is to determine when two general words, as defined in our context, are equal. Let us be more explicit, assume that ω x and ω x ′ are words respectively associated with the trajectories Γ x and Γ x ′ . The problem is that ω x and ω x ′ are not equal as functions since their domains are different: they are respectively F x and F x ′ . Since the order on F x and F x ′ is possibly not discrete, and even not well-founded, we need to introduce a general notion of synchronization for ordered sets which is nothing else than an isomorphism of ordered structures. So we will say that ω x and ω x ′ are equal if and only there exist an isomorphism σ between the ordered structures F x and F x ′ such that for all I ∈ F x we have that ω x (I) = ω x ′ (σ(I)). Let us remark that the partition T (P) is in general even not definable by a first-order L-formula where L is the language given by the order and the initial partition: L = {<, P, γ}. However we have shown that in the case of o-minimal structures the first step of Procedure Bisiω already provides interesting results. A discussion about computation of the words and the dynamical types in this particular case can be found in [START_REF] Brihaye | On the expressiveness and decidability of o-minimal hybrid systems[END_REF].

Remark 3.21 Given P ∈ T (P) it can be seen as a subset of M k2 , or it can be seen as a dynamical type w.r.t. P i.e. a set of words on P. Lemma 3.22 Given y a point of the output space M k2 , the first letter of each ω ∈ T P (y) is P where P ∈ P and y ∈ P . This is true for the each kind of dynamical type defined previously.

Proof: This is an immediate consequence of the different definitions of the dynamical types. ✷ Lemma 3.23 Given a dynamical system (M, γ) and P a partition of M k2 we have that T (P) refines P.

Proof: This a direct consequence of Remark 3.17 and the fact that P = 1Sub(P). ✷ Remark 3.24 By Lemma 3.23 we have that Procedure Bisiω generates a decreasing sequence of partitions:

P ⊇ T (P) ⊇ T 2 (P) ⊇ • • • ⊇ T i (P) ⊇ • • •
To illustrate how Procedure Bisiω works, let us give an example.

Example 3.25 We consider the dynamical system (M, γ) of Example 2.22. We associate to (M, γ) the initial partition P = {A 1 , A 2 } where A 1 = {(0, 0)} and A 2 = R 2 \ {(0, 0)} (see Figure 4). We apply Procedure Bisiω on (M, γ) with P as initial partition and using the suffix dynamical type.

A 1 A 2 Fig. 4: P = {A1, A2}
First, we compute the set of words w.r.t. P,

Ω P = {A 2 , A 1 A 2 , A 2 A 1 A 2 }.
From Ω P we see that there exist three dynamical types w.r.t. P:

B 1 = {A 2 , A 2 A 1 A 2 } ; B 2 = {A 1 A 2 } ; B 3 = {A 2 }.
These dynamical types lead to the new partition Suf (P) = {B 1 , B 2 , B 3 } (see Figure 5) where

B 1 = {(y 1 , 0) | y 1 < 0} ∪ {(0, y 2 ) | y 2 < 0}, B 2 = {(0, 0)} and B 3 = R 2 \ (B 1 ∪ B 2 ).
Notice that Suf (P) is a strict refinement of P, so we iterate the construction. We compute the set of words w.r.t. Suf (P),

Ω Suf(P) = {B 1 B 2 B 3 , B 3 B 1 B 3 , B 2 B 3 , B 1 B 3 , B 3 }.
From Ω Suf(P) we see that there exist four dynamical types w.r.t. Suf (P):

C 1 = {B 1 B 2 B 3 , B 1 B 3 } ; C 2 = {B 3 B 1 B 3 } ; C 3 = {B 2 B 3 } ; C 4 = {B 3 }
Again these dynamical types lead to a new partition Suf 2 (P) = {C 1 , C 2 , C 3 , C 4 } (see Figure 6). Let us compute the set of words w.r.t. Suf 2 (P),

Ω Suf 2 (P) = {C 2 C 1 C 4 , C 1 C 3 C 4 , C 1 C 4 , C 3 C 4 , C 4 }. B 1 B 1 B 2 B 3 B 3
Fig. 5:

Suf (P) C 1 C 1 C 3 C 2 C 4 Fig. 6: Suf 2 (P) D 1 D 1 D 3 D 2 D 4
Fig. 7: Suf 3 (P)

From Ω Suf 2 (P) we see that there exist four dynamical types w.r.t. Suf 2 (P):

D 1 = {C 1 C 3 C 4 , C 1 C 4 } ; D 2 = {C 2 C 1 C 4 } ; D 3 = {C 3 C 4 } ; D 4 = {C 4 }
Those four dynamical types do not refine the partition Suf 2 (P) (see Figure 7). In other words, we have the following equality Suf 2 (P) = Suf 3 (P). One can check that Suf 2 (P) is a bisimulation on (M, γ) w.r.t. P.

Remark 3.26 The dynamical system of Example 3.25 is non-deterministic. Indeed two trajectories are associated with each point y of the output space M k2 . In the papers [BMRT04, BM05], we were unable to deal with such situations.

The situation of Example 3.25 is not a particular case. Indeed if Procedure Bisiω terminates, it provides a bisimulation. We can now state the main result of the paper: Theorem 3.27 Let (M, γ) be a dynamical system, let T γ be the associated transition system on M k2 , and let P 0 be a finite partition of M k2 . If Procedure Bisiω terminates, then it provides a bisimulation on T γ w.r.t. P 0 .

Proof: By hypothesis, Procedure Bisiω returns a partition P such that P = T (P). To prove that the equivalence relation induced from P is a bisimulation on T γ w.r.t. P 0 . We will show that given any y 1 , y 2 ∈ A and y ′ 1 ∈ B (for some A, B ∈ P) if y 1 → γ y ′ 1 then there exists y ′ 2 ∈ B such that y 2 → γ y ′ 2 . Since P = T (P), A corresponds to a dynamical type on P (i.e. an element of T (P)). Hence we have that T P (y 1 ) = T P (y 2 ). Depending of the kind of dynamical type, the argument to find y ′ 2 is slightly different. We do the rest of the proof with the suffix dynamical type, the other (x) cases are similar.

Since y 1 → γ y ′ 1 there exists x 1 ∈ M k1 and t 1 , t ′ 1 ∈ M with t 1 t ′ 1 such that γ(x 1 , t 1 ) = y 1 and γ(x 1 , t ′ 1 ) = y ′ 1 . By definition of the suffix dynamical type, ω (x1,t1) ∈ Suf P (y 1 ). Since y 1 ∈ A and y ′ 1 ∈ B, we have that AB is a subword (xi) of ω (x1,t1) . Using the fact that Suf P (y 1 ) = Suf P (y 2 ), we can find x 2 ∈ M k1 and t 2 ∈ M such that γ(x 2 , t 2 ) = y 2 and ω (x2,t2) = ω (x1,t1) . Hence it is possible to find an interval (or a point) I ∈ F (x2,t2) such that ω (x2,t2) (I) = B. We pick any point t ′ 2 ∈ I and clearly we have that y ′ 2 = γ(x 2 , t ′ 2 ) is the desired point.

(x) This of course does not hold for the 0-subword and the 1-subword dynamical types.

(xi) Formally, we have to take {t 1 , t ′ 1 } = M ′ ⊆ M .

We have that P respects P 0 by iterating Lemma 3.23. ✷ Corollary 3.28 Under the assumptions of Theorem 3.27 we have that if there exists P ′ 0 a refinement of P 0 such that P ′ 0 = T (P ′ 0 ) then P ′ 0 is a bisimulation on T γ w.r.t. P 0 . Unfortunately, Procedure Bisiω does not provide in general the coarsest bisimulation on T γ w.r.t. P. Here are two examples that illustrate this fact.

Example 3.29 We consider a dynamical system where the output space consists of two parallel straight lines and the dynamics is completely deterministic, given a point on one of the lines, it goes to infinity without leaving the line. In other words, we have that M = R, < and the dynamics γ : R × {0, 1} × R → R × {0, 1} is defined by γ(x 1 , x 2 , t) = (x 1 + t, x 2 ). We associate with (M, γ) the partition P = {A, B} where B = R × {0, 1} \ A and A is defined as follows:

A = (n -(1/m), 0) | n ∈ N, m ∈ N \ {0} ∪ (n, 1) | n ∈ N .
Let us consider the suffix dynamical type of the two points y 1 = (1/2, 0) and y 2 = (1, 1):

Suf P (y 1 ) = (AB) ω ω
and Suf P (y 2 ) = (AB) ω .

Clearly, y 1 and y 2 do not have the same suffix dynamical type w.r.t. P however one can show that P is the coarsest bisimulation w.r.t. P.

Remark 3.30 In the previous example, the fact that the partition is too fine is due to the fact that the bisimulation does not distinguish (AB) ω and ((AB) ω ) ω . Indeed, in this case the transition system T γ is completely deterministic, so the bisimulation only need to know that the dynamics goes infinitely often from A to B and from B to A. The bisimulation does not care about the "kind of infinity". It is well-known that in the case of deterministic finite transition systems, the bisimulation and language correspond. Example 3.29 shows that considering more complex system make not clear how the notions of language equivalence and bisimulation are related.

Remark 3.31 Let us notice that if we consider n-subword or subword dynamical type on Example 3.29 we obtain the coarsest bisimulation.

However when considering non deterministic system, the next example shows that using 3subword dynamical type leads already to a too fine analysis.

Example 3.32 Let us consider the dynamical system of Figure 8 with the partition P = {A, B, C}. Let us consider the 3-subword dynamical type of the two points y 1 and y 2 . 3Sub P (y 1 ) = {ABC} and 3Sub P (y 2 ) = {AB, AC} .

Clearly, y 1 and y 2 do not have the same 3-subword dynamical type w.r.t. P, however one can show that P is the coarsest bisimulation w.r.t. P.

Nevertheless if we look at the 2-subword dynamical type, we always obtain the coarsest bisimulation as stated in the following theorem. Theorem 3.33 Let (M, γ) be a dynamical system, let T γ be the associated transition system on M k2 , and let P 0 be a finite partition of M k2 . If Procedure Bisiω terminates with the 2-subword dynamical type, then it provides the coarsest bisimulation on T γ w.r.t. P 0 .

Proof: By Theorem 3.27 we already know that Procedure Bisiω provides a bisimulation on T γ w.r.t. P 0 , it remains to show that it is the coarsest. We proceed ab absurdo. Hence we suppose there exists some step of Procedure Bisiω and y 1 , y 2 ∈ M k2 such that y 1 ∼ P0 y 2 and 2Sub P (y 1 ) = 2Sub P (y 2 ). We can choose this step such that each piece of P is a union of equivalence classes for ∼ P0 . We have that y 1 ∈ A for some A ∈ P. Since 2Sub P (y 1 ) = 2Sub P (y 2 ), we can suppose AB ∈ 2Sub P (y 1 ) and AB / ∈ 2Sub P (y 2 ) for some B ∈ P. This means that there exists y ′ 1 ∈ B with y 1 → γ y ′ 1 and that it is impossible to find y ′ 2 ∈ B with y 2 → γ y ′ 2 . Since y 1 ∼ P0 y 2 and B is a union of equivalence classes for ∼ P0 , this contradicts that ∼ P0 is a bisimulation. ✷ Corollary 3.34 Let (M, γ) be a dynamical system, let T γ be the associated transition system on M k2 , and let P 0 be a finite partition of M k2 . Procedure Bisiω terminates with the 2-subword dynamical type if and only if there exists a finite bisimulation on T γ w.r.t. P 0 .

Proof: If there exists a finite bisimulation on T γ w.r.t. P 0 , the proof of Theorem 3.33 shows that Procedure Bisiω terminates.

Let us now suppose that Procedure Bisiω terminates. Since P 0 is finite, the number of 2subword dynamical types is finite, (i.e. 2Sub (P 0 ) is finite). By an easy induction using the same argument, one can see that 2Sub i (P 0 ) is finite for all i ∈ N. Hence if Procedure Bisiω terminates, we clearly have that there exists a finite bisimulation on T γ w.r.t. P 0 . ✷

In the sequel, we investigate extra assumptions which provide that Procedure Bisiω terminates with the coarsest bisimulation. Theorem 3.35 Let (M, γ) be a dynamical system and let P 0 be a finite partition of M k2 such that for all n ∈ N and for all y ∈ M k2 we have that Suf Sub n (P0) (y) reduces to a singleton, and let T γ be the associated transition system on M k2 . If Procedure Bisiω terminates with the subword dynamical type, then it provides the coarsest bisimulation on T γ w.r.t. P 0 .

Proof: The proof is similar to the proof of Theorem 3.33. We also proceed ab absurdo. Hence we can find some step of Procedure Bisiω and y 1 , y ′ 1 ∈ M k2 such that y 1 ∼ P0 y ′ point y ∈ Γ + 1 is given by {B}. If we now consider points on Γ - 1 , one can see that their subword dynamical consists of words in (AB) + or (BA) + . Let us now show that there are infinitely many subword dynamical types by describing explicitely the dynamical types of the points on Γ - 1 . Given y ∈ Γ - 1 , we have that y = γ(1, t) for some t 0, two cases can occur.

If t = -2kπ then (AB) k+1 ∈ Sub P (y) and (AB) k+2 / ∈ Sub P (y), if t ∈ ] -2(k + 1)π, -2kπ[ then (BA) k+1 B ∈ Sub P (y) and (BA) k+2 B / ∈ Sub P (y).

Hence the first step of Procedure Bisiω with subword dynamical types, already provides an infinite partition Sub (P). This shows that there is no finite bisimulation on T γ w.r.t. P by Corollary 3.37. However one can see that Sub (P) = Sub 2 (P). This means that Sub (P) is the coarsest bisimulation on T γ w.r.t. P.

Remark 4.2 In Example 4.1, we have just seen that T γ does not admit a finite bisimulation w.r.t. P. However T γ admits a finite back-bisimulation w.r.t. P. In particular when considering points on the trajectory Γ 1 , we only have two prefixes to consider, (AB) ω and (BA) ω . That justifies the interest of considering both back-bisimulations and bisimulations given a dynamical system.

We now consider an example with self intersecting curve (xii) .

Example 4.3 We consider the dynamical system of Figure 11 with initial partition P = {A 1 , A 2 }.

There are four suffix dynamical types w.r.t. P:

B 1 = {A 1 A 2 A 1 } ; B 2 = {A 2 A 1 } ; B 3 = {A 1 } ; B 4 = {A 1 , A 1 A 2 A 1 }.
This leads to the four pieces partition T (P). The set Ω T (P) consists of the unique word B 1 B 4 B 1 B 2 B 3 B 4 B 3 . There are six dynamical types w.r.t. T (P):

C 1 = {B 1 B 4 B 1 B 2 B 3 B 4 B 3 } ; C 2 = {B 4 B 1 B 2 B 3 B 4 B 3 , B 4 B 3 } ; C 3 = {B 1 B 2 B 3 B 4 B 3 } ; C 4 = {B 2 B 3 B 4 B 3 } ; C 5 = {B 3 B 4 B 3 } ; C 6 = {B 3 }.
We obtain the partition T 2 (P). One can easily check that T 2 (P) = T 3 (P). (xii) This kind of behavior motivated the notion of multidotted words in [START_REF] Brihaye | On o-minimal hybrid systems[END_REF].

Conclusion

In this paper we introduced a merely conceptual algorithm called Procedure Bisiω. This procedure aims to build a finite bisimulation of a given dynamical system w.r.t. a given partition using words. Procedure Bisiω gives a more "global" vision of the bisimulation than the well-known bisimulation algorithm. The papers [START_REF] Korovina | Pfaffian hybrid systems[END_REF][START_REF] Korovina | Upper and lower bounds on sizes of finite bisimulations of Pfaffian hybrid systems[END_REF] illustrates that Procedure Bisiω can help to compute complexity bound on the size of the coarsest bisimulation.

Two of the main challenges for futur work are the following questions, "When is Procedure Bisiω effective?", "When does Procedure Bisiω terminate?".

Another question to address is the following. In Section 3, we introduced several "intermediate"equivalence relations (see Definition 3.14). These equivalence relations deserve to be investigate for their own. At present we did not manage to find any relevant property of these equivalence relations.

  The different dynamical types induced different partitions. Those partitions are related as follows in term of refinement. P ⊇ 2Sub (P) ⊇ ... ⊇ nSub (P) ⊇ ... ⊇ i∈N (iSub (P)) = Sub (P) ⊇ Suf (P)

  Procedure 3.19 Initialization: P := P 0 Do Compute the set of words Ω P Associate T P (y) with each y ∈ M k2 use it to Build T (P) If P = T (P) Then Return P Else P := T (P) End Do

Fig. 8 :

 8 Fig. 8: 3-subword dynamical types do not provide the coarsest bisimulation

Fig. 12 :

 12 Fig. 11: A simple loop

  is a bisimulation on T w.r.t. P}

	Remarks 2.11 Definition 2.10 makes sense since the union of bisimulations on T w.r.t. P is
	still a bisimulation on T w.r.t. P.
	One can show that the coarsest bisimulation on T w.r.t. P is an equivalence relation, moreover
	each piece of the partition P is an union of equivalence classes of ∼ P .

Acknowledgments. The author would like to thank Véronique Bruyère for helpfull discussions and Christian Michaux for careful reading of the drafts of this paper and numerous relevant comments. He also want to thank the referees for their serious work and useful remarks.

Modnet MRTN-CT-2004-512234 and by a grant from the National Bank of Belgium (i) introduced in [LPS00]. 1365-8050

Thomas Brihaye

Sub P (y ′ 1 ). We can choose this step such that each piece of P is a union of equivalence classes for ∼ P0 .

Given any ω = A 1 ...A n ∈ Sub P (y 1 ), we can build the following sequence of transitions.

y 1 → γ y 2 → γ ... → γ y n , with y i ∈ A i for i = 1, ..., n. Since y 1 ∼ P y ′ 1 we can build a similar sequence of transitions.

with y i ∼ P0 y ′ i for i = 1, ..., n. Since each A i is a union of equivalence classes for ∼ P0 , we have that y ′ i ∈ A i for i = 1, ..., n. Let us now prove that the suffix uniqueness hypothesis implies that there exists x ∈ M k1 and t 1 ,...,t n ∈ M with t 1 ... t n such that γ(x, t i ) ∈ A i for i = 1, ..., n ; meaning that ω ∈ Sub P (y ′ 1 ). Clearly we can find x, t 1 , t 2 with t 1 t 2 , γ(x, t 1 ) ∈ A 1 and γ(x, t 2 ) ∈ A 2 (since y ′ 1 → γ y ′ 2 ). Let us suppose, for a contradiction, that given x, t 1 , t 2 such that t 1 t 2 , γ(x, t 1 ) ∈ A 1 and γ(x, t 2 ) ∈ A 2 we have that γ(x, t 3 ) / ∈ A 3 for all t 3 t 2 . In particular, using the suffix uniqueness hypothesis, this means that the unique word of Suf P (y ′ 2 ) does not contain the letter A 3 . This contradicts the existence of the transition y ′ 2 → γ y ′ 3 where y ′ 3 ∈ A 3 . Thus we can find t 3 with the desired conditions. Iterating the same argument we find the other t i 's.

Similarly, given any ω ∈ Sub P (y ′ 1 ), we can prove that ω ∈ Sub P (y 1 ). This contradicts that Sub P (y 1 ) = Sub P (y ′ 1 ). ✷

The assumptions of Theorem 3.35 are very strong. To weaken these assumptions, one could investigate cases where T γ is transitive or deterministic.

Corollary 3.36 Under the hypothesis of Theorem 3.35, if there exists a finite bisimulation on T γ w.r.t. P 0 , Procedure Bisiω terminates with the subword dynamical type.

Corollary 3.37 Under the hypothesis of Theorem 3.35, if some step of Procedure Bisiω, with the subword dynamical type, provides an infinite partition P there is no finite bisimulation on T γ w.r.t. P 0 .

Corollary 3.38 Under the hypothesis of Theorem 3.35, when Procedure Bisiω has terminated, we have that: 2Sub (P) = ... = nSub (P) = ... = Sub (P) ⊇ Suf (P)

Remark 3.39 The assumptions of Theorem 3.35 are satisfied when γ(., .) is a flow of a vector field F : R n → R n which does not depend on the time (this is the assumption in [START_REF] Lafferriere | O-minimal hybrid systems[END_REF]). In this case, T γ is both transitive and deterministic. Remark 3.43 In [START_REF] Brihaye | On o-minimal hybrid systems[END_REF] in order to define the dynamical type of a point w.r.t. some partition, we introduced the notion of (multi)dotted words (instead of the suffixes). One can show that the finite bisimulation obtained with (multi)dotted words is both forward and backward stable. However the use of suffixes instead of (multi)dotted words leads to a coarser bisimulation than the one obtained with the suffixes. This is illustrated in Figures 9 and10. In Figure 9, the partition induced by the dotted words have nine pieces corresponding to the dotted words Ȧ, ȦBA, ..., AB Ȧ, ȦBABA, ..., ABAB Ȧ. In Figure 10, the partition induced by the suffixes have five pieces corresponding to the non empty suffixes of the word ABABA.

Examples

This section illustrates Procedure Bisiω on some examples. In each case, we give a dynamical system (M, γ) and an initial partition P and we observe how Procedure Bisiω behaves.

Example 4.1 We consider a dynamical system (M, γ) related to the spiral example of [START_REF] Lafferriere | O-minimal hybrid systems[END_REF].

We have M = R, < and γ : R 2 × R → R 2 are defined as follows.

γ(x, t) = e t (x cos t, x sin t)

The dynamics γ is a solution of the system of differential equations (2) which is not time depending. Hence we can apply Corollary 3.37 (see Remark 3.39) to this example.

The dynamics γ describes spirals moving away from the origin when time elapses. We associate with this dynamical system the partiton P = {A, B} where A = {(y 1 , 0) | 0 y 1 1} and B = R 2 \ {A}. Let us focus on the the trajectory Γ 1 = {(e t cos t, e t sin t) | t ∈ R}. We divide the trajectory Γ 1 into two distinct parts:

Γ - 1 = {(e t cos t, e t sin t) | t 0} and Γ + 1 = {(e t cos t, e t sin t) | t > 0}

We have that Γ - 1 is included in the ball of radius 1 centered at the origin (0, 0) and Γ + 1 has no interesection with this ball. In particular we have that the subword dynamical type of any