Dual Billiards, Fagnano Orbits, and Regular Polygons.

Serge Troubetzkoy

In this article we consider the dual version of two results on polygonal billiards. We begin by describing these original results. The first result is about the dynamics of the so-called pedal map related to billiards in a triangle P . The three altitudes of P intersect the opposite sides (or their extensions) in three points called the feet. These three points form the vertices of a new triangle Q called the pedal triangle of the triangle P (Figure 1). It is well known that for acute triangles the pedal triangle forms a period-three billiard orbit often referred to as the Fagnano orbit, i.e., the polygon Q is inscribed in P and satisfies the usual law of geometric optics (the angle of incidence equals the angle of reflection) or equivalently (this is a theorem) the pedal triangle has least perimeter among all inscribed triangles. The name Fagnano is used since in 1775 J. F. F. Fagnano gave the first proof of the variational characterization. In a sequence of elegant and entertaining articles, J. Kingston and J. Synge [START_REF] Kingston | The sequence of pedal triangles[END_REF], P. Lax [START_REF] Lax | The ergodic character of sequences of pedal triangles[END_REF], P. Ungar [START_REF] Ungar | Mixing property of the pedal mapping[END_REF], and J. Alexander [START_REF] Alexander | The symbolic dynamics of the sequence of pedal triangles[END_REF] studied the dynamics of the pedal map given by iterating this process. The second result, due to DeTemple and Robertson [START_REF] Detemple | A billiard path characterization of regular polygons[END_REF], is that a closed convex polygon P is regular if and only if P contains a periodic billiard path Q similar to P .

There is a dual notion to billiards, called dual or outer billiards. The game of dual billiards is played outside the billiard table. Suppose the table is a polygon P and that z is a point outside P and not on the continuation of any of P 's There are two support lines to P through z; choose the right one as viewed from z. If z is not on the continuation of a side of the convex hull of P then this support line intersects P at a single point which we call the support vertex of z. Reflect z in its support vertex to obtain z's image under the dual billiard map denoted by T (see Figure 2). The map T n is defined for all n at the point z if none of its images belongs to the continuation of a side of the convex hull of the polygon. Dual billiards have been extensively studied by S. Tabachnikov (see [START_REF] Tabachnikov | Panoramas et Synthèses[END_REF]- [START_REF] Tabachnikov | Dual billiards[END_REF] and the reference therein).

Throughout the article we will identify the polygon having vertices z i ∈ C, i = 1, . . . , n, ordered cyclically with the point z = (z 1 , . . . , z n ) ∈ C n . In particular a polygon for us is an oriented object. The notion of polygon includes self-intersecting polygons (which we call star shaped polygons) and geometrically degenerate n-gons: those with a side of length 0, or an angle of π or 2π at a vertex. Corresponding to the fact that the Fagnano billiard orbit hits each side of the triangle, we call an n-periodic dual billiard orbit consisting of n points consecutively reflected in the vertices z 1 , z 2 , . . . , z n a Fagnano dual billiard orbit. Fagnano orbits for dual billiards were introduce by Tabachnikov in [START_REF]Fagnano orbits of polygonal dual billiards[END_REF], where he studied a certain variational property analogous to one in the pedal case studied by Gutkin [START_REF] Gutkin | Two applications of calculus to triangular billiards[END_REF].

Motivated by the notion of pedal triangles, we introduce here dedal n-gons. An n-gon Q is called a dedal n-gon of the n-gon P if reflecting the vertex w i of Q in the vertex z i of P yields the vertex w i+1 . (Throughout the article all subscripts will be taken modulo n without explicit mention.) There is no requirement that the sides of Q touch P only at a vertex. From the definition it is clear that if a Fagnano orbit of an n-gon P exists then it is a dedal n-gon. A nondegenerate polygon can have a degenerate dedal polygon and vice-versa. Examples are shown in Figures 3 and4. The degeneracy not shown cannot occur: i.e., it is impossible for two consecutive vertices of P to coincide if Q is nondegenerate. We will not dwell on this aspect.

w 1 w 2 w 3 w 4 w 5 z 1 z 2 z 3 z 4 z 5 w 1 w 2 w 3 w 4 w 5 z 1 z 3 z 4 z 2 = z 5
1 w 2 w 5 z 1 z 2 z 4 z 5 w 3 = w 4 = z 3 w 1 w 2 w 3 w 4 w 5 z 1 z 2 z 3 z 4 z 5 w 1 w 2 w 3 w 4 w 5 z 1 z 2 z 3 z 4 z 5
In this article we study the dedal n-gon(s) Q of an n-gon P . Our main results are the following. If n is odd then its dedal n-gon exists and is unique.

For n even we give a necessary and sufficient condition for the existence of dedal n-gons and describe the space of all dedal n-gons of P . Then we go on to characterize regular and affinely regular n-gons by similarity to their dedal n-gons. Finally we give a complete description of the dynamics of the developing map µ(Q) := P . The proofs of all our results boil down to some linear algebra of the dedal map.

After we wrote this article one of the anonymous referees pointed out that iteration of the developing map has already been studied by Berlekamp, Gilbert, and Sinden in 1965 [START_REF] Berlekamp | A polygon problem[END_REF]. They answer a question they attribute to G. R. MacLane, namely, they prove that for almost every polygon Q there exists an M ≥ 1 such that µ M (Q) is convex. Note that the image of a convex polygon is convex; thus this implies that for almost every Q there exists an

M such that µ m (Q) is convex for all m ≥ M . Suppose Q(w 1 , . . . , w n ) is a dedal polygon of P (z 1 , . . . , z n ). The definition implies that z i = (w i + w i+1 )/2
(see Figures 3,4, and 5). The linear transformation µ :

C n → C n given by µ(w 1 , . . . , w n ) = (z 1 , . . . , z n ) is called the developing map. The characteristic polynomial of µ is (1 -2x) n -(-1) n .
Its eigenvalues are (1 + q i )/2 for i = 0, 1, . . . , n -1, where q := exp(2πi/n).

All the eigenvalues differ from zero except for the (n/2)th eigenvalue when n is even. The ith eigenvector is X i := (1, q i , q 2i , . . . , q (n-1)i ). The vectors X i form a basis of our space of polygons. If i divides n then X i is a polygon with n/i sides. Nonetheless for the sake of clarity (avoiding stating special cases) we will think of this as an n-gon which is traced i times; for example if n = 6 then X 2 = (1, q 2 , q 4 , q 6 , q 8 , q 10 ) = (1, q 2 , q 4 , 1, q 2 , q 4 ) traces the triangle (1, q 2 , q 4 ) twice. An exception to this rule is the case n even and i = n/2. In this case X n/2 is a segment which we do not consider as a polygon.

The following proposition clarifies the existence of dedal polygons.

Proposition 1 a) Suppose that n ≥ 3 is odd. Then for any n-gon P there is a unique dedal n-gon Q. b) If n ≥ 3 is even then dedal n-gons exist if and only if the vertices of P satisfy

z 1 -z 2 + z 3 -• • • -z n = 0. If this equation is satisfied then there is a unique dedal n-gon Q 0 in the space X ⊥ n/2 := {z ∈ C n : z • X n/2 = 0}.
The set D := {Q 0 + sX n/2 : s ∈ C} consists of the dedal n-gons of P . In particular for each i ∈ {1, . . . , n} every point w ∈ C is the ith vertex of a unique dedal n-gon Q i (w).

We remark that the condition z 1z 2 + z 3 -• • •z n = 0 means that the center of mass of the even vertices coincides with the center of mass of the odd vertices. Proof of Proposition 1. If n ≥ 3 is odd then the map µ is invertible with

w i = z i -z i+1 + z i+2 -• • • + z i-1 ,
and thus the dedal polygon exists and is unique.

On the other hand, if n ≥ 3 is even then the map µ is not invertible. The kernel is one (complex) dimensional and is generated by the vector X n/2 := (1, -1, 1, -1, . . . , 1, -1). Dedal polygons exist if and only if z = (z 1 , z 2 , . . . , z n ) is in the range of µ, i.e., the space spanned by the X i for i = n/2. The range and kernel of µ are orthogonal since if i = n/2 then

X i • X n/2 = (1 + q 2i + q 4i + • • • + q (n-2)i ) -(q i + q 3i + • • • + q (n-1)i ) = 0 -0 = 0.
Thus z is in the range of µ if and only if it satisfies z • X n/2 = 0, or equivalently Alternatively, to see this note that

z 1 -z 2 + z 3 -• • • -z n = 0. ( 1
)
w 1 w 2 w 3 w 4 w 5 z 1 z 2 z 3 z 4 z 5
z 1 + z 3 + • • • + z n-1 = 1 2 ((w 1 + w 2 ) + (w 3 + w 4 ) + • • • + (w n-1 + w n )) = 1 2 ((w 2 + w 3 ) + (w 4 + w 5 ) + • • • + (w n + w 1 )) = z 2 + z 4 + • • • + z n .
The uniqueness of Q 0 follows since the map µ is invertible on the space X ⊥ n/2 . The statement about the set D follows immediately since X n/2 is the kernel of µ. Let Q 0 := (w 0 1 , . . . , w 0 n ). For each i, any point w ∈ C can be uniquely expressed as w 0 i + s for some s ∈ C.

Suppose that a polygon Q without self intersection is a dedal polygon of P . If Q is convex then it is clearly a Fagnano orbit of P since by convexity the polygon P must be contained in Q. On the other hand if Q is not convex then it cannot be a Fagnano orbit since P cannot be contained in Q. In particular Fagnano orbits always exist for triangles, but not for polygons with more sides. An example of a pentagon without a Fagnano orbit is given in Figure 5. Although not every polygon has a Fagnano orbit, it does have a periodic orbit that is nearly as simple. Namely, consider the second iteration T 2 of the dual billiard map. Connecting the consecutive points of a periodic orbit of T 2 yields a polygon. Cutler has shown that the map T 2 has a periodic orbit which lies outside any compact neighborhood of P and the polygon constructed from the orbit makes a single turn about P [START_REF]A proof of Culter's theorem on the existence of periodic orbits in polygonal outer billiards[END_REF]. The existence of a periodic orbit for the usual billiard in an arbitrary polygon remains open.

The set of polygons with center of mass at the origin is

C := {(w 1 , . . . , w n ) ∈ C n : w 1 + • • • + w n = 0}.
The eigenvector X 0 = (1, 1, . . . , 1) represents a polygon which degenerates to a point. The set C is the orthogonal complement of X 0 , i.e., C = {w = (w 1 , . . . , w n ) ∈ C n : w • X 0 = 0}. We will express polygons in the eigenbasis, i.e., we write P = n-1 i=0 a i X i ; the coefficients a i are complex numbers. Since the map µ preserves the center of mass, throughout the rest of the article we assume that the center of mass is at the origin, i.e., a 0 = 0. X 1 and X n-1 are the usual regular n-gon in counterclockwise and clockwise orientation (Figure 6a). If i and n are relatively prime and i ∈ {1, n-1} then X i is star shaped and we also call it regular (Figures 6b andc). Finally if i divides n and i = n/2 then X i is naturally a regular n/i-gon which, as mentioned above, we will think of as (a multiple cover of) a regular n-gon.

Two (unoriented) polygons are called similar if all corresponding angles are equal and all distances are increased (or decreased) in the same ratio. Since we study oriented ordered polygons we additionally want the marking of the vertices of P and Q to correspond, in which case we will call P and Q ⋆-similar.

Thus two polygons

P = n-1 i=1 b i X i and Q = n-1
i=1 a i X i are ⋆-similar if there exists a nonzero complex constant ℓ such that b i = ℓ a i for all i. We will also write this as P = ℓ Q. Note that if P and Q are ⋆-similar then they are similar. On the other hand if P and Q are similar then P is ⋆-similar to a cyclic permutation Q (k) := (w k , w k+1 , w k+2 , . . . , w k-1 ) of Q or a cyclic permutation Q(k) := (w k , w k-1 , w k-2 , . . . , w k+1 ) of Q with the opposite orientation.

In analogy to DeTemple and Robertson's result we have:

Theorem 2 Fix n ≥ 3. An n-gon P is regular if and only if it has a dedal polygon Q which is ⋆-similar to P .

Note that if n is odd then Q is the unique dedal polygon of P , while if n is even then Q is the unique dedal polygon Q 0 ∈ X ⊥ n/2 . Proof. Suppose P is regular, i.e., there is a nonzero complex constant ℓ such that P = ℓ X j , where j = n/2 if n is even. If n is odd then let Q be the unique dedal polygon of P . If n is even then since P is regular it satisfies [START_REF] Alexander | The symbolic dynamics of the sequence of pedal triangles[END_REF]. Thus P has dedal polygons and we choose Q

= Q 0 ∈ X ⊥ n/2 . In both cases let Q = a i X i . Since P = µ(Q) = 1+q i 2 a i X i , we have a i = 0 for i = j, i.e., Q = a j X j . Thus Q is ⋆-similar to P = ℓ X j .
Conversely suppose that Q = a i X i is a dedal polygon of P = b i X i and that P and Q are ⋆-similar, i.e., there is a nonzero complex constant ℓ such that a i = ℓ b i . Since P = µ(Q) we have 1+q i 2 a i = b i for i = 1, . . . , n. Combining this with the ⋆-similarity yields 1+q i 2 = 1/ℓ (a constant) for each i such that a i = 0. It follows q i = q j if a i = 0 and a j = 0. Since q i = q j for i = j it follows that only a single a j is nonnull. Therefore Q = a j X j and thus P = ℓ -1 a j X j , and both are regular. Note that if n is even then i = n/2, since if i = n/2 then (1 + q i )/2 = 0 and thus b i = a i = 0.

Of course we would like to have the analog of Theorem 2 with the usual notion of similarity. We call an n-gon affinely regular if there exists a j (j = n/2 when n is even) such that P is in the subspace A j generated by X j and X n-j . This is equivalent to P being the image of a regular n-gon by an affine transformation, which explains the name.

Theorem 3 a) Suppose n ≥ 3 is odd. An n-gon P is affinely regular if and only if it has a dedal polygon Q which is similar to P . b) If n ≥ 4 is even then an n-gon P appears in the following list of affinely regular polygons if and only if it has a dedal polygon Q which is similar to P . i) Regular n-gons ii) Any P ∈ A j such that there exists k ∈ {1, , . . . , n} \ {n/2} such that n divides j(2k -1)

iii) Any P = b j X j + b n-j X n-j ∈ A j such that there exists k ∈ {1, . . . , n} with b j /b n-j = ±q j(k+3/2)
All triangles are affinely regular. Berlekamp et al. noticed that every triangle is similar to its dedal triangle [START_REF] Berlekamp | A polygon problem[END_REF]. One would like to know if there are other special properties of the polygons in the list.

Proof. Suppose Q (1) = Q = n-1 i=1 a i X i .
Then it is a simple exercise in linear algebra to verify that Q (k) = a i q i(k-1) X i and that Q(k) = a n-i q i(k+1) X i . Thus the similarity of P to Q is equivalent to the existence of a k ∈ {1, . . . , n} and a nonzero complex constant ℓ such that b i = ℓ a i q i(k-1) for i = 1, . . . , n -1 or b i = ℓ a n-i q i(k+1) for i = 1, . . . , n -1.

The structure of the proof is as follows. We group the even and odd cases together and start by proving that the various classes of affinely regular polygons are similar to their dedal polygons. Then we turn to the converse.

Suppose that n is odd and

P = b j X j + b n-j X n-j is affinely regular. Let Q = Q (1) = a i X i be the unique dedal polygon of P . Since P = µ(Q) = 1+q i
2 a i X i , we have a i = 0 for i ∈ {j, n -j}. We claim that there is a nonzero complex constant ℓ such that P = ℓ Q ((n+3)/2) . To see this note that 1 + q j = q j (1 + q -j ) = q j(n+1) (1 + q -j ) = q j(n+1)/2 q j(n+1)/2 (1 + q -j ) or 1 + q j 2q j(n+1)/2 = 1 + q -j 2q -j(n+1)/2 . Thus P = ℓ Q ((n+3)/2) for ℓ := (1 + q j )/(2q j(n+1)/2 ).

The case n is even and P of class (ii) is similar. Consider the dedal polygon Q = Q 0 ∈ X ⊥ n/2 . Again P = µ(Q) implies that a i = 0 if i ∈ {j, n -j}. We claim that there is a nonzero complex constant ℓ such that P = ℓ Q (k+1) . Since n divides j(2k -1) we have 1 + q j = q j (1 + q -j ) = q j+j(2k-1) (1 + q -j ) = q kj q kj (1 + q -j ) or 1 + q j 2q kj = 1 + q -j 2q -kj .

Thus P = ℓ Q (k+1) for ℓ := (1 + q j )/(2q kj ). The case n even and P regular has already been treated in Theorem 2; therefore it remains to treat case (iii) of n even. We suppose P is of this form and want to show that P is similar to Q(k) , i.e., that there is a nonzero complex constant ℓ such that b i = ℓ a n-i q i(k+1) for all i. As before P = µ(Q) implies that a i = 0 if i ∈ {j, n -j}. Combining the two relations, b i = 1+q i 2 a i and b j /b n-j = ±q j(k+3/2) yields b j ±q j(k+3/2) b n-j = ±q j(k+3/2) 1 + q -j 2 a n-j = ±q j(k+1) q j/2 + q -j/2 2 a n-j and b n-j = ±q -j(k+3/2) b j = ±q -j(k+3/2) 1 + q j 2 a j = ±q -j(k+1) q j/2 + q -j/2 2 a j .

Choosing ℓ := ±(q j/2 + q -j/2 )/2 ∈ R yields P = ℓ Q(k) .

We turn now to the converse. We will first prove that for n even or odd if Q = a i X i is similar to P = b i X i then P is affinely regular. We first treat that case when P = ℓ Q (k+1) for some k and ℓ ∈ C \ {0}, i.e., b i = ℓ a i q ik . Since P = µ(Q) we have 1+q i 2 a i = b i for i = 1, . . . , n -1. Note that if n is even then (1 + q n/2 )/2 = 0, and thus b n/2 = 1+q n/2 2 a n/2 = 0 and a n/2 = ℓ -1 q -nk/2 b n/2 is zero as well. For each i such that a i = 0, combining the two relations between a i and b i yields q -ik 1+q i 2 = ℓ. If only a single a j is nonnull, then Q is regular, and since P is similar to Q it is regular as well. Now suppose that a i and a j are nonnull. Then the previous equation implies that (

1 + q i )/(1 + q j ) = q k(i-j) . (2)
Taking absolute values yields |(1 + q i )| = |(1 + q j )|, which implies i = ±j. Thus P is affinely regular.

If n is even we need to conclude more. Note that (1 + q -j )/(1 + q j ) = q -j . Thus taking i = -j in (2) implies 1 = q j(1-2k) . Thus j(2k -1) is a multiple of n, i.e., we are in case (ii) of the list.

Finally suppose that P = µ(Q) and Q are similar but have the opposite orientation, i.e., P = ℓ Q(k) for some ℓ ∈ C \ {0}, or equivalently b i = ℓ a n-i q i(k+1) . the quotient space Ĉ := {[Q] : Q ∈ C}. If Q 1 and Q 2 are ⋆-similar then so are µ(Q 1 ) and µ(Q 2 ), and thus the map µ defines a map μ of Ĉ to itself.

We remark that the equivalence class [Q] of a polygon Q = a i X i can be represented by the vector (a 1 , . . . , a n-1 ) ∈ C n-1 \ {(0, . . . , 0)} with the identification (a 1 , . . . , a n-1 ) ≡ (ℓa 1 , . . . , ℓa n-1 ) with ℓ ∈ C \ {0}. Thus the quotient space Ĉ is naturally identified with the complex projective space CP n-2 .

Let S be the unit sphere in C, i.e., the set of all For each j ∈ {1, . . . , ⌈n/2⌉ -1} let B j ⊂ C be the subspace generated by {X j , X j+1 , . . . , X n-j }. Let B ⌈n/2⌉ := ∅, and Aff := ∪ ⌈n/2⌉-1 j=1 A j . For any subset D ⊂ C let D := {[P ] : P ∈ D}. We will only use this notation for sets D which are maximal in the sense that if D = Ê then E ⊂ D.

Q = a i X i ∈ C such that |a i | 2 = 1. Each equivalence class [Q] intersects the unit sphere S in a circle, i.e., [Q] ∩ S = {ℓQ : |ℓ| = 1/ |a i | 2 }. We define dist([P ], [Q]) = inf{d(P 0 , Q 0 ) : P 0 ∈ [P ] ∩ S, Q 0 ∈ [Q] ∩ S},
Theorem 5 For each j ∈ {1, . . . , ⌈n/2⌉ -1} the set Âj is an exponential attractor with basin Bj \ B j+1 and thus Âff is a global exponential attractor for μ. The map μ is n-periodic (i.e., μn = Id) on each Âj , and thus on Âff.

Proof. Suppose Q ∈ B j \B j+1 . Equation [START_REF] Kingston | The sequence of pedal triangles[END_REF] implies that the polygon µ m (Q) = n-1 i=1 ( 1+q i 2 ) m a i X i = n-j i=j ( 1+q i 2 ) m a i X i is ⋆-similar to 2 1 + q j m µ m (Q) = a j X j + n-j-1 i=j+1 1 + q i 1 + q j m a i X i + 1 + q n-j 1 + q j m a n-j X n-j .

Since |(1+q i )/(1+q j )| < 1 the terms in the middle sum are exponentially small. Thus μm ([Q]) is exponentially close to the equivalence class [P m ] ∈ Âj of the polygon P m := a j X j + (1 + q n-j )/(1 + q j ) m a n-j X n-j . The fact that Âff is a global attractor follows from this since Ĉ is the union of the Bj . Lemma 4 immediately implies that μ is periodic on each Âj .

Figure 1 :Figure 2 :

 12 Figure 1: A pedal triangle.

Figure 3 :

 3 Figure 3: Nondegenerate dedal pentagons corresponding to degenerate pentagons, with angle π and 2π.

  w

Figure 4 :

 4 Figure 4: Degenerate dedal polygons: loss of a vertex, angle π, and angle 2π.

Figure 5 :

 5 Figure 5: A pentagon without a Fagnano orbit. The unique dedal pentagon is pictured.

Figure 6 :

 6 Figure 6: Up to orientation there are three regular 7-gons.

  where d((a 1 , . . . , a n-1 ), (b1 , . . . , b n-1 )) = ( |a ib i | 2 ) 1/2 is the Euclidean distance on S.It is a simple exercise to verify that this defines a metric on Ĉ.A μ-invariant set A ⊂ Ĉ is an exponential attractor with basin B for μ if there exists c, γ > 0 such that dist(μ m ([Q]), A) ≤ c exp(-γm) for all m ≥ 0 and all [Q] ∈ B. If B = Ĉ then we say that A is a global exponential attractor.

Acknowledgments. Many thanks to Sergei Tabachnikov and the two anonymous referees for helpful remarks.

Combing this with 1+q i 2 a i = b i yields 1+q i 2 a i = ℓ a n-i q i(k+1) . If n is even and i = n/2 then this equation implies that a n/2 = 0. For all other cases it implies that a i and a n-i are simultaneous zero or nonzero. For any i such that they are nonzero there are two such equations, and they imply

This in turn yields

It is easy to see that f (i) = f (j) if and only if j = i or j = ni. Since the left-hand side of Equation ( 4) does not depend on i, there is exactly one pair (a j , a n-j ) of nonzero coefficients, i.e., Q is affinely regular. Since P is similar to Q it is also affinely regular.

Finally suppose that n is even. Equations ( 3) and ( 4) imply that for each j there exists k ∈ {1, 2 . . . , n} such that b j b n-j = ± f (j)q j(k+1) 1 + q -j = ± 1 + q j 1 + q -j q j(k+1) = ±q j(k+3/2) , i.e., we are in case (iii) of the list.

Proof. Suppose Q = a j X j + a n-j X n-j . Then

In analogy to the billiard results stated in the introduction we now study the dynamics of µ. On the space C the dynamics are not very interesting: µ m (Q) → (0, . . . , 0) as m → ∞ for all Q ∈ C. To get a somewhat more interesting behavior notice that ⋆-similarity is an equivalence relation. Let [Q] := {ℓQ : ℓ ∈ C \ {0}} denote the equivalence class of Q. By identifying ⋆-similar polygons we obtain


Franck Cassez
email: franck.cassez@cnrs.irccyn.fr

Emmanuel David

Kim G Fleury

Larsen

Efficient On-the-Fly Algorithms for Partially Observable Timed Games ⋆

In this paper, we review some recent results on the efficient synthesis of controllers for timed systems. We first recall the basics of controller synthesis for timed games and then present an efficient onthe-fly algorithm for reachability games and its extension to partially observable timed games.

 that introduced truly on-the-fly algorithms for the synthesis of controllers for timed games. These results were obtained together with Alexandre

Introduction

The control problem (CP) for discrete event systems was first studied by Ramadge & Wonham in [START_REF] Ramadge | The control of discrete event systems[END_REF]. The CP is the following: "Given a finite-state model of a plant P (open system) with controllable and uncontrollable discrete actions and a control objective Φ, does there exist a controller f such that the plant supervised by f (closed system) satisfies Φ?"

The dense-time version of the CP with an untimed control objective has been investigated and solved in [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. In this seminal paper, Maler et al. consider a plant P given by a timed game automaton which is a standard timed automaton [START_REF] Alur | A theory of timed automata[END_REF] with its set of discrete actions partitioned into controllable and uncontrollable actions. They give an algorithm to decide whether a controller exists or not, and show that if one such controller exists, a witness can be effectively computed. In [START_REF] Wong-Toi | The synthesis of controllers for linear hybrid automata[END_REF], Wong-Toi has given a semi-algorithm to solve the CP when the plant is defined by an extended class of timed game which is a hybrid (game) automaton.

The algorithms for computing controllers for timed games are based on backwards fix-point computations of the set of winning states [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF][START_REF] Asarin | Controller synthesis for timed automata[END_REF][START_REF] De Alfaro | Symbolic algorithms for infinitestate games[END_REF]. For timed game automata, they were implemented in the tool Kronos [START_REF] Altisen | A framework for scheduler synthesis[END_REF] at the end of 90's but lack efficiency because they require the computation of the complete set of winning states. Moreover the backward computation may sometimes not terminate or be very expensive for some extended classes of timed game automata, for instance if integer assignments of the form i := j + k are allowed on discrete transitions.

In the last ten years, a lot of progress has been made in the design of efficient tools for the analysis (model-checking) of timed systems. Tools like Kronos [12] or Uppaal [START_REF] Larsen | Uppaal in a Nutshell[END_REF] have become very efficient and widely used to check properties of timed automata but still no real efficient counterpart had been designed for timed games.

One of the reason may be that on-the-fly algorithms have been absolutely crucial to the success of these model-checking tools. Both reachability, safety as well as general liveness properties of such timed models may be decided using on-the-fly algorithms i.e. by exploring the reachable state-space in a symbolic forward manner with the possibility of early termination. Timed automata technology has also been successfully applied to optimal scheduling problems with on-the-fly algorithms which quickly lead to near-optimal (time-or cost-wise) schedules [START_REF] Asarin | As soon as possible: Time optimal control for timed automata[END_REF]5,18,[START_REF] Rasmussen | Resource-optimal scheduling using priced timed automata[END_REF]1].

Regarding timed games, in [START_REF] Tripakis | On-the-Fly Controller Synthesis for Discrete and Timed Systems[END_REF]3], Altisen and Tripakis have proposed a partially on-the-fly method for solving timed games. However, this method involves an extremely expensive preprocessing step in which the quotient graph of the timed game w.r.t. time-abstracted bisimulation 1 needs to be built. Once obtained this quotient graph may be used with any on-the-fly game-solving algorithms for untimed systems.

In a recent paper [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF], we have proposed an efficient, truly on-the-fly algorithm for the computation of winning states for (reachability) timed game automata. Our algorithm is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka in [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] for linear-time model-checking of finite-state systems. Being on-the-fly, this symbolic algorithm may terminate before having explored the entire state-space, i.e. as soon as a winning strategy has been identified. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure.

This algorithm has been implemented in Uppaal-TiGA [START_REF] Behrmann | Uppaaltiga: Time for playing games![END_REF] which is an extension of the tool Uppaal [START_REF] Larsen | Uppaal in a Nutshell[END_REF]. Some recent experiments with Uppaal-TiGA are reported in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] and show promising results. More recently in [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF], we have extended this algorithm to deal with partially observable timed games and implemented it in a prototype based on Uppaal-TiGA.

In this paper we focus on reachability timed games and present the on-the-fly algorithms of [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF][START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF] and conclude with some current research directions.

The plan of the paper is the following: in Section 2 we recall the basics of timed game automata and the backwards algorithms used to compute safety and reachability games. In Section 3 we present the efficient truly on-the-fly algorithm for reachability games that was introduced in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] and implemented in Uppaal-TiGA. In Section 4 we show how it can be adapted [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF] to compute winning states for timed games under partial observation. Finally in Section 5 we give some current research directions.

Backward Algorithms for Solving Timed Games

Timed Game Automata (TGA) were introduced in [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] for solving control problems on timed systems. This section recalls the basic results for the controller synthesis for TGA. For a more complete survey the reader is referred to [START_REF] Bouyer | On the control of timed and hybrid systems[END_REF].

Notations

Let X be a finite set of real-valued variables called clocks. R ≥0 stands for the set of non-negative reals. We note C(X) the set of constraints ϕ generated by the grammar:

ϕ ::= x ∼ k | x -y ∼ k | ϕ ∧ ϕ where k ∈ Z, x, y ∈ X and ∼∈ {<, ≤, = , >, ≥}. B(X) is the subset of C(X) that uses only rectangular constraints of the form x ∼ k. A valuation v of the variables in X is a mapping v : X → R ≥0 . We let R X
≥0 be the set of valuations of the clocks in X. We write 0 for the valuation that assigns 0 to each clock. For Y ⊆ X, we denote by v[Y ] the valuation assigning 0 (resp. v(x)) to any x ∈ Y (resp. x ∈ X \ Y ). We denote v + δ for δ ∈ R ≥0 the valuation s.t. for all x ∈ X,

(v + δ)(x) = v(x) + δ. For g ∈ C(X) and v ∈ R X ≥0 , we write v |= g if v satisfies g and [[g]] denotes the set of valuations {v ∈ R X ≥0 | v |= g}. A zone Z is a subset of R X ≥0 s.t. [[g]]= Z for some g ∈ C(X).

Timed Automata & Simulation Graph

Definition 1 (Timed Automaton [START_REF] Alur | A theory of timed automata[END_REF]). A Timed Automaton (TA) is a tuple A = (L, ℓ 0 , Act, X, E, Inv) where L is a finite set of locations, ℓ 0 ∈ L is the initial location, Act is the set of actions, X is a finite set of real-valued clocks,

E ⊆ L × B(X) × Act × 2 X × L is a finite set of transitions, Inv : L → B(X)
associates with each location its invariant.

A state of a TA is a pair (ℓ, v) ∈ L × R X ≥0 that consists of a location and a valuation of the clocks. From a state (ℓ, v) ∈ L × R X ≥0 s.t. v |= Inv(ℓ), a TA can either let time progress or do a discrete transition. This is defined by the transition relation -→⊆

(L × R ≥0 ) × Act ∪ R ≥0 × (L × R ≥0 ) built as follows: -for a ∈ Act, (ℓ, v) a --→ (ℓ ′ , v ′ ) if there exists a transition ℓ g,a,Y -----→ ℓ ′ in E s.t. v |= g, v ′ = v[Y ] and v ′ |= Inv(ℓ ′ ); -for δ ≥ 0, (ℓ, v) δ --→ (ℓ, v ′ ) if v ′ = v + δ and v, v ′ ∈[[Inv(ℓ)]].
Thus the semantics of a TA is the labeled transition system S A = (Q, q 0 , Act × R ≥0 , -→) where Q = L × R X ≥0 , q 0 = (ℓ 0 , 0) and the set of labels is Act ∪ R ≥0 . A run of a timed automaton A is a (finite or infinite) sequence of alternating time and discrete transitions in S A . We use Runs((ℓ, v), A) for the set of runs that start in (ℓ, v). We write Runs(A) for Runs((ℓ 0 , 0), A). If ρ is a finite run we denote last (ρ) the last state of the run. An example of a timed automaton is given in Figure 1 where [x ≤ 4] denotes the invariant of location ℓ 4 .

ℓ1 ℓ2 ℓ3 ℓ4 [x ≤ 4] Goal ℓ5 x ≤ 1;c1 x > 1;u1 x < 1 u2 x := 0 x ≥ 2;c2 x < 1 u3 c3 x ≤ 1;c4 Fig. 1. A Timed Game Automaton
The analysis of TA is based on the exploration of a graph, the simulation graph, where the nodes are symbolic states. A symbolic state is a pair (ℓ, Z) where ℓ ∈ L and Z is a zone of R X ≥0 . Let S ⊆ Q and a ∈ Act we define the a-successors and a-predecessors of S respectively by:

Post a (S) = {(ℓ ′ , v ′ ) | ∃(ℓ, v) ∈ S, (ℓ, v) a --→ (ℓ ′ , v ′ )} Pred a (S) = {(ℓ, v) | ∃(ℓ ′ , v ′ ) ∈ S, (ℓ, v) a --→ (ℓ ′ , v ′ )}.
The set of timed successors, S ր , of S is defined by:

S ր = {(ℓ, v + d) | (ℓ, v) ∈ S∩ [[Inv(ℓ)]], (ℓ, v + d) ∈[[Inv(ℓ)]], d ∈ R ≥0 }.
Let =⇒ be the relation defined on symbolic states by: (ℓ, Z)

a =⇒ (ℓ ′ , Z ′ ) if (ℓ, g, a, Y, ℓ ′ ) ∈ E and Z ′ = ((Z∩ [[g ]])[Y ]) ր .

The simulation graph SG(A) of

