エージェントの分散制約充足に基づく計算機システムの検証および診断

1997 Fiscal Year Annual Research Report

• Project/Area Number: 09650444
• Research Category: Grant-in-Aid for Scientific Research (C)
• Research Institution: Hokkaido Institute of Technology
• Principal Investigator: 栗原 正仁 北海道工業大学, 工学部・電気工学科, 教授 (50133707)
• Keywords: エージェント / 分散制約充足 / 検証 / 診断

Research Abstract

本研究課題を大別すると、ソフトウェアの検証とハードウェアの診断に分けられる。本年度は、まず、エージェントによる分散制約充足という枠組みにおいて、両者に共通したシステムアーキテクチャとして、自己反映計算メカニズムと二分決定グラフを検討した。具体的には以下のような研究成果を得て公表した。
1.エージェントが自己認識に基づいて動作をするような構造的枠組みとして、書換え型言語への自己反映計算メカニズムの導入を提案し、ベースレベルとメタレベルのメッセージ交換プロトコルを設計した。また、これを実装するのに適したプログラミング言語の計算モデルとしてCrepsを提案した。Crepsの計算は抽象リダクションマシンとしての書換えエージェントによるオブジェクトの書換えによってモデル化される。本研究では、エージェントの動作を公理論的に定義し、その操作的意味により計算を定義した。次に、ベースレベルとメタレベルのメッセージ交換のために、ベース変換およびメタ交換というオブジェクト交換プロトコルを設計し、エージェントの自己反映動作を可能とした。
2.ソフトウェアの検証問題として、ルール型言語(項書換え系)で記述されたプログラムの停止性検証を取り上げ、エージェントの組織を二分決定グラフで構造化し、効率的なシステムのプロトタイプを実装した。停止性の検証には、関数記号の集合上にある半順序を固定しなければならない。従来システムはそれをシングルエージェントで一つに固定していたため、検証に失敗することが多かった。本研究では、それをマルチエージェントとし、複数の半順序を並行して扱うことを可能にした。その技術的ポイントは、各エージェントが単に独立して動作するのではなく、二分決定グラフにより組織化されることにより、情報交換による情報共有が可能となり、システムが効率的に動作することにある。

Research Products

• [Publications] 沼沢政信,栗原正仁: "Crepsにおける自己反映計算の実現" 第7回インテリジェント・シンポジウム論文集. 1. 1-6 (1997)
• [Publications] 近藤久,栗原正仁: "二分決定グラフを用いた書換え型プログラムの停止性検証器" 情報処理学会研究報告. 97・112. 1-6 (1997)
• [Publications] 近藤久,栗原正仁: "二分決定グラフを用いた項書換え系の停止性検証システム" 人工知能学会誌. 13・5(掲載予定). (1998)