• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

自律分散ロボットアルゴリズムの形式的検証に対する実用的な枠組み

研究課題

研究課題/領域番号 21K11748
研究種目

基盤研究(C)

配分区分基金
応募区分一般
審査区分 小区分60010:情報学基礎論関連
研究機関東京工業大学

研究代表者

DEFAGO Xavier  東京工業大学, 情報理工学院, 教授 (70333557)

研究分担者 和田 幸一  法政大学, 理工学部, 教授 (90167198)
田村 康将  東京工業大学, 情報理工学院, 特定助教 (50773701)
研究期間 (年度) 2021-04-01 – 2025-03-31
研究課題ステータス 交付 (2023年度)
配分額 *注記
4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2023年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
2022年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2021年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
キーワード自律分散ロボット群 / モデル検証 / 分散アルゴリズム / 自己安定
研究開始時の研究の概要

本研究は,形式手法 (モデル検査) の適用によって,自律分散ロボット群アルゴリズムに対する実用的な正統性検証の枠組みを与えることを目的とする.
モデル検査法はしらみつぶし探索を自動化するものであり,与えられた証明の正しさに対して十分な説得力を与える.具体的には本研究の貢献は以下のとおりである.
・ロボットの集合問題に対するアルゴリズムの正しさの検証法を与える.
・それ以外の問題にも適用可能で十分に一般性のあるモデル検証法の枠組みを開発する.
・検証モデルにより,アルゴリズム合成を自動化にする.

研究実績の概要

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.

現在までの達成度 (区分)
現在までの達成度 (区分)

3: やや遅れている

理由

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.

今後の研究の推進方策

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.

報告書

(3件)
  • 2023 実施状況報告書
  • 2022 実施状況報告書
  • 2021 実施状況報告書
  • 研究成果

    (20件)

すべて 2023 2022 2021 その他

