ACOに基づくモデル検査の匂いフェロモンを用いた拡張

• Item type: Symposium(1)
• 公開日: 2018-01-19
• タイトル: ACOに基づくモデル検査の匂いフェロモンを用いた拡張
• タイトル / 言語: en
• タイトル: ACO Based Model Checking Extended by Smell-like Pheromone with Hop Counts
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: モデル検査，蟻コロニー最適化法，群知能，状態爆発問題
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_5794
• 資源タイプ: conference paper
• 著者所属: 東京理科大学
• 著者所属: 東京理科大学
• 著者所属: 株式会社SRA
• 著者所属: 日本工業大学
• 著者所属(英): en
• 著者所属(英): Tokyo University of Science
• 著者所属(英): en
• 著者所属(英): Tokyo University of Science
• 著者所属(英): en
• 著者所属(英): Software Research Associates, Inc.
• 著者所属(英): en
• 著者所属(英): Nippon Institute of Technology
• 著者名: 高田, 圭一郎; 滝本, 宗宏; 熊澤, 努; 神林, 靖
• 著者名(英): Keiichiro, Takada; Munehiro, Takimoto; Tsutomu, Kumazawa; Yasushi, Kambayashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本論文では，ACO(蟻コロニー最適化法) の改良アルゴリズムを用いた，効率的なモデル検査手法を提案する．モデル検査とは，ハードウェアやソフトウェアの設計が，目的の仕様を満たしているか，モデル検査器によって自動的に検証する技術である．設計は，状態遷移系のモデルとして表現し，仕様は時相論理によって指定する．一般的なモデル検査器は，決定的アルゴリズムに基づいて動いているので，検証に膨大な実行時間とメモリが必要になる場合がある．これは状態爆発問題と呼ばれる．状態爆発問題を低減する手法の一つに，蟻の振る舞いを真似たメタヒューリスティクスであるACO に基づく手法が提案されている．本論文では，ACO を，餌から発せられる匂いに相当する特殊なフェロモンによって拡張した，新しいACO に基づくモデル検査法を提案する．匂いフェロモンは最終状態から開始状態に向けて，到達に必要なホップ数をモデル内の各辺に記録する．本手法では，蟻はホップ数が減少する方向へ最終状態を探索するので，効率的に検査を進めることができる．本手法に基づいた検査器を実現し，実験を行ったところ，解の品質を下げることなく，実行時間を短縮できることが分かった．
• 書誌情報: 第59回プログラミング・シンポジウム予稿集; 巻 2018, p. 19-29, 発行日 2018-01-19
• 出版者 / 言語: ja
• 出版者: 情報処理学会