| 講演名 | 2008-03-04 反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法 長岡 武志, 岡野 浩三, 楠本 真二, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 時間オートマトンを対象としたモデル抽象化手法を著者らは提案している.提案手法では,反例を元に抽象モデルを改良し,適切な抽象モデルを自動的に生成するCEGAR(CounterExample-Guided Abstraction Refinement)ループに基づく.抽象モデルの改良の際,元になる時間オートマトンの変形で行うなどの特徴を持つ.本稿では,提案手法の具体的なアルゴリズムを形式的に記述し,アルゴリズムの正当性の証明を与える. |
| 抄録(英) | We have proposed a method of model abstraction for timed automata. The proposed method is based on CEGAR (CounterExample-Guided Abstraction Refinement) loop which automatically refines an abstract model using counter examples. Our algorithm has some features such as refinements are performed indirectly through transformation of the original timed automation. This paper gives formal descriptions of the algorithm and the correctness proof of the algorithm. |
| キーワード(和) | モデル検査 / 時間オートマトン / モデル抽象化 / CEGAR |
| キーワード(英) | Model Checking / Timed Automation / Model Abstraction / CEGAR |
| 資料番号 | SS2007-74 |
| 発行日 |
| 研究会情報 | |
| 研究会 | SS |
|---|---|
| 開催期間 | 2008/2/25(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Software Science (SS) |
|---|---|
| 本文の言語 | ENG |
| タイトル（和） | 反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法 |
| サブタイトル（和） | |
| タイトル（英） | Abstraction of Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop |
| サブタイトル（和） | |
| キーワード(1)（和/英） | モデル検査 / Model Checking |
| キーワード(2)（和/英） | 時間オートマトン / Timed Automation |
| キーワード(3)（和/英） | モデル抽象化 / Model Abstraction |
| キーワード(4)（和/英） | CEGAR / CEGAR |
| 第 1 著者 氏名（和/英） | 長岡 武志 / Takeshi NAGAOKA |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 岡野 浩三 / Kozo OKANO |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 楠本 真二 / Shinji KUSUMOTO |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2008-03-04 |
| 資料番号 | SS2007-74 |
| 巻番号（vol） | vol.107 |
| 号番号（no） | 505 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |