移动机器人算法综合：以环上聚集为例

分布式计算的最新进展突出了自主移动机器人群体的模型和算法，这些机器人能够自组织并协作以实现全局目标。迄今为止，绝大多数工作都考虑手工设计的算法和正确性证明。本文首次提出了一个形式化框架，用于自动设计专用于在离散空间中演化的自主移动机器人的分布式算法。作为案例研究，我们考虑了将所有机器人聚集到某个事先未知的特定位置的问题。我们的贡献有三方面。首先，我们将聚集问题编码为一个可达性博弈。然后，我们自动生成了一个针对在固定大小均匀环上演化的三个机器人的最优分布式算法。最后，我们通过归纳证明，生成的算法对于任何环大小也是正确的，除非存在不可能性结果（即当机器人数量整除环大小时）。