すべて 国際共同研究 (3件) 雑誌論文 (12件) (うち国際共著 12件、 査読あり 12件、 オープンアクセス 9件) 学会発表 (1件) (うち国際学会 1件、 招待講演 1件) 備考 (4件)

  • [国際共同研究] Sorbonne University(フランス)

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究] Sorbonne University(フランス)

    • 関連する報告書
      2022 実施状況報告書
  • [国際共同研究] Sorbonne University(フランス)

    • 関連する報告書
      2021 実施状況報告書
  • [雑誌論文] Using Model Checking to Formally Verify Rendezvous Algorithms for Robots with Lights in Euclidean Space2023

    • 著者名/発表者名
      X. Defago, A. Heriban, S. Tixeuil, K. Wada
    • 雑誌名

      Robotics and Autonomous Systems

      巻: 163 ページ: 104378-104378

    • DOI

      10.1016/j.robot.2023.104378

    • 関連する報告書
      2023 実施状況報告書 2022 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] Optimal L-algorithms for rendezvous of asynchronous mobile robots with external-lights2023

    • 著者名/発表者名
      Okumura Takashi、Wada Koichi、Defago Xavier
    • 雑誌名

      Theoretical Computer Science

      巻: 979 ページ: 114198-114198

    • DOI

      10.1016/j.tcs.2023.114198

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Solving simultaneous target assignment and path planning efficiently with time-independent execution2023

    • 著者名/発表者名
      Okumura Keisuke、Defago Xavier
    • 雑誌名

      Artificial Intelligence

      巻: 321 ページ: 103946-103946

    • DOI

      10.1016/j.artint.2023.103946

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] Offline Time-Independent Multiagent Path Planning2023

    • 著者名/発表者名
      Okumura Keisuke、Bonnet Francois、Tamura Yasumasa、Defago Xavier
    • 雑誌名

      IEEE Transactions on Robotics (T-RO)

      巻: - 号: 4 ページ: 1-18

    • DOI

      10.1109/tro.2023.3258690

    • 関連する報告書
      2023 実施状況報告書 2022 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Quick Multi-Robot Motion Planning by Combining Sampling and Search2023

    • 著者名/発表者名
      Okumura Keisuke, Defago Xavier
    • 雑誌名

      IJCAI '23: Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence

      巻: 29 ページ: 252-261

    • DOI

      10.24963/ijcai.2023/29

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Priority inheritance with backtracking for iterative multi-agent path finding2022

    • 著者名/発表者名
      Okumura Keisuke、Machida Manao、Defago Xavier、Tamura Yasumasa
    • 雑誌名

      Artificial Intelligence

      巻: 310 ページ: 103752-103752

    • DOI

      10.1016/j.artint.2022.103752

    • 関連する報告書
      2022 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Offline Time-Independent Multi-agent Path Planning2022

    • 著者名/発表者名
      K. Okumura, F. Bonnet, Y. Tamura, X. Defago
    • 雑誌名

      31st International Conference on Artificial Intelligence (IJCAI)

      巻: n/a ページ: 4649-4656

    • DOI

      10.24963/ijcai.2022/645

    • NAID

      130008052002

    • 関連する報告書
      2022 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Solving Simultaneous Target Assignment and Path Planning Efficiently with Time-Independent Execution2022

    • 著者名/発表者名
      Okumura Keisuke、Defago Xavier
    • 雑誌名

      Proceedings of the International Conference on Automated Planning and Scheduling

      巻: 32 ページ: 270-278

    • DOI

      10.1609/icaps.v32i1.19810

    • 関連する報告書
      2022 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Resilient real-valued consensus in spite of mobile malicious agents on directed graphs2022

    • 著者名/発表者名
      Y. Wang, H. Ishii, F. Bonnet, X. Defago
    • 雑誌名

      IEEE Transactions on Parallel and Distributed Systems

      巻: Vol. 33 No. 3 号: 3 ページ: 586-603

    • DOI

      10.1109/tpds.2021.3096074

    • 関連する報告書
      2021 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] Time-Independent Planning for Multiple Moving Agents2021

    • 著者名/発表者名
      Keisuke Okumura, Yasumasa Tamura, Xavier Defago
    • 雑誌名

      Proceedings of the AAAI Conference on Artificial Intelligence

      巻: 35(13) ページ: 11299-11307

    • 関連する報告書
      2021 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Active Modular Environment for Robot Navigation2021

    • 著者名/発表者名
      Shota Kameyama, Keisuke Okumura, Yasumasa Tamura, Xavier Defago
    • 雑誌名

      2021 IEEE International Conference on Robotics and Automation (ICRA)

      巻: None ページ: 8636-8642

    • DOI

      10.1109/icra48506.2021.9561111

    • 関連する報告書
      2021 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Iterative Refinement for Real-Time Multi-Robot Path Planning2021

    • 著者名/発表者名
      Keisuke Okumura, Yasumasa Tamura, Xavier Defago
    • 雑誌名

      2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)

      巻: None ページ: 9690-9697

    • DOI

      10.1109/iros51168.2021.9636071

    • 関連する報告書
      2021 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [学会発表] Verification and Synthesis of Rendezvous Algorithms for Luminous Robots2022

    • 著者名/発表者名
      Xavier Defago
    • 学会等名
      Research Meeting and School on Distributed Computing by Mobile Robots
    • 関連する報告書
      2022 実施状況報告書
    • 国際学会 / 招待講演
  • [備考] Verification model (public github repository)

    • URL

      https://github.com/xdefago/spin-light

    • 関連する報告書
      2023 実施状況報告書 2022 実施状況報告書
  • [備考] Algorithm synthesis (private github repository)

    • URL

      https://github.com/xdefago/synth-lights

    • 関連する報告書
      2023 実施状況報告書 2022 実施状況報告書
  • [備考] Verification model (github repository)

    • URL

      https://github.com/xdefago/spinlights

    • 関連する報告書
      2021 実施状況報告書
  • [備考] Algorithm synthesis (github repository)

    • URL

      https://github.com/xdefago/synth-lights

    • 関連する報告書
      2021 実施状況報告書

URL: 

公開日: 2021-04-28   更新日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi