Formal verification of robotics navigation algorithms

BUGs algorithms are navigation algorithms that have been designed to seek of a target in a plane that contains obstacles. Many new navigation algorithms have been inspired from them and their applications can be found in autonomous mobile robots, e.g., self driving vehicles. These algorithms are inspired from insects and are comparable to the motion of ants, which yields motion strategies for the robot that guarantees the elusive target will be detected, if such strategies exist. However, these algorithms have not been formally verified using existing formal verification tools. Therefore, the aim of this paper is to apply model checking for verifying the correctness of BUGs algorithms and draw conclusions for future uses of formal methods in the design and model checking of navigation algorithms.