发表机构
Mohamed bin Zayed University of Artificial Intelligence (MBZUAI); Technical University of Munich; Ludwig Maximilian University of Munich; New York University Abu Dhabi（穆罕默德·本·扎耶德人工智能大学（MBZUAI）; 慕尼黑工业大学; 慕尼黑大学; 纽约大学阿布扎比分校）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出CSymPlan框架，通过离线预计算可验证策略与在线运行时循环，使高自由度机械臂完成可达-规避任务时零安全违规，无验证动作时安全处理。
AI 中文摘要
机器人机械臂通常围绕解耦的运动生成栈进行设计：规划器计算无碰撞路径，底层控制器跟踪该参考轨迹。这种分离在计算上较为便利，但会产生难以在执行器极限、跟踪误差、模型失配及小障碍物间隙下执行的参考轨迹。本文提出CSymPlan，这是面向高自由度机械臂的可验证符号规划与控制框架，包含两种互补实现：离线实现针对已知工作空间预计算可验证的可达-规避反馈策略；在线实现利用并行化，根据动态任务与感知信息在运行时合成或更新符号策略。离线实现通过反馈线性化将机械臂动力学简化为操作空间中采样的扰动双积分模型，将力矩实现误差、建模不准确性及测量不确定性视为有界扰动，并通过量化-查找-力矩实现流水线将合成的符号策略细化到Franka FR3机械臂。在线实现采用相同的抽象与细化接口，将预计算的策略表替换为运行时pFaces请求-合成-执行循环。在随机模拟基准测试及感知驱动的Franka FR3实验中，两种实现均以零安全违规完成可达-规避任务；当不存在可验证动作时，机器人会保持、重规划或安全停止，而非执行未经验证的指令。
英文摘要
Robot manipulators are commonly engineered around a decoupled motion-generation stack: a planner computes a collision-free path and a lower-level controller tracks the resulting reference. This separation is computationally convenient, but it can produce references that are difficult to execute under actuator limits, tracking error, model mismatch, and small obstacle clearances. We present CSymPlan, a certified symbolic planning and control framework for high-DOF manipulators with two complementary implementations: an offline implementation that precomputes certified reach-avoid feedback policies for known workspaces; and an online implementation that synthesizes or updates symbolic policies at runtime from changing task and perception information using parallelization. The offline implementation reduces the manipulator dynamics to a sampled perturbed double-integrator model in operational space through feedback linearization, treats torque-realization errors, modeling inaccuracies, and measurement uncertainty as bounded disturbances, and refines the synthesized symbolic policy to the Franka FR3 through a quantization--lookup--torque realization pipeline. The online implementation uses the same abstraction and refinement interface, but replaces the precomputed policy table with a runtime pFaces request--synthesis--execution loop. In randomized simulated benchmarks and perception-driven Franka FR3 experiments, both implementations complete reach-avoid tasks with zero safety violations; whenever no certified action exists, the robot holds, replans, or stops safely instead of executing an uncertified command.
