Sara Bouraine
email: sbouraine@yahoo.fr

Thierry Fraichard
email: thierry.fraichard@inria.fr

Hassen Salhi
email: hassensalhi@yahoo.fr

Provably Safe Navigation for Mobile Robots with Limited Field-of-Views in Dynamic Environments

Keywords: Mobile Robots, Dynamic Environments, Autonomous Navigation, Motion Safety, Collision Avoidance, Inevitable Collision States CR Subject Classification Robotics, Autonomous vehicles

This paper addresses the problem of navigating in a provably safe manner a mobile robot with a limited fieldof-view placed in a unknown dynamic environment. In such a situation, absolute motion safety (in the sense that no collision will ever take place whatever happens in the environment) is impossible to guarantee in general. It is therefore settled for a weaker level of motion safety dubbed passive motion safety: it guarantees that, if a collision takes place, the robot will be at rest. The primary contribution of this paper is the concept of Braking Inevitable Collision States (ICS), i.e. a version of the ICS corresponding to passive motion safety. Braking ICS are defined as states such that, whatever the future braking trajectory followed by the robot, a collision occurs before it is at rest. Passive motion safety is obtained by avoiding Braking ICS at all times. It is shown that Braking ICS verify properties that allow the design of an efficient Braking ICS-Checking algorithm, i.e. an algorithm that determines whether a given state is a Braking ICS or not. To validate the Braking ICS concept and demonstrate its usefulness, the Braking ICS-Checking algorithm is integrated in a reactive navigation scheme called PASSAVOID. It is formally established that PASSAVOID is provably passively safe in the sense that it is guaranteed that the robot will always stay away from Braking ICS no matter what happens in the environment.

Introduction

Robotics technology has matured and Autonomous Ground Vehicles (AGVs) are becoming a reality: consider the successes of the DARPA Challenges 1 or the VisLab Intercontinental Autonomous Challenge 2 . They demonstrate robotics systems traveling significant distances at high speed in complex and realistic environments. However such systems remains prone to accidents (see [START_REF] Fletcher | The MIT -Cornell collision and why it happened[END_REF]. While moving (especially at high speed), AGVs (and other robotic systems as well) can be potentially dangerous should a collision occur; this is a critical issue if such systems are to transport or share space with human beings.

Roboticists have long been aware of the motion safety issue; there is a rich literature on collision avoidance and collision-free navigation. Nonetheless, motion safety has for a long time remained a taken-for-granted and ill-defined notion (see [START_REF] Fraichard | A short paper about motion safety[END_REF]. Demonstrating that a robot avoids collision on a limited set of experiments is not enough. If autonomous robots are ever to be deployed among human beings on a large scale, there is a need to design collision avoidance and navigation schemes for which motion safety can be characterized and even guaranteed. The literature review of Section 2 shows that the Robotics community is displaying a growing interest in designing such provably safe collision avoidance and navigation schemes. It also shows that motion safety in the real world remains an open problem as soon as the term real world implies that:

1. The environment features both fixed and moving objects whose future behaviour is unknown. 2. The robot has only a partial knowledge of its surroundings because of its sensory limitations.

Fig. 1: Robot with a limited field-of-view in an unknown environment with fixed and moving objects (the dark grey region is unobserved and may contain anything).

1 www.darpa.mil/grandchallenge 2 www.IntercontinentalChallenge.eu

The purpose of this paper is precisely to address such problems, i.e. that of navigating autonomous robots with sensors having a limited field-of-view in unknown environments featuring moving objects whose future behaviour is unknown (see Fig. 1). Furthermore, the primary motivation is to study whether, in such situations, it is possible to obtain strict motion safety guarantees, strict in the sense that they can be established formally.

Given that motion safety has to do with staying away from states where a collision occurs (now or eventually), the first position taken in this work is to address the motion safety issue within the formal Inevitable Collision State (ICS) framework developed in [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF]. An ICS is a state for which, no matter what the future trajectory of the robot is, a collision eventually occurs. ICS are defined with an absolute motion safety perspective (absolute in the sense that no collision will ever take place whatever happens in the environment).

In theory, absolute motion safety requires a complete knowledge of the future, up to infinity in some singular situations (see the motion safety criteria laid down in [START_REF] Fraichard | A short paper about motion safety[END_REF] and the discussion on motion safety of [START_REF] Macek | Towards safe vehicle navigation in dynamic urban scenarios[END_REF]). It can be argued then that absolute motion safety is impossible to guarantee in general unless questionable assumptions concerning the robot and its environment are made, e.g. requiring that the velocity of the robot is a multiple of the maximum velocity of the objects [START_REF] Lumelsky | Velocity bounds for motion planning in the presence of moving planar obstacles[END_REF], or that the moving objects should appear beyond a distance which is a function of their number, sizes and velocities [START_REF] Kohout | Guaranteeing safety in spatially situated agents[END_REF].

In situations such as Fig. 1, absolute motion safety is impossible to guarantee (primarily because the lack of knowledge about the future renders ICS ineffective). To cope with that issue, the second position taken in this work is: better guarantee less than guarantee nothing. To that end, it is settled for a weaker level of motion safety that guarantees that, if a collision takes place, the robot will be at rest. As per [START_REF] Macek | Towards safe vehicle navigation in dynamic urban scenarios[END_REF], this motion safety level is dubbed passive motion safety.

The primary contribution of this paper is the concept of Braking ICS, i.e. a version of the ICS corresponding to passive motion safety. Braking ICS are defined as states such that, whatever the future braking trajectory followed by the robot, a collision occurs before it is at rest. Passive motion safety is obtained by avoiding Braking ICS at all times.

It is shown that Braking ICS verify properties that allow the design of an efficient Braking ICS-Checking algorithm, i.e. an algorithm that determines whether a given state is a Braking ICS or not. This algorithm is derived from the original ICS-checking algorithm presented in [START_REF] Martinez-Gomez | An Efficient and Generic 2D Inevitable Collision State-Checker[END_REF].

To validate the Braking ICS concept and demonstrate its usefulness, the Braking ICS-Checking algorithm is inte-grated in a navigation scheme henceforth called PASSAVOID. It is a reactive scheme for a mobile robot with a limited field-of-view placed in an unknown dynamic environment. It operates with a given time step and its purpose is to compute the control that will be applied to the robot at the next time step. It is formally established that PASSAVOID is provably passively safe in the sense that it is guaranteed that the robot will always stay away from Braking ICS no matter what happens in the environment.

In itself, the central idea behind passive motion safety, i.e. using braking trajectories, is not new, it has been used before in different contexts (see Section 2). However, to the best of the authors'knowledge, it is the first time it is given a formal treatment in as general a context as possible whether it concerns the robot's dynamics, its field-of-view, or the knowledge (or lack thereof) about the future behaviour of the moving objects. As limited as it may appear, passive motion safety is interesting for two reasons: (1) it allows to provide at least one form of motion safety guarantee in challenging scenarios such as Fig. 1, and (2) if every moving object in the environment enforces it then no collision will take place at all.

The paper is organized as follows: a review of the relevant literature is done in Section 2. Section 3 discusses motion safety issues and defines passive motion safety. The adaptation of the ICS concept to Braking ICS is done in Section 4. The Braking ICS-checking algorithm and the navigation scheme are respectively detailed in Sections 5 and 6. Finally, experimental results obtained in simulation are presented in Section 7.

Related Works

As mentioned above, the Robotics literature is teeming with works concerned with collision avoidance but most of them do not offer an explicit formulation of the safety guarantees they provide or the conditions under which they must operate (see [START_REF] Fraichard | A short paper about motion safety[END_REF].

The earliest relevant works addressed the so-called "Asteroid Avoidance Problem" (wherein objects traveling at a constant linear velocity must be avoided): in the 3D case, [START_REF] Reif | Motion planning in the presence of moving obstacles[END_REF] shows that collision avoidance is always possible if the robot's velocity is greater than the asteroids' velocities and if the robot is not initially in the "shadow" of an asteroid. In the 2D case, [START_REF] Kohout | Guaranteeing safety in spatially situated agents[END_REF] shows that collision avoidance is always possible iff the asteroids appear beyond a "threat horizon", i.e. a distance which is a function of the number, size and velocity of the asteroids. Likewise, [START_REF] Lumelsky | Velocity bounds for motion planning in the presence of moving planar obstacles[END_REF] shows that, for a robot operating in a planar environment with arbitrarily moving objects, collision-free motion is guaranteed iff the maximum velocity of the robot is a multiple of the maximum velocity of the objects. Such results are very interesting. Unfortunately, they rely on assumptions that rarely occur in the real world.

A related family of research works are those seeking to coordinate the motion of a set of robots. Different distributed coordination schemes have been proposed for which collision avoidance is guaranteed, (e.g. [START_REF] Pallottino | Decentralized cooperative policy for conflict resolution in multivehicle systems[END_REF]Van den Berg et al 2008;[START_REF] Lalish | Decentralized reactive collision avoidance for multivehicle systems[END_REF][START_REF] Bekris | Safe and distributed kinodynamic replanning for vehicular networks[END_REF]. However, this guarantee is lost if the environment contains uncontrolled moving objects.

General motion safety issues have been studied thanks to the Inevitable Collision States3 (ICS) concept developed in [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF]. An ICS is a state for which, no matter what the future trajectory of the robot is, a collision eventually occurs. ICS provides insight into the complexity of guaranteeing motion safety since it shows that it requires to reason about the future evolution of the environment and to do so with an appropriate lookahead4 that can possibly be infinite. Such conditions being next to impossible to obtain in the real world plus the fact that ICS characterization is very complex has led a number of authors to consider relaxations of ICS such as:

-ICS approximation, (e.g. [START_REF] Chan | Towards safe motion planning for dynamic systems using regions of inevitable collision[END_REF][START_REF] Kalisiak | Faster motion planning using learned local viability models[END_REF]: such approximations being not conservative, the motion safety guarantee is lost. -τ-Safety, (e.g. [START_REF] Frazzoli | Real-time motion planning for agile autonomous vehicle[END_REF][START_REF] Vatcha | Perceived CT-Space for Motion Planning in Unknown and Unpredictable Environments[END_REF]:

the robot is guaranteed to remain in states where it is safe for a given duration (hopefully sufficient to compute an updated safe trajectory. . . ). -Evasive trajectories, (e.g. [START_REF] Hsu | Randomized kinodynamic motion planning with moving obstacles[END_REF][START_REF] Bekris | Greedy but safe replanning under kinodynamic constraints[END_REF][START_REF] Seder | Dynamic window based approach to mobile robot motion control in the presence of moving obstacles[END_REF][START_REF] Macek | Towards safe vehicle navigation in dynamic urban scenarios[END_REF]: they guarantee that the robot can only be in states where it is possible to execute an evasive trajectory, e.g. a braking manoeuvre for a car or a circling manoeuvre for a plane.

Recently, authors have proposed probabilistic versions of the ICS concept, (e.g. [START_REF] Bautin | Inevitable collision states, a probabilistic perspective[END_REF][START_REF] Althoff | Probabilistic collision state checker for crowded environments[END_REF], so as to better capture the uncertainty that prevails in real world situations, in particular the uncertainty concerning the future behaviour of the moving objects. These approaches are interesting but they offer no strict motion safety guarantees since probabilistic models are used.

There are a few research works taking into account sensory limitations. For instance, the occlusion problem, i.e. the existence of regions that are hidden by other objects, is addressed in a coarse manner in [START_REF] Sadou | Occlusion in obstacle detection for safe navigation[END_REF] and in a more principled manner in [START_REF] Chung | Safe navigation of a mobile robot considering visibility of environment[END_REF]. The occlusion and the limited field-of-view problems are addressed in [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF] and Madhava [START_REF] Krishna | Safe proactive plans and their execution[END_REF]. [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF] addresses the case of a mobile robot moving in a static environment; its approach is general and ICS-based. While Madhava [START_REF] Krishna | Safe proactive plans and their execution[END_REF] considers dynamic environments, it does so primarily with a path-velocity decomposition perspective [START_REF] Kant | Toward efficient trajectory planning: the pathvelocity decomposition[END_REF].

The contribution of this paper is an extension of [START_REF] Macek | Towards safe vehicle navigation in dynamic urban scenarios[END_REF] that deals with limited field-of-views, occlusions and unknown future behaviour of the objects. The approach proposed is based upon a relaxation of ICS that falls into the "evasive trajectories" family. As mentioned in §1, this paper addresses the problem of navigating in a provably safe manner a mobile robot with sensors having a limited field-of-view in an unknown environment featuring fixed and moving objects with upperbounded velocity and unknown future behaviour. Let A denote the mobile robot at hand. It operates in a 2D workspace W ; a state of A is denoted by s with s ∈ S , the state space of A . Assuming that A is equipped with range sensors such as laser telemeters or range cameras, it can only perceive a subset of W ; this subset is A 's field-of-view; its shape is arbitrary; it depends on the current surroundings of A and the maximum range of its sensors. It is henceforth denoted FOV. Accordingly, W is partitioned in three subsets: (1) FOV, (2) FOV c , the part which is unseen (FOV c = W \cl(FOV)) and (3) ∂ FOV, the boundary between the two.

Safety Issues

Outline of the Problem

Both FOV and FOV c are open sets. It seems reasonable to assume that A is "looking around itself"; in other words that A (s) ⊂ FOV where A (s) denotes the region of W occupied by A when it is in s. To account for the existence of 3D range sensors, e.g. Velodyne LIDAR or PrimeSensor range camera, FOV can contain "holes" representing objects entirely perceived by the sensory system of A . Accordingly, FOV, ∂ FOV and FOV c are not necessarily singly connected (see Fig. 2). FOV represents the region of W which is free of objects at the sensing time.

This generic field-of-view model can further be enriched if the sensors of A can differentiate the fixed vs the moving objects. In that case, ∂ FOV can be partitioned into three parts respectively corresponding to fixed objects, moving objects and so-called "unseen" objects, i.e. the sensing limits and the occluding lines:

∂ FOV = ∂ FOV f ∪ ∂ FOV m ∪ ∂ FOV u (1)
When the sensors of A cannot differentiate between fixed and moving objects,

∂ FOV = ∂ FOV u .
3.2 Modeling the Future Fig. 3: Models of the future (from left to right): fixed disk (1); moving disk with constant velocity (2); conservative models for a moving point with unknown future motion and upper-bounded velocity (3), and upper-bounded acceleration and velocity (4).

The ICS concept brings to light two things: the first one is that there is more to motion safety than the simple fact that A 's trajectory be collision-free; it must be ICS-free, i.e. A must always be in a state for which an evasive trajectory is available. The second one is that motion safety is always defined wrt the model of the future that is used. When dealing with objects whose future behaviour is unknown, what model of the future should be used? The answer is to be conservative: one must consider all possible future motions for the object at hand. Consider the case of a point object with upper-bounded velocity whose future behaviour is unknown. Given the initial position of the object, the region of the workspace that is possibly not collision-free is modeled by a disc that grows over time with a growth rate corresponding to the maximal velocity of the object (Van den Berg and Overmars 2008). In space×time, it is represented as an inverted cone (see Fig. 3). Such a cone is the reachable set (LaValle 2006, Chap. 14) of a point object whose dynamics is characterized by infinite acceleration and upperbounded velocity capabilities. In general, reachable sets can be used to represent all possible future motions for object with arbitrary dynamics, e.g. an object with upper-bounded velocity and acceleration (see Fig. 3-right). Now, in a situation such as the one depicted in Fig. 2, how does one take into account the unseen parts of W that belongs to ∂ FOV u or FOV c ? Walking in the footsteps of [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF] or [START_REF] Krishna | Safe proactive plans and their execution[END_REF]), the answer is once again to be conservative and to treat every point of ∂ FOV u or FOV c as a potential moving object with unknown future behaviour. In conclusion, the space×time model of the future for A can be defined as follows for the different components of A 's field-of-view (see Fig. 4):

-∂ FOV u ∪ FOV C (the unseen objects): every point in this set is modeled as a disc that grows as time passes (i.e. a cone in space×time). -∂ FOV f (the fixed objects): every point in this set remains constant over time (i.e. a vertical line in space× time). -∂ FOV m (the moving objects): if the information about their future behaviour is available and reliable, every point in this set is modelled accordingly (i.e. a curve in space× time), otherwise it is treated as an unseen object and modeled as a growing disc.

This of course is the case when the sensors of A can differentiate between fixed and moving objects. If it is not the case then every point in ∂ FOV is modeled as a disc that grows as time passes (i.e. a cone in space×time). Within such a model of the future, it is worth noting that the region of W which is free of objects at the sensing time, i.e. FOV, gradually shrinks as time passes and eventually vanishes (see Fig. 5). Henceforth, FOV(t) denotes the region of W which is free of objects at time t in the conservative model of the future. Likewise, ∂ FOV(t) denotes its boundary.

From now on, the worst possible scenario is considered: it is assumed that A cannot distinguish the fixed from the moving objects5 and that it has no information whatsoever about their future behaviour. In that case, the minimal knowledge required about the environment is an upper-bound on the objects'velocity (otherwise, it is impossible to derive a conservative and useful model of the future). Now, if additional information is available about an object, e.g. whether it is fixed or moving, about its dynamics or its future behaviour, it can easily be integrated into the model of the future one way (see Fig. 3). The important thing is to derive a conservative model so that the motion safety properties that will be obtained can actually be guaranteed no matter what happens in the environment.

Absolute vs. Passive Motion Safety

The ICS concept laid down in [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF] guarantees absolute motion safety in the sense that, for a state not to be an ICS, there must exist a collision-free trajectory of infinite duration. Now, an object with unknown future behaviour is a challenge. If it is modeled conservatively as above then, at some point in the future, the whole workspace is entirely covered by the growing disc representing it. At that moment, the whole state space of the robot is forbidden and it becomes impossible to find a collision-free trajectory of infinite duration. This is a situation where the ICS concept becomes ineffective. In the authors'opinion, the only answer to this challenge is to settle for a weaker level of motion safety; the rationale being: better guarantee less than guarantee nothing. The choice here is to guarantee that, if a collision takes place, the robot will be at rest. This motion safety level, dubbed passive motion safety in [START_REF] Macek | Towards safe vehicle navigation in dynamic urban scenarios[END_REF], seems a reasonable choice given the harsh constraints imposed by a limited field-of-view. It yields the following definition:

Definition 1 given a model of the future workspace evolution, a passively safe or p-safe state for A is a state s such that there exists one braking trajectory starting at s which is collision-free until A has stopped.

From ICS to Braking ICS

Using braking trajectories in order to evaluate the safety of a given state has been done before, e.g. [START_REF] Petti | Safe motion planning in dynamic environments[END_REF][START_REF] Bekris | Greedy but safe replanning under kinodynamic constraints[END_REF][START_REF] Seder | Dynamic window based approach to mobile robot motion control in the presence of moving obstacles[END_REF][START_REF] Ferguson | Motion planning in urban environments[END_REF][START_REF] Kuwata | Real-time motion planning with applications to autonomous urban driving[END_REF]. The focus in this paper is to do it in the formal framework of the ICS concept. The concept of Braking ICS (ICS b ) is first derived from the original ICS concept. It is then used to design ICS b -CHECK, i.e. the corresponding variant of the ICS checking algorithm proposed in [START_REF] Martinez-Gomez | An Efficient and Generic 2D Inevitable Collision State-Checker[END_REF], and to use it in the passively safe navigation scheme PASSAVOID. ICS b -CHECK and PASSAVOID are respectively detailed in §5 and §6.

Notations

The dynamics of the robot A is generally described by differential equations of the form:

ṡ = f (s, u) subject to g(s, ṡ) ≤ 0 (2)
where s ∈ S is the state of A , ṡ its time derivative and u ∈ U a control. S and U respectively denote the state space and the control space of A . Let A (s) denote the closed subset of the workspace W occupied by A when it is in s. Let ũ : [0,t f ] -→ U denote a control trajectory, i.e. a time-sequence of controls, t f is the duration of ũ. The set of all possible control trajectories is denoted Ũ . Starting from an initial state s 0 at time 0, a state trajectory s, i.e. a timesequence of states, is derived from a control trajectory ũ by integrating (2); s(s 0 , ũ,t) denotes the state reached at time t.

A control trajectory ũb ∈ Ũ such that sb (s 0 , ũb ,t b ) is a state where A comes to a halt (and remains so) is a braking trajectory for s 0 and t b is its braking time. The set of all possible braking trajectories for s 0 is denoted Ũ s 0 b . In a situation such as the one depicted in Fig. 2, the open subset FOV is the free part of the workspace while ∂ FOV f , ∂ FOV m , ∂ FOV u and FOV c represent objects (seen and unseen). Let B i denote the space×time model of the future evolution of the corresponding object (according to the modeling rules defined in §3.2). At time 0, i.e. the sensing time, To ease notations, it is assumed that

B i (0) corresponds to a subset of ∂ FOV f , ∂ FOV m , ∂ FOV u or FOV c . B i (t)
B i ≡ B i ([0, ∞)).

Braking ICS Definition

A Braking ICS (ICS b ) is informally defined as a state for which no matter what the future braking trajectory followed by A is, a collision occurs before A is at rest. Hence the following formal definition:

Definition 2 (Braking ICS) s is a ICS b iff ∀ ũb ∈ Ũ s b , ∃t ∈ [0,t b [, s(s, ũb ,t) is a collision state at time t.
It is worth noting that when A is in a state s where A is at rest, Ũ s b reduces to ũ• b that denotes the braking trajectory where a null control is applied to A . Accordingly, s is always p-safe (even if A (s) is in collision).

It is then possible to define the set of ICS b yielding a collision with a particular object B i :

ICS b (B i ) = {s ∈ S |∀ ũb ∈ Ũ s b , ∃t ∈ [0,t b [, A ( s(s, ũb ,t)) ∩ B i (t) = / 0} (3)
Likewise, the ICS b set yielding a collision with B i for a given trajectory ũb is defined as:

ICS b (B i , ũb ) = {s ∈ S |∃t ∈ [0,t b [, A ( s(s, ũb ,t)) ∩ B i (t) = / 0} (4)

Braking ICS Properties

The first two ICS b properties that can be shown are the equivalent of two key ICS properties established in [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF] and seminal in the design of an ICS checking algorithm. Let B = n 1 B i . The first property shows that ICS b (B) can be derived from ICS b (B i , ũb ) for every object B i and every possible braking trajectory ũb .

Property 1 (ICS b Characterization)

ICS b (B) = ũb ∈ Ũb n i=1 ICS b (B i , ũb )
Proof The proof of property 1 is done in two stages: it is first established that:

s ∈ ICS b (B) ⇔ s ∈ ũb ∈ Ũ s b ICS b (B, ũb )
and then that:

s ∈ ICS b ( n i=1 B i , ũb ) ⇔ s ∈ n i=1 ICS b (B i , ũb )
These two properties are demonstrated in a straightforward manner as in [START_REF] Fraichard | Inevitable collision states. a step towards safer robots[END_REF]. Combining the two properties above yields property 1.

⊓ ⊔

The next property permits to compute a conservative approximation of ICS b (B) by using a subset only of the whole set of possible braking trajectories.

Property 2 (ICS b Approximation)

ICS b (B) ⊆ ICS b (B, E )
with E ⊆ Ũb , a subset of the whole set of possible braking trajectories.

Proof

ICS b (B) = ũb ∈E ICS b (B, ũb ) ∩ ũb ∈ Ũb \E ICS b (B, ũb ) ⊆ ũb ∈E ICS b (B, ũb ) ⊓ ⊔
One distinctive feature of the ICS concept is that trajectories of infinite duration are checked for collision, i.e. it has an infinite lookahead (it is this infinite lookahead that guarantees safety). While the ICS b concept also considers trajectories ũb of infinite duration, collision checking is limited to the time interval [0,t b [ where t b is the braking time of ũb . For an arbitrary subset E of the whole set of possible braking trajectories, a finite lookahead T h exists:

T h = max ũb ∈E {t b } (5)
T h is a valid lookahead in the sense that, in order to compute ICS b (B, E ), it suffices to consider the model of the future up to time T h . This is established by the following property:

Property 3 (ICS b Lookahead) ICS b (B, E ) = ICS b (B([0, T h [), E )
Proof Property 3 stems from the very definition of a Braking ICS which, for a given braking manoeuvre ũb , is only concerned with collisions taking place before t b < T h .

⊓ ⊔

Finally, recall from §3.1 that, for the case of a robot with a limited field-of-view, B comprises ∂ FOV and FOV c , i.e. the unseen part of W . From a motion safety perspective, the next property is very important since it establishes that FOV c can be ignored in the computation of ICS b (B). In other words, considering ∂ FOV suffices to guarantee motion safety.

Property 4 (Field-of-View Boundary)

ICS b (B) = ICS b (∂ FOV ∪ FOV c ) = ICS b (∂ FOV)
Proof The equality between ICS b (B) and ICS b (∂ FOV) is done is two stages. Let s denote a collision-free state whose corresponding position is located inside FOV and such that s ∈ ICS b (∂ FOV). As per Definition 2, it stems that:

∀B i , ∀B j , ICS b (B i ) ⊆ ICS b (B i ∪ B j ) Accordingly: s ∈ ICS b (∂ FOV) ⇒ s ∈ ICS b (∂ FOV ∪ FOV c ). It is assumed now that s ∈ ICS b (FOV c ), it means that ∀ ũb ∈ Ũ s b , ∃t ∈ [0,t b [ such that s(s, ũb ,t
) is in collision with a point of FOV c (t). Since s is located inside FOV, it takes a simple topological argument to realize that ∃t ′ < t such that s(s, ũb ,t ′ ) is in collision with a point of ∂ FOV(t ′ ). Accordingly s ∈ ICS b (∂ FOV) and the following holds:

s ∈ ICS b (∂ FOV ∪ FOV c ) ⇒ s ∈ ICS b (∂ FOV). ⊓ ⊔
In other words, it suffices to consider ∂ FOV in order to compute ICS b (B). As in (Martinez-Gomez and Fraichard 2008), when A is planar, it becomes possible to design ICS b -CHECK, i.e. an efficient version of Algorithm 1. In that case, a state s of A can be rewritten s = (x, y, ẑ) with (x, y) the workspace coordinates of A 's reference point, and ẑ the rest of the state parameters. The primary design principle behind ICS b -CHECK is to compute the ICS b set corresponding to a 2D slice of the state space S of A (instead of attempting to perform computation in the fully-dimensional state space), and then to check if s c belongs to this set. Assuming the state to be checked is s c = (x c , y c , ẑc ), the 2D slice considered is the ẑcslice and it is possible to define the ICS b set of the ẑc -slice considered that yields a collision with B i at a particular time t ∈ [0,t b [ for the braking trajectory ũb :

ICS b ẑc (B i , ũb ,t) = {s ∈ ẑc -slice| (6)
A ( s(s, ũb ,t)) ∩ B i (t) = / 0}

Likewise:

ICS b ẑc (B i , ũb ) = t∈[0,t b [ ICS b ẑc (B i , ũb ,t) (7)
Applying this 2D reasoning principle, ICS b -CHECK is similar to the general ICS b Checking Algorithm detailed in Algorithm 1 except that, at all steps of the algorithm, ICS b ẑc is computed instead of ICS b (see Algorithm 2). It is by keeping all computations in 2D (notwithstanding the actual dimensionality of S ) that it is possible to efficiently compute the ICS b set corresponding to a given ẑc -slice.

For the sake of brevity and because of the similarity between ICS b -CHECK and ICS-CHECK, the inner workings of ICS b -CHECK are not detailed here. The reader is referred to (Martinez-Gomez and Fraichard 2008) instead. Suffice to say that ICS b -CHECK provides an efficient way to check whether a given state is a ICS b or not.

Passively Safe Navigation

In order to demonstrate passive motion safety and to validate the Braking ICS concept, a navigation scheme (henceforth called PASSAVOID) has been developed for a mobile

PASSAVOID's Principle

PASSAVOID is a reactive navigation scheme that operates with a given time step δt. At each time step, its purpose is to compute the constant control u that will be applied to A during the next time step; u must be admissible, i.e. the corresponding state trajectory must be p-safe (in other words, it must be ICS b -free). PASSAVOID operates like most standard reactive collision avoidance schemes, e.g. [START_REF] Fox | The dynamic window approach to collision avoidance[END_REF][START_REF] Fiorini | Motion planning in dynamic environments using velocity obstacles[END_REF]. In all cases, their operating principle is to first characterize forbidden regions in a given control space and then select an admissible control, i.e. one which is not forbidden. Accordingly collision avoidance also depends on the ability of the collision avoidance scheme at hand to find such an admissible control. In the absence of a formal characterization of the forbidden regions, all schemes resort to some form of sampling of the control space with the inherent risk of missing the admissible regions. PASSAVOID also resorts to sampling in order to find an admissible control. However, in contrast with standard collision avoidance schemes, PASSAVOID is designed in such a way that it is guaranteed that an admissible control always exists and that it will be part of the sampling set.

The operating principle of PASSAVOID is illustrated in Fig. 6. Let s 0 denote the current state of A and U a sampled set of controls: U = {u 1 . . . u m }. A given control u j ∈ U is applied to A for a duration δt. It takes A from the state s 0 to the state s j = s(s 0 , u j , δt). If the state trajectory between s 0 and s j is p-safe then u j is admissible. Using the Sufficient Safety Condition established in [START_REF] Petti | Safe motion planning in dynamic environments[END_REF], the admissibility of u j can equivalently be verified by checking that (1) the state trajectory between s 0 and s j is collision-free (with respect to the conservative model of the future B i , i = 1 . . . n), and that (2) s j is p-safe, i.e. it is not a Braking ICS. This procedure is applied for every control in U; it yields a set of admissible controls denoted U * from which PASSAVOID can pick the control to apply during the next time step. This selection can be made arbitrarily if one is only concerned with the survival of A or it can be made so as to ensure convergence towards a given goal (using for instance a global navigation function, a potential field, or even a partial motion planning scheme).

Passive Motion Safety Guarantee

A scheme such as PASSAVOID works well as long as an admissible control can be found in U. But if, at the end of the day, U * is empty, it means that every control in U takes A to a Braking ICS. In other words, passive motion safety will not be achieved and a collision will take place while A is still moving. To address this issue, it is necessary to guarantee that U = {u 1 . . . u m } is never empty and always contains at least one admissible control. It is possible to achieve this by carefully designing PASSAVOID. To that end, a number of definitions and properties are required. They are introduced now. The concepts of δ -braking trajectory and δpassive safety are defined first.

Definition 3 (δ -Braking Trajectory) A braking trajectory ũ * ∈

Ũ s 0 b of duration t * is a δ -braking trajectory if it is constant over intervals of fixed duration δt.

A δ -braking trajectory is just a special type of braking trajectory (see Fig. 7). It yields a corresponding type of passive motion safety: Definition 4 (δ -Passive Safety) A state s 0 is δ -passively safe or δ -p-safe if it exists one δ -braking trajectory ũ * starting at s 0 which is collision-free until A has stopped. Then two useful properties are established:

Property 5 (P-Safe States)

If the state s 0 is p-safe and the braking trajectory ũb ∈ Ũ s 0 b starting at s 0 is collision-free until A has stopped then every state s(s 0 , ũb ,t), 0 < t ≤ t b is also p-safe.

Proof Suppose that ∃t i ∈]0,t b ] such that s(s 0 , ũb ,t i ) is not p-safe then, by definition, ∀ ũ j ∈ Ũ s i b , ũ j yields a collision before A stops. This also applies to the braking trajectory corresponding to the restriction of ũb to the time interval [t i ,t b ] which yields a contradiction.

⊓ ⊔

Note that Property 5 also applies to δ -p-safe states and δpassive safety.

Property 6 (δ -Passive Safety Guarantee) If the state s 0 is δ -p-safe then there exists at least one admissible control u * that can be used to drive A to a state which is also δ -p-safe.

Proof Since s 0 is δ -p-safe, there exists at least a one δbraking trajectory ũ * starting at s 0 which is collision-free until A has stopped. As per Property 5, the state s(s 0 , ũ * , δt) is δ -p-safe. Let u * denote the value of ũ * over the time interval [0, δt[, u * is an admissible control.

⊓ ⊔ Algorithm 3: PASSAVOID.

Input: s 0 , the current δ -p-safe state of A ; B i , i = 1 . . . n; δt, the time step. Property 6 is fundamental for the design of a version of PASSAVOID whose passive motion safety can be guar-anteed. PASSAVOID simply has to drive A from one δ -psafe state to the next. Now, assuming that s 0 is δ -p-safe, property 6 guarantees the existence of at least one admissible control u * which, if applied to A for the duration δt, will take it to another δ -p-safe state. In general, a δ -p-safe state s has more than one admissible control. Let K(s) denote this set of admissible controls, it is dubbed the kernel of K(s). Now, in order to guarantee its passive motion safety, PASSAVOID must include K(s 0 ) in its control space sampling set. This is precisely what PASSAVOID does (see Algorithm 3, line #2).

Output: u Sample U ❀ U = {u 1 . . . u m }; // Select
Algorithm 4: ICS b -CHECK + Kernel Computation.

Input: s c , the state to be checked; B i , i = 1 . . . n. Output: Boolean value; K(s c ), the kernel of s c .

Select E ⊂

Ũ s c b , a set of δ -braking trajectories for s c ; PASSAVOID features two important steps: computing the kernel K(s 0 ) (line #2) and checking whether the state s(δt) is δ -p-safe (line #6). It turns out that these two procedures are related and can be done by an adaptation of ICS b -CHECK which is detailed now: given that, by definition, a state which is not p-safe is a Braking ICS, ICS b -CHECK is used to check whether a given state is p-safe or not. To that end, ICS b -CHECK relies upon a selected set of braking trajectories. In a similar manner, ICS b -CHECK can be used to check whether a given state is δ -p-safe or not by considering δ -braking trajectories instead (line #1 of Algorithm 1).

1 K(s c ) = / 0; 2 forall ũ * ∈ E do 3 forall B i do 4 Compute ICS b ẑc (B i , ũ * ); 5 end 6 Compute ICS b ẑc (B, ũ * ) = n i=1 ICS b ẑc (B i , ũ * ); 7 if s c ∈ ICS b ẑc (B, ũ * ) then 8 K(s c ) = K(s c ) ∪ u * ; // s c is δ -p-
Besides, when ICS b -CHECK computes ICS b (B, ũb ) for a given braking trajectory ũb (line #3 of Algorithm 1), it is straightforward to determine if ũb is collision-free when starting from s c : it is the case if s c ∈ ICS b (B, ũb ). In that case, ũb is a candidate for K(s c ), the kernel of s c . Algorithm 4 is a version of ICS b modified so as (1) to check if its input state s c is δ -p-safe or not (line #1), and (2) to compute the kernel of s c (line #9). It is this version of ICS b -CHECK which is used inside PASSAVOID.

Provided that the initial state of the system A is δ -psafe, Property 6 allows PASSAVOID to have at its disposal at each time step an admissible control that can be used to drive A from one δ -p-safe state to the next (forever if need be). Concerning the assumption on the initial state being δp-safe, it is satisfied when A is at rest (see Section 4.2), and the null control is admissible. In other words, starting with A at rest, PASSAVOID has an admissible control readily available that can be used right away if the situation demands it (this is true even if δt is very small).

At the end of the day, PASSAVOID is provably passively safe in the sense that it is guaranteed that A will always stay away from Braking ICS no matter what happens in the environment.

Passively Safe Multi-Robot Navigation

In the introduction, it was stated that, if every moving object in a given environment was passively safe, i.e. stayed away from Braking ICS, then no collision should take place at all. It turns out that this property is straightforward to demonstrate.

Let A 1 and A 2 denote two robots that are driven by a provably passively safe navigation scheme such as PASSAVOID. As per Properties 5 and 6, both A 1 and A 2 are in a δ -p-safe state at all times. In other words, the following holds:

∀t, s 1 (t) ∈ ICS b 1 and s 2 (t) ∈ ICS b 2 (8)
where s i (t) and ICS b i respectively denote the state at time t and the corresponding Braking ICS set for robot A i , i = 1, 2.

Assuming that a collision can take place between A 1 and A 2 with one of them having a non zero velocity yields a contradiction. It cannot happen.

Simulation Results

To validate the Braking ICS concept and demonstrate its usefulness, ICS b -CHECK and PASSAVOID have both been implemented and tested in simulation on scenarios similar to that of Fig. 1.

Model of the Robot

The model of A is that of a standard car-like vehicle with two fixed rear wheels and two orientable front wheels. A state of A is a 5-tuple s = (x, y, θ , v, ξ ) with (x, y) the coordinates of the rear axle midpoint, θ the orientation of A , v the linear velocity of system, and ξ the orientation of the front wheels (steering angle). A control of A is a couple u = (u α , u ξ ) with u α the linear acceleration of the rear wheels and u ξ the steering angle velocity. Let L denote the wheelbase of A . The motion of A is governed by the following differential equations:

      ẋ ẏ θ v ξ       =       v cos θ v sin θ v tan ξ /L 0 0       +       0 0 0 1 0       u α +       0 0 0 0 1       u ξ (9) with |v| ≤ v max , |ξ | ≤ ξ max , |u α | ≤ u α max and |u ξ | ≤ u ξ max .
7.2 Workspace and Field-of-View Fig. 8: Test scenario: three fixed rectangles and two moving discs (with their future trajectories). The robot A is the disc at the center.

A typical test scenario is depicted in Fig. 8. The planar workspace W contains polygonal objects and disks that can be fixed or moving with a given maximum velocity. Assuming that A is equipped with an omnidirectional laser range finder mounted at the center of A , the field-of-view of A is depicted in Fig. 9. The circular arc corresponding to the maximum range of the range finder have been replaced by straight segments; this conservative simplification could easily be lifted.

ICS b -CHECK at Work

To briefly illustrate how ICS b -CHECK works, the scenario in Fig. 8 is used. In contrast with the worst case assumption made in Section 3.2, it is assumed here that the sensors can differentiate between the fixed and the moving objects and that the future motion of the observed moving objects is A set E of braking trajectories must be selected. They can be chosen arbitrarily since they always yield a conservative approximation of the ICS b set (as per Property 2). In this case, E comprised nine braking trajectories defined by a constant minimum linear deceleration u α = -u α max and a constant steering angle velocity |u ξ | ≤ u ξ max . These braking trajectories are depicted in Fig. 10. For a given braking trajectory ũb , a state corresponding to a pixel included in the colored region of the ẑc -slice is a Braking ICS for ũb . All the steps of ICS b -CHECK that involves computing unions and intersections of arbitrary shapes are performed very efficiently on this OpenGL buffer by taking advantage of the Red-Green-Blue color coding and the bitwise logical operators available; for additional details, the reader is referred to [START_REF] Martinez-Gomez | An Efficient and Generic 2D Inevitable Collision State-Checker[END_REF]. The final output of this process is illustrated in Figs. 12 and 13 where it appears that s c = (0, 0, -1, 20, 0) is not a ICS b : the color of the (0, 0) pixel in the ẑc -slice is not black.

PASSAVOID at Work

To illustrate how PASSAVOID works, two scenarios have been selected. The first one is called the 1D Compactor scenario, it is simple but it helps to understand the kind of behaviour that PASSAVOID will yield when A is confronted to a clearly identified dangerous situation. The second one is called the Blind Crowd scenario; its primary purpose is to illustrate the performances of PASSAVOID in complex situations. These two scenarios are presented in the next sections. The results obtained are also illustrated in a short film provided as a multimedia attachment to this paper7 .

In both cases, PASSAVOID had no information regarding the future trajectories of the moving objects. PASSAVOID did not attempt to drive A to a given goal. Its primary purpose was to keep A in p-safe states. Its secondary purpose was to keep A moving. In other words, the admissible control selection (line #10 of Algorithm 3) was biased towards controls yielding a non-zero linear velocity. This choice was made so as to avoid the straightforward answer to the passive motion safety problem which is simply to brake down and stop forever (by doing so, A reaches and stays in a p-safe state). The 1D Compactor scenario features one fixed object B f and one moving object B m . The moving object is moving towards the fixed object (see Fig. 14). B f and B m are like the two jaws of a compactor (hence the name of the scenario). A is placed between B f and B m and it is further assumed that A can only move along the vertical line connecting B f and B m . At the beginning, A is moving upward with a positive linear velocity. In such a situation, the initial state s 0 of A is clearly an ICS (no matter what A does it will end up being crushed by B m ). It is however possible to select A 's initial position and linear velocity such that s 0 is p-safe.

1D Compactor Scenario

The parameters for this scenario were set as follows: v max = 20m.s -1 (maximum velocity of A and B m ), u α max = 7m.s -2 . The radius of A and B m was 2.5m and the sensor range, i.e. the maximum radius of the field-of-view, was 80m. The control space sampling set U was obtained through a regular discretization of the control set [-u α max , u α max ]. The set of braking trajectories E used by ICS b -CHECK comprised one δ -braking trajectory defined by a constant minimum linear deceleration u α = -u α max .

In this scenario, when driven by PASSAVOID, A exhibits the following behaviour in order to always remain in p-safe states:

1. the increasing approach of B m forces A to gradually decrease its velocity until it stops. 2. A backs up in order to avoid collision with B m (recall that PASSAVOID is biased towards keeping A in motion). 3. while backing up, A gets closer to B f . At some point, it forces A to reduce its velocity. 4. A is now at rest next to B f , it will soon be hit by B m . 5. A is in collision with B m (t = 7s). 6. when the collision with B m is over8 , A resumes its upward motion.

The evolution of A 's velocity in this scenario is depicted in Fig. 15. As simple as it may appear, this scenario shows how PASSAVOID seeks to avoid collision with B m in a natural way (by braking down and shifting in reverse). However, when A is trapped, PASSAVOID guarantees that the robot will be at rest when the collision occurs.

Blind Crowd Scenario

The blind crowd scenario is more challenging. It features 22 moving objects moving arbitrarily in a 2D workspace. The objects are blind in the sense that their motion is unaffected by the other objects. The parameters for this scenario were set as follows: v max = 15m.s -1 (maximum velocity of A and of the moving objects), ξ max = π/3rad, u α max = 7m.s -2 , u ξ max = 1.54rad.s -1 .

Complexity and Performance

The computational time complexity of PASSAVOID grows linearly with n s , the size of the control space sampling set U (forall loop of Algorithm 3), and the complexity of one iteration depends primarily on the complexity of ICS b -CHECK (δ -p-safety test in line #6 of Algorithm 3).

Central to ICS b -CHECK is the computation of ICS b ẑc (B i , ũ * ) (line #5 of Algorithm 4). Assuming a temporally discrete model of the future (with a fixed time step ∆t), and thanks to the use of standard graphics rendering technique and GPU-based programming, this step can be done in time linear with n t = T h /∆t, the number of the time steps used to represent the model of the future. As illustrated in Section 7.3, the union and the intersection in lines #7 and #12 of Algorithm 4 are readily obtained as by-products of the computation of ICS b ẑc (B i , ũ * ) for every braking trajectory.

Concerning the overall complexity of ICS b -CHECK, it grows linearly with n b , the size of the set of braking trajectories and n o , the number of objects (forall loops of Algorithm 4). The final time complexity of PASSAVOID is O(n s n b n o n t ). The current implementation of both ICS b -CHECK and PASSAVOID has been done in C++ on an average laptop computer 9 . As expected, the running times observed for ICS b -CHECK depends on the values of n b , n o and n t . Table 1 gives the average running times of ICS b -CHECK wrt n 0 , the number of objects. These running times are encouraging and could further be improved thanks to code optimization 10 or the use of a more powerful desktop.

Conclusion and Future Work

This paper has addressed the problem of navigating in a provably safe manner a mobile robot with a limited fieldof-view placed in a unknown dynamic environment. Since absolute motion safety is impossible to guarantee in such a situation, the position taken in this paper was to settle for a weaker level of motion safety dubbed passive motion safety: it guarantees that, if a collision takes place, the robot will be at rest. It seemed a reasonable choice given the harsh constraints imposed by a limited field-of-view and the lack of information about the environment and its future evolution. As limited as it may appear, passive motion safety is interesting for two reasons: (1) it allows to provide at least one form of motion safety guarantee in the challenging scenarios considered, and (2) if every moving object in the environment enforces it then no collision will take place at all.

The primary contribution of this paper has been the concept of Braking ICS, i.e. a version of the ICS corresponding to passive motion safety. Passive motion safety can be obtained by avoiding Braking ICS at all times. It has been shown that Braking ICS verified properties that have allowed the design of an efficient Braking ICS-Checking algorithm. 9 Intel Core i7 1.6GHz CPU, 4GB RAM, ATI Mobility Radeon HD 4500 GPU.

10 A CUDA implementation is underway. -In certain situations, PASSAVOID may drive the robot to a collision state although such a collision could have been avoided. This is due to PASSAVOID's lack of foresight 11 and the fact that it is constrained to drive the robot from a ICS b -free state to another ICS b -free state. Besides, PASSAVOID is not concerned with driving the robot to a given goal. These issues could be addressed by turning PASSAVOID into a Partial Motion Planner, i.e. an interruptible motion planning scheme that strives to compute a trajectory towards a given goal and valid for the next k time steps, k being determined by the constraints imposed by the current situation [START_REF] Petti | Safe motion planning in dynamic environments[END_REF]. Such an extension would yield a navigation scheme better able to avoid collisions and to reach a given goal while retaining the passive motion safety guarantee. -In some applications, passive motion safety can be too limited; it could be interesting to explore more sophisticated levels of motion safety such as the passive friendly motion safety mentioned in [START_REF] Macek | Towards safe vehicle navigation in dynamic urban scenarios[END_REF]: it guarantees that, if a collision takes place, the robot will be at rest and the colliding object could have had the time to stop or avoid the collision (if it wanted to). Such a motion safety level assume that the moving objects have cognitive abilities and are not hostile (which happens to be true in many situations).

In general, it could be interesting to explore other forms of motion safety depending on the particulars of the navigation problem at hand.

Fig. 2 :

 2 Fig. 2: Field-of-view for the scenario of Fig. 1. FOV is the grey area; ∂ FOV and FOV c have two connected components.

Fig. 4 :

 4 Fig. 4: Conservative model of the future (partially represented for visualisation purposes) for the scenario of Fig. 1.

Fig. 5 :

 5 Fig. 5: Conservative model of the future: how FOV shrinks as time passes (for a time t 1 greater than the sensing time).

5

  Braking ICS CheckingPASSAVOID primarily relies upon ICS b -CHECK, an algorithm that checks whether a given state is a Braking ICS or not. ICS b -CHECK is the passively safe version of the ICS checking algorithm (called ICS-CHECK) presented in[START_REF] Martinez-Gomez | An Efficient and Generic 2D Inevitable Collision State-Checker[END_REF]. The passively safe version of ICS-CHECK can be designed because Properties 1 and 2 are verified for Braking ICS. The steps involved in checking whether a given state s c is a ICS b are given in Algorithm 1. Besides the state to be checked, the algorithm takes as input the model of the environment and the conservative space× model of the future (see §4.1). Steps 2, 3 and 4 are the direct translation of Property 1. Algorithm 1: General ICS b Checking Algorithm. Input: s c , the state to be checked; B i , i = 1 . . . n. Output: Boolean value. Select E ⊂ Ũ s c b , a set of braking trajectories for s c ; 1 Compute ICS b (B i , ũb ) for every B i and every ũb ∈ E ; 2 Compute ICS b (B, ũb ) = n i=1 ICS b (B i , ũb ) for every ũb ∈ E ; 3 Compute ICS b (B, E ) = ũb ∈E ICS b (B, ũb ); 4 if s c ∈ ICS b (B, E )

Fig. 6 :

 6 Fig. 6: PASSAVOID's operating principle (see text).

Fig. 7 :

 7 Fig. 7: Example of a δ -braking trajectory (1D case).

Fig. 9 :

 9 Fig. 9: Field-of-view FOV and its boundary ∂ FOV for the scenario of Fig. 8.

Fig. 10 :

 10 Fig. 10: E , the set of braking trajectories considered by ICS b -CHECK.

  Fig. 11: ICS b ẑc (B, ũb ) for different braking trajectories.

Fig. 12 :

 12 Fig. 12: Two dimensional ẑc -slice of the 5D state space of A : a region of a given color indicates that it is a ICS b for the corresponding braking trajectory. Black regions are ICS b .

Fig. 14 :

 14 Fig. 14: 1D compactor scenario.

Fig. 15 :

 15 Fig. 15: Velocity profile of A for the 1D compactor scenario.

Fig. 16 :

 16 Fig. 16: Blind crowd scenario: it features 22 moving objects with their future trajectories. The robot A is at the centre facing left.

Table 1 :

 1 Average running time of ICS b -CHECK wrt n o , the number of objects (n b = 9, n t = 71).

Fig. 17 :

 17 Fig. 17: Four snapshots of PASSAVOID at work in the blind crowd scenario (the black region represents the ICS b ). A is at rest in the bottom-left snapshot (a collision is imminent) and in collision in the bottom-right one.

  denotes the subset of W occupied by B i at a particular time t in the conservative model of the future. It is assumed that each B i (t) is a closed subset of W and that the total number of objects is n. Likewise B i ([t 1 ,t 2 ]) denote the space×time region occupied by the object during the interval [t 1 ,t 2 ].

Algorithm 2 :

 2 ICS b -CHECK. : s c , the state to be checked; B i , i = 1 . . . n.

		Output: Boolean value.
	1 2	Select E ⊂ forall ũb ∈ E do Ũ s c b , a set of braking trajectories for s c ;
	3	forall B i do
	4	Compute ICS b	ẑc	(B i , ũb );
	5	end
	6	Compute ICS b	ẑc	(B, ũb ) = n i=1 ICS b	ẑc	(B i , ũb );
	7	end
	8	Compute ICS b	ẑc	(B, E ) = ũb ∈E ICS b	ẑc	(B, ũb );
	9	if s c ∈ ICS b (B, E ) then
	10	return TRUE;
	11	else
		return FALSE;

Input12 end 13 robot A with a limited field-of-view placed in a unknown dynamic environment. PASSAVOID's primary task is to keep A in p-safe states, or equivalently, to drive A away from Braking ICS. PASSAVOID guarantees passive motion safety no matter what happens in the environment. In other words, if a collision takes place, it is guaranteed that A will be at rest when it occurs. PASSAVOID relies upon ICS b -CHECK to operate.

Aka Obstacle Shadow[START_REF] Reif | Motion planning in the presence of moving obstacles[END_REF] or Region of Inevitable Collision (LaValle and Kuffner 1999).

4 I.e. how far into the future the reasoning is done.

Accordingly, every object that is observed is treated as a moving object.

Through a priori knowledge or communication for instance.

Downloadable from http://emotion.inrialpes.fr/fraichard/films/11auro-passavoid.wmv.

Assuming that B m sort of passes through A .

PASSAVOID is purely reactive, its sole purpose is to compute the control to apply for the next time step.