Practical Framework for the Formal Verification of Cooperative Mobile Robots Algorithms
| Project/Area Number |
21K11748
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60010:Theory of informatics-related
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
DEFAGO Xavier 東京工業大学, 情報理工学院, 教授 (70333557)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
和田 幸一 法政大学, 理工学部, 教授 (90167198)
田村 康将 東京工業大学, 情報理工学院, 助教 (50773701)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2022: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2021: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | 自律分散ロボット群 / モデル検証 / 分散アルゴリズム / 自己安定 |
|---|
| Outline of Research at the Start |
本研究は，形式手法 (モデル検査) の適用によって，自律分散ロボット群アルゴリズムに対する実用的な正統性検証の枠組みを与えることを目的とする．
モデル検査法はしらみつぶし探索を自動化するものであり，与えられた証明の正しさに対して十分な説得力を与える．具体的には本研究の貢献は以下のとおりである．
・ロボットの集合問題に対するアルゴリズムの正しさの検証法を与える．
・それ以外の問題にも適用可能で十分に一般性のあるモデル検証法の枠組みを開発する．
・検証モデルにより，アルゴリズム合成を自動化にする．
|
| Outline of Annual Research Achievements |
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.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
We have proved considerably solidified our results on the verification model and the variants of self-stabilization and, after several rounds of review, published the results in a journal paper (Robotics and Autonomous Systems; https://doi.org/10.1016/j.robot.2023.104378) to appear in May 2023. In addition, the verification has been released publicly under the MIT license (https://github.com/xdefago/spin-light) in June 2022.
We have presented the results on synthesis and developed further results at a workshop in 2022 (http://sbrinz.di.unipi.it/peppe/MAC2022/MAC2022.html). The synthesis program, written in Promela and Rust, is in a github repository (https://github.com/xdefago/synth-lights) currently private but that will be made public after our results have been accepted for publication. Since last year, the program has been extended for parallel execution and more aggressive filters.
|
| Strategy for Future Research Activity |
Our short term plan is to complete the manuscript on synthesis for publication. The core of the investigation work on the problem of rendezvous is now essentially done. We have now begun to investigate additional models and apply the method to other problems.
|
Report
(2 results)
Research Products
(16 results)