A is given by the labeled transition system (Z(Q), S 0 , Act, =⇒), where Z(Q) is the set of zones of Q, S 0 = (({(ℓ 0 , 0)} ր )∩ [[Inv(ℓ 0 )]] and =⇒ defined as above. If A is bounded, i.e. all the clocks are bounded, the number of symbolic states is finite and SG(A) is finite as well. Otherwise, a finite simulation graph that preserves for instance reachability property can be constructed for any TA. In this case, we can either transform the given TA into an equivalent one in which all location-invariants insist on an upper bound on all clocks or, alternatively, we can apply standard extrapolation w.r.t. maximal constant occurring in the TA (which is correct up to time-abstracted bisimulation).

Safety and Reachability Games

Definition 2 (Timed Game Automaton [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]). A Timed Game Automaton (TGA) G is a timed automaton with its set of actions Act partitioned into controllable (Act c ) and uncontrollable (Act u ) actions.

The automaton in Figure 1 is also a TGA: controllable actions are depicted with plain arrows and uncontrollable ones with dashed arrows.

Given a TGA G and a set2 of states K ⊆ L × R X ≥0 the reachability control problem consists in finding a strategy f s.t. G supervised by f enforces G to enter a state in K. The safety control problem is the dual asking for the strategy to constantly avoid K. By "a reachability game (G, K)" (resp. safety) we refer to the reachability (resp. safety) control problem for G and K.

Let (G, K) be a reachability (resp. safety) game. Assume that all the states reachable from (l, v) ∈ K are also in K. A finite or infinite run ρ = (ℓ 0 , v 0 )

e0 -→ (ℓ 1 , v 1 ) e1 -→ • • • en -→ (ℓ n+1 , v n+1 ) • • • in Runs(G) is winning if there is some k ≥ 0 s.t. (ℓ k , v k ) ∈ K (resp. for all k ≥ 0, (ℓ k , v k ) ∈ K).
We rule out runs with an infinite number of consecutive time transitions of duration 0. The set of winning runs in G from (ℓ, v) is denoted WinRuns((ℓ, v), G).

The formal definition of the control problems is based on the definitions of strategies and outcomes. A strategy [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] is a function that during the course of the game constantly gives information as to what the controller should do in order to win the game. In a given situation, the strategy could suggest the controller to either i) "do a particular controllable action" or ii) "do nothing at this point in time, just wait" which will be denoted by the special symbol λ. Let G = (L, ℓ 0 , Act, X, E, Inv) be a TGA and S G = (Q, q 0 , →) its semantics.

Definition 3 (Strategy).

A strategy f over G is a partial function from the finite runs of Runs(G) to Act c ∪ {λ} s.t. for every finite run ρ

-if f (ρ) ∈ Act c then last (ρ) f (ρ) ---→ (ℓ ′ , v ′ ) for some (ℓ ′ , v ′ ) and -if f (ρ) = λ then last (ρ) δ -→ (ℓ ′ , v ′ ) for some δ > 0 and (ℓ ′ , v ′ ). We denote Strat(G) the set of strategies over G. A strategy f is state-based if ∀ρ, ρ ′ ∈ Runs(G), last (ρ) = last (ρ ′ ) implies that f (ρ) = f (ρ ′ ).
State-based strategies are also called memoryless strategies in game theory [START_REF] De Alfaro | Symbolic algorithms for infinitestate games[END_REF][START_REF] Thomas | On the synthesis of strategies in infinite games[END_REF].

The restricted behavior of a TGA G controlled with some strategy f is defined by the notion of outcome [START_REF] De Alfaro | Symbolic algorithms for infinitestate games[END_REF].

Definition 4 (Outcome). Let f be a strategy over G. The (set of ) outcomes Outcome(q, f ) of f from q in S G is the subset of Runs(q, G) defined inductively by:

-q ∈ Outcome(q, f ), -if ρ ∈ Outcome(q, f ) then ρ ′ = ρ e --→ q ′ ∈ Outcome(q, f ) if ρ ′ ∈ Runs(q, G)
and one of the following three conditions hold:

1. e ∈ Act u , 2. e ∈ Act c and e = f (ρ),

3. e ∈ R ≥0 and ∀0 ≤ e ′ < e, ∃q ′′ ∈ Q s.t. last (ρ) e ′ --→ q ′′ ∧f (ρ e ′ --→ q ′′ ) = λ.
-for an infinite run ρ, ρ ∈ Outcome(q, f ) if all the finite prefixes of ρ are in Outcome(q, f ).

We assume that uncontrollable actions can only spoil the game and the controller has to do some controllable action to win [START_REF] Asarin | Controller synthesis for timed automata[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]18]. In other words, an uncontrollable action cannot be forced to happen in G. Thus, a run may end in a state where only uncontrollable actions can be taken. For reachability games we assume w.l.o.g. that the goal is a particular location Goal i.e.

K = {(Goal, v) | v ∈ R X
≥0 } as depicted on Figure 1. For safety games we have to avoid a particular location Bad i.e.

K = {(Bad, v) | v ∈ R X ≥0 }.
In the sequel we focus on reachability games. A maximal run ρ is either an infinite run (supposing no infinite sequence of delay transitions of duration 0) or a finite run ρ that satisfies either

i) last (ρ) ∈ K or ii) if ρ a --→ then a ∈ Act u i.e.
the only possible discrete actions from last (ρ) (if any) are uncontrollable actions. A strategy f is winning from q if all maximal runs in Outcome(q, f ) are in WinRuns(q, G). A state q in a TGA G is winning if there exists a winning strategy f from q in G. We denote by W(G) the set of winning states in G and WinStrat(q, G) the set of winning strategies from q over G.

Backward Algorithms for Solving Timed Games

