Provably safe navigation for mobile robots with limited field-of-views in dynamic environments

This paper addresses the problem of navigating in a provably safe manner a mobile robot with a limited field-of-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.