確率時間オートマトンを用いた自律移動ロボットの振舞いのモデル化

• Item type: SIG Technical Reports(1)
• 公開日: 2016-05-26
• タイトル: 確率時間オートマトンを用いた自律移動ロボットの振舞いのモデル化
• タイトル / 言語: en
• タイトル: Modeling of an autonomous mobile robot using probabilistic timed automaton
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: モデル
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_18gh
• 資源タイプ: technical report
• 著者所属: 日本大学
• 著者所属: 信州大学
• 著者所属: 日本大学
• 著者所属(英): en
• 著者所属(英): Nihon University
• 著者所属(英): en
• 著者所属(英): Shinshu University
• 著者所属(英): en
• 著者所属(英): Nihon University
• 著者名: 小林, 佳正; 岡野, 浩三; 関澤, 俊弦
• 著者名(英): Yoshimasa, Kobayashi; Kozo, Okano; Toshifusa, Sekizawa
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 近年，自律移動システムの開発が進んでいる．自律移動システムを搭載したロボットは物理環境下で動作する際，位置に誤差が生じる．ロボットは誤差検出及び誤差補正を行なっても座標には誤差が生じ，到達座標は確率的な分布をとる．このような確率的に振舞う系の信頼性を保証する研究は十分とは言い難い．本研究では，離散的な状態で誤差検出及び補正を行なう系を具体的な対象とし，モデル検査による検証に向けて，ロボットの振舞いをモデル化する．既存研究では，ロボットの確率的な振舞いをマルコフ決定過程でモデル化し，確率モデル検査を用いて検証を行なっている．しかし，この検証では移動時間などの時間的な振舞いを考慮に入れた検証はなされていない．本研究では，より現実的なロボットの振舞いを対象とするため，確率的性質及び時間的性質を考慮に入れた振舞いのモデル化を行なう．ロボットの振舞いを確率的性質と時間的性質に分類し，それぞれの性質を併せ持つ要素を考えることで，確率的性質及び時間的性質を考慮に入れたロボットの振舞いを確率時間オートマトンで表現する．また，確率時間オートマトンで表現することにより，確率的性質及び時間的性質を考慮に入れた振舞いがモデル検査の検証対象となり得ることを示す．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: In recent years, development of autonomous mobile system has been developed. Errors occur when a robot equipped with autonomous mobile system is operated under physical environment. Therefore, coordinates of the robot take probabilistic distribution even if the robot performs error detection and correction. Verification of reliability of such probabilistic systems are not yet sufficient. In this study towards model checking, we construct a model representing behaviors of an autonomous robot which performs error detection and correction in discrete states. In our previous study, probabilistic behaviors of a robot are modeled using Markov decision processes, and are verified by probabilistic model checker. However, the verification does not consider time related properties such as movement time. In this study, we construct a model in consideration of probabilistic and time related properties, for handling more realistic robot behaviors. For that purpose, robot behaviors are classified into probabilistic property and time related property. Then, a model expressed in probabilistic timed automaton is constructed in which both of these properties are considered. We also describe that robot behaviors consisting of probabilistic and time related properties can be verification target using model checking.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA12149313
• 書誌情報: 研究報告組込みシステム（EMB）; 巻 2016-EMB-41, 号 14, p. 1-6, 発行日 2016-05-26
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 2188-868X
• Notice: SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc.
• 出版者 / 言語: ja
• 出版者: 情報処理学会