Let G = (L, ℓ 0 , Act, X, E, Inv) be a TGA. For timed games, the computation of the winning set of states is based on the definition of a controllable predecessors operator [START_REF] De Alfaro | Symbolic algorithms for infinitestate games[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. The controllable and uncontrollable discrete predecessors of S ⊆ Q are defined by cPred(S) = c∈Actc Pred c (S) and uPred(S) = u∈Actu Pred u (S). A notion of safe timed predecessors of a set S w.r.t. a set U is also needed. Intuitively a state q is in Pred t (S, U ) if from q we can reach q ′ ∈ S by time elapsing and along the path from q to q ′ we avoid U . This operator is formally defined by:

Pred t (S, U ) = {q ∈ Q | ∃δ ∈ R ≥0 s.t. q δ -→ q ′ , q ′ ∈ S and Post [0,δ] (q) ⊆ U} (1)
where

Post [0,δ] (q) = {q ′ ∈ Q | ∃t ∈ [0, δ] s.t. q t --→ q ′ } and U = Q \ U .
The controllable predecessors operator π is formally defined as follows (Figure 2):

π(S) = Pred t S ∪ cPred(S), uPred(S) (2)
s s ′ st S S u × t δ -t c Fig. 2. π(S)
Note that according to this definition, even forced uncontrollable actions (e.g. by an invariant) are not bound to happen and cannot help to win. A controllable action must be taken to reach a winning state and uncontrollable actions can only spoil the game.

If S is a finite union of symbolic states, then π(S) is again a finite union of symbolic states and π(S) is effectively computable. Assume (G, K) is a reachability game. In this case the least fix-point of S = K ∪ π(S) can be computed by the iterative process given by W 0 = K and W n+1 = W n ∪ π(W n ). This computation will converge after finitely many steps for TGA [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF] and the we denote W * the fix-point. As it is proved in [START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF], W * = W(G). Note that W * is the maximal (complete) set of winning states of G i.e. a state is winning iff it is in W * . Thus there is a winning strategy in G iff (ℓ 0 , 0) ∈ W * . Altogether this gives a symbolic algorithm for solving reachability games. For safety games, it suffices to take the greatest fix-point W * of S = K ∩ π(S) and again W * = W(G).

Another important result for reachability and safety TGA is that memoryless strategies are sufficient to win [START_REF] Asarin | Controller synthesis for timed automata[END_REF][START_REF] Maler | On the synthesis of discrete controllers for timed systems[END_REF]. This makes it possible to compute a most permissive state-based strategy. Extracting strategies can be done using the set of winning states W * (see [START_REF] Bouyer | Optimal Strategies in Priced Timed Game Automata[END_REF] for reachability games).

For the example of Figure 1, the set of symbolic winning states is given by: W = {(ℓ 1 , x ≤ 1), (ℓ 2 , x ≤ 2), (ℓ 3 , x ≤ 1), (ℓ 4 , x ≤ 1), (Goal, x ≥ 0)}.

A winning strategy would consist in taking c 1 immediately in all states (ℓ 1 , x) with x ≤ 1; taking c 2 immediately in all states (ℓ 2 , x) with x ≤ 2; taking c 3 immediately in all states (ℓ 3 , x) and delaying in all states (ℓ 4 , x) with x < 1 until the value of x is 1 at which point the edge c 4 is taken.

On-the-Fly Algorithm for Reachability Games

For finite-state systems, on-the-fly model-checking algorithms has been an active and successful research area since the end of the 80's, with the algorithm proposed by Liu & Smolka [START_REF] Liu | Simple Linear-Time Algorithm for Minimal Fixed Points[END_REF] being particularly elegant (and optimal).

In [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF], we have proposed a version of this algorithm for timed games. In the sequel we first present the on-the-fly algorithm for reachability untimed games and then show how to design a symbolic version for timed games.

On-the-Fly Algorithm for Discrete Games

Untimed games are a restricted class of timed games with only finitely many states Q and with only discrete actions, i.e. the set of labels in the semantics of the game is Act. Hence (memoryless) strategies amounts to choosing a controllable action given the current state, i.e. f : Q -→ Act c . For (untimed) reachability games we assume a designated location Goal and the purpose of the analysis is to decide the existence of a strategy f where all runs contains Goal.

The on-the-fly algorithm, OTFUR, we have proposed in [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] is given in Fig. 3. The idea for this algorithm is the following: we assume that some variables store two sets of transitions: ToExplore store the transitions that have explored and ToBackPropagate store the transitions the target states of which has been declared winning. Another variable, P assed, stores the set of states that have already been encountered. Each encountered state q ∈ P assed has a status, W in[q] which is either winning (1) or unknown (0). We also use a variable Depend[q] that stores for each q, the set of explored transitions t s.t. q is a target of t. The initial values of the variables are set by lines 2 to 6.

To perform a step of the on-the-fly algorithm OTFUR, we pick transition a (q, α, q ′ ) in ToExplore ∪ ToBackPropagate (line 10) and process it as follows:

-if the target state q ′ is encountered for the first time (q ′ ∈ P assed), we update P assed, Depend and W in[q ′ ] (lines [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF][15][START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF]. We also initialize some counters (lines 12 and 13) c(q ′ ) and u(q ′ ) which have the following meaning: at each time, c(q ′ ) represents the number of controllable transitions that can be taken to reach a winning state from q ′ and u(s) represents the number of uncontrollable hazardous transitions from q ′ i.e. those for which we do not know yet if they lead to a winning state. When q ′ is first encountered u(q ′ ) is simply the number of outgoing uncontrollable transitions from q ′ . Finally (lines 17 to 20), depending on the status of q ′ we add the outgoing transitions to ToExplore or just schedule the current transition for back propagation if q ′ is winning. -in case q ′ ∈ P assed, it means that either its status has been changed recently (and we just popped a transition from ToBackPropagate) or that a new transition leading to q ′ has been chosen (from ToExplore). We thus check whether the status of q ′ is winning and if yes, we update some information on q: lines 24 and 25 updates the counters c(q) or u(q) depending on the type of the transition being processed (controllable or not). The state q can be declared winning (line 27) if at least one controllable transition leads to a winning state (c(q) ≥ 1) and all outgoing uncontrollable transitions lead to a winning state as well (u(q) = 0). In this case the transitions leading to q (Depend[q]) are scheduled for back propagation (line 29). Otherwise we have just picked a new transition leading to q ′ and we only update Depend[q ′ ] (line 31).

The correctness proof of this algorithm is given by the following theorem:

Theorem 1 ( [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF]). Upon termination of OTFUR on a given untimed game G the following holds:

1. If q ∈ P assed and W in[q] = 1 then q ∈ W(G); 2. If (ToExplore ∪ ToBackPropagate) = ∅ and W in[q] = 0 then q ∈ W(G).

1:

Initialization 2: P assed ← {q0}; 3: ToExplore ← {(q0, α, q ′ ) | α ∈ Act, q α -→ q ′ }; 4:
ToBackPropagate ← ∅; 5:

W in[q0] ← (q0 = Goal ? 1 : 0); // set status to 1 if q0 is Goal 6:

Depend[q0] ← ∅; 7: Main 8:

while

((ToExplore ∪ ToBackPropagate = ∅)) ∧ W in[q0] = 1)) do 9:
// pick a transition from ToExplore or ToBackPropagate 10: e = (q, α, q ′ ) ← pop(ToExplore) or pop(ToBackPropagate); 11:

if q ′ ∈ P assed then 12:

c(q ′ ) = 0; 13:

u(q ′ ) = |{(q ′ a -→ q ′′ , a ∈ Actu}|; 14:

P assed ← P assed ∪ {q ′ }; 15:

Depend[q ′ ] ← {(q, α, q ′ )}; 16:

W in[q ′ ] ← (q ′ = Goal ? 1 : 0); 17:

if W in[q ′ ] = 0 then 18:

ToExplore ← ToExplore ∪ {(q ′ , α, q ′′ ) | q ′ α -→ q ′′ }; 19: else 20:

ToBackPropagate ← ToBackPropagate ∪ {e}; 21:

else 22: if W in[q ′ ] = 1 then 23:
// update the counters of the state q 24:

if α ∈ Actc then c(q) ← c(q) + 1; 25:

else u(q) ← u(q) -1; 26:

// re-evaluate the status of the state q 27:

W in[q] ← (c(q) ≥ 1) ∧ (u(q) = 0); 28:

if W in[q] then 29:

ToBackPropagate ← ToBackPropagate ∪ Depend[q]; 30:

else // W in[q ′ ] = 0 31:

Depend[q ′ ] ← Depend[q ′ ] ∪ {e}; 32: endif 33:
endif 34: endwhile Fig. 3. OTFUR: On-The-Fly Algorithm for Untimed Reachability Games

In addition to being on-the-fly and correct, this algorithm terminates and is optimal in that it has linear time complexity in the size of the underlying untimed game: it is easy to see that each edge e = (q, α, q ′ ) will be added to ToExplore at most once and to ToBackPropagate at most once as well, the first time q is encountered (and added to P assed) and the second time when W in[q ′ ] changes winning status from 0 to 1. Notice that to obtain an algorithm running in linear time in the size of G (i.e. |Q| + |E|) it is important that the reevaluation of the winning status of a state q is performed using the two variables c(q) and u(q).

On-the-Fly Algorithm for Timed Games

We can extend algorithm OTFUR to the timed case using a zone-based forward and on-the-fly algorithm for solving timed reachability games. The algorithm, SOTFTR, is given in Fig. 4 and may be viewed as an interleaved combination of forward computation of the simulation graph of the timed game automaton together with back-propagation of information of winning states. As in the untimed case the algorithm is based on two sets, ToExplore and ToBackPropagate, of symbolic edges in the simulation-graph, and a passed-list, P assed, containing all the symbolic states of the simulation-graph encountered so far by the algorithm. The crucial point of our symbolic extension is that the winning status of an individual symbolic state is no more 0 or 1 but is now the subset W in[S] ⊆ S (union of zones) of the symbolic state S which is currently known to be winning. The set Depend[S] indicates the set of edges (or predecessors of S) which must be reevaluated (i.e. added to ToBackPropagate) when new information about W in[S] is obtained, i.e. when W in[S] W in * . Whenever a symbolic edge e = (S, α, S ′ ) is considered with S ′ ∈ P assed, the edge e is added to the dependency set of S ′ so that that possible future information about additional winning states within S ′ may also be back-propagated to S. In Table 1, we illustrate the forward exploration and backwards propagation steps of the algorithm.

The correctness of the symbolic on-the-fly algorithm SOTFTR is given by the theorem: Theorem 2 ( [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF]). Upon termination of the algorithm SOTFTR on a given timed game automaton G the following holds:

1. If (ℓ, v) ∈ W in[S] for some S ∈ P assed then (ℓ, v) ∈ W(G); 2. If ToExplore ∪ ToBackPropagate = ∅, (ℓ, v) ∈ S \ W in[S] for some S ∈ P assed then (ℓ, v) ∈ W(G).
Termination of the algorithm SOTFTR is guaranteed by the finiteness of the number of symbolic states of SG(A). Moreover, each edge (S, α, T ) will be present in the ToExplore and ToBackPropagate at most 1 + |T | times, where |T | is the number of regions of T : (S, α, T ) will be in ToExplore the first time that S is encountered and subsequently in ToBackPropagate each time the set W in[T ] increases. Now, any given region may be contained in several symbolic states of the simulation graph (due to overlap). Thus the SOTFTR algorithm 1:

Initialization 2:
P assed ← {S0} where S0 = {(ℓ0, 0)} ր ; 3:

ToExplore ← {(S0, α, S ′ ) | S ′ = Postα(S0) ր }; 4: ToBackPropagate ← ∅; 5: W in[S0] ← S0 ∩ ({Goal} × R X ≥0 ); 6: Depend[S0] ← ∅; 7: Main 8: while ((ToExplore ∪ ToBackPropagate = ∅) ∧ (ℓ0, 0) ∈ = W in[S0])) do 9:
// pick a transition from ToExplore or ToBackPropagate 10: e = (S, α, S ′ ) ← pop(ToExplore) or pop(ToBackPropagate); 11:

if S ′ ∈ P assed then 12:

P assed ← P assed ∪ {S ′ }; 13: is not linear in the region-graph and hence not theoretically optimal, as an algorithm with linear worst-case time-complexity could be obtained by applying the untimed algorithm directly to the region-graph. However, this is only a theoretical result and it turns out that the implementation of the algorithm in Uppaal-TiGA is very efficient.

