| 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 – 2025-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| 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 progressed on algorithm synthesis; that is, given a model, automatically generate correct algorithms for that model if they exist. The main challenge consists in finding appropriate rules to considerably reduce the search space. This year we found rules that allowed us to tackle model of the classical models. In addition, we have completed the journal publication of the model-checker started last year, and we have also looked at related robot problems in the hope of finding opportunities to adapt our models; a task that remains elusive at this point.
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
During this year, Defago was involved as PC chair for the IEEE/IFIP conference DSN 2023. Then, Wada and Defago were both acting as general chair for organizing the conference OPODIS 2023. Due to these activities, our research has not progressed as quickly as anticipated and we have faced some delays as a result.
|
| Strategy for Future Research Activity |
We are currently trying to push the limits in order to find via synthesis algorithms for previously unknown cases. This still requires significant work prior to submitting the work on algorithm synthesis to a top-rated journal. This is our main goal during this last research year. Upon publication of the results, the source code of the synthesis algorithm will also be published as open source.
|
