1992 年度実績報告書

様相構造記述言語を用いるリアクティブシステム構成法の研究

研究課題

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

研究成果
(8件)

すべてその他

すべて文献書誌 (8件)

[文献書誌] Ryousei Mori,Naoki Yonezaki: "Several realizability concepts in reactive objects" Proceeding of 2nd European-Japanese Seminar on Information modelling and knowledge Bases. (1993)
[文献書誌] Noriaki Yoshiura,Naoki Yonezaki: "More expressive Temporal Logic for Specifications" The fifth International Conference on Software Engeering and Knowledge Engeering. (1993)
[文献書誌] 端山毅,米崎直樹: "様相記号列統一化による様相論理定理証明器における自己代入の利用" コンピュータソフトウェア. vol.10,No.3. (1993)
[文献書誌] 端山毅,米崎直樹: "様相記号列統一化による様相論理定理証明器の健全性と完全性" コンピュータソフトウェア. vol.10 No.3. (1993)
[文献書誌] 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)
[文献書誌] 川村美代子,米崎直樹: "Linear Logicの自動証明法" 人工知能学会全国大会第6回論文集. 95-98 (1992)
[文献書誌] Naoki Yonezaki(分担): "Advances in Information Modeling and Knowledge Bases" ISO press, 18 (1991)
[文献書誌] Naoki Yonezaki,Takeshi Hayama(分担): "Advances in Information Modeling and Knowledge Bases" ISO press, 16 (1993)

1992 年度 実績報告書

様相構造記述言語を用いるリアクティブシステム構成法の研究

研究代表者

米崎 直樹 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00126286)

研究成果

[文献書誌] Ryousei Mori,Naoki Yonezaki: "Several realizability concepts in reactive objects" Proceeding of 2nd European-Japanese Seminar on Information modelling and knowledge Bases. (1993)

[文献書誌] Noriaki Yoshiura,Naoki Yonezaki: "More expressive Temporal Logic for Specifications" The fifth International Conference on Software Engeering and Knowledge Engeering. (1993)

[文献書誌] 端山 毅,米崎 直樹: "様相記号列統一化による様相論理定理証明器における自己代入の利用" コンピュータソフトウェア. vol.10,No.3. (1993)

[文献書誌] 端山 毅,米崎 直樹: "様相記号列統一化による様相論理定理証明器の健全性と完全性" コンピュータソフトウェア. vol.10 No.3. (1993)

[文献書誌] 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)

[文献書誌] 川村 美代子,米崎 直樹: "Linear Logicの自動証明法" 人工知能学会全国大会第6回論文集. 95-98 (1992)

[文献書誌] Naoki Yonezaki(分担): "Advances in Information Modeling and Knowledge Bases" ISO press, 18 (1991)

[文献書誌] Naoki Yonezaki,Takeshi Hayama(分担): "Advances in Information Modeling and Knowledge Bases" ISO press, 16 (1993)

1992 年度実績報告書

米崎直樹北陸先端科学技術大学院大学, 情報科学研究科, 教授 (00126286)

[文献書誌] 端山毅,米崎直樹: "様相記号列統一化による様相論理定理証明器における自己代入の利用" コンピュータソフトウェア. vol.10,No.3. (1993)

[文献書誌] 端山毅,米崎直樹: "様相記号列統一化による様相論理定理証明器の健全性と完全性" コンピュータソフトウェア. vol.10 No.3. (1993)

[文献書誌] 川村美代子,米崎直樹: "Linear Logicの自動証明法" 人工知能学会全国大会第6回論文集. 95-98 (1992)