| 講演名 | 2003/5/22 モデル生成型定理証明手続きによるCTLのモデル検査(<特集>「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論) 清水 亮, 長谷川 隆三, 越村 三幸, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本論文では、モデル生成型定理証明手続きを用いたCTLのモデル検査を行う手法を提案する。本提案手法では、状態遷移システムと仕様の否定を節集合として表現する。そして、それらをあわせた節集合の充足可能性にモデル検査を帰着させる。遷移システムが仕様を満足すれば充足不能であり、満足しなければ反例をモデルとして出力する。本論文で提案する手法により、CTLのモデルと意味論を節形式で記述することができるので、モデル生成法を利用してモデル検査が原理的にできることを示すことができた。 |
| 抄録(英) | This paper presents a method performing CTL model checking with a model generation theorem prover. In this method, a transition system and a negation of its specification are represented by a clause set. The model checking is performed by checking satisfiability of the clause set. If the transition system satisfies the specification, the clause set are unsatisfiable, otherwise, it is satisfiable. In the latter, the theorem prover returns a model as a counter example which show a possible error of the transition system. |
| キーワード(和) | CTL / モデル検査 / モデル生成法 |
| キーワード(英) | CTL / model checking / model generation |
| 資料番号 | AI2003-7 |
| 発行日 |
| 研究会情報 | |
| 研究会 | AI |
|---|---|
| 開催期間 | 2003/5/22(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Artificial Intelligence and Knowledge-Based Processing (AI) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル生成型定理証明手続きによるCTLのモデル検査(<特集>「自動推論:帰納,演繹,モデル検査/生成,学習,発見,仮説推論,論理プログラム,プランニングetc.」及び一般)(自動推論) |
| サブタイトル（和） | |
| タイトル（英） | CTL Model cheking with Model Generation Theorem Prover |
| サブタイトル（和） | |
| キーワード(1)（和/英） | CTL / CTL |
| キーワード(2)（和/英） | モデル検査 / model checking |
| キーワード(3)（和/英） | モデル生成法 / model generation |
| 第 1 著者 氏名（和/英） | 清水 亮 / Ryo SHIMIZU |
| 第 1 著者 所属（和/英） | 九州大学大学院システム情報科学府 Graduate School of Information Science and Electrical Engineering Kyushu Univercity |
| 第 2 著者 氏名（和/英） | 長谷川 隆三 / Ryuzo HASEGAWA |
| 第 2 著者 所属（和/英） | 九州大学大学院システム情報科学府 Graduate School of Information Science and Electrical Engineering Kyushu Univercity |
| 第 3 著者 氏名（和/英） | 越村 三幸 / Miyuki KOSHIMURA |
| 第 3 著者 所属（和/英） | 九州大学大学院システム情報科学府 Graduate School of Information Science and Electrical Engineering Kyushu Univercity |
| 発表年月日 | 2003/5/22 |
| 資料番号 | AI2003-7 |
| 巻番号（vol） | vol.103 |
| 号番号（no） | 103 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |