An Assume-Guarantee Framework for Multiple-Obstacle Collision Avoidanc

In this paper, an assume-guarantee reasoning approach is developed for obstacle avoidance in unmanned aerial vehicles (UAVs) in the presence of multiple obstacles in an obstacle field. This construct assumes certain properties of the environment and the vehicle to guarantee the safety and performance of the UAV (in this case, executing safe collision-avoidance trajectories). In the presence of a single obstacle, the assumptions on the environment and the vehicle parameters are constructed such that the UAV can plan a safe trajectory once the obstacle is detected. The approach to guaranteeing safety in the presence of multiple obstacles requires enforcing additional assumptions which is done by constructing a region of influence (RoI) around each obstacle, whose size depends on the environment and the vehicle parameters. The safe combinations of these parameters (codified as contracts) are developed such that the RoIs in the obstacle field do not intersect. The aforementioned approach is then used to decompose the general multiple-obstacle avoidance problem into a sequential single-obstacle avoidance problem by constructing an induction-based algorithm framework. The proposed methodology is validated by an illustrative example with minimum obstacle detection range, maximum allowed cruise velocity, maximum allowable agility as vehicle properties; and maximum obstacle size and minimum obstacle separation as environmental properties. Contract generation for specific scenarios and implementation of sequential avoidance on a 6-DoF quadcopter simulation are demonstrated. Finally, the effect of tracking error on the contract-based framework is discussed, along with a mechanism to incorporate this source of uncertainty into the contract.