| 研究概要 |
1)非標準論理定理証明法の研究
様相論理を用いて記述されたシステムの無矛盾性等を形式的に検証するための,新しい効率的証明方法を与えた。すなわち,様相記号列の統一化を用いる方法において,ある制約された自己代入を許すことにより大幅に証明圧縮が行なえるとこを示した。また,このような代入に関して証明システムが健全で完全であることを示した。また並列処理の資源に関する局面を表現可能な論理として,線形論理が注目されているが,様相記号(!)を含んだ命題線形論理について,標準形を用いない簡易な証明方法を与え,それが完全であることを示した。さらに,通常のuntil演算子より表現力を持ち,要求回数を考慮した公平性などを表現可能な時相論理を提案し,それが決定可能であることを証明した。
2)リアクティブシステムの実現に関する研究
一般的に仕様記述は,不十分でまた矛盾を含み,そのままでは実現不能であることが多い。ここでは実現不能な仕様に関してクラス分けを行ない,その包含関係について考察すると同時に,その判定アルゴリズムを与えた。また,図形を対象としたリアクティブシステムである図形編集環境の,時間付きの属性超グラフ文法による構成方法を示した。
3)ソフトウェアプロセスに関する研究
ソフトウェアプロセスも,ある種のリアクティブシステムとして捉えることが可能である。しかし,各アクティビィティについて,様々なオブジェクトが付随し,その属性に関しては様々な制約が存在する。ここではTask,Agent,Productを中心とする新しいアプローチを提案した。また,代数を基にした仕様記述言語であるLOTOSを,プロセス仕様記述に適用し,必要とされるその拡張機能について明らかにした。
|
