| 研究概要 |
本研究では,「高階の時制論理に基づき,大局的な時間的制約を陽に表現できる代数的並行プロセス記述システムを提案し,与えられた仕様から実際の並行プロセスを自動的に合成するための方法論を開発することを目的とする」.本年度は,次の研究項目を達成した.
研究項目0並行プロセスの帰納推論に関する継続研究
研究項目1並行プロセス記述支援システムの開発
並行プロセスの帰納推論に関しては,これまで強等価性に関する基本プロセスの推論法を中心に研究してきた.本年度は,より複雑なプロセスまでその範囲を広げた.具体的には,対象を再帰を許した再帰プロセスまで対象を広げ,強等価を同定基準とした場合と,強等価性以外の等価性も考慮した場合の帰納推論法について検討した.また,計算機上に合成アルゴリズムをPrologを用いて実際に実装し,具体例を通してアルゴリズムの妥当性を実証した.
研究項目1については,μ計算における再帰の論理構造と大局的な時間的制約が記述できる高階の時制論理体系を提案し,プロセスによる充足可能性に関して健全かつ完全な証明システムを与えた.さらに,この論理体系に基づいて,検証システムなどを備えた記述言語を設計し,並行プロセス記述支援システムを完成させた.従来,並行プロセスための計算システムとしてCCS,CSP,LOTOS,CHOCSなどが有名である.上記システムを開発する際これらのシステムの機能を十分に反映させた.
最後に,一般の並行プロセス計算を対象とした汎用の並行プロセス計算システムを設計し,実際にシステムを試作した.また,CCS,LOTOS,π計算などの実際の並行計算を具体的に記述することにより,提案したシステムの妥当性を確認した.
|
