• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 09780303
Research Category

Grant-in-Aid for Encouragement of Young Scientists (A)

Allocation TypeSingle-year Grants
Research Field 計算機科学
Research InstitutionIwate Prefectural University (1998)
Shizuoka Institute of Science and Technology (1997)

Principal Investigator

猪股 俊光  岩手県立大学, ソフトウェア情報学部, 助教授 (30213193)

Project Period (FY) 1997 – 1998
Project Status Completed (Fiscal Year 1998)
Budget Amount *help
¥1,700,000 (Direct Cost: ¥1,700,000)
Fiscal Year 1998: ¥600,000 (Direct Cost: ¥600,000)
Fiscal Year 1997: ¥1,100,000 (Direct Cost: ¥1,100,000)
Keywords線形論理 / ペトリネット / 可達性 / 形式的仕様記述 / 構成的設計法
Research Abstract

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

Report

(2 results)
  • 1998 Annual Research Report
  • 1997 Annual Research Report
  • Research Products

    (2 results)

All Other

All Publications (2 results)

  • [Publications] 堀本浩,猪股俊光: "線形論理を用いたペトリネットの解析と設計に関する考察" 電子情報通信学会技術研究報告. CST97-37. 41-50 (1998)

    • Related Report
      1998 Annual Research Report
  • [Publications] 堀本浩, 猪股俊光: "線形論理を用いたペトリネットの解析と設計に関する考察" 電子情報通信学会技術研究報告. CST97-37. 41-50 (1998)

    • Related Report
      1997 Annual Research Report

URL: 

Published: 1997-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi