Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space
Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space
复制标题
使用模型检查正式验证欧几里得空间中带灯机器人的交会算法
DOI：
10.1016/j.robot.2023.104378
复制
发表时间：
2023
影响因子：
4.3
通讯作者：
Wada Koichi
中科院分区：
文献类型：
--
作者：
Defago Xavier;Heriban Adam;Tixeuil Sebastien;Wada Koichi
本文详细介绍了首次使用模型检测技术来验证连续环境中机器人演化的分布式算法的正确性的成功尝试。研究了两个有光机器人的交会问题，在不同的同步模型(如FSYNC、SSYNC、ASYNC)中，存在许多不同的交会算法，目的是寻找求解交会所需的最少颜色数。虽然这些交会算法通常非常简单，但它们的分析和正确性证明往往非常复杂、繁琐和容易出错，因为不可能结果是基于机器人激活计划之间的微妙交互。特别是，我们解释了允许保持搜索空间有限和易处理的微妙设计决策，以及证明了支持它们的几个重要定理。作为有效性检验，我们使用该模型在六种不同的同步模型中验证了几种已知的会合算法。在每种情况下，我们发现从模型检查器获得的结果与文献中已知的结果是一致的。在开发和证明模型有效性的过程中，我们确定了几个基本定理，包括选择合适的算法和ASYNC调度器在不经意的移动机器人系统中产生新的内存特性的能力，以及为什么执行采集算法的机器人配备灯时不是问题。
The paper details the first successful attempt at using model checking techniques to verify the correctness of distributed algorithms for robots evolving in acontinuousenvironment. The study focuses on the problem of rendezvous of two robots with lights.There exist many different rendezvous algorithms that aim at finding the minimal number of colors needed to solve rendezvous in various synchrony models (e.g., FSYNC, SSYNC, ASYNC). While these rendezvous algorithms are typically very simple, their analysis and proof of correctness tend to be extremely complex, tedious, and error-prone as impossibility results are based on subtle interactions between the activation schedules of the robots.The paper presents a generic verification model that can be concretely expressed in available software model-checkers. In particular, we explain the subtle design decisions that allow to keep the search space finite and tractable, as well as prove several important theorems that support them. As a sanity check, we use the model to verify several known rendezvous algorithms in six different models of synchrony. In each case, we find that the results obtained from the model checker are consistent with the results known in the literature. The model checker outputs a counter-example execution in every case that is known to fail.In the course of developing and proving the validity of the model, we identified several fundamental theorems, including the ability for a well chosen algorithm and ASYNC scheduler to produce an emerging property of memory in a system of oblivious mobile robots, and why it is not a problem when robots executing the gathering algorithms are equipped with lights.