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