線形論理に基づく並列プログラムの形式的設計法と並列計算機によるその実現

本研究では,線形論理に基づいた並列プログラム設計法の開発,ならびにその方法にしたがう設計システムの実現を目的とし,平成9年度から10年度にかけて下記の4つのステップに分けて実施し,それぞれ以下の結論を得た.1. 対象とする並列計算モデルと線形論理体系の考案並列計算のためのモデル概念としてはペトリネットを,要求・条件の形式的記述や妥当性判定のために論理式を用いることとし,ペトリネットで表現される並列動作や計算資源などを記述するための直観主義的線形論理ILL^*を考案した.2. ペトリネットのILL^*による記述と解析ペトリネットとILL^*の対応関係について考察し,ペトリネットからILL^*への変換規則を考案した.そして,ペトリネットの可達性とILL^*の証明可能性が同値であることを明らかにした.3. 仕様のILL^*による記述とそれを実現するぺトリネットの構成ILL^*からペトリネットへの変換規則を考案した.これにより,対象とする並列システムの仕様をILL^*で記述すれば,それを実現するペトリネットが構成される.4. ILL^*の証明の妥当性を検討するための証明チェッカの実現証明チェッカを利用することにより,可達性検証のための証明が正しいかなどを判定することができる.今後の課題として,ILL^*のための自動証明の処理系の開発があげられる.

本研究では,線形論理に基づいた並列プログラム設計法の開発,ならびにその方法にしたがう設計システムの実現を目的とし,平成9年度から10年度にかけて下記の4つのステップに分けて実施し,それぞれ以下の結論を得た.1. 対象とする並列計算モデルと線形論理体系の考案並列計算のためのモデル概念としてはペトリネットを,要求・条件の形式的記述や妥当性判定のために論理式を用いることとし,ペトリネットで表現される並列動作や計算資源などを記述するための直観主義的線形論理ILL^*を考案した.2. ペトリネットのILL^*による記述と解析ペトリネットとILL^*の対応関係について考察し,ペトリネットからILL^*への変換規則を考案した.そして,ペトリネットの可達性とILL^*の証明可能性が同値であることを明らかにした.3. 仕様のILL^*による記述とそれを実現するぺトリネットの構成ILL^*からペトリネットへの変換規則を考案した.これにより,対象とする並列システムの仕様をILL^*で記述すれば,それを実現するペトリネットが構成される.4. ILL^*の証明の妥当性を検討するための証明チェッカの実現証明チェッカを利用することにより,可達性検証のための証明が正しいかなどを判定することができる.今後の課題として,ILL^*のための自動証明の処理系の開発があげられる.