@techreport{oai:ipsj.ixsq.nii.ac.jp:00163648,
 author = {小林, 佳正 and 岡野, 浩三 and 関澤, 俊弦 and Yoshimasa, Kobayashi and Kozo, Okano and Toshifusa, Sekizawa},
 issue = {14},
 month = {May},
 note = {近年，自律移動システムの開発が進んでいる．自律移動システムを搭載したロボットは物理環境下で動作する際，位置に誤差が生じる．ロボットは誤差検出及び誤差補正を行なっても座標には誤差が生じ，到達座標は確率的な分布をとる．このような確率的に振舞う系の信頼性を保証する研究は十分とは言い難い．本研究では，離散的な状態で誤差検出及び補正を行なう系を具体的な対象とし，モデル検査による検証に向けて，ロボットの振舞いをモデル化する．既存研究では，ロボットの確率的な振舞いをマルコフ決定過程でモデル化し，確率モデル検査を用いて検証を行なっている．しかし，この検証では移動時間などの時間的な振舞いを考慮に入れた検証はなされていない．本研究では，より現実的なロボットの振舞いを対象とするため，確率的性質及び時間的性質を考慮に入れた振舞いのモデル化を行なう．ロボットの振舞いを確率的性質と時間的性質に分類し，それぞれの性質を併せ持つ要素を考えることで，確率的性質及び時間的性質を考慮に入れたロボットの振舞いを確率時間オートマトンで表現する．また，確率時間オートマトンで表現することにより，確率的性質及び時間的性質を考慮に入れた振舞いがモデル検査の検証対象となり得ることを示す．, 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.},
 title = {確率時間オートマトンを用いた自律移動ロボットの振舞いのモデル化},
 year = {2016}
}