1992 Fiscal Year Annual Research Report
様相構造記述言語を用いるリアクティブシステム構成法の研究
| Project/Area Number |
03680027
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology,Hokuriku |
|---|
Principal Investigator |
米崎 直樹 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00126286)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
徳田 雄洋 東京工業大学, 工学部情報工学科, 助教授 (30111644)
|
|---|
| Keywords | 時相論理 / 仕様記述 / リアクティブシステム / 実現可能性 / プロセスモデル / 非標準論理 / 様相論理 / 定理自動証明 |
|---|
| Research Abstract |
1)非標準論理定理証明法の研究
様相論理を用いて記述されたシステムの無矛盾性等を形式的に検証するための、新しい効率的証明方法を与えた。すなわち、様相記号列の統一化を用いる方法において、ある制約された自己代入を許すことにより大幅に証明圧縮が行なえることを示した。また、このような代入に関して証明システムが健全で完全であることを示した。また並列処理の資源に関する局面を表現可能な論理として、線形論理が注目されているが、様相記号(!)を含んだ命題線形論理について、標準形を用いない簡易な証明方法を与え、それが完全であることを示した。さらに、通常のuntil演算子より表現力を持ち、要求回数を考慮した公平性などを表現可能な時相論理を提案し、それが決定可能であることを証明した。
2)リアクティブシステムの実現に関する研究
一般的に仕様記述は、不十分でまた矛盾を含み、そのままでは実現不能であることが多い。ここでは実現不能な仕様に関してクラス分けを行ない、その包含関係について考察すると同時に、その判定アルゴリズムを与えた。また、図形を対象としたリアクティブシステムである図形編集環境の、時間付きの属性超グラフ文法による構成方法を示した。
3)ソフトウェアプロセスに関する研究
ソフトウェアプロセスも、ある種のリアクティブシステムとして捉えることが可能である。しかし、各アクティビティについて、様々なオブジェクトが付随し、その属性に関しては様々な制約が存在する。ここではTask、Agent、Productを中心とする新しいアプローチを提案した。また、代数を基にした仕様記述言語であるLOTOSを、プロセス仕様記述に適用し、必要とされるその拡張機能について明らかにした。
|
Research Products
(8 results)
-
[Publications] Ryousei Mori,Naoki Yonezaki: "Several realizability concepts in reactive objects" Proceeding of 2nd European-Japanese Seminar on Information modelling and knowledge Bases. (1993)
-
[Publications] Noriaki Yoshiura,Naoki Yonezaki: "More expressive Temporal Logic for Specifications" The fifth International Conference on Software Engeering and Knowledge Engeering. (1993)
-
[Publications] 端山 毅,米崎 直樹: "様相記号列統一化による様相論理定理証明器における自己代入の利用" コンピュータソフトウェア. vol.10,No.3. (1993)
-
[Publications] 端山 毅,米崎 直樹: "様相記号列統一化による様相論理定理証明器の健全性と完全性" コンピュータソフトウェア. vol.10 No.3. (1993)
-
[Publications] Naoki Yonezaki,Tapani Kinnula.Motoshi Saeki,Jan Ljungberg: "TAP:A new model for software process Tasks-Agents-Products" The fifth International Conferece on Software Engeering and Knowledge Engeering. (1993)
-
[Publications] 川村 美代子,米崎 直樹: "Linear Logicの自動証明法" 人工知能学会全国大会第6回論文集. 95-98 (1992)
-
[Publications] Naoki Yonezaki(分担): "Advances in Information Modeling and Knowledge Bases" ISO press, 18 (1991)
-
[Publications] Naoki Yonezaki,Takeshi Hayama(分担): "Advances in Information Modeling and Knowledge Bases" ISO press, 16 (1993)
