Practical Framework for the Formal Verification of Cooperative Mobile Robots Algorithms

协作移动机器人算法形式化验证的实用框架

• 批准号: 21K11748
• 负责人: DEFAGO Xavier
• 金额: $ 2.58万
• 依托单位: Tokyo Institute of Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 2021
• 资助国家: 日本
• 起止时间: 2021-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-21K11748/
• 关键词: 自律分散ロボット群; モデル検証; 分散アルゴリズム; 自己安定

The project aims at applying model checking to automatically verify the correctness of multi-robot algorithms and the problem of rendezvous in particular. Based on several important theorems that we have proved, we have developed a verification model that allows us to automatically verify the correctness of a given rendezvous algorithm in a model-checker (SPIN). Our model is designed to be conservative in the sense that, if an algorithm A passes the verification in the model, then this algorithm is correct in the real-world but the reverse is not true (A could be correct in the real-world even if it fails in the model).During this year, we have further extended the verification model with support for several consistency models and found novel algorithms that can work in these models. We have published the results as a journal version and made the model publicly available under an open-source license.In addition, we have progressed on the front of algorithm synthesis. In short, given a system model, we generate all possible algorithms, reduce the search space with several filtering rules to keep only those that are viable, and check each remaining algorithm with the model checker. This allows us to find known algorithms as well as new ones in models that are solvable, and partially map the known models for the existence of algorithms.Our model does not allow to prove the non-existence: when an algorithm is found it is guaranteed to be correct, but some correct algorithm can possibly be evaluated as incorrect.

该项目旨在应用模型检查以自动验证多机器人算法的正确性和尤其是Rendezvous的问题。基于我们已经证明的几个重要定理，我们开发了一个验证模型，该模型使我们能够自动验证模型检查器中给定的会合算法的正确性（spin）。 Our model is designed to be conservative in the sense that, if an algorithm A passes the verification in the model, then this algorithm is correct in the real-world but the reverse is not true (A could be correct in the real-world even if it fails in the model).During this year, we have further extended the verification model with support for several consistency models and found novel algorithms that can work in these models.我们已将结果作为期刊版本发布，并根据开源许可证公开获得该模型。此外，我们在算法合成的前面进步。简而言之，给定系统模型，我们生成所有可能的算法，使用几个过滤规则减少搜索空间以保持可行的规则，并使用模型检查器检查每个剩余的算法。这使我们能够在可求解的模型中找到已知的算法以及新算法，并部分映射了存在算法的已知模型。

项目成果

Solving Simultaneous Target Assignment and Path Planning Efficiently with Time-Independent Execution

• DOI: 10.1609/icaps.v32i1.19810
• 发表时间: 2021-09
• 期刊: Artif. Intell.
• 作者: Keisuke Okumura;Xavier D'efago

Verification model (public github repository)

验证模型（公共github仓库）

Using model checking to formally verify rendezvous algorithms for robots with lights in Euclidean space

使用模型检查正式验证欧几里得空间中带灯机器人的交会算法

• DOI: 10.1016/j.robot.2023.104378
• 发表时间: 2023
• 期刊: Robotics and Autonomous Systems
• 影响因子: 4.3
• 作者: Defago Xavier;Heriban Adam;Tixeuil Sebastien;Wada Koichi
• 通讯作者: Wada Koichi

Algorithm synthesis (private github repository)

算法综合（私人github仓库）

Offline Time-Independent Multi-agent Path Planning

离线时间无关的多智能体路径规划

• DOI: 10.24963/ijcai.2022/645
• 发表时间: 2022
• 期刊: 31st International Conference on Artificial Intelligence (IJCAI)
• 作者: K. Okumura;F. Bonnet;Y. Tamura;X. Defago
• 通讯作者: X. Defago