2019
A Formal Safety Net for Waypoint-Following in Ground Robots
RA-L 2019
We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for two-dimensional waypoint-following of Dubins-type ground robots with tolerances and acceleration. First, we model a robot in differential dynamic logic and specify assumptions on the contro