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.

该项目旨在应用模型检测来自动验证多机器人算法的正确性，特别是交会问题。基于我们已经证明的几个重要定理，我们开发了一个验证模型，该模型允许我们在模型检验器(SPIN)中自动验证给定会合算法的正确性。我们的模型被设计成保守的，如果一个算法A在模型中通过了验证，那么这个算法在现实世界中是正确的，但反之亦然(A在现实世界中可能是正确的，即使它在模型中失败了)。在这一年里，我们进一步扩展了验证模型，支持几个一致性模型，并发现了可以在这些模型中工作的新算法。我们已经将结果作为期刊版本发表，并在开放源码许可下公开提供该模型。此外，我们在算法合成方面取得了进展。简而言之，给定一个系统模型，我们生成所有可能的算法，用几个过滤规则来减少搜索空间，只保留那些可行的，并用模型检查器检查剩下的每个算法。这允许我们在可解的模型中找到已知算法以及新算法，并部分映射已知模型以确定算法的存在。我们的模型不允许证明算法的不存在：当发现算法时，保证该算法是正确的，但某些正确的算法可能被评估为不正确。

项目成果

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