Method and system for formally analyzing the motion planning of a robotic arm based on conformal geometric algebra

A system for formally analyzing a motion planning of a robotic arm based on conformal geometric algebra, the system comprising a computing system comprising a processor configured to:

• determine specific structural parameters and motion planning parameters of a robot;
• establish a corresponding geometric model for basic components and motion planning constraints of the robot according to the specific structural parameters and the motion planning parameters based on a conformal geometric algebra theory, wherein the established geometric model is described in a higher-order logic language;
• establish a logical model of geometric relations involved in the motion process of the robot, configured for performing formal modeling for a motion process of the robot based on the established geometric model, to obtain a logical model of geometric relations involved in the motion process of the robot;
• obtain a motion logic relationship corresponding to a constraint or attribute of a motion process to be verified of the robot, using the logical model of geometric relations;
• verify whether the motion logic relationship is correct;
• when the motion logic relationship is correct, this indicates that the logical model of geometric relations meets the constraint of the motion process to be verified or has an attribute of the motion process to be verified, or when the motion logic relationship is not correct, this indicates that the logical model of geometric relations does not meet the constraint of the motion process to be verified or does not have the attribute of the motion process to be verified;
• and
• update the motion planning of a robotic arm when the motion logic relationship is not correct.

An electronic device comprising:

• a processor, a memory, a communication interface, and a bus,
• wherein the processor, the memory, and the communication interface are connected and communicate with each other through the bus,
• the memory stores an executable program code,
• the processor executes a program corresponding to the executable program code by reading the executable program code stored in the memory, to perform the method for formally analyzing the motion planning of a robotic arm based on conformal geometric algebra, comprising:
• determining specific structural parameters and motion planning parameters of a robot;
• establishing a corresponding geometric model for basic components and motion planning constraints of the robot according to the specific structural parameters and the motion planning parameters based on a conformal geometric algebra theory, wherein the established geometric model is described in a higher-order logic language;
• performing formal modeling for a motion process of the robot based on the established geometric model, to obtain a logical model of geometric relations involved in the motion process of the robot;
• obtaining a motion logic relationship corresponding to a constraint or attribute of a motion process to be verified of the robot, using the logical model of geometric relations;
• verifying whether the motion logic relationship is correct;
• when the motion logic relationship is correct, this indicates that the logical model of geometric relations meets the constraint of the motion process to be verified or has an attribute of the motion process to be verified, or when the motion logic relationship is not correct, this indicates that the logical model of geometric relations does not meet the constraint of the motion process to be verified or does not have the attribute of the motion process to be verified;
• and
• updating the motion planning of a robotic arm when the motion logic relationship is not correct.