发表机构
Christopher Newport University（克里斯托弗纽波特大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一个开源流水线，用于合成和审计ROS 2 FlexBE机器人监督器，通过编码、活性假设和审计确保可部署性，实验表明枚举编码与系统目标活性更优。
AI 中文摘要
高层机器人监督器协调各项能力，其报告的结果决定机器人的下一步行动。反应式合成可以生成具有形式化保证的此类监督器，但部署所需的不仅仅是证明广义反应性(1)（GR(1)）规范可实现。设计者必须对易失效的能力进行编码，选择与重试意图匹配的活性假设，审计策略，并将其转化为机器人软件。我们提出了一个用于机器人操作系统（ROS）2灵活行为引擎（FlexBE）监督器的开源流水线，该流水线生成基于能力的GR(1)规范，在合成前分析假设，审计策略，通过行为保持证明减少状态，并生成可执行的状态机。在四个案例研究（六次比较）中，包括在两个四旋翼平台上的硬件实验，我们比较了枚举编码和独热编码以及两种活性公式。在测试的后端下，枚举编码通常合成更快，尽管更少的命题并不能可靠地预测更小的控制器或更低的符号成本。无待处理内存的系统目标（System-Goal）是唯一被确认在两种编码下都能在报告的网格上产生可执行控制器的活性处理方式；公平结果（Fair-Outcome）可能允许可实现循环而无需设计者意图的完成。对于该后端和模型，我们建议使用枚举编码和系统目标（System-Goal），并审计每个实现的策略，因为命题数量和可实现性并不衡量可部署性。审计器对四类结构缺陷（协议违规、死锁、有界失效违规、目标不可达陷阱）是完备且健全的，但不是通用的活性验证器，并且约简保持了能力级行为。这些阶段共同缩小了形式化可实现性与通过协议和结构进展检查的控制器之间的差距。
英文摘要
High-level robotic supervisors coordinate capabilities whose reported outcomes determine the robot's next action. Reactive synthesis can generate such supervisors with formal guarantees, but deployment requires more than proving a Generalized Reactivity (1) (GR(1)) specification realizable. Designers must encode failure-prone capabilities, choose liveness assumptions that match retry intent, audit strategies, and translate them into robot software. We present an open-source pipeline for Robot Operating System (ROS) 2 Flexible Behavior Engine (FlexBE) supervisors that generates capability-based GR(1) specifications, analyzes assumptions before synthesis, audits strategies, reduces states with a behavior-preservation proof, and emits executable state machines. Across four case studies (six comparisons), including hardware on two quadcopter platforms, we compare enumerated and one-hot encodings and two liveness formulations. Under the tested backend, enumerated encoding usually synthesizes faster, although fewer propositions do not reliably predict smaller controllers or lower symbolic cost. System-Goal without pending memory is the only liveness treatment confirmed to yield executable controllers under both encodings across the reported grid; Fair-Outcome can permit realizable cycles without designer-intended completion. For this backend and model, we recommend enumerated encoding with System-Goal and auditing every realized strategy, since proposition count and realizability do not measure deployability. The auditor is sound and complete for four structural defect classes (protocol violations, deadlocks, bounded-failure violations, goal-unreachable traps) but is not a general liveness verifier, and the reduction preserves capability-level behavior. Together, these stages narrow the gap between formal realizability and controllers that pass protocol and structural-progress checks.
Comments88 pages, 14 figures. Includes detailed technical appendices and experimental results for four application domains
