对机器人碰撞检测方法进行形式化验证, 以球体和胶囊体形式化模型为基础, 构建基本几何体单元之间最短距离和机器人碰撞的高阶逻辑模型, 证明其相关属性及碰撞条件, 建立机器人碰撞检测方法基础定理库, 为多机系统碰撞检测算法可靠性与稳定性的验证提供技术支撑和验证框架...随后, 梁孟德[15]提出了以球体和胶囊体表示的机器人关节和连杆的空间机器臂碰撞检测方法....针对各类几何体模型间最短距离问题, 在不同假设条件下, 将最短距离模型高阶逻辑建模及其相关性质证明分为球体与球体之间最短距离、球体与胶囊体之间最短距离、胶囊体与胶囊体之间最短距离这3类情况进行处理; 然后...具体如图 2所示.图片图 2 胶囊体在图 2中, sp和ep分别表示胶囊体两端的端点, c1和c2分别表示胶囊体中心线两端的端点, u表示从端点sp到端点ep的向量, r表示胶囊体中心线上对应球体的半径...由于胶囊体是由中心线上移动球体内的所有点组成的集合, 所以胶囊体的相关性质都与球体和中心线相关. 因此, 这里我们只简单介绍部分中心线的相关性质.通过分析中心线定义可知, 中心线的两端必在中心线上.