Depend[S ′ ] ← {(S, α, S ′ )}; 14: W in[S ′ ] ← S ′ ∩ ({Goal} × R X ≥0 ); 15: if W in[S ′ ] S ′ then 16: ToExplore ← ToExplore ∪ {(S ′ , α, S ′′ ) | S ′′ = Postα(S ′ ) ր }; 17: if W in[S ′ ] = ∅
We can optimize (space-wise) the previous algorithm. When we explore the automaton forward, we check if any newly generated symbolic state S ′ belongs P assed. As an optimization we may instead use the classical inclusion check: ∃S ′′ ∈ P assed s.t. S ′ ⊆ S ′′ , in which case, S ′ is discarded and we update Depend[S ′′ ] instead. Indeed, new information learned for S ′′ can be new information on S ′ but not necessarily. This introduces an overhead (time-wise) in the sense that we may back-propagate irrelevant information. On the other hand, back-propagating only the relevant information would be unnecessarily complex and would void most of the memory gain introduced by the use of inclusion. In practice, the reduction of the number of forward steps obtained by the inclusion check pays off for large systems and is a little overhead otherwise, as shown in our experiments. It is also possible to propagate information about losing states: in the case of reachability games, if a state is a deadlock state and is not winning, for sure it is losing. This can also speed-up the algorithm. For the example of Figure 1, we can propagate the information that (ℓ 5 , x > 1) is losing which entails (ℓ 1 , x > 1) is losing as well. Then it only remains to obtain the status of (ℓ 1 , x ≤ 1) to determine if the game is winning or not.

4 On-the-Fly Algorithm for Partially Observable Games

Partial Observability

In the previous sections we have assumed that the controller has perfect information about the system: at any time, the controller will know precisely in what state the system is. In general however -e.g. due to limited sensors -a controller will only have imperfect (or partial) information about the state of the environment. For instance some uncontrollable actions may be unobservable. In the discrete case it is well known how to handle partial observability of actions as it roughly amounts to determinize a finite state system.

However for the timed case under partial observability of events, it has been shown in [START_REF] Bouyer | Timed control with partial observability[END_REF] that the controller synthesis problem is in general undecidable. Fixing the resources of the controller (i.e. a maximum number of clocks and maximum allowed constants in guards) regains decidability [START_REF] Bouyer | Timed control with partial observability[END_REF], a result which also follows from the quotient and model construction results of [START_REF] Laroussinie | CMC: A tool for compositional model-checking of real-time systems[END_REF]20].

Another line of work [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF] recently revisited partial observability for finite state systems. This time, the partial observability amounts to imperfect information on the state of the system. Only a finite number of possible observations can be made on the system configurations and this provides the sole basis for the strategy of the controller. The framework of [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF] is essentially turn-based. Moreover, the controller can make an observation after each discrete transition. It could be that it makes the same observation several times in a row, being able to count the number of steps that have been taken by the system.

If we want to extend this work to timed systems, we need to add some more constraints. In particular, the strategy of the controller will have to be stuttering invariant, i.e. the strategy cannot be affected by a sequence of environment or time steps unless changes in the observations occur. In this sense the strategy is "triggered" by the changes of observations. x := 0 x ≥ 0

x ≥ 8

x := 0

x ≥ 8

x := 0

x ≥ 8 kick?

Fig. 5. Timed Game with Imperfect Information.

To illustrate the concepts of imperfect information and stuttering invariance consider the timed game automaton in Figure 5 modelling a production system for painting a box moving on a conveyor belt. The various locations indicate the position of the box in the system: in Sensor a sensor is assumed to reveal the presence of the box, in Sensed the box is moving along the belt towards the painting area, in Paint the actual painting of the box takes place, in Piston the box may be kick?'ed off the belt leading to Off; if the box is not kicked off it ends in End. All phases are assumed to last between 8 and 10 seconds, except for the phase Sensor, which is instantaneous. The uncontrollability of this timing uncertainty is indicated by the dashed transitions between phases. The controller should now issue a single kick?'command at the appropriate moment in order to guarantee that the box will -regardless of the above timing uncertaintybe kicked off the belt. However the controller has imperfect information of the position of the box in the system. In particular, the controller cannot directly observe whether the box is in the Sensed, Paint or in the Piston phase nor can the value of the clock x be observed. Still equipping the controller with its own clock y -which it may reset and test (against a finite number of predicates)it might be possible to synthesize a control strategy despite having only partial information: in fact it may be deduced that the box will definitely be in the Piston area within 20-24 seconds after being sensed. In contrast, an increased timing uncertainty where a phase may last between 6 and 10 seconds will make a single-kick? strategy impossible.

Observation-Based Stuttering Invariant Strategies

In the untimed setting of [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF], each state change produces a new observation. For instance, if a run of the system is

ρ = l 0 a0 --→ l 1 a1 --→ l 2 • • • an --→ l n+1
we make the observation Obs(ρ) = Obs(l 0 )Obs(l 1 ) • • • Obs(l n+1 ) where Obs is a mapping from states to a finite set of observations. In the previous example, even if Sensed, Paint and Piston produce the same observation, say O1, we could deduce where the box is by counting the number of O1.

Also, if each state change produces a new observation in the untimed setting, it cannot be a realistic assumption in the timed setting: time is continuous and the state of the system continuously changes.

A more realistic assumption about the system under observation is that the controller can only see changes of observations. In the previous piston example, assume the system makes the following steps:

(On, x = 0) 8 -→ (On, x = 8) -→ (Sensor, x = 0) -→ (Sensed, x = 0) • • • • • • 9 -→ (Sensed, x = 9) -→ (Paint, x = 0)
The sequence of observations the controller makes is: On Sensor O1 if Obs(On) = On, Obs(Sensor) = Sensor and Obs(Sensed) = Obs(Paint) = O1. This is why in [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF] we consider stuttering-free observations. We assume we are given a finite set of observations

O = {o 1 , o 2 , • • • , o k } and a mapping Obs : L × R X ≥0 → O (i.e.
from the state space of the timed game automaton to O). Given a run of timed game automaton

ρ = (l 0 , v 0 ) e0 --→ (l 1 , v 1 ) e1 --→ (l 2 , v 2 ) • • • en --→ (l n+1 , v n+1 ) • • •
we can define the observation of ρ by the sequence:

Obs(ρ) = Obs(l 0 , v 0 )Obs(l 1 , v 1 ) • • • Obs(l n+1 , v n+1 ) • • •
The stuttering-free observation of ρ is Obs * (ρ) and is obtained from Obs(ρ) by collapsing successive identical observations

o 1 o 1 • • • o 1 into one o 1 .
In this setting the controller has to make a decision on what to do after a finite run ρ, according to the stuttering-free observation of ρ. Let f be a strategy in Strat(G). f is (observation based) stuttering invariant if for all ρ, ρ ′ , finite runs in Runs(G), if

Obs * (ρ) = Obs * (ρ ′ ) then f (ρ) = f (ρ ′ ).
The control problem under partial observation thus becomes: given a reachability game (G, K), is there an observation based stuttering invariant strategy to win (G, K)?

This raises an issue about the shapes of observations in timed systems: assume for the piston game, we define two observations o 1 = (On, x ≤ 3) and o 2 = (On, x > 3). Given any finite run (On, x = 0) r -→ (On, x = r) with r ≤ 10 there is one stuttering-free observation: either o 1 if r ≤ 3 or o 1 o 2 if r > 3. Still we would like our controller to be able to determine its strategy right after each change of observations, i.e. the controller continuously monitors the observations and can detect rising edges of each new observation. This implies that a first instant exists where a change of observations occurs. To ensure this we can impose syntactic constraints on the shape of the zones that define observations. They must be conjunctions of constraints of the form k 1 ≤ x < k 2 where x is a clock and k 1 , k 2 ∈ N.

Playing with Stuttering Invariant Strategies

The controller has to play according to (observation based) stuttering invariant strategies (OBSI strategies for short). Initially and whenever the current observation of the system state changes, the controller either proposes a controllable action c ∈ Act c , or the special action λ (do nothing i.e. delay). When the controller proposes c ∈ Act c , this intuitively means that he wants to play the action c as soon as this action is enabled in the system. When he proposes λ, this means that he does not want to play any discrete actions until the next change of observation, he is simply waiting for the next observation. Thus, in the two cases, the controller sticks to his choice until the observation of the system changes: in this sense he is playing with an observation based stuttering invariant strategy.

Once the controller has committed to a choice, the environment decides of the evolution of the system until the next observation. The game can be thought of to be a two-player game with the following rules:

1. if the choice of the controller is a discrete action c ∈ Act c , the environment can choose to play, as long as the observation does not change, either (i) discrete actions in u ∈ Act u ∪ {c} or (ii) let time elapse as long as c is not enabled. Thus it can produce sequences of discrete and time steps that respect the (i) and (ii) with action c being urgent, 2. if the choice of the controller is the special action λ the environment can choose to play, as long as the observation does not change, any of its discrete actions in Act u or let time pass; it can produce sequences of discrete and time steps respecting the previous constraints; 3. the turn is back to the controller as soon as the next observation is reached.

We have imposes special shape of constraints to ensure that a next first new observation always exists.

The previous scheme formalizes the intuition of observation based stuttering invariant strategies.

To solve the control problem for G under partial observation given by a finite set O, we reduce it to a control problem on a new game G ′ under full observation.

An Efficient Algorithm for Partially Observable Timed Games

The reduction we have proposed in [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF] follows the idea of knowledge based subset construction for discrete games introduced in [START_REF] Chatterjee | Algorithms for omegaregular games with imperfect information[END_REF][START_REF] Wulf | A lattice theory for solving games of imperfect information[END_REF].

Let G = (L, ℓ 0 , Act, X, E, Inv) be a TGA, and Obs : L × R X ≥0 → O be an observation map. Let K be particular location such that (G, K) is a reachability game and there is an observation o s.t. Obs(s) = o ⇐⇒ s ∈ K i.e. the controller can observe if the system is in a winning state. We use Obs(K) for this particular observation. From G we build a finite discrete game G the states of which are unions of pairs of symbolic states (l, Z) (ℓ ∈ L and Z is a zone). Moreover, we require that each state of G contains pairs (l, Z) that have the same observation.

Each set of states S of G corresponds to a set of points where, in the course of the game G, the controller can choose a new action because a new observation has just been seen. The controller can choose either to do a c ∈ Act c or to let time pass (λ). Once the controller has made a choice, it cannot do anything until a new observation occurs. Given a state (l, v) ∈ S and a choice a of the controller, we can define the tree T ree((l, v), a) of possible runs starting in (l, v): this tree is just the unfolding of the game where we keep only the branches with actions in Act u ∪ {a} (see Figure 6, left). In this section, we assume that every finite run can be extended in an infinite run. Then on each infinite branch of this tree, 1. either there is a state with an observation o ′ different from Obs(l, v). In this case we can define the first (time-wise) state with a new observation. Such an example is depicted on Figure 6 (left): from (l, v), there is a first state with a new observation in o 1 and in o 2 . Because we require that our observations have special shapes, this first state always exists. 2. or all the states have the same observation on the branch: this is depicted by the infinite path starting from (l ′ , v ′ ).

• (l, v) • (l ′ , v ′ ) • • o1 o2 S, Obs(S) = o T ree((l, v), a) S S1 Obs = o1 S2 Obs = o2 S k Obs = o k Bad a a a a
Fig. 6. From G to G

We denote Next a (l, v) the set of first (time-wise) states with a new observation that can be reached from (l, v) if the controller plays a. If there is an infinite run from (l ′ , v ′ ) on which all the states have the same observation, we say that (l ′ , v ′ ) is a sink state for a.

We can now define the game G as follows (Figure 6, right):

-the initial state of G is {(ℓ 0 , 0)}; -let S be a state of G with an observation different from Obs(K) (not winning). Let a ∈ Act c ∪ {λ}. If there is a state (l ′ , v ′ ) which is a sink state for a, we add a transition (S, a, Bad) in G. -for each o i ∈ O with o i = Obs(S), if 3 Next a (S) ∩ o i = ∅ we add a transition (S, a, S i ) with

S i = Next a (S) ∩ o i , in G.
Given a state S of G, we let Enabled(S) be the set of actions a s.t. (S, a, S ′ ) for some S ′ . A state S of G is winning if its observation is Obs(K). We let K be the set of winning states of G. Notice that G contains only controllable actions. Still G is non-deterministic and thus it can be considered to be a two-player game: from S, the controller chooses an action and the environment chooses the next state among the successors of S by a. This construction of G has the following property:

Theorem 3 ( [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF]). The controller has a observation-based stuttering invariant strategy in (G, K) iff there is a winning strategy in ( G, K).

We can prove that ( G, K) is finite and furthermore solving (G, K) amounts to solving a finite non-deterministic game. As we have an efficient algorithm, OTFUR (Fig. 3) to solve this type of games we can solve (G, K). To obtain an efficient algorithm written for (G, K) we simply have to use the Next operator to compute the transition relation "as needed" in OFTUR. Moreover, in case a state (l, v) ∈ S is a sink state for a and Obs(l, v) = Obs(S) = Obs(K), there is a transition (S, a, Bad) in G. We assume that Obs(Bad) = Bad and this observation in not winning so that if the controller plays a from S, then he looses which is consistent as there is a infinite run in G which does not encounter any state with the goal observation. In the version of OFTUR for partially observable timed games it is even more important to propagate backwards the information on losing states like Bad.

The version of the efficient algorithm OTFUR (Fig. 3) for discrete game can be adapted to deal with partially observable games: we obtain a new algorithm OTFPOR given in Fig. 7. In this version, Sink a (S) = ∅ stands for "there exists some (l, v) ∈ S s.t. (l, v) is a sink state for a".

Lines 13 to 22 consist in determining the status of the new symbolic state W ′ and push it into ToExplore or ToBackPropagate. Lines 24 and 28 are rather expensive as we have to compute all the symbolic successors of W to determine its new status.

Conclusion & Future Work

In [START_REF] Cassez | Efficient on-the-fly algorithms for the analysis of timed games[END_REF] we have proposed an efficient for the analysis of reachability timed games. It has been implemented in the tool Uppaal-TiGA [START_REF] Behrmann | Uppaaltiga: Time for playing games![END_REF]. Recently in [START_REF] Cassez | Timed Control with Observation Based and Stuttering Invariant Strategies[END_REF] we have proposed a version of this algorithm for partially observable timed games which is currently being implemented.

There are various directions in which this work can be extended:

-for finite state games, we can generalize our results for reachability games to safety games or more general games with Büchi objectives for instance. This can lead to efficient on-the-fly algorithm for finite games. Also we would like to study particular versions of Büchi objectives, e.g. with one repeated location as we may obtain more efficient algorithms for this case; -for timed games, we can write a dual algorithm for safety objectives. Even in this case this is not always satisfactory as the controller could win with a so-called zeno strategy i.e. a strategy with which he keeps the game in a good state by playing infinitely many discrete controllable actions in a finite amount of time [15]. It is thus of great importance to ensure that the controller can win in a fair way. This can be encoded by a control objective which is a strengthened by a Büchi objective: we add a particular clock which is reset when it hits the value 1, and the Büchi objective is to hit 1 infinitely often which ensures time divergence. This Büchi objective can be encoded by a single location being forced infinitely often. If we can design an efficient algorithm for a single repeated state in the finite state case, we may be able to obtain efficient algorithms for synthesizing non-zeno controllers for safety timed systems.

These new efficient algorithms are going to be implemented in the tool Uppaal-TiGA and it is expected that new useful practical results will be obtained for real case-studies.

On x ≤ 10 Sensor

 10

Table 1 .

 1 Running SOTFTG

		then
	18:	ToBackPropagate ← ToBackPropagate ∪ {e};
	19:	else
	20:	// If T ∈ P assed, we assume W in[T ] = ∅
	21: 22:	Good ← W in[S] ∪ Bad ← S S	S	S	c -→T Predc(W in[T ]);
	28:	endif
	29:	endwhile

u -→T Predu(T \ W in[T ])) ∩ S; 23: W in * ← Predt(Good, Bad); 24: if (W in[S] W in * ) then 25: W aiting ← W aiting ∪ Depend[S]; 26: W in[S] ← W in * ; 27: Depend[S ′ ] ← Depend[S ′ ] ∪ {e}; Fig. 4. SOTFTR: Symbolic On-The-Fly Algo. for Timed Reachability Games

For real computation we shall require that K is defined as a finite union of symbolic states.

We let Nexta(S) = ∪s∈SNexta(s).

Acknowledgements

The author wishes to thank Didier Lime and Jean-François Raskin for their careful reading and useful comments on preliminary versions of this paper.

⋆ Work supported by the French National Research Agency ANR-06-SETI-DOTS and by the Fonds National de la Recherche Scientifique, Belgium.

Steps

ToExplore ∪ ToBackPropagate P assed Depend Win # S S ′ 0 --(S0, u1, S1), (S0, u2, S2), (S0, c1, S3) S0 -(S0, ∅)

1 S0 S3 (S0, u1, S1), (S0, u2, S2)

At step n, (S, α, S ′ ) is the transition popped at step n + 1; At step n, +(S, α, S ′ ) the transition added to ToBackPropagate or ToExplore at step n;