Guillaume Halet
email: guillaume.halet@univ-rennes1.fr

Monitoring calcium oscillations in fertilized mouse eggs

Keywords: oocyte, egg, sperm, fertilization, calcium, Ca 2+, fluorescence, imaging

Ca 2+ oscillations in mouse

Introduction

In the great majority of mammalian species, the ovulated egg is blocked at metaphase of the second meiotic division (Metaphase II, or MII). Only fertilization will allow for meiosis to resume, leading to the extrusion of one set of the segregated maternal chromatids, into the second polar body. This is immediately followed by meiotic exit, formation of male and female pronuclei, and progression to the first embryonic mitotic division (cleavage). In conjunction with these cell cycle events, fertilization also elicits the release of the egg's cortical granules in order to prevent polyspermy, and the recruitment of maternal mRNAs for translation of new proteins important for the early stages of embryo development. These events are collectively referred to as "egg activation" (1-4).

In all mammalian species studied to date, the earliest activation event that is detected in the fertilized egg is the triggering of cytoplasmic Ca 2+ oscillations (Figure 1A) that last for several hours (1,4).

Detailed description of the spatio-temporal dynamics of these Ca 2+ oscillations, and the mechanism of their generation, have been provided using the mouse egg as a model (5-7). The importance of these Ca 2+ oscillations is demonstrated by the fact that their inhibition, using Ca 2+ chelators, results in a complete failure of meiotic resumption and egg activation (8). Interestingly, the initiation and completion of the various egg activation events are differentially sensitive to the number, amplitude, and duration of the Ca 2+ spikes, suggesting that the timing and temporal sequence of these events are encoded in the pattern of the fertilization-induced Ca 2+ oscillations (9-12). Intracellular Ca 2+ concentration ([Ca 2+ ]i) also increases in fertilized eggs from non-mammalian species, such as amphibians, fish and marine invertebrates, where the sperm-induced Ca 2+ signal takes the form of a single transient, or a series of oscillations (13).

The monitoring of Ca 2+ oscillations in fertilized eggs can serve both research and clinical purposes. On the egg side, Ca 2+ oscillations are recorded to investigate the dynamics and molecular aspects of egg activation events, such as the regulation of cell cycle resumption by Ca 2+ -calmodulin-dependent protein kinase II, a downstream effector of the [Ca 2+ ]i rise (14). There has been also considerable efforts to uncover the molecular identity of the sperm factor responsible for initiating these Ca 2+ oscillations, with compelling evidence pointing to the sperm-specific phospholipase C zeta (4,7,15).

Accordingly, the recording of [Ca 2+ ] fluctuations in the egg cytoplasm represents a valuable assay to evaluate sperm "quality", i.e. its ability to induce long lasting Ca 2+ oscillations that are required for full egg activation. In line with this, a number of studies have reported the use of mouse eggs as "reporter" of the fertilizing capacity of human sperm, via the monitoring of cytoplasmic Ca 2+ oscillations elicited after ICSI, or injection of human sperm extract or of human recombinant PLCzeta

(16-19).

A number of fluorescent Ca 2+ indicators have been used to investigate fluctuations in [Ca 2+ ]i in mammalian eggs (20). In this chapter, I describe our protocol for the monitoring of Ca 2+ oscillations in fertilized mouse eggs, using the popular ratiometric fluorescent Ca 2+ indicator Fura-2. Fura-2 is a high affinity Ca 2+ indicator (Kd = 145 nM, in vitro), which shows a shift in its excitation spectrum when bound to Ca 2+ , while the fluorescence emission peak (510 nm) remains unchanged. It is therefore classified as a dual-excitation indicator. Free Fura-2 shows an excitation peak around 380 nm, while Ca 2+ -bound Fura-2 shows an excitation peak around 340 nm. Fluctuations in [Ca 2+ ]i are therefore translated into reciprocal fluctuations in Fura-2 emitted fluorescence (F) when excited at 340 or 380 nm [Figure 1 near here] : upon [Ca 2+ ]i increase, the emitted fluorescence at 340-nm excitation (F340) will increase; conversely, the emitted fluorescence at 380-nm excitation (F380) will decrease. The corresponding fluctuations in [Ca 2+ ]i are displayed as the F340/F380 ratio (Figure 1B). The advantage of a ratiometric measurement is that the ratio signal is less affected by fluorescence bleaching, or by variations in Fura-2 loading among the egg population. Note that the F340/F380 signal is not a quantitative measurement of the actual Ca 2+ concentration, which would require calibration of the signal (20). It provides however useful informations regarding the rate, duration, frequency and relative amplitude of the Ca 2+ oscillations.

Materials

All solutions and culture media are prepared with ultrapure water with a resistivity of 18.2M-cm. 2. hCG : Lyophilised pellet of human Chorionic Gonadotrophin/hCG (Intervet) is resuspended in filtered (0.20 µm) ice-cold PBS to a final concentration of 25 IU/ml, and aliquoted as ready-made syringes as described for PMSG.

2.2. T6 medium for sperm capacitation : 100 mM NaCl, 1.42 mM KCl, 0.47 mM MgCl2, 0.36 mM Na2HPO4, 1.78 mM CaCl2, 25 mM NaHCO3, 25 mM Na lactate, 0.47 mM Na pyruvate, 5.56 mM glucose, 10 mg/L phenol red. Store in fridge for 2 weeks. The day before the experiment, add 16 mg/ml BSA, filter (0.20 µm) and incubate overnight in a 5% CO2 incubator.

Egg handling media

1. M2 medium : for egg collection. We use commercial M2 medium (SIGMA) 2. M2-hyaluronidase : A 10x stock solution is prepared by dissolving hyaluronidase (from bovine testes, SIGMA) into M2 medium to a final concentration of 3 mg/ml, and immediately frozen into 250-µl aliquots.

3. H-KSOM medium for [Ca 2+ ]i recordings : 95 mM NaCl, 2.5 mM KCl, 0.35 mM KH2PO4, 0.2 mM Na pyruvate, 1 mM L-glutamine, 0.01 mM EDTA, 0.2 mM MgSO4, 10 mM Na lactate, 4 mM NaHCO3, 1.71 mM CaCl2, 0.2 mM glucose, 20 mM HEPES, 10 mg/L phenol red (see Note 1), pH 7.4. This medium does not contain BSA, so as to promote egg adhesion to the glass coverslip.

Acidic Tyrode for zona removal

We use commercial acidic Tyrode's solution (pH 2.5, SIGMA) that is stored at -20°C as 500-µl aliquots.

Keeping the eggs warm

Eggs must be kept warm for the whole duration of the isolation and dye-loading steps. To do so, culture media and dishes are stored on a hot block set to 37°C (see Note 2).

Egg manipulation using a mouth pipette

The manipulation and transfer of eggs from one dish to another, is facilitated using a "mouth pipette", consisting of a rubber aspiration tube connected to a glass Pasteur pipette. The Pasteur pipette needs to be narrowed at the tip to an inside diameter slightly bigger than the eggs diameter. This is achieved by heating the glass using a Bunsen burner followed by sharp pulling. Cut the pulled glass pipette to the desired length and allow for the pipette to cool down to room temperature before manipulating the eggs.

Fura-2

Prepare a stock solution by resuspending Fura-2-AM in DMSO to a final concentration of 1 mM.

Aliquote and store at -20°C. Avoid exposure of the aliquots to light.

Fluorescence microscopy

In brief, ratiometric Ca 2+ imaging using Fura-2 is performed with an inverted epifluorescence microscope equipped with a 20x objective, a UV light source and a filter wheel with the relevant filters for Fura-2 dual excitation (peak transmission at 340-nm and 380-nm), a 510-nm dichroic mirror, and a 520-nm long-pass emission filter. Fluorescence images (F340 and F380) are captured using a cooled CCD camera, and stored on a computer running a fluorescence imaging software that controls the camera shutter and the excitation filter wheel. To prevent photo-toxicity, a neutral density filter is placed in the path of the excitation light. Importantly, the microscope must also be fitted with a stage incubator, in order to provide a warm (37°C) environment to the cells during imaging (see Note 3).

Fluorescence analysis

Fluorescence measurements (F340 and F380) are realized by drawing a circular region of interest on the fluorescence images, such as to collect fluorescence intensity from the bulk of the egg cytoplasm.

The numerical values reporting the fluctuations in F340 and F380 intensities are exported towards Microsoft Excel to generate line graphs and for calculation of the F340/F380 ratio.

Methods

Superovulation of mice

We use mice from either the CD-1 or MF-1 strains. In order to obtain large amounts of ovulated eggs (see Note 4), inject female mice intraperitoneally with 5-7.5 units pregnant mare's serum gonadotrophin (PMSG), followed 44-48 hours later with 5-7.5 units human chorionic gonadotrophin (hCG) to induce ovulation. Ovulation occurs around 12h following hCG injection.

Preparation of mouse sperm

1. On the day preceding the experiment, prepare two 35-mm dishes each containing 0.5 ml of T6 medium with BSA, under a layer of mineral oil to prevent evaporation. Leave overnight in a 5% CO2 incubator at 37°C for equilibration.

2. On the day of the experiment, sacrify a male mouse of proven fertility, dissect out the epididymides and place them in the drop of T6-BSA under oil. With the help of the dissection binocular and a sterile needle, puncture the epididymides in order to release sperm into the medium.

Discard the epididymal tissue fragments and return the dish to the incubator. Allow 20 minutes for the sperm to disperse.

3. Add 100 µl of this sperm suspension into the second dish containing 0.5 ml T6-BSA. Make sure the drop remains covered with oil. Return the dish to the incubator and incubate for 3 hours to achieve sperm capacitation.

Egg collection

1. Ovulated MII eggs are collected 13-15h after hCG injection. Sacrifice the mice by cervical dislocation and collect the two oviducts in a small tube containing 1 ml warm M2 medium.

2. Thaw one aliquot (250 µl) of M2-hyaluronidase and dissolve into a final volume of 2.5 ml M2, to reach a working concentration of 0.3 mg/ml. 2. Using a dissection binocular, slice open the oviducts using a sterile needle, in order to release the cumulus masses (i.e., ovulated oocytes surrounded by a cloud of granulosa cells, see Note 5) into a 35-mm dish containing pre-warmed M2-hyaluronidase.

3. Following a 3-5 minutes incubation at 37°C on a hot-block, the cumulus cells are dispersed under the action of hyaluronidase and cumulus-free oocytes can be collected by mouth-pipetting (see Note 6). This is followed by two extensive washes in fresh M2 in order to rinse out hyaluronidase.

Preparation of the eggs for Ca 2+ imaging

In the following procedures, it is advisable to protect the eggs from light, as Fura-2 is light-sensitive.

During egg incubation on the hot block, an opaque plastic box is placed on top of the dish to reduce light exposure to a minimum.

1. Thaw a Fura-2-AM aliquot and incubate the MII eggs in M2 medium containing 2 µM Fura-2-AM (see Note 7), for 10 minutes at 37°C on a hot block. Next, transfer the eggs in a new dish filled with fresh M2 in order to wash off the residual Fura-2-AM. Leave the eggs on the hot block for an additional 15 minutes, to allow for cytoplasmic esterases to cleave off the AM groups.

2. Remove the zona pellucida, in order to accelerate the fusion of the fertilizing sperm with the egg. Place a drop (500 µl) of acidic Tyrode medium in the center of a culture dish, on the hot block at 37°C for warming. Using a pipette filled with acidic Tyrode, transfer the eggs into the drop of acidic Tyrode, then return the dish on the hot block. The acidic medium will induce a progressive dissolving of the zona pellucida (see Note 8). Once the zona has fully dissolved, return the eggs to M2 medium on the hot block.

3. Prepare the imaging chamber. We use 35-mm glass-bottom dishes (MatTek) with a 20-mm glass diameter. A 500-µl drop of H-KSOM without BSA is deposited on the glass coverslip and covered with mineral oil to prevent evaporation, avoiding flattening of the drop. Place the imaging dish on the pre-warmed stage of the inverted microscope inside the incubation system (see Note 3).

4. Using a mouth pipette filled with H-KSOM, transfer the zona-free eggs to the center of the imaging dish. This is accomplished by careful mouth pipetting, while looking down the microscope eyepieces to adjust the positioning of the pipette close to the surface of the glass coverslip. Slowly release the eggs so that they remain grouped in the field of view.

Setting up fluorescence recordings

Start aquiring F340 and F380 fluorescence in order to adjust the exposure time for each wavelength (in the order of 100-300 ms) to obtain a good fluorescence signal, and to set the wavelength-switching time and the frequency of acquisition (such as one image every 5 sec, see Figure 1). Using the ROI (Region Of Interest) function of the imaging software, draw a large circle in the cytoplasmic area of each egg to collect F340 and F380 fluorescence values to be exported in Excel. Background fluorescence should be subtracted from each excitation wavelength before creating the ratio image.

Fertilization

Add 5-10 µl of the capacitated sperm suspension to the imaging dish containing the eggs loaded with Fura-2 (see Note 9). Add the sperm slowly and away from the egg area, to avoid creating a drift that could lead to the eggs detaching from the coverslip. Look down the eyepieces to check for sperm binding to the eggs surface, before starting the actual experimental recording.

Notes

1. The use of phenol red as an indicator of pH changes in the culture medium is not an absolute requirement. Actually, it can be omitted in the medium used for performing the actual Ca 2+ imaging experiment (H-KSOM), as the dye generates background fluorescence at the wavelengths used to excite Fura-2.

2. It is recommended to adjust the hot block temperature slightly above 37°C, such that a temperature of 37°C is effectively delivered in the culture dish where the eggs are seated, and which is exposed to ambiant air. This calibration is accomplished by using a wire temperature probe that is positioned against the bottom of a test dish filled with M2.

3. To ensure eggs and sperm will be kept warm for the duration of the Ca 2+ recording, we use a multiple temperature control scheme : in addition to the large size incubator covering the entire microscope, an additional mini-incubator (Tokai Hit) is fitted on the stage of the microscope, while the 20x objective is fitted with a lens heater (Tokai Hit). Temperature controls are set to generate 37°C inside the drop of medium in the imaging dish, as verified with a wire temperature probe. 4. Superovulation is not an absolute requirement to obtain mouse eggs, i.e. injection of hCG alone can be envisaged. However, superovulation (PMSG + hCG) will substantially increase the egg yield, allowing performing the experiment using a minimal number of animals (one or two mice). The efficiency of superovulation may vary with the mouse strain, the age of the females, and the dose of hormone administered. Using the common CD-1 strain, young females (4-5 week old) will be efficiently stimulated with 5 units of PMSG and hCG. Older females may require up to 7.5 units of each hormone. In addition to the increased overall body weight, the increased amount of fat in the peritoneal cavity of older females may act as a sink for the injected hormones. Using the CD-1 strain, we routinely obtain 30-40 healthy MII eggs from one mouse. 5. The cumulus mass is easy to spot as it induces a distinct dilation of the oviduct. The size of the cumulus mass is generally proportional to the number of MII eggs that have been ovulated, and which are buried into the mass.

6. Healthy MII eggs should fill most of the space within the zona pellucida, except in the region where the first polar body was emitted. In contrast, eggs that appear shrunk and that make no contact with the ZP must be discarded. Occasionally, some eggs will be found already separated from the rest of the mass, before hyaluronidase had started to disperse the cumulus cells. These eggs generally display a shrunk morphology and must be discarded. 7. The "AM" form of Fura-2 means it is modified by addition of acetoxymethyl groups via an ester bond, which renders the dye membrane-permeant (passive diffusion), thus avoiding invasive loading techniques. Once the indicator has penetrated the egg, cytosolic esterases cleave the ester bond to release anionic Fura-2, which remains trapped inside the cell. However, a fraction of Fura-2-AM may also penetrate and remain sequestered into cytoplasmic organelles (compartmentalization), and generate a contaminating fluorescent signal that is unaffected by changes in [Ca 2+ ]i. To avoid this, Fura-2 salt (such as pentapotassium salt) can be used instead of Fura-2-AM, however it has to be micro-injected into the egg cytoplasm.

8. It is important to manipulate the eggs with a pipette filled with warm acidic Tyrode and not M2 medium, as the latter would contaminate the drop of acidic Tyrode and slow down the zona dissolving process. In addition, occasional gentle pipetting of the eggs using a pipette filled with acidic Tyrode, will accelerate zona removal, by promoting the rupture of the thinned zona pellucida. Note that the eggs are more fragile and prone to damage and lysis when denuded of their protective zona pellucida, and must therefore be manipulated with extra care. 9. Zona-free eggs have lost their barrier against polyspermy, which is provided primarily by the zona pellucida. It is therefore frequent to observe several sperm fusing with the same egg. This can be an issue when the aim of the experiment is to investigate Ca 2+ oscillations parameters, because polyspermy notoriously increases Ca 2+ oscillation frequency (21). For this reason, it is recommended to start by adding little amount of the sperm suspension at first, to increase the probability to obtain monospermic fertilization. This also means that the time required to obtain sperm-egg binding may be longer, only a fraction of the eggs layered on the imaging dish may be fertilized, and fertilization events in the egg pool may happen asynchronously. If no fertilization event happens during a prolonged period, add a second sample of the sperm suspension.

2. 1 .

 1 PMSG and hCG hormones for superovulation 1. PMSG : Lyophilised pellet of Pregnant Mare Serum Gonadotrophin/PMSG (Intervet) is resuspended in filtered (0.20 µm) ice-cold PBS to a final concentration of 25 IU/ml. The solution is then distributed into 1-ml syringes, which are next fitted with 27-gauge needles and immediately frozen at -20°C.

Figure caption Figure 1 .

 caption1 Figure caption

Acknowledgement

My laboratory is supported by the CNRS, the University of Rennes 1, Agence de la biomédecine and Ligue contre le cancer.


Pierre-Jean Meyer
email: pjmeyer@kth.se

Dimos V Dimarogonas

Abstraction refinement and plan revision for control synthesis under high level specifications

Keywords: Reachability analysis, verification and abstraction of hybrid systems, Abstraction refinement, Plan revision, Hybrid systems

This paper presents a novel framework combining abstraction refinement and plan revision for control synthesis problems under temporal logic specifications. The control problem is first solved on a simpler nominal model in order to obtain a satisfying plan to be followed by the real system. A controller synthesis is then attempted for an abstraction of the real system to follow this plan. Upon failure of this synthesis, cost functions are defined to guide towards either refining the initially coarse partition to obtain a finer abstraction, or looking for an alternative plan using the nominal model as above. This tentative synthesis is then repeated until a plan and an abstraction of the real system able to follow this plan are found. The obtained controller also ensures that the real system satisfies the initial specification. A numerical example is provided to illustrate this framework.

INTRODUCTION

In model checking and control synthesis problems under temporal logic specifications, when the desired specification is unsatisfiable by the considered system, classical methods would stop and announce that the problem is not feasible [START_REF] Baier | Principles of model checking[END_REF]. To overcome this limitation, we can try to create an automated framework which iteratively reformulates or relaxes the problem until satisfaction is reached. Two main approaches can be considered.

The first option is to keep the desired specification while considering a new model which should satisfy it and remain as close as possible to the initial model [START_REF] Ding | A logic approach for LTL system modification[END_REF]. A subset of these methods is based on the notion of abstraction refinement. When checking the satisfaction of the specification on the original model is too complicated, we can rely on creating an abstraction of this model which over-approximates its behavior while being simpler to deal with [START_REF] Tabuada | Verification and control of hybrid systems: a symbolic approach[END_REF]. As a result of this over-approximation, a specification satisfied on the abstraction will also be satisfied on the initial model, but its unsatisfaction may be due to the choice of a too coarse abstraction. Abstraction refinement thus aims at iteratively improving the accuracy of the abstraction until it satisfies the specification, see e.g. [START_REF] Clarke | Counterexample-guided abstraction refinement for symbolic model checking[END_REF]; Esmaeil Zadeh Soudjani and Abate (2013); [START_REF] Lee | Tearing based automatic abstraction for ctl model checking[END_REF] for model checking and [START_REF] Henzinger | Counterexample-guided control[END_REF]; [START_REF] Nilsson | Incremental synthesis of switching protocols via abstraction refinement[END_REF]; [START_REF] Moor | Learning by doing: systematic abstraction refinement for hybrid control synthesis[END_REF] for control synthesis problems.

The dual approach consists in keeping the initial model of interest while tuning down the verification or control objective. This can be achieved by a (minimal) specification revision problem, where one looks for a more permissive specification (as close as possible to the initial one) which is satisfied by the model, see e.g. [START_REF] Kim | On the minimal revision problem of specification automata[END_REF] where specifications are described by Büchi automata, or [START_REF] Cizelj | Negotiating the probabilistic satisfaction of temporal logic motion specifications[END_REF] considering Probabilistic Computational Tree Logic. Another relevant work on specification revision is [START_REF] Finger | Revising specifications with CTL properties using bounded model checking[END_REF] where the unsatisfied specification is iteratively expended to allow counterexamples provided by the model checker. Specification relaxation is an alternative method where one designs some metric to measure the level of satisfaction of the initial unsatisfied specification and thus looks for a path of the model with maximal satisfaction [START_REF] Guo | Reconfiguration in motion planning of single-and multi-agent systems under infeasible local LTL specifications[END_REF] or equivalently, minimal violation [START_REF] Tumova | Minimum-violation ltl planning with conflicting specifications[END_REF] of the specification.

The purpose of this paper is to address control synthesis under temporal logic specifications by combining both abstraction refinement and specification revision approaches in a single framework composed of 3 main elements, as described below and sketched in Figure 1. The first step (in purple in Figure 1) considers a nominal system which is simple enough to be abstracted (with respect to an initial coarse partition P of the state space) into a deterministic finite transition system S n . This determinism then enables the use of classical model checkers [START_REF] Baier | Principles of model checking[END_REF] to find a plan ψ of S n satisfying the main specification θ expressed as a Linear Temporal Logic (LTL) formula. The initial control problem of satisfying θ on the real system can then be converted into finding a control strategy such that the real system (which can be seen as a disturbed version of the nominal one introduced above) follows this satisfying plan ψ defined as a sequence in the partition P . When we fail to synthesize a satisfying controller for an abstraction of the real system (with respect to P ), we adapt the problem with one of the following methods. The abstraction refinement (in red in Figure 1) aims at creating a more accurate abstraction by splitting elements of the partition P into smaller elements. The plan revision (in blue in Figure 1) reuses the nominal abstraction S n to synthesize an alternative plan ψ satisfying the formula θ. To the knowledge of the authors, the proposed approach combining abstraction refinement and plan revision has not been explored yet. In addition, the plan revision approach introduced in this paper is significantly different from the mentioned literature on specification revision and relaxation in that we do not assume the main specification to be unfeasible on the real system. On the contrary, we aim at synthesizing a satisfying controller through a secondary control problem which can be iteratively revised. A compositional approach of the abstraction refinement was presented in [START_REF] Meyer | Compositional abstraction refinement for control synthesis under lassoshaped specifications[END_REF].

The structure of this paper follows the decomposition in Figure 1: Section 2 formulates the problem and details the specification conversion, Section 3 presents the abstraction refinement and Section 4 introduces the plan revision. The overall algorithm is given in Section 5. Section 6 provides a numerical illustration of this approach.

PROBLEM FORMULATION

Let N, Z + , R and R + 0 be the sets of positive integers, non-negative integers, reals and non-negative reals, respectively

. For a, b ∈ R n , the interval [a, b] ⊆ R n is defined as [a, b] = {x ∈ R n | a ≤ x ≤ b} using componentwise inequalities.
For a set S, |S| denotes its cardinality.

System description

We consider a nonlinear control system subject to disturbances described by ẋ

= f (x, w) + u, (1)
with state x ∈ X ⊆ R n , bounded additive control input u ∈ U ⊆ R n and bounded disturbance input w ∈ W ⊆ R q . Φ(t, x, u, w) denotes the state (assumed to exist and be unique) reached by (1) at time t ∈ R + 0 from initial state x ∈ X , under the constant control input u ∈ U and the piecewise continuous disturbance input w : R + 0 → W. The reachable set of (1) at time t ∈ R + 0 , from a set of initial states X ⊆ X and for a subset of constant control inputs U ⊆ U is defined as

RS(t, X , U ) = Φ(t, x, u, w) x ∈ X , u ∈ U , w : [0, t] → W . (2)
Throughout this paper, we assume that we are able to compute over-approximations RS(t, X , U ) of the reachable set defined in (2):

RS(t, X , U ) ⊆ RS(t, X , U ).
(3) Several methods exist for over-approximating reachable sets for fairly large classes of linear [START_REF] Kurzhanskiy | Ellipsoidal techniques for reachability analysis of discrete-time linear systems[END_REF][START_REF] Girard | Reachability of uncertain linear systems using zonotopes[END_REF] and nonlinear systems [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF][START_REF] Coogan | Efficient finite abstraction of mixed monotone systems[END_REF].

For a sampling period τ ∈ R + 0 whose value is defined in the next section, a sampled version of system (1) can be described as a non-deterministic infinite transition system

S τ = (X τ , U τ , -→ τ ) where • X τ = X is the set of states, • U τ = U is the set of control inputs, • x u -→ τ x (equivalently written as x ∈ P ost τ (x, u))
if there exists a disturbance w : [0, τ ] → W such that x = Φ(τ, x, u, w), i.e. x can be reached from x exactly in time τ by applying u on [0, τ ].

Specification conversion

In this section, we define the initial problem and detail the specification conversion mentioned in Section 1 and sketched in the purple rectangle of Figure 1. We first assume that the state space X ⊆ R n is an interval of R n and we consider a uniform partition P of X into smaller identical intervals. To ensure that P is a partition, all intervals (including X ) are assumed to be half-closed. In what follows, the elements of P are called cells of the state space. Next, we consider a control specification θ written as a Linear Temporal Logic (LTL) formula over the set of atomic propositions corresponding to the elements of the partition P . The reader is referred to [START_REF] Baier | Principles of model checking[END_REF] for an introduction on the LTL framework. In this paper, we focus on subclasses of LTL formulas which can be satisfied by finite traces ψ = ψ(0)ψ(1) . . . ψ(r) ∈ P r+1 for some r ∈ N, e.g. if θ is a syntactically co-safe formula [START_REF] Kupferman | Model checking of safety properties[END_REF] or if it is defined over finite traces [START_REF] De Giacomo | Linear temporal logic and linear dynamic logic on finite traces[END_REF]. In what follows, we denote as F(θ) the set of all finite plans in P satisfying θ. Problem 1. Find a controller C : X → U such that the closed loop of the system S τ (with x k+1 ∈ P ost τ (x k , C(x k )) for all k ∈ Z + ) satisfies the specification θ.

Although our initial objective is to synthesize a controller such that the system S τ satisfies the specification θ as in Problem 1, we rely on solving this control problem on a simplified model to define a secondary control problem for S τ consisting in following one of the satisfying finite plans ψ ∈ F(θ) in P . We thus temporarily consider the single integrator model in the same state space R n : ẋ = u, (4) typically used for motion of fully-actuated kinematic robotic agents [START_REF] Mesbahi | Graph theoretic methods in multiagent networks[END_REF] and such that (1) can be seen as a disturbed version (by disturbance w and state interactions) of the nominal system (4). Let size(P, i) ∈ R + 0 be the width in the i th dimension of R n of any cell in the uniform partition P and denote as

u i ∈ R the i th component of u ∈ R n . Then the time τ = max i∈{1,...,n} min u∈U ,ui =0 size(P, i) |u i | (5)
corresponds to the minimal time such that steering any continuous state of (4) between any two neighbor cells of P (i.e. whose boundaries have a common facet) exactly in time τ can be done with a constant control u satisfying the constraints u ∈ U. Using τ as a sampling period, we can then abstract the behavior of the nominal system (4) by a deterministic transition system. Since throughout this paper, the input used in a transition of this nominal abstraction is irrelevant to the control synthesis on the disturbed system (1), we rather consider the following nondeterministic finite transition system S n = (X n , -→ n , σ 0 ) defined without input:

• X n = P is the set of states (cells of the partition P ), • σ -→ n σ ⇔ ∃u ∈ U | ∀x ∈ σ, x + τ u ∈ σ , • σ 0 ∈ P is the initial cell.
A transition in S n between two partition cells σ, σ ∈ P thus exists when there exists a constant input u over the time period [0, τ ] steering any continuous state x ∈ σ of (4) to a state in cell σ . The above definitions of τ and S n thus ensure that for any two neighbor cells σ and σ of P , the transition σ -→ n σ exists in S n . Similarly to F(θ), we define F(S n ) as the set of all finite runs that can be generated by S n , i.e. if ψ ∈ P r+1 ∩ F(S n ), then ψ(0) = σ 0 and ψ(k) -→ n ψ(k + 1) for all k ∈ {0, . . . , r -1}.

As described in Figure 1, this nominal abstraction S n will be used for both the initial problem conversion described below and the plan revision method in Section 4. Both these steps can be done using classical tools of model checking [START_REF] Baier | Principles of model checking[END_REF] to find a finite plan ψ ∈ F(θ)∩ F(S n ) satisfying the specification θ on S n . Problem 1 can then be replaced by a new problem where the plan ψ is to be followed by S τ . Problem 2. Find a plan ψ = ψ(0)ψ(1) . . . ψ(r) ∈ F(θ) satisfying the specification θ and a controller C : X → U such that the sampled system S τ follows ψ, i.e. for any

trajectory x 0 C(x 0 ) -→ τ x 1 C(x 1 ) -→ τ . . . C(x r-1 ) -→ τ x r of the controlled system, we have x k ∈ ψ(k) for all k ∈ {0, . . . , r}.
Since ψ is a satisfying plan for the nominal system (4), Problem 2 can also be seen as the robustification of the plan ψ with respect to the disturbances and state interactions in (1). Remark 3. Although Problem 2 is expressed on the discrete-time system S τ , considering the continuous-time systems (1) and ( 4) is necessary to compute the minimal sampling period τ in ( 5) such that a simple abstraction S n satisfying the initial specification θ can be created.

Arbitrarily larger sampling periods are also admissible. Assumption 4. For any k, l ∈ {0, . . . , r} such that k = l, we have ψ(k) = ψ(l).

For clarity of notation, we assume that no finite plan ψ = ψ(0)ψ(1) . . . ψ(r) as considered in Problem 2 visits the same cell twice, as provided by Assumption 4. This is motivated by the fact that in the following Sections 4 and 5, we look for ψ among the shortest satisfying plans in F(θ) ∩ F(S n ). The case when Assumption 4 is relaxed can be covered by designing controllers depending on both the current state of the system and the current position in ψ in order to know which cell is to be targeted next.

ABSTRACTION REFINEMENT

This section details the principle of the abstraction refinement component of Figure 1 (in the red rectangle). Firstly, we discuss the necessity to introduce abstraction to solve Problems 1 and 2. Then, two functions to be used in the main algorithm in Section 5 are presented: ValidSet in Algorithm 1 aims at computing a subset of a cell ψ(k) ∈ P which can be driven towards the next cell ψ(k + 1) of a plan ψ; Refine in Algorithm 2 details the procedure when a cell ψ(j) ∈ P of the plan ψ is to be refined.

Abstraction

Since in most cases Problems 1 and 2 cannot be solved directly on the infinite transition system S τ , we rely on creating an abstraction S a of S τ which can be described as a finite transition system S a = (X a , U a , -→ a ) where:

• X a is a partition of the continuous state space X into a finite set of intervals called symbols. In the abstraction refinement procedure, X a is initially taken equal to P and is then iteratively refined in Algorithm 2,

• U a ⊆ U is a finite subset of the control set U, • a transition s u -→ a s exists if s ∩ RS(τ, s, {u}) = ∅.
A transition s u -→ a s is equivalently written as s ∈ P ost a (s, u). The set P ost a (s, u) thus contains all symbols in X a which intersect the over-approximation of the reachable set of (1) at time τ from any initial state in the symbol s ∈ X a and with the constant control u ∈ U a . The use of these over-approximations (3) guarantees the existence of a behavioral relationship between S τ and S a (defined formally and proven in Section 5), which ensures that a controller solving Problem 1 for S a can be converted into a controller solving Problem 1 for S τ .

Instead of creating the whole abstraction S a as defined above followed by a controller synthesis (which may fail if the chosen partition is too coarse), the abstraction refinement proposed in this section is guided by the specification and iteratively synthesizes a controller alongside the creation of the abstraction. If no satisfying controller is found, an element of the initial coarse partition P is refined by splitting it into smaller elements and the synthesis is tried again. This approach thus aims at creating the abstraction S a from a refined partition X a which is as coarse as possible, but still fine enough to satisfy the specification.

Valid sets

We first introduce the function P a : P → 2 Xa such that P a (σ) = {s ∈ X a | s ⊆ σ} corresponds to the projection of a cell σ ∈ P onto a given finer partition X a . Next, we define the notion of valid sets. Definition 5. Given a finite plan ψ = ψ(0) . . . ψ(r) as in Problem 2, we define the function V : P → 2 Xa such that V (ψ(r)) = {ψ(r)} and for all k ∈ {0, . . . , r -1}:

V (ψ(k)) = {s ∈ P a (ψ(k)) | ∃u ∈ U a such that P ost a (s, u) ⊆ V (ψ(k + 1)) } . The set V (ψ(k)) is called the valid set of cell ψ(k). A cell σ ∈ P and a symbol s ∈ X a such that s ∈ P a (σ) are said to be valid if V (σ) = ∅ and s ∈ V (σ), respectively. Conversely, a symbol s ∈ P a (σ) is invalid if s / ∈ V (σ).
Since ψ(r) is the final cell of the plan ψ to be reached in Problem 2, it is considered as valid and the function

V : P → 2 Xa is initialized with V (ψ(r)) = {ψ(r)}.
We then proceed backwards on the plan ψ to iteratively define the other valid sets V (ψ(k)) as the subset of symbols in ψ(k) which can be driven towards the valid set V (ψ(k+1)) of the next cell for at least one control input in U a .

The function ValidSet(ψ(k), V (ψ(k + 1))) in Algorithm 1 first computes the valid set V (ψ(k)) with respect to a plan ψ as in Definition 5. Then, the controller C a : X a → U a associates to each valid symbol s ∈ V (ψ(k)) the first control value ensuring that s is valid, therefore reducing the computational complexity by stopping the search of such inputs as soon as one is found. An alternative version of Algorithm 1 can be proposed by defining a non-deterministic controller C a : X a → 2 Ua containing all satisfying inputs, thus allowing for a future optimization on the choice of the control.

Data: P , X a , U a , P a : P → 2 Xa . Input: Considered cell ψ(k) ∈ P .

Input: Targeted valid set V (ψ(k + 1)) ⊆ P a (ψ(k + 1)). V (ψ(k)) = {s ∈ P a (ψ(k)) | ∃u ∈ U a such that P ost a (s, u) ⊆ V (ψ(k + 1)) } forall s ∈ V (ψ(k)) do C a (s) taken in {u ∈ U a | P ost a (s, u) ⊆ V (ψ(k + 1)) } return {V (ψ(k)), C a : X a → U a } Algorithm 1: ValidSet(ψ(k), V (ψ(k + 1))).
Computes the valid set V (ψ(k)) and associated controller C a at step k ∈ {0, . . . , r -1} of the plan ψ = ψ(0)ψ(1) . . . ψ(r).

Refinement

As stated in Section 3.1, the abstraction S a is initialized with respect to the initial coarse partition X a = P . We then iteratively compute the valid sets V (ψ(k)) from k = r back to k = 0 as in Definition 5. If an empty valid set V (ψ(k)) = ∅ is found for some step k (i.e. the associated controller synthesis in Algorithm 1 fails), the overall algorithm in Section 5 may choose to overcome this problem through abstraction refinement by calling the function Refine(ψ, j) in Algorithm 2 in order to refine one of the previously visited cells ψ(j) with j ∈ {k, . . . , r -1}. The rule guiding the choice of j is detailed in Section 5. This refinement is achieved in the following two steps. Firstly, the cell ψ(j) is refined by splitting each of its invalid symbols s into a set of subsymbols (∀s ∈ Split(s), s ⊆ s) and updating the partition X a accordingly. The definition of Split can be arbitrary, although one should aim at obtaining subsymbols which remain compatible with the over-approximation method chosen in (3). Classical examples include: splitting the symbol s along its longest dimension only; and uniformly splitting s ⊆ R n into 2 n subsymbols (2 per dimension). The second step consists in calling Algorithm 1 for all the cells of ψ whose valid sets may be expanded as a result of this refinement, i.e. from the refined cell ψ(j) back to the cell ψ(k) (with k ≤ j) whose valid set was empty.

Data: P , X a , P a : P → 2 Xa , V : P → 2 Xa , V (ψ(k)) = ∅. Input: Plan ψ = ψ(0) . . . ψ(r). Input: Step j ∈ {k, . . . , r -1} of the refinement. forall s ∈ P a (ψ(j))\V (ψ(j)) do X a = (X a \{s}) ∪ Split(s) for l from j to k do {V (ψ(l)), C a } = ValidSet (ψ(l), V (ψ(l + 1))) return {X a , V : P → 2 Xa , C a : X a → U a } Algorithm 2: Refine(ψ, j). Refinement of the cell ψ(l)
and update of the affected valid sets.

Remark 6. From Definition 5, refining a cell ψ(j) has no effect on the valid sets V (ψ(l)) for l > j and can only expand the valid sets V (ψ(l)) for l ≤ j. We are thus guaranteed that the previously obtained valid sets and controllers are not lost after a call of Algorithm 2.

Note that Algorithm 2 only describes a single iteration of refinement, to be called in the overall algorithm of Section 5. A complete abstraction refinement algorithm appears as a particular case of Algorithm 5 in Section 5.

PLAN REVISION

This section details the principle of the second adaptation method featured in Figure 1 consisting in revising the initial plan ψ considered in Problem 2. This plan revision is achieved through an iterative deepening depth-first search (function Revise in Algorithm 3) on the product automaton capturing both the LTL formula θ from Problem 1 and the nominal abstraction S n from Section 2.2.

Büchi and product automata

We first define a Büchi automaton, where the considered set of atomic propositions is the partition P . Definition 7. A Büchi automaton A = (Q, P, δ, q 0 , F ) is described by: a finite set of states Q, an input alphabet P , a transition relation δ : Q × P → 2 Q , an initial state q 0 ∈ Q and a set of accepting states F ⊆ Q. For an infinite word σ 0 σ 1 σ 2 . . . over P , the associated run q 0 q 1 q 2 . . . of A (such that q i+1 ∈ δ(q i , σ i ) for all i ∈ Z + ) is said to be accepting if it visits the accepting set F infinitely often.

Büchi automata are used as an alternative structure capturing the set of words that satisfy an LTL formula [START_REF] Baier | Principles of model checking[END_REF]. Let A θ denote the Büchi automaton associated to the LTL formula θ in Problem 1. We can then consider the product of the transition system S n and A θ . Definition 8. The product of S n = (P, -→ n , σ 0 ) and A θ = (Q, P, δ, q 0 , F ) is described by the automaton Π = (Q Π , ∅, δ Π , q 0 Π , F Π ) where: Q Π = P × Q; there is no input set (as in S n ); δ Π : Q Π → 2 QΠ and (σ , q ) ∈ δ Π ((σ, q)) if σ -→ n σ and q ∈ δ(q, σ); q 0 Π = (σ 0 , q 0 ); and F Π = P × F .

Given a run ω = (σ 0 , q 0 )(σ 1 , q 1 ) . . . of Π, we denote as ω| Sn = σ 0 σ 1 . . . the projection of ω onto a run of S n .

From Definition 8, an accepting run ω of Π can thus be projected onto a run ω| Sn of S n satisfying the formula θ.

Due to our focus on LTL formulas defined over finite traces or syntactically co-safe formulas as in Section 2.2, this run is either finite or can be reduced to a finite prefix such that any infinite run starting with this prefix also satisfies θ [START_REF] Kupferman | Model checking of safety properties[END_REF], i.e. ω| Sn ∈ F(θ) ∩ F(S n ) with the notations introduced in Section 2.2.

Iterative Deepening Search

We are interested in a search of Π allowing to be repeatedly called, each time returning a satisfying plan ψ ∈ F(θ) ∩ F(S n ) which was not previously returned. The first call of this search corresponds to the initial specification conversion as in the purple rectangle of Figure 1 and follow-up calls are iterations of the plan revision (blue rectangle).

More precisely, a call of Revise(ψ, j) as in Algorithm 3 aims at finding an admissible revision of ψ up to ψ(j), i.e. a new satisfying plan ψ ending with the sequence ψ(j + 1) . . . ψ(r). Such a revision thus needs to satisfy the following three conditions. Since the search is done on the product automaton Π from its initial state q 0 Π , the first condition ψ ∈ F(θ) ∩ F(S n ) can be reduced to checking whether the explored path in Π ends with an accepting state. The second condition is ψ ∈ AdmRev(ψ, j) where AdmRev(ψ, j) = {σ 0 . . . σ p ψ(j + 1) . . . ψ(r) | σ p = ψ(j)} ensures that the end sequence ψ(j + 1) . . . ψ(r) is kept in ψ while forcing the revision to start in ψ(j). Denoting as U sedP lans ⊆ F(θ) ∩ F(S n ) the set of plans previously considered and discarded in the main algorithm of Section 5, the third condition preventing reusing these discarded plans is combined with the above second condition by considering ψ ∈ N ewRev(ψ, j) where N ewRev(ψ, j) = AdmRev(ψ, j)\U sedP lans.

(6)

Algorithm 3 implements the search algorithm on the product automaton Π as an Iterative Deepening Depth-First Search [START_REF] Korf | Depth-first iterative-deepening: An optimal admissible tree search[END_REF], consisting in calling a Limited-Depth Depth-First Search (function LDDFS defined recursively in Algorithm 4) with iteratively increasing depth limit until a satisfying plan is found. Intuitively, the function Revise initially searches for runs of Π of length 1 (search depth limited to 0) generating admissible revisions as above. If no such revision is found, this limited-depth search is repeated with an allowed search depth increased by 1.

The Limited-Depth Depth-First Search is initialized in Algorithm 3 to start from the initial state q 0 Π of Π with Data: Initial state q 0 Π of Π. Input: Current plan ψ = ψ(0) . . . ψ(r) ∈ F(θ) ∩ F(S n ). Input: Revision step j ∈ {0, . . . , r}. for depth from 0 to ∞ do ψ = LDDFS(q 0 Π , depth) if ψ = ∅ then return {ψ , depthr + j}; Algorithm 3: Revise(ψ, j). Generates a possible revision ψ of ψ keeping its end sequence from j + 1 up to r, and provides the index of the cell in ψ replacing ψ(j).

a depth limit denoted as depth ∈ Z + . This search then proceeds in Algorithm 4, where a successor q 1 Π of q 0 Π is chosen and the function LDDFS is called again with the new explored path q 0 Π q 1 Π and an allowed depth reduced to depth -1. This recursive call is repeated until the allowed depth reaches 0, where we check whether the explored path in Π (thus containing depth + 1 elements) corresponds to an admissible revision, i.e. if its last state is accepting in Π and if its projection onto a plan of S n (using the notation •| Sn introduced in Section 4.1) belongs to N ewRev(ψ, j) as defined in ( 6). This plan is returned to Algorithm 3 if it is an admissible revision. Otherwise, the search backtracks and explores other paths of Π. Since this search has a limited depth and is applied to the finite graph Π, it will explore all paths of length depth + 1 in Π in finite time if no admissible revision is found. In such cases, an empty set is returned to Algorithm 3 which will repeat the limiteddepth search with an increased depth limit.

Data: Π, S n , ψ, j, N ewRev(ψ, j) as in ( 6). Input: Explored path q 0 Π . . . q l Π in Q Π . Input: Remaining allowed search depth: depth ∈ Z + . if depth > 0 then forall q l+1 Π ∈ δ Π (q l Π ) do candidate = LDDFS(q 0 Π . . . q l Π q l+1 Π , depth -1) if candidate = ∅ then return candidate; else if q l Π ∈ F Π and (q 0 Π . . . q l Π )| Sn ∈ N ewRev(ψ, j) then return (q 0 Π . . . q l Π )| Sn return ∅ Algorithm 4: LDDFS(q 0 Π . . . q l Π , depth). Recursive implementation of a limited-depth search.

Once Algorithm 3 receives a non-empty plan ψ from Algorithm 4, it then returns this plan as well as the index corresponding to the cell of ψ that replaces ψ(j). For the specification conversion as in Figure 1, the initial plan considered in Problem 2 is obtained from a first call of Algorithm 3 denoted as Revise(∅, 0) (since no previous plan is to be revised) and where the condition ψ ∈ N ewRev(∅, 0) in Algorithm 4 is always true.

OVERALL APPROACH

Algorithm

In this section we present an implementation of the whole structure in Figure 1 that relies on the functions ValidSet, Refine and Revise detailed in Algorithms 1 to 3. In Algorithm 5, the refined partition X a of the abstraction S a is initialized with the partition P , an initial plan ψ = ψ(0) . . . ψ(r) is obtained from Algorithm 3 for the specification conversion block of Figure 1, and the last cell ψ(r) of the plan ψ is valid as in Definition 5. The main loop then aims at computing the valid sets and associated controllers as in Algorithm 1 for all cells ψ(k) from k = r -1 back to k = 0.

If a non-empty valid set V (ψ(k)) is obtained, the while loop proceeds with step k -1. Otherwise (V (ψ(k)) = ∅ for some k), Algorithm 5 needs to pick a method between the abstraction refinement and the plan revision, as well as one of the previously explored cells ψ(j) (with j ∈ {k, . . . , r}) where this method should be applied. This choice is made by introducing two cost functions J AR , J P R : P → R + associating the cost of applying either method to each cell of the plan ψ respectively. These functions can be chosen arbitrarily in order to prioritize one method over the other. In Section 6, we provide an example where J AR and J P R estimate the complexity of the future computations after applying each of the respective methods.

We first compute the indices j AR and j P R corresponding to the cells of ψ minimizing the costs J AR (ψ(j AR )) and J P R (ψ(j P R )), respectively. If the abstraction refinement offers the smallest cost (J AR (ψ(j AR )) < J P R (ψ(j P R ))), Algorithm 2 is called on cell ψ(j AR ) and the next step of the while loop proceeds without updating k, to check if V (ψ(k)) is still empty. Otherwise, the plan revision is applied on cell ψ(j P R ), where we first reset the valid sets for all cells that will be discarded by the revision, add ψ to the set U sedP lans from Section 4.2 and then call Algorithm 3 to obtain the new plan (overwriting ψ) and the associated index k such that V (ψ(k)) is to be computed next. The main loop is repeated until V (ψ(0)) = ∅ is found for some plan ψ. Algorithm 5 then outputs the final plan ψ, the refined partition X a , the valid symbols (in X a ) associated to each cell of ψ and the controller C a .

Data: P , J AR : P → R + , J P R : P → R + . Initialization: X a = P , ψ(0) . . . ψ(r) = Revise(∅, 0)

Initialization: V (ψ(r)) = {ψ(r)}, k = r -1 while k ≥ 0 do {V (ψ(k)), C a } = ValidSet (ψ(k), V (ψ(k + 1))) if V (ψ(k)) = ∅ then k = k -1; else j AR = arg min j∈{k,...,r-1}
J AR (ψ(j))

j P R = arg min j∈{k,...,r}

J P R (ψ(j)) if J AR (ψ(j AR )) < J P R (ψ(j P R )) then {X a , V, C a } = Refine(ψ, j AR ) else forall l ∈ {k, . . . , j P R } do V (ψ(l)) = ∅;
U sedP lans = U sedP lans ∪ {ψ} {ψ, k} = Revise(ψ, j P R )

Output: {ψ, X a , V : P → 2 Xa , C a : X a → U a } Algorithm 5: Global algorithm.

Remark 9. The particular case where Algorithm 5 only applies abstraction refinement (similarly to [START_REF] Meyer | Compositional abstraction refinement for control synthesis under lassoshaped specifications[END_REF]) can be obtained by choosing J P R : P → {+∞}. A case with only plan revision can similarly be obtained, although it is unlikely to succeed in having S a (the abstraction of the disturbed system S τ ) follow the same plan as obtained on the nominal abstraction S n without relying on abstraction refinement.

Solution to Problem 1

To control the sampled system S τ with the controller C a obtained in Algorithm 5, the systems S τ = (X τ , U τ , -→ τ ) and S a = (X a , U a , -→ a ), defined in Sections 2.1 and 3 respectively, must satisfy a feedback refinement relation as defined below, adapted from [START_REF] Reissig | Feedback refinement relations for the synthesis of symbolic controllers[END_REF]. Definition 10. A map H : X τ → X a is a feedback refinement relation from S τ to S a if: ∀x ∈ X τ , s = H(x), ∀u ∈ U a ⊆ U τ , ∀x ∈ P ost τ (x, u), H(x ) ∈ P ost a (s, u).

Such a relation implies that for any pair (x, s) of matching state and symbol and any control u of the abstraction S a , the behaviors of the original system S τ with the same control u can be matched by behaviors of S a . As a consequence, if a controller is synthesized so that S a satisfies some specification, then this controller ensures that S τ satisfies the same specification. By proving that such a relation can be found, we obtain the following result. Theorem 11. Let H : X τ → X a such that H(x) = s ⇔ x ∈ s. Then the controller C : X τ → U τ defined by C(x) = C a (H(x)) for all x ∈ X τ solves Problem 1.

Proof. We first prove that the map H is a feedback refinement relation from S τ to S a . Let x ∈ X τ , s = H(x) ∈ X a , u ∈ U a ⊆ U τ , x ∈ P ost τ (x, u) and s = H(x ). By definition of the reachable set of system (1) in ( 2) and its over-approximation in (3), we have x ∈ RS(τ, s, {u}) ⊆ RS(τ, s, {u}). Since we also have x ∈ s , then, s ∩ RS(τ, s, {u}) = ∅ which implies that s ∈ P ost a (s, u) as in the definition of S a in Section 3. It is therefore sufficient to prove that the controller C a : X a → U a solves Problem 1 for the abstraction S a .

Consider the outputs ψ = ψ(0) . . . ψ(r), X a , V and C a from Algorithm 5. Let s 0 ∈ V (ψ(0)) be an initial symbol of S a and consider any finite trajectory (s 0 , . . . , s r ) of S a controlled by C a (i.e. with s k+1 ∈ P ost a (s k , C a (s k ))). Then, by definition of C a and V (ψ(k)) in Algorithm 1, we have P ost a (s k , C a (s k )) ⊆ V (ψ(k + 1)) and thus s k+1 ⊆ ψ(k+1) for all k ∈ {0, . . . , r-1}. Therefore, ψ and C a from Algorithm 5 solve Problem 2 for the abstraction S a defined on the refined partition X a . Since the plan ψ ∈ F(θ) obtained in Algorithm 3 is a satisfying trace of the LTL formula θ, C a thus also solves Problem 1 for S a . From the above feedback refinement, this implies that C = C a (H(•)) solve Problem 1 for the sampled system S τ with an initial state

x 0 ∈ {x ∈ X τ | H(x) ∈ V (ψ(0))}. 2
Therefore, if Algorithm 5 terminates in finite time, the controller C in Theorem 11 ensures that the sampled system S τ follows a finite plan ψ satisfying the main specification θ if it starts in the valid set V (ψ(0)). On the other hand, guarantees for the converse implication (if θ can be satisfied on S τ , then Algorithm 5 will find in finite time a controller C solving Problem 1) cannot be provided in general due to the use of over-approximations in the definition of the abstraction S a .

NUMERICAL ILLUSTRATION

The use of intervals as the elements of the state partition (required by the extraction of a plan ψ satisfying the main specification θ in Section 2.2) particularly suits the computation of over-approximations of the reachable set using the monotonicity property. The reader is referred to [START_REF] Angeli | Monotone control systems[END_REF] for a description of monotone control systems and to e.g. [START_REF] Meyer | Invariance and symbolic control of cooperative systems for temperature regulation in intelligent buildings[END_REF] for their use to overapproximate the reachable set and create abstractions. For visualization purposes, we consider a 2D system described by the nonlinear monotone dynamics:

ẋ = -1 0.3 0.3 -1 x -0.01x 3 + u, (7)
with state x ∈ R 2 , bounded control input u ∈ [-5, 5] 2 and componentwise cubic power x 3 .

The considered state space X = [-9, 9] 2 is partitioned into 3 elements per dimension, thus resulting in a partition P of 9 cells. The control interval U = [-5, 5] 2 is discretized uniformly into 5 values per dimension: U a = {-5, -2.5, 0, 2.5, 5} 2 . Following the guidelines in (5), we take the sampling period τ = 6/5 = 1.2. Below, the cells of the partition P are denoted as σ x,y with x, y ∈ {1, 2, 3} such that for example, σ 1,3 represents the top-left cell in Figure 2. The nominal abstraction S n is created such that each cell of P has a transition towards its immediate neighbors (but not in diagonal), and the initial cell is σ 1,1 .

The main control specification is taken as the syntactically co-safe LTL formula θ = 3σ 1,3 , meaning that we want to eventually reach the top-left cell of P . The corresponding Büchi automaton A θ and the product Π of S n and A θ are computed with the software P-MAS-TG described in [START_REF] Guo | Multi-agent plan reconfiguration under local LTL specifications[END_REF]. The remaining implementation of Algorithm 5 is done on Matlab.

The cost functions J AR , J P R : P → R + are defined as an estimate of the complexity of the future computations after applying either abstraction refinement or plan revision on a cell of P . This complexity is measured in the number of symbols s ∈ X a (elements of the refined partition) whose set of successors P ost a (s, u) needs to be computed for some u ∈ U a . Assuming that we are in Algorithm 5 with V (ψ(k)) = ∅ for some plan ψ, then a call Refine(ψ, j) for j ∈ {k, . . . , r -1} is associated with the cost

J AR (ψ(j)) = 2 n * |P a (ψ(j))\V (ψ(j))| (8) + j-1 l=k |P a (ψ(l))\V (ψ(l))| + (k + 1) * (2 n ) 2 ,
where the first term is the number of subsymbols obtained after splitting the invalid symbols of ψ(j) (assuming that the function Split(s) returns 2 n = 4 subsymbols of s), the second term is all the invalid symbols of ψ(j -1) back to ψ(k) to be updated as in Algorithm 2 and the last term is a forecast that all invalid cells ψ(0) to ψ(k) that remains to be explored will be refined twice (assuming no plan revision is called in the future). The cost associated to calling Revise(ψ, j) is defined similarly to the third term of (8):

