様相概念を用いる知識のモジュール化とその処理に関する研究

1.非標準論理体系の一般的証明方法とその効率化に関する研究一般的な様相論理式に関して、様相記号列の統一化を用いる方法をもとに自己代入を許すことにより、証明を圧縮する方法を与えた。この考え方は、Until様相オペレータを持つ時相論理体系にも拡張され、非節形式の解証明法として形式化した。次に、線形論理の自動証明向きの証明系を構成し、その体系が健全かつ完全なものであることを示した上で、実現のための手続きやその効率化の手法を与えた。2.時相論理の拡張と検証方式に関する研究要求回数を考慮した公平性を表現可能な時間論理を提案し、その充足可能性問題が決定可能であることを示した。また、仕様の段階的追加に応じて充足可能性のチェックを差分的に行なう、新しいタブローを提案した。3.リアクティブシステムの実現に関する研究時相論理で記述されたリアクティブシステムの実現不能な仕様に対して、クラス分けを行いそのそれぞれの包含関係を明らかにすると同時に、その判定アルゴリズムを与えた。また強充足可能でないクラスの仕様について、どのような制約を入力イベント列に加えれば強充足可能になるかに関する、最弱の制約を式の形で求める方法を与えた。これはタブローから、、最弱の制約を構成する一般的方法として実現された。4.ソフトウェアプロセスに関する研究Task,Agent,Processを中心とする新しいプロセスモデル(TAP)を与えた。そのそれぞれのソートを持つオブジェクトにクラス-インスタンスの階層、部分-全体の階層が存在し、またプロセスには、計画やプロセス変更を行うメタプロセスを含めることが可能であり、プロセスのインスタンスであるアクティビティーには、その実行主体であるエージェントのインスタンスと使用されるツールのインスタンスが必ず付随する。

1.非標準論理体系の一般的証明方法とその効率化に関する研究一般的な様相論理式に関して、様相記号列の統一化を用いる方法をもとに自己代入を許すことにより、証明を圧縮する方法を与えた。この考え方は、Until様相オペレータを持つ時相論理体系にも拡張され、非節形式の解証明法として形式化した。次に、線形論理の自動証明向きの証明系を構成し、その体系が健全かつ完全なものであることを示した上で、実現のための手続きやその効率化の手法を与えた。2.時相論理の拡張と検証方式に関する研究要求回数を考慮した公平性を表現可能な時間論理を提案し、その充足可能性問題が決定可能であることを示した。また、仕様の段階的追加に応じて充足可能性のチェックを差分的に行なう、新しいタブローを提案した。3.リアクティブシステムの実現に関する研究時相論理で記述されたリアクティブシステムの実現不能な仕様に対して、クラス分けを行いそのそれぞれの包含関係を明らかにすると同時に、その判定アルゴリズムを与えた。また強充足可能でないクラスの仕様について、どのような制約を入力イベント列に加えれば強充足可能になるかに関する、最弱の制約を式の形で求める方法を与えた。これはタブローから、、最弱の制約を構成する一般的方法として実現された。4.ソフトウェアプロセスに関する研究Task,Agent,Processを中心とする新しいプロセスモデル(TAP)を与えた。そのそれぞれのソートを持つオブジェクトにクラス-インスタンスの階層、部分-全体の階層が存在し、またプロセスには、計画やプロセス変更を行うメタプロセスを含めることが可能であり、プロセスのインスタンスであるアクティビティーには、その実行主体であるエージェントのインスタンスと使用されるツールのインスタンスが必ず付随する。