发表机构
Texas Robotics; Walker Department of Mechanical Engineering, The University of Texas at Austin（得克萨斯机器人研究所; 得克萨斯大学奥斯汀分校沃克机械工程系）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出基于持久分类建模的组合框架，将机器人系统形式化为抽象电路，通过SMT求解器实现硬件软件行为的同步合成，经搜救场景验证可恢复机器人运行，并开源了相关求解器与软件。
AI 中文摘要
传统机器人系统以静态配置设计和部署，设计阶段的假设在运行时成为不可变约束。这种“先设计后部署”的范式在狭窄操作条件下能生成高性能系统，但当机器人自身、任务或环境属性意外变化时，会导致机器人脆弱性。本文提出一种组合框架，将机器人系统形式化为严格对称幺半群范畴内的抽象电路，其中硬件、软件与行为的设计及运行时组合通过基于SMT的求解器同步合成；幺半群函子将系统投影到生命周期特定视图，自由符号变量同时求解更大组合内的参数与整个组件规格。该持久模型还支持长寿命系统在整个生命周期内超出规划存在性的查询，包括绘制候选组合的帕累托前沿、诊断组合不可行原因、找到最小恢复方案、以最小变更重新配置已部署系统。我们在已部署机器人上实测最优数值规划器、基于流的规划器及基于SMT的规划器的官方实现，在搜救场景中验证了该方法的端到端能力：机器人识别自身不适用后，合成并采用全新整体配置恢复运行。我们将该求解器及配套软件开源。
英文摘要
Robotic systems are traditionally designed and deployed in static configurations, with assumptions made at design-time becoming immutable constraints during runtime. This design-then-deploy paradigm produces performant systems under narrow operating conditions, but renders robots brittle when qualities of themselves, their tasks, or their environments unexpectedly change. We address this challenge with a compositional framework that formalizes robotic systems as abstract circuits within a strict symmetric monoidal category, in which design and runtime composition of hardware, software, and behavior are synthesized simultaneously via an SMT-based solver, with monoidal functors projecting the system into lifecycle-specific views and free symbolic variables simultaneously solving for parameters and entire component specifications within larger compositions. This persistent model also supports queries a long-lived system needs beyond plan existence across its entire lifecycle, including mapping Pareto fronts over candidate compositions, diagnosing why a composition has become infeasible, finding its minimal restoration, and reconfiguring with limited change to the deployed system. We evaluate against official implementations of optimal numeric, stream-based, and SMT-based planners all measured onboard a deployed robot and demonstrate the approach end-to-end in a search-and-rescue scenario in which the robot recognizes when it has become unfit and synthesizes and assumes new holistic configurations to restore operation. We release our solver and supporting software open-source.
