为机器人集体设计可验证的鲁棒控制器，解决任务重复与环境不确定问题。
Synthesising Robust Controllers for Robot Collectives with Recurrent Tasks: A Case Study
- 将多智能体博弈简化为部分可观测马尔可夫决策过程（POMDP），用部分观测建模环境不确定性。
- 在真实场景中实现电池驱动清洁机器人的规模化控制，满足能耗、任务重复和安全约束。
- 适用于需要长期运行、资源受限的自主机器人系统，如公共建筑清洁场景。
在设计自主机器人集体的正确性保障控制器时，面临任务定义、建模及实际规模应用三大挑战。本文聚焦于一种简洁但实用的高层控制器合成抽象，适用于具有优化目标（如最大清洁度、最低能耗）和重复性任务（如重新污染、充电阈值）以及安全性约束（如避免完全放电、互斥区域占用）的机器人集体。由于技术限制（如可扩展性及约束在合成中的使用），我们将基于图的随机双人博弈简化为部分可观测马尔可夫决策过程（POMDP）的单人博弈。通过部分可观测性编码对环境不确定性的鲁棒性。线性时序正确性性质在合成POMDP策略后独立验证。我们提供了针对任务型机器人集体的可扩展POMDP建模与控制器合成指导，以电池驱动机器人负责公共建筑清洁并受使用约束的场景为例。
原文摘要 · Abstract (English)
When designing correct-by-construction controllers for autonomous collectives, three key challenges are the task specification, the modelling, and its use at practical scale. In this paper, we focus on a simple yet useful abstraction for high-level controller synthesis for robot collectives with optimisation goals (e.g., maximum cleanliness, minimum energy consumption) and recurrence (e.g., re-establish contamination and charge thresholds) and safety (e.g., avoid full discharge, mutually exclusive room occupation) constraints. Due to technical limitations (related to scalability and using constraints in the synthesis), we simplify our graph-based setting from a stochastic two-player game into a single-player game on a partially observable Markov decision process (POMDP). Robustness against environmental uncertainty is encoded via partial observability. Linear-time correctness properties are verified separately after synthesising the POMDP strategy. We contribute at-scale guidance on POMDP modelling and controller synthesis for tasked robot collectives exemplified by the scenario of battery-driven robots responsible for cleaning public buildings with utilisation constraints.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。