2021 Fiscal Year Research-status Report
Practical Framework for the Formal Verification of Cooperative Mobile Robots Algorithms
| Project/Area Number |
21K11748
|
|---|
| 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
|
| Keywords | 自律分散ロボット群 / モデル検証 / 分散アルゴリズム / 自己安定 |
|---|
| 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 been able to extend the verification model by proving some important theorems that allow us to extend the model to verify additional properties of self-stabilization.
In addition, we have also used the model to develop algorithm synthesis. In short, this is a program which, given the description of a model (type of lights, number of colors, level of synchrony), will generate all possible algorithms, filter them to keep only those that are viable, and use the model-checker to find if they are correct. As long as the number of algorithms that remain after the filtering is not too high (about 100,000 or less), the exhaustive search is feasible.
|
| 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 several important theorems allowing us to generalize our verification model to variants of self-stabilization. We are preparing these results in a manuscript for a journal extension of our SRDS 2020 paper.
We have developed a synthesis program for rendezvous with lights. Given a description of the model (number of colors, type of lights, synchrony model) the program generates all possible algorithms, filters algorithms to retain those that are viable, and verify each of them in the model checker. Our preliminary results allow us to confirm results known in the literature, as well as find new algorithms and study new cases that were not known before. We are in the process of writing a manuscript to present at an international conference. 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.
|
| Strategy for Future Research Activity |
Our plans consist first in extending the work on synthesis. One of the key aspect of this work is to find proper filtering rules that allow to bring down the number of viable algorithms in a model to a number that is tractable. For instance, in the "simple" case of so-called "class L" algorithms in a system of 7 external colors, there is a total of 1,801,088,541 possible algorithms, but this number can be reduced to 75,600 algorithm with proper filtering, which only takes several hours for an exhaustive verification.
Our other plans are to design a second model with the opposite bias of our current verification model. In other words, if an algorithm A fails in the second model then A fails in the real-world but, even if A succeeds in the second model, it is still possible that it fails in the real-world.
Lastly, we plan to extend our method to study new problems. In particular, we want to address a problem involving more robots.
|
| Causes of Carryover |
Due to the covid-19 situation, all travel plans had to be postponed to the next year.
|
| Remarks |
The two URL above point to the github repositories related to this project. At the time of writing, these repositories are private. They will both be opened after publication of the relevant results.
|