J P R (ψ(j)) = (|Revise(ψ, j)| -|ψ|+j + 1) * (2 n ) 2 /0.6, (9)

where the number of cells that remains to be explored now depends on the size difference between the current plan ψ and the candidate revision obtained in Revise(ψ, j).

The weight 1/0.6 is added in (9) to prioritize the use of abstraction refinement over plan revision.

Figure 2 provides 3 snapshots of the refined partition X a and the valid symbols (filled in red) during the execution of Algorithm 5. The initialization with Revise(∅, 0) provides a first plan ψ = σ 1,1 σ 1,2 σ 1,3 and the whole cell σ 1,3 (topleft in Figure 2a) is a valid symbol since it has no successor in ψ. Algorithm 5 then proceeds to compute the valid set of ψ(1) = σ 1,2 which is found to be empty until 3 successive calls of Refine(ψ, 1), where V (σ 1,2 ) contains 6 elements. Then, ψ(0) = σ 1,1 is considered and its valid set remains empty despite 3 calls of Refine(ψ, 0). At this point, displayed in Figure 2a, Algorithm 5 considers it less costly to revise the plan ψ rather than refining a fourth time σ 1,1 or σ 1,2 . The function Revise(ψ, 0) is thus called to change the beginning sequence of ψ while keeping the end σ 1,2 σ 1,3 (displayed in Figure 2b). This results in a revision ψ = σ 1,1 σ 2,1 σ 2,2 σ 1,2 σ 1,3 . Algorithm 5 then proceeds on ψ (2) = σ 2,2 whose valid set contains one symbol after two calls of Refine(ψ , 2), then on ψ (1) = σ 2,1 where |V (ψ (1))| = 5 after two calls of Refine(ψ , 1) and finally on ψ (0) = σ 1,1 where |V (ψ (0))| = 1 after one call of Refine(ψ , 0). Since V (ψ (0)) = ∅, the algorithm stops (after 25.8 seconds on a laptop with a 2.6 GHz CPU and 8 GB of RAM) and the final partition and valid symbols are displayed in Figure 2c.

CONCLUSION

In this paper, we presented a novel framework combining abstraction refinement and plan revision for control synthesis problems under temporal logic specifications. The control problem is first solved on a simpler nominal model in order to obtain a satisfying plan to be followed by the real system. We then try to synthesize a controller for an abstraction of the real system to follow this plan. When this synthesis fails, some cost functions guide us towards either refining the initially coarse partition to obtain a finer abstraction, or looking for an alternative plan using the nominal model as above. This tentative synthesis is then repeated until we find a plan and an abstraction of the real system able to follow this plan. The controller obtained on this abstraction can then be used to define a controller for the real system to satisfy the initial specification.

While this paper mainly focuses on providing the general framework combining abstraction refinement with plan revision, current efforts aim at optimizing the obtained results based on the definition of the cost functions.

Fig. 1 .

 1 Fig. 1. General structure of the approach

This work was supported by the H2020 ERC Starting Grant BUCOPHSYS, the EU H2020 AEROWORKS project, the EU H2020 Co4Robots project, the Swedish Foundation for Strategic Research and the KAW Foundation.


Alexandre Meyer
email: a.meyer@cs.ucl.ac.uk

Real-Time Reflection on Moving Vehicles in Urban Environments

Keywords: I.3.7 [Computer Graphics]: Three-Dimensional Graphics and Realism.Color, shading, shadowing, and texture Environment Maps, Image-Based Rendering, Ray Tracing, Real-Time Rendering

In the context of virtual reality, the simulation of complex environments with many animated objects is becoming more and more common. Virtual reality applications have always promoted the development of new efficient algorithms and image-based rendering techniques for real-time interaction. In this paper, we propose a technique which allows the realtime simulation in a city of the reflections of static geometry (eg. building) on specular dynamic objects (vehicles). For this, we introduce the idea of multiple environment maps. We pre-compute a set of reference environment maps at strategic positions in the scene, that are used at run time and for each visible dynamic object, to compute local environment maps by resampling images. To efficiently manage a small number of reference environment maps, compared to the scene dimension, for each vertex of the reconstructed environment we perform a ray tracing in a heightfield representation of the scene. We control the frame rate by adaptative reconstruction of environment maps. We have implemented this approach, and the results show that it is efficient and scalable to many dynamic objects while maintaining interactive frame rates.

INTRODUCTION

In the context of mixed-reality, content often comes from different sources mixing real data sources with virtual ones. When merging the information, one needs to make sure that the added virtual information stays consistent with the rest of the scene. Often, the information coming from real sources looks highly realistic as the 3D model can be mapped with the textures extracted directly from pictures. In the European project CREATE1 , we test a constructivist approach (learning through activity) in the context of cultural heritage and urban planning. A typical scenario for the urban planning application is to simulate a new configuration of a city on immersive displays. The real environment is captured and built from photographs [START_REF] Realviz | Imagemodeler[END_REF] with additional post-processing to finalize the lighting consistency. Additional features are then added to com-plement the simulation: crowd simulation, car simulation, tramway insertion, new placement of pedestrian areas, pedestrian crossings, trees, etc. The system will be used by urban professionals to understand and visualize changes and also by the general public to whom it is important to sell the feasibility and the benefits of modifying some areas. It is therefore important for the simulation to be believable, and as photorealistic as possible. In figure 1, the reconstructed model from a real scene is shown, together with the insertion of virtual trees and a tramway. Shadows of virtual elements onto the reconstructed model are simulated. However, no reflections were computed on the tramway making it easy to recognize it as computer graphics rendering.

Lighting effects ranging from shadows, direct illumination, to global illumination as well as transparency and reflection/refraction, have been shown to be extremely important for realism in certain applications [START_REF] Rademacher | Measuring the Perception of Visual Realism in Images[END_REF], giving to the user valuable cues on the environment, about where objects are physically placed, and their material properties, making it easier to identify them. However, the computation of these effects is often restricted to very limited local areas and too few dynamic (moving) objects. In our mixed-reality application, the available computation time is even smaller as it needs to be shared by the display of the static model, the various dynamic objects, their simulation, the sound simulation and the haptic interaction. To be general, our main goal is thus to increase the photo-realism in real-time computer graphics applications with no restriction on the geometry and the number of dynamic objects.

In this paper, we concentrate on simulating reflections of the environment onto animated, specular virtual objects moving in a structured complex virtual environment: vehicles driving in a city. Often, environment maps (EMs) [START_REF] Blinn | Texture and reflection in computer generated images[END_REF][START_REF] Greene | Environment mapping and other applications of world projections[END_REF][START_REF] Voorhies | Reflection vector shading hardware[END_REF] are used for real-time applications instead of computationally intense algorithms such as ray tracing. The concept of EM techniques is to store images of the environment onto a simple geometric object (a sphere or a cube) and to use this information as a texture for computing the reflections onto an object, instead of using the geometry of the scene. Since environment maps are valid for one particular point or its surrounding, the case of moving objects far from this point forces an expensive re-computation of the EM for each object's new position. In the case of environment cube maps it corresponds to rendering the scene six times per object, once for each face of the cube. Currently, to maintain a constant frame rate, only a few moving objects are allowed (usually one).

We propose a new technique, called multiple environment maps or MEM, making use of the advantages of imagebased approaches, to interactively compute individual environment maps around each moving object, thus obtaining realistic reflections with a quality comparable to ray-traced rendering. Our approach is simple and needs a classical graphic hardware since the most advanced feature we use is the well-supported cube map and multi-texturing extension.

In section 2, we briefly introduce previous work relevant to our method. We then summarize our contributions by giving an overview of the MEM in section 3. In section 4, we describe the techniques used for each of the steps of the method. Section 5 describes our levels of detail and we, then present some implementation and discussion in section 6 and results in section 7, and then conclude.

PREVIOUS WORK 2.1 Environment Maps

Accurate reflections between arbitrary objects can be produced by ray tracing [START_REF] Whitted | An improved illumination model for shaded display[END_REF], even at interactive frame rates with a cluster of PCs [23]. Nevertheless, with a single computer with a common graphic board the cost is significantly higher than texture-mapped polygon rendering, and thus it is fair to say that ray tracing is still difficult to use for realtime applications.

Environment maps are heavily used nowadays in computer graphics. They were introduced to approximate reflections for interactive rendering [START_REF] Blinn | Texture and reflection in computer generated images[END_REF][START_REF] Greene | Environment mapping and other applications of world projections[END_REF][START_REF] Voorhies | Reflection vector shading hardware[END_REF]. But they can be used as a means to render glossy reflections [START_REF] Miller | Illumination and reflection maps: Simulated objects in simulated and real environments[END_REF][START_REF] Cabral | Reflection space image based rendering[END_REF][START_REF] Heidrich | Realistic, hardware-accelerated shading and lighting[END_REF][START_REF] Kautz | Approximation of glossy reflection with prefiltered environment maps[END_REF] by pre-filtering a map with a fixed reflection model or a BRDF (bidirectional reflectance distribution function). Recent graphics card extensions support the use of environment maps in realtime. Graphics cards now support commonly cube maps [START_REF] Nvidia | Cube environment mapping[END_REF], and last year, ATI [START_REF]ATI. Car paint[END_REF] presented at SIGGRAPH a realtime demonstration of high-resolution normal maps to illustrate the importance of normal precision in this technique.

Attempts have been made to use environment maps for less constrained navigation than the one described previously. Quicktime VR [START_REF] Eric | Quicktime VR -an image-based approach to virtual environment navigation[END_REF] is a pure image-based technique, which uses a series of captured environment maps to allow the user to look around a scene from fixed points in space. Cabral et al. [START_REF] Cabral | Reflection space image based rendering[END_REF] store a collection of view-dependent EMs. Hakura et al. [START_REF] Hakura | Parameterized environment maps[END_REF][START_REF] Ziyad | Realistic reflections and refractions on graphics hardware with hybrid rendering and layered environment maps[END_REF] tackle the problem of transition between EMs. Our framework is similar to these methods,however we differ in two different aspects. First, in the way we capture the EM. Their parameterized EM is a sequence of EMs recorded over a dense set of viewpoints whereas our technique needs a less dense set of pre-computed EMs. Second, to recompute an intermediate EM, they represent reflected geometry by simple geometry, such as a box, a parallelepiped, a sphere, an ellipsoids. In contrast, we represent the environment by an accurate representation of the geometry.

Computing New Views

The problem of computing an intermediate view starting from pre-computed is well known in image-based rendering. Only few papers [START_REF] Hakura | Parameterized environment maps[END_REF][START_REF] Ziyad | Realistic reflections and refractions on graphics hardware with hybrid rendering and layered environment maps[END_REF] apply this to EM. The spectrum of image-based methods to solve this problem ranges from those that exclusively use images to those that re-project acquired imagery onto geometric models.

Quicktime VR [START_REF] Eric | Quicktime VR -an image-based approach to virtual environment navigation[END_REF] offers a realistic view of the scene, but the user has a correct perspective from a set of specific locations. Image morphing approaches [START_REF] Chen | View interpolation for image synthesis[END_REF][START_REF] Seitz | View morphing: Synthesizing 3D metamorphoses using image transforms[END_REF] allow some range of motion. However, the transformation of the reference views to the desired views is approximated by interpolation. To maintain a high frame rate, the Talisman architecture [START_REF] Torborg | Talisman: Commodity Real-time 3D graphics for the PC[END_REF] reused portions of rendered images and re-project them onto a new view using 2D warping. The Lumigraph [START_REF] Gortler | The lumigraph[END_REF] and Light Field [START_REF] Levoy | Light field rendering[END_REF] densely sample light rays to create a ray database. Unfortunately, these techniques are not designed to manage objects with very different scales as we have in our case.

At the other end of the spectrum are methods based largely on geometry. Texture mapping is the most common way to incorporate images into the scene description. Debevec et al. [START_REF] Debevec | Modeling and rendering architecture from photographs: A hybrid geometry-and image-based approach[END_REF] represent the scene with an approximate geometric model (semi-automatically created) texture-mapped, in a view dependent fashion, from photographs.

McMillan and Bishop's [START_REF] Mcmillan | Plenoptic modeling: An image-based rendering system[END_REF] and Shade et al. [START_REF] Shade | Layered depth images[END_REF] methods are in the middle of the spectrum, representing the scene as a collection of images that in addition to color also store depth at each pixel. The desired view is generated by a 3D-warp of the depth images. Buehler et al. in [START_REF] Buehler | Unstructured lumigraph rendering[END_REF] generalize both the Lumigraph and texture mapping approaches. Their algorithm is defined to work on a wide range of differing inputs, from few images with an accurate geometric model to many images with minimal geometric information.

We differ from texture-based approaches in the sense that we do not re-project all pre-computed images, nor all geometry. Indeed, with the help of a geometry representation we find which parts of the pre-computed images can be used. Moreover, because our algorithm is based on this geometry, it minimizes the size of the stored data, which makes it more accurate than morphing techniques.

OVERVIEW

Since re-rendering the whole scene on a new EM around each moving objects makes it impossible for real-time (See table 1), we propose a new method based on pre-computed EMs to interactively, on-the-fly reconstruct these new EMs. We place around the environment a set of reference environment maps or REMs, pre-computed before the simulation. Each of these REMs stores information both on colors and on the depth from the static surrounding environment. The positions of the pre-computed REMs define in the scene a non-constraining path, where the objects will be able to move. The current navigation algorithm allows objects to move away from this area, however there is no guarantee that the information provided by the REMs will be sufficient for the computation of the reflections onto these objects. Our paper does not address the problem of positioning the REMs. We assume that the REMs are set around the scene, so that a maximum of visible objects are captured in the area where dynamic reflective objects move. Several papers tackle this problem [START_REF] Fleishman | Automatic camera placement for image-based modeling[END_REF][START_REF] Stuerzlinger | Imaging all visible surfaces[END_REF][START_REF] Daniel | Automatic image placement to provide a guaranteed frame rate[END_REF]. At run time, each time a reflective vehicle moves we need to reconstruct a local EM around it using surrounding REMs. Instead of a simple blending2 between pre-computed EMs, which would provide many artifacts3 , we reconstruct a local EM by extracting and blending the correct sub-parts of surrounding REMs (See section 4.1 and 4.2). In section 4.3, we adapt our algorithm to possibly invalid REMs and we introduce an adaptative reconstruction to avoid discontinuity (See section 4.4) and control the frame rate (See section 5).

To summarize our contributions, we provide a framework to use reference environment maps, placed around a complex scene. We propose a method for computing dynamic environment maps for multiple moving objects, blending information provided by a subset of the reference environment maps; the blending is geometry-based and uses discontinuities detection, by efficiently analyzing changes in visibility in the geometry, to provide accurate reflections of the environment. With this new technique we also improve the frame rate using different levels of detail for EMs.

V P I C A C B Figure 2:
At the geometric point P the camera views the reflection of the scene as in point I. This information can be associated to the two pre-computed REMs (A and B). The vector CAI can be used as texture coordinates for the EM A, and similarly the vector CBI can be used as texture coordinates for the EM B.

INTERACTIVE RECONSTRUCTION OF THE LOCAL ENVIRONMENT MAP 4.1 General Idea

This section explains the heart of our method. Given a point P on the reflective object, we need to deduce a reflected color from the pre-computed REMs. We use here the term point in the general sense of geometric point, we will see next paragraph how this idea is used in practice. As describe on figure 2, the normal of the object in P and the view-point position V define the reflected ray by through the angle of reflection about the normal being equal to the angle of incidence, with the incident and reflected ray in the same plane. This reflected ray intersects the surrounding environment at a point I. With the classical local illumination model, the color at the point P is the sum of the ambient/diffuse term of the object with the color of I (specular term). If we assume that reflected objects such as building are only diffuse, the color of I can be associated with the surrounding two REMs A and B. Notice, we use only two REMs because this number is appropriate in our case of vehicles moving in paths defined by streets. Nevertheless, for other types of scene, one might consider a larger number of REMs if necessary.

The reflection is applied as a texture on each polygon of the reflective object combining these two REMs with multitexturing. For each vertex, a computation as previously explains for the point P is done: a point I is computed and the vector --→ CAI is passed to the hardware as texture coordinates (CA is the center of the EM A). Similarly, with the multi-texturing, the vector --→ CBI is used with the EM B. We avoid complex computation for each pixel of the polygon, since texture coordinates are interpolated during the rasterisation. Because the texture interpolation does not match necessary with the geometry of the environment, it may result some discontinuities. We propose a solution to this problem in section 4.

Computation of the Intersection Point I

The technique presented in section 4.1 does not need to know which primitive of the scene is intersected by the reflective ray, only the intersection point I is needed. To find I, we avoid a complete ray tracing computation by tracing our ray from P in a discrete representation of the geometry. Notice that it could be possible to perform this ray tracing on images of the REMs since we have also the depth values, as presented in [START_REF] Lischinski | Image-based rendering for non-diffuse synthetic scenes[END_REF]. We excluded these methods because they are dependent on the number of pre-computed images, since the ray tracing has to be done in each image. Not so far from this idea, we prefer to use a heightfield representation since urban scenes are often 2.5D. Note that for other scene a regular grid could be used. The heightfield is a greyscale image of the city taken from a top view with an orthographic projection, where each pixel refers to the height of the scene. An example of the heightfield used for one of our model is presented in figure 4.

To find I, we trace the ray from P through the heightfield representation as described in [START_REF] Musgrave | Grid tracing: Fast ray tracing for height fields[END_REF][START_REF] Amanatides | A fast voxel traversal algorithm for ray tracing[END_REF]. The ray stops when it arrives in a pixel where the value is higher than the height of the ray. We assume that the heightfield representation is close enough to the geometric representation of the scene to use the entering point Ie of the ray into the cell instead of I. By using this heightfield representation instead of the whole geometry for the ray tracing we introduce artifacts, since it does not match exactly with the geometric representation. Typically, this results in errors as in figure 9 (c) where discontinuities are not always well defined. The important point to notice is that the error introduced here is constant and continue, since we use the heightfield representation as a continuous structure. This continuity permits to avoid sudden variation on the reconstructed EM. However, there is a trade off on the resolution of the discreet representation. The more precise the resolution of the heightfield is, the more accurate the results will be. However, in terms of computation time a small resolution is preferable.

Reference Environment Map Validity

As illustrated in figure 5, sometime the point I is not visible from one of the REMs which is then considered as invalid for the vertex currently considered. To test the local validity of the REM, we add a depth-test after finding the point I.

Together with the textures of the REMs, we store depth maps for each face of the cube. Then, we compare the depth value stored in the pixel corresponding to the direction [CA, I] of the depth map with the depth value of I (distance between CA and I). If the depth value of the direction [CA, I] is less than the distance between CA and I, this means that the REM is invalid for the vertex currently considered, because an object occludes the point I from CA. Therefore, we cannot use this REM and associated weight WA is set to 0. Since we compute the intersection point I for each vertex of a polygon, each vertex has its weight that can be potentially null. Notice, the depth-test is similar to the one carried out in the shadow map algorithm [START_REF] Reeves | Rendering antialiased shadows with depth maps[END_REF].

If all the REMs are invalid we do not have the information we are looking for, and thus a special treatment needs to be done to avoid black regions that can appear in the reflection. One solution would be to add a REM at this point. The detection of such a case could be used to add automatically a new REM at this position. In our implementation, the closest REM (the one with the highest weight before the validity test) is considered to avoid gaps regions being displayed.

V P I

I C A C B

Adaptative Mesh

The complete process of extracting information from the REMs could be performed at each polygon of the reflective object. However, this has several drawbacks. First, the computation cost depends on the number of polygons. Second, the distribution of the vertices might be irregular, resulting in distortion and discontinuity of the reflection for some areas and too high precision for others. Third, because reflections depend on the camera position, if the object stops moving, we still have to perform our algorithm when the camera moves.

For this reasons, we decided to compute first a local EM as the one presented in figure 6, and then use it as a regular EM. Thus, we are able to control the operation cost and the desired quality. The reconstruction is done separately for each of the six images of the cube with an off-screen rendering. The aim is to reconstruct faster an EM without rendering the whole scene, but with a similar quality. Such a reconstructed EM is presented figure 7.

We compute each face of the new EM with a mesh on which we apply the process described in the previous sections 4.1, 4.2 and 4.3. We start with a regular mesh 10 × 10 that will be refined if necessary. For each vertex of this mesh, we trace a ray starting from the center of the moving object and going through the vertex. Then the intersecting point is used to compute the texture coordinate of the vertex and two weights for the two surrounding REM are computed. The reflected environment has some depth discontinuities to which our algorithm is sensitive, resulting in some popping effects. The method used to overcome this problem is illustrated in figure 6. We recursively subdivide the initial mesh depending on the depth variations of the reflected point at the vertices. Given a quad of the mesh described by the vertices 1, 2, 3, 4, and the associate depth values Z1, Z2, Z3, Z4, we subdivide if our criteria is true. Our criteria is true if one of |Zi -Zj |/min(Zi, Zj ) > R is true for i, j = 1, 2, 3, 4, i = j and where R is a constant ratio chosen to reflect important changing in the scale of our model. This criteria means that if there is a large variation in depth between vertices of a patch of the mesh, the patch is subdivided until the appropriate level is found. The maximum subdivision corresponds to either a threshold set by the user or to the size of a pixel. A result of this subdivision process is shown in figure 7.

ADAPTIVE QUALITY FOR CONTROL-LING THE INTERACTIVITY

In our case, we need to consider multiple objects in very complex environments. Therefore, we absolutely need to be able to control and adapt the rendering cost to keep a constant frame rate. For example, the algorithm can be modified to treat the reflections differently, depending on the viewpoint distance or on the degree of interest of the user. With our algorithm we can produce several levels of detail by controlling the resolution of the mesh of the reconstructed EM. Two other parameters, also existing in the case of re-rendering all the geometry, can be added: controlling the resolution of the reconstructed images of the EM and deciding which blending to apply for far objects.

We control the resolution of the mesh of the reconstructed EM according to the size of the object on the screen. The size of the smallest quad of our adaptive mesh (See figure 7) does not have to be smaller than a pixel after being projected on the final image. For a dynamic object, we then compute the size in pixels of the projected bounding box of the dynamic object on the screen. We divide this size by the resolution of the EM (128 or 256 pixels in our implementation) to obtain the minimum size in pixels of the quads that compose our mesh. Notice, this number can be deliberately increased to give a blur effect to the reflection that can fake motion blur and then significantly increases the realism of the dynamic object.

When objects are sufficiently far away, a simple blending is applied. As shown in section 7, this also significantly helps to accelerate the results.

IMPLEMENTATION AND DISCUSSION

Our simulation runs on a 2Ghz Intel Pentium PC with a GeForce4 Ti4600 graphics card. The basic display is handled by Performer TM on Linux, and therefore we benefit from view-frustum culling and the scene graph. We also use the hardware capacity to accelerate the rendering. Our method, consist in computing the texture coordinates of each vertex with a ray tracing on the heightfield, which is done in software. Then the hardware capacity is used for the environment map rendering. Since we do not use unusual features of graphics hardware, our implementation will be able to run both on SGI and on PCs that could drive different kinds of display: CAVE-like, immersive desk, etc.

Moreover, according to the latest nVIDIA information on ray tracing in the vertex engine 4 , we believe that the performance could be improved with the latest graphics boards (GeForce FX). Indeed, this generation of board will allow enough functionality to compute the texture coordinates (mostly the ray tracing in heightfield) in a vertex shader program.

Our method provides an efficient solution to reconstruct EMs around moving objects. Due to the pre-computation of the REM, our technique is able to manage only static objects like buildings as object that can be reflected. Of course the reflecting objects are dynamic. It is clear that static objects are the major components of a typical scene. Nevertheless, we can render other dynamic objects on the reconstructed EM to reflect both static and dynamic geometry. We have started to explore this direction by rendering dynamic virtual humans [START_REF] Franco Tecchia | Imagebased crowd rendering[END_REF] in a second pass on the reconstructed EM (See images (e), (f) and (g) on figure 10). We have not implemented yet the rendering of other dynamic vehicles on the reconstructed EM because of technical difficulties about Performer.

RESULTS

Since the complete reconstruction of the "Place Massena" in Nice has not been achieved yet, we have tested our technique in a virtual city. This virtual model provides extended polygonal complexity and thus dynamic objects can provide complex reflective results. In this paper, we focused on the rendering of reflection effects, and therefore the behavior of objects, especially for cars, inside the virtual scene is very simplistic. We applied our algorithm for the case of vehicles moving around a virtual city composed of buildings (25,600 triangles) and 8 trees (59,100 triangles each) with a total of 500,000 triangles. The local model where the simulation runs has 8 roads and covers an area of 1 km 2 . For our heightfield ray tracing the size of one cell is 1 meter. The simulation we tested uses 54 REMs placed as shown in figure 8. Each EM has a resolution of 128x128 pixels for each of its 6 faces, with 4 bytes per pixel (3 bytes for the color plus one for the depth), using 6x65Kb=390Kb of memory. The total memory used to store all the reference maps is therefore 54x390=21.6Mb without using any compression.

Texture compression gives at least a 4:1 compression ratio while introducing very limited artifacts (compression ratio can go up to 6:1 with nVIDIA cards). If we assume a compression ratio of 4:1, we consume 5Mb of texture memory. With a graphics board of 128Mb of memory we can apply our technique in a city 10 to 15 times bigger.

We measured the scalability of the algorithm in relation to the number of dynamic objects, as it is summarized in the table shown in table 1. In a first experiment (column No reflection), we perform the simulation using the OpenGL Phong rendering: diffuse and specular (N.L) without any reflection. We compare the technique consisting of re-render Table 1: Table showing the different frame rates obtained for a scene with moving vehicles. We compare our algorithm to others using just Phong shading, or with the complete re-computation of environment maps for each moving object.

the whole scene onto the 6 faces of the cube (column Rerendering) with our technique (column MEM) in both conditions with or without levels of detail.

Using our method increases greatly the visual quality and therefore the realism. For certain cases, it might be that the error introduced due to approximation makes the result of the blend blurred compared to the computation of the environment map by rendering the entire scene. In figure 9, we compare the result of the reflection of the environment on a sphere accessing reflection information from a surrounding environment EM. In (a), the EM results from a simple blending between two REMs. In (b), we computed the EM from scratch, rendering the whole scene onto each face of the cube. In (c), we applied our MEM technique, interpolating between two REMs using an adaptive mesh on the cube and taking into account the discontinuities of the environment. Image (a) is obviously completely wrong. Image (b) has a very high quality. The results of our method, as shown in image (c), are very close to image (b), but the reflection is less sharp. However the obtained reflection is very similar to the one obtained with environment maps, thus validating our method. Also the case of the reflection on the sphere is one of the worst since the object has a regular distribution of the normals. For an object as complex as a car, the imprecisions would not be perceptible.

In term of relative performance, our technique is much more efficient comparing to the re-rendering of the scene on a new EM, with a factor from 6 to 8 times faster when levels of detail is applied. A comparison between the column No reflection and the column With LOD shows that our technique is only from 1.5 to 1.75 time slower than rendering vehicles without any reflection, while our technique increases greatly the realism. In term of absolute performance, one thing to consider is that the frame-rate is already low for 30 cars simulated without computing the reflections (See column No reflection). This is due to the large number of polygons (500 000) of the scene. Another thing to consider is that Performer TM performs only view-frustum culling, and therefore cars behind the buildings also use the multiple environment maps technique. Using occlusion culling and point-base rendering for trees could significantly improve the frame rate.

In figure 10, the quality of the results is illustrated for different configurations, showing that the algorithm works for a wide range of geometry and not only for simple objects constraint on the floor. Small objects like trees are the bottleneck of our method, producing easily inaccurate reflections, since the precision of the reflection is strongly dependent on the size of the heightfield representation used for the ray tracing. Nevertheless, quality of the results for this kind of objects are reasonable as you can see figure 7 (a).

CONCLUSION AND FUTURE WORK

In this paper, we presented a technique that makes use of the properties of environment maps to enable the reflections of a complex environment onto dynamic objects. We presented a new method, called multiple environment maps, that allows the use of a set of pre-computed environment maps, placed around the scene, that dynamically deduce new environment maps associated with the dynamic objects. We thus avoid rendering the scene six times per object at every frame. To reconstruct the environment maps, we merge reference environment maps using geometric information to retrieve the correct texture coordinates. We control the quality and the complexity by sampling the faces of the EMs with a resolution adapted to the geometry. Moreover, we applied levels of detail on the environment maps to accelerate the rendering. The visual quality of the results and the computation times are satisfactory, and they prove that combined with other acceleration techniques, such as occlusion culling or levels of detail of the geometry, the technique can be extremely powerful and used for virtual reality applications.

However, this method needs to be more automatic. First, REMs should be automatically positioned in the environment. Second, the development of the levels of detail technique with new metrics could allow EMs to be reused for several objects or several frames. Third, this method could be generalized for any environment (not just cities). Instead of using a heightfield, a 3D grid could store the information for allowing any kind of static geometry like arch, balcony, etc. It would, also, be interesting to reconstruct our EM around dynamic objects by extracting informations from more than two REMs since common graphics hardware allow up to eight textures simultaneously. Finally, work on the behavior of vehicles and specially on the interaction between vehicles and crowd has to be done to increase the global realism of the simulation.

Figure 1 :

 1 Figure 1: Simulation on immersive displays of a new configuration of a city, here the "place Massena" in Nice where a tramway is added. This image was generated by REVES/INRIA Sophia-Antipolis (http://www-sop.inria.fr/reves), in the context of the CREATE project.

Figure 3 :

 3 Figure 3: For each vertex, a weight for each surrounding REM is applied to take into account the distance and the validity of the computed coordinates from each REM.For each vertex, a weight for each surrounding REM is applied to take into account the distance and the validity of the computed coordinates from each REM. The point Ip is the projection of I on the axis defined by the center of each of the two REMs. From the distance of the center of the EMs to the projected point Ip we can deduce the weight to apply on each reference map for the blending: DA = dist(CA, Ip)/dist(CA, CB)

Figure 4 :

 4 Figure 4: To find the reflected point (See figure 2) we perform a discrete ray tracing in a heightfiel representation of the scene.

Figure 5 :

 5 Figure 5: Example of an invalid case when using the reference maps. Point I should be reflected on the dynamic object in point P . However, it is occluded from one of the REMs, in this case A, by an object. To avoid errors in the reflection, A needs to be invalidated and dismissed when computing the local EM around the dynamic object.

Figure 6 :

 6 Figure 6: Illustration of the decision on the mesh subdivision of the EM, depending on the depth variation at vertices.

Figure 7 :

 7 Figure 7: An example of a reconstructed EM. In red, one can see the adaptive mesh subdivision depending on the depth variation at vertices.

Figure 8 :

 8 Figure 8: Cropped view of the distribution of the reference environment maps.

Figure 9 :

 9 Figure 9: (a) Using a simple blending between REM produces ghost effects in the blend. (b) Rendering the entire scene on the 6 faces of the EM gives a good image quality but it is difficult to achieve that in real time for several objects. (c) Using geometric information and REM, our algorithm provides accurate reflections. Without LOD With LOD # of cars # of cars displayed No reflection (Fps) Re-rendering EM (Fps) MEM (Fps) Re-rendering EM (Fps) MEM (Fps) 15 3-5 14 0.2-0.8 4 1.2 8 30 10 8.5 0.1 1.3 1 5-6

Figure 10 :

 10 Figure 10: (a), (b), (c) Close views on reflective moving cars in a city. (d) Sequence of animation of a virtual car driving in a virtual city. (e), (f ), (g) Invasion of the city by a whale, reflective trees and animated virtual humans.

CREATE is a 3-year RTD project funded by the 5th Framework Information Society Technologies (IST) Programme of the European Union (EU). The official contract with the EU was signed under the contract number IST-2001-34231. The project started in

March 2002. www.cs.ucl.ac.uk/create/

The reflection direction is used to access the pixel color in the REM and a blend is applied to get the final color.

For example, when a camera tracks an object, the surrounding environment reflection seems to be translating. With a simple blend, the environment would simply appear and disappear with a ghosting blur effect as you can see in figure9(a).

Ray-traced Reflection Demo, http://www.cgshaders.org/shaders

Acknowledgement

This work has been funded by the European Union though CREATE (contract number IST-2001-34231) which is a 3year RTD project funded by the 5th Framework Information Society Technologies (IST) Programme of the European Union. We wish to thank Mel Slater and Hila Ritter Widenfeld for proofreading this paper.