文献

J-GLOBAL ID：201702233305151500   整理番号：17A1774661

リングに関する忘れられているロボットのためのアルゴリズムのパラメータ化された検証【Powered by NICT】

Parameterized verification of algorithms for oblivious robots on a ring

著者 (4件)： Sangnier Arnaud (IRIF, Univ Paris Diderot) ,  Sznajder Nathalie (Sorbonne Universite ́s, UPMC Univ Paris 06, LIP6) ,  Potop-Butucaru Maria (Sorbonne Universite ́s, UPMC Univ Paris 06, LIP6) ,  Tixeuil Sebastien (Sorbonne Universite ́s, UPMC Univ Paris 06, LIP6)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FMCAD  ページ： 212-219  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： グローバルな目標を解決するために自己組織化と協調する移動ロボットの自律的スウォームに対する検証問題を研究した。特に,有限数位置の(ここでは,リング)と不連続空間に出現する匿名ロボットのSuzuki及び山下によって提案されたモデルに本論文で焦点を当てた。多数のアルゴリズムは,その大きさは事前固定されていない,従ってパラメータと考えられる環の提案されている。これらアルゴリズムの手作り正当性の証明は誤りがちであることが示されており,自動的にそれを証明するための形式的方法の適用に投与されていた最近注目されてきた。著者らの研究は,パラメータ化された場合,このようなアルゴリズムの検証問題を研究した最初のものである。安全性と到達可能性問題は非同期的に発展するロボットのための決定不能であることを示した。積極的面として,筆者らは,安全特性は,同期の場合だけでなく,特定のクラスのアルゴリズムのための非同期的な場合は決定可能であることを示した。プロトコルにいくつかの性質も決定できる。決定手続きはSMTソルバによる検証できるPresburger算術式の符号化に依存している。提案アプローチの実現可能性をいくつかの事例研究の符号化により実証した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： 不連続性 ,  移動ロボット ,  *アルゴリズム ,  モデル ,  スウォーム ,  *パラメタリゼーション ,  安全性 ,  自己組織化 ,  符号化 ,  *ロボット ,  プロトコル ,  事例研究
準シソーラス用語： ソルバ ,  匿名 ,  自律性 , 【Automatic Indexing@JST】

分類 (2件)： ロボットの運動・制御  (IC04012J) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (4件)： ロボット ,  アルゴリズム ,  パラメータ ,  検証