| 研究概要 |
本研究では,線形論理に基づいた並列プログラム設計法の開発,ならびにその方法にしたがう設計システムの実現を目的とした.本年度の研究は3つのステップに分けて実施し,それぞれ以下の結論を得た.
1.対象とする並列計算モデルと線形論理体系の考案
設計仕様の表現法には,並列計算に固有な動作が記述できるなどの性質が要求される。そのため,並列計算のためのモデル概念としてはペトリネットを,要求・条件の形式的記述や妥当性判定のために論理式を用いることとした.具体的には,ペトリネットで表現される並列動作や計算資源などを記述するために,古典論理の枠組としてではなく,線形論理に基づく論理体系とすることとし,直観主義的線形論理ILL^*を考案した.
2.ペトリネットのILL^*による記述と解析
ペトリネットとILL^*の対応関係について考察し,ペトリネットからILL^*への変換規則を考案した.そして,ペトリネットの可達性とILL^*の証明可能性が同値であることを明らかにした.
3.仕様のILL^*による記述とそれを実現するペトリネットの構成
ILL^*からペトリネットへの変換規則を考案した.これにより,対象とする並列システムの仕様をILL^*で記述すれば,それを実現するペトリネットが構成される.また,構成されたペトリネットが仕様を満足していることは,そのペトリネットに対応するILL^*が証明可能であることから保証される.
来年度以降は,考案した解析法および設計法の有効性を確かめるために,解析・設計システムの計算機上での実現を試みる.
|
