Abstract:In order to cope with the demands of more complex tasks, the development of modern robotics industry becomes rapidly. Considering the flexibility, compliance, and intelligence required for coordinated work, multi-arm/multi-robots give full play to the powerful role of robots and become an important research hotspot in the modern robotics industry. In the coordinated operation of the two arms of the robot, collisions between the robot arms and external obstacles are prone to occur, which may cause property damage and even casualties. In this study, a formal verification of the robot collision detection method is carried out. Based on the formal model of sphere and capsule, the shortest distance model of the robot geometric units and the robotic collision model are established. Meanwhile, its related attributes and the collision conditions have been formally verified. Based on the above content, the basic theorem library of robot collision detection has been successfully established, which provides technical support and method reference for further realizing the reliability and stability verification of the collision detection algorithm of the multi-machine system.