1999 Fiscal Year Annual Research Report
エージェントの分散制約充足に基づく計算機システムの検証および診断
| Project/Area Number |
09650444
|
|---|
| Research Institution | HOKKAIDO INSTITUTE OF TECHNOLOGY |
|---|
Principal Investigator |
栗原 正仁 北海道工業大学, 工学部, 教授 (50133707)
|
|---|
| Keywords | エージェント / 分散制約充足 / 検証 / 診断 / 書換え系 / 停止性 / 完備化 |
|---|
| Research Abstract |
本研究はエ一ジェントの分散制約充足に基づいて,計算機システムにおけるソフトウェアの検証およびハードウェアの診断を行うシステムのモデルを開発し,それを実装し評価することを目的として,3年間の計画で実施している.
本年度はその最終年度として,まず,ソフトウェアの検証のうち特にこれまで検討してきた停止性の検証を引き続き取り上げ,エ一ジェント間の制約を二分決定グラフ(BDD)を用いて効率的に充足する手法とその評価結果をまとめて公表した.さらに,本研究で対象としている書換え系言語において,プログラム自らが自己反映的に自分自身の正当性の検証を行うための実装上のフレームワークとして独創的なメタレベル計算モデルを開発して発表した.
次に,ハードウェアの診断に関しては,組合せ論理回路の各コンポーネントの機能やそれらの接続に関する仕様を制約として等式で記述し,それを完備化と呼ばれる推論規則で充足性を判定する際に,その計算のNP完全性を少しでも緩和するために複数のエ一ジェントがそれぞれ1つの簡約順序を担当して分散して自律的に推論しながらも,独自の真偽維持システムを通して協調することにより,効率的な制約充足判定を実現する手法を開発し発表した.さらに,エ一ジェントを実装するためのソフトウェアアーキテクチャとしてJava言語に基づく分散オブジェクト指向アーキテクチャを示し,実際にシステムを実装し,典型的なテスト問題により評価した結果,期待されていたような良好なパフォ一マンスを確認することができた.
最後に,3年間のプロジェクトを総括し,成果を整理して関連づけるとともに,今後の課題を抽出した.
|
-
[Publications] 近藤久,栗原正仁: "二分決定グラフを用いた項書換え系の停止性検証システム"人工知能学会誌. 13・5. 822-834 (1998)
-
[Publications] 沼澤政信,栗原正仁,大内東: "条件付き項書換え系に基づく言語におけるメタ計算"情報処理学会論文誌. 39・11. 3035-3043 (1998)
-
[Publications] M.Kurihira,H.Kondo: "Completion for multiple reduction orderings"Journal of Automated Reasoning. 23・1. 25-42 (1999)
-
[Publications] M.Kurihira,H.Kondo: "Heuristics and experiments on BDD representation of Boolean functions for expert systems in software verification"Lecture Notes in Artificial Intelligence. 1747. 353-364 (1999)
-
[Publications] M.Kurihira,H.Kondo: "Design and heuristics for BDD-based automated termination verification system for rule-based programs"Proc.IEEE Int.Conf.On System,Man,and Cybern.. 5. 738-743 (1999)
-
[Publications] M.Numasawa,M.Kurihara: "Reflective agents for conditional rewriting"Proc.Australian Joint Conf.on Artificial Intelligence. 11. 85-96 (1998)
