Formal Proofs for Trajectory Computation in the Plane with Straight Obstacles

Speaker: Yves Bertot, INRIA Antipolis

Tuesday, 4 July 2023, 9:20, 1Z14

Our goal is to describe smooth trajectories for robots, so that these robots don't have to stop to change direction. Several formats of trajectories could be used, but we decided to focus on trajectories given by Bézier curves. It happens that these curves have mathematical properties that make it easy to verify formally that there are no collisions. Work in collaboration with Quentin Vermande (ENS, Paris) and Reynald Affeldt (AIST, Tokyo, Japan).