1996 Fiscal Year Annual Research Report
| Project/Area Number |
08680343
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Shizuoka University |
|---|
Principal Investigator |
富樫 敦 静岡大学, 情報学部, 助教授 (20172140)
|
|---|
| Keywords | 高階並行プロセス計算 / 動作的意味論 / 計算モデル / 高階様相論理 / タイプシステム / モデルチェッキング / 等価性 / 双模倣 |
|---|
| Research Abstract |
本研究の目的は,「高階並行プロセス計算モデル」を構築し,その動作的意味論に関する基礎理論を確立すること,および,以上に基づいたプログラミング言語を開発し,実践を通して本モデルと基礎理論の妥当性を実証することである.本年度は,以下の項目に関して,以下の成果を得た.
(1)高階並行プロセス計算モデルの構築
高度な計算パラダイムを有する並行システムを記述・解析するための「高階プロセス計算モデル」を構築した.このモデルは,それぞれ研究項目(2),(3)で展開する数学的議論とプログラミング言語のベースモデルとなる.
(2)高階並行プロセス計算の動作的意味に関する数学的基礎理論の確立
(1)で提案した計算モデルに対して,以下の小項目に関する研究を実施し,その数学的基礎を確立させた.
(a)双模倣の概念による等価性:第2階のλ計算などに適用された適用双模倣性に基づいた等価性について検討し、高階プロセスの動作的意味を十分に反映した等価性の理論を与えた.
(b)高階様相論理体系とモデルチェッキング:高階論理を用いた高階プロセスの記述に適した証明システムを提案し,その健全性・完全性などの諸性質や,(a)で与えた等価性との関係に関する特性化定理を与えた.また,タブロ-法などのテクニックを用いたモデルチェッキング法の可能性を模索した。その場合計算可能性を考慮し,プロセスに妥当な制限を与え,ベース論理の1階論理への帰着可能性を示すことが重要となった.
(c)多相タイプシステム:高階システムに適したタイプ原理と具体的な多相タイプシステムを与えた.タイプシステムは,静的解析に用いられる他,高階プロセス計算の体系を与える際にも重要となった.
(d)等価性の公理化:より現実世界のモデルに制限した場合の公理化の可能性について検討した.
|
-
[Publications] 富樫敦: "Automatic Synthesis of Specifications from System Requirements" ソフトウェア工学の基礎III「レクチャーノート/ソフトウェア工学17,日本ソフトウェア科学会FOSE'96」. 9-17 (1996)
-
[Publications] A.Togashi,G.Mansfield,N.Shiratori: "Animating LOTOS Specifications using AMLOG" Int.Journal on Soff.Eng.and Knowledge Eng.6・1. 5-19 (1996)
-
[Publications] S.Kimura,A.Togashi,N.Shiratori: "Extension of Synthesis Algorithm of Recursiue Processes to μ-Calculus" Infor.Processing Letter. 58. 97-104 (1996)
-
[Publications] 宋,富樫,白鳥: "命題論理に基づいた要求記述法と状態遷移システムによる意味記述" 情報処理学会論文誌. 37・4. 511-519 (1996)
-
[Publications] A.Togashi: "On Typing Systems for the Polyadic π-Calculus" Technical Report,COGS,Univ.of Sussex.(1996)
-
[Publications] 富樫、臼井、宋、白鳥: "Methodologies for the Description of System Regurements and the Derivation of Specification (Extended Abstract)" 情報処理学会マルチメディア通信と分散処理ワークショック論文集. 297-304 (1996)
-
[Publications] 富樫敦: "新版情報処理ハンドブック「1.4.2並行/分散計算の理論とアルゴリズム」" オーム社(情報処理学会編), 11(2000) (1996)
