| 研究課題/領域番号 |
63580025
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
坂部 俊樹 名古屋大学, 工学部, 助教授 (60111829)
|
|---|
| 研究分担者 |
平田 富夫 名古屋大学, 工学部, 助教授 (10144205)
稲垣 康善 名古屋大学, 工学部, 教授 (10023079)
|
|---|
| キーワード | 非停止プロセス / 等式論理 / 代数的仕様記述 / 並行プロセス / CCS / 木パタ-ンマッチング |
|---|
| 研究概要 |
本年度の研究実績は以下の通りである。
1.非停止プロセスが陽に記述できる有理等式論理の拡張については、論理の意味の研究が進められた。すなわち有理等式論理の基本構文である項書換え系の代数的意味論と計算複雑さについての研究に基づく項書換え系の等価交換法を示し、その正当性を証明した。
2.代数的仕様記述言語の設計及び処理系の開発については、最外戦略による項書換えアルゴリズムについて研究し、代数的言語の処理系の開発の基礎を確立した。
3.仕様の検証法についての検討では、仕様の帰納的定理の証明法について研究した。この研究では、従来の構造帰納法を拡張した被覆集合に基づく構造帰納法を提案し、その証明法による証明支援システムの開発に着手した。
4.CCSと有理等式論理の関係の解明については、両者の意味論の対応をとるため、CCSの意味論を中心に研究を行った。すなわち、CCSの意味論として観測等価関係を採用し、それによって並行処理の基本モデルであるモニタの排他制御、同期制御、抽象化機構が自然に説明できることを明らかにした。
5.その他、研究計画に挙げられていない項目として、関数型の並行プロセスのモデルとして通信機能付項書換え系を考案した。主な結果はプロセス内計算とプロセス間通信計算の独立性と計算の一意味を示したことである。
|
