1993 Fiscal Year Annual Research Report
代数的並行プロセス自動合成のための時制論理に基づいた新しい方法論の開発
| Project/Area Number |
05680262
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
富樫 敦 東北大学, 電気通信研究所, 助教授 (20172140)
|
|---|
| Keywords | 並行プロセス / 自動合成 / 帰納推論 / 時制論理 / 等価性 / μ計算 / プロセス記述支援システム / プロセス計算 |
|---|
| Research Abstract |
本研究では,「高階の時制論理に基づき,大局的な時間的制約を陽に表現できる代数的並行プロセス記述システムを提案し,与えられた仕様から実際の並行プロセスを自動的に合成するための方法論を開発することを目的とする」.本年度は,次の研究項目を達成した.
研究項目0並行プロセスの帰納推論に関する継続研究
研究項目1並行プロセス記述支援システムの開発
並行プロセスの帰納推論に関しては,これまで強等価性に関する基本プロセスの推論法を中心に研究してきた.本年度は,より複雑なプロセスまでその範囲を広げた.具体的には,対象を再帰を許した再帰プロセスまで対象を広げ,強等価を同定基準とした場合と,強等価性以外の等価性も考慮した場合の帰納推論法について検討した.また,計算機上に合成アルゴリズムをPrologを用いて実際に実装し,具体例を通してアルゴリズムの妥当性を実証した.
研究項目1については,μ計算における再帰の論理構造と大局的な時間的制約が記述できる高階の時制論理体系を提案し,プロセスによる充足可能性に関して健全かつ完全な証明システムを与えた.さらに,この論理体系に基づいて,検証システムなどを備えた記述言語を設計し,並行プロセス記述支援システムを完成させた.従来,並行プロセスための計算システムとしてCCS,CSP,LOTOS,CHOCSなどが有名である.上記システムを開発する際これらのシステムの機能を十分に反映させた.
最後に,一般の並行プロセス計算を対象とした汎用の並行プロセス計算システムを設計し,実際にシステムを試作した.また,CCS,LOTOS,π計算などの実際の並行計算を具体的に記述することにより,提案したシステムの妥当性を確認した.
|
-
[Publications] Togashi,Atsushi: "On the relationship between Concurrent Process Calculi and Logic" Proc. of 6th Karuizawa Workshop on Circuits and Systems. 537-542 (1993)
-
[Publications] 富樫敦: "様相論理に基づいた代数的並行プロセスの帰納推論" 東北大学・応用情報学研究年報. 18. 131-155 (1993)
-
[Publications] 吉田仙: "汎用並行プロセス計算システムの設計開発" 電子情報通信学会コンピュテーション研究会技術報告. COMP93-30. 41-50 (1993)
-
[Publications] 木村成伴: "μ計算による再帰プロセスの合成" 電子情報通信学会コンピュテーション研究会技術報告. COMP93-86. 73-80 (1994)
-
[Publications] 白井伸幸: "プロセス合成のための支援環境に関する研究" 電子情報通信学会コンピュテーション研究会技術報告. COMP93-84. 57-64 (1994)
-
[Publications] 吉田仙: "並行プロセス計算の開発・利用支援環境" 電子情報通信学会コンピュテーション研究会技術報告. COMP93-85. 65-72 (1994)
