代数的並行プロセス自動合成のための時制論理に基づいた新しい方法論の開発

开发基于时态逻辑的代数并行过程自动综合新方法

• 批准号: 05680262
• 负责人: 富樫 敦
• 金额: $ 0.9万
• 依托单位: Tohoku University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 1995
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-05680262/
• 关键词: 並行プロセス; 自動合成; 帰納推論; 時制論理; 等価性; μ計算; プロセス記述; プロセス計算; プロセス記述支援システム

本研究では,「高階の時制論理に基づき,大局的な時間的制約を陽に表現できる代数的並行プロセス記述システムを提案し,与えられた仕様から実際の並行プロセスを自動的に合成するための方法論を開発することを目的とする」.本年度は,次の研究項目を達成した.研究項目1並行プロセス記述支援システムの開発に関する継続研究研究項目2並行プロセス自動合成法の開発研究項目1については,μ計算における再帰の論理構造と大局的な時間的制約が記述できる高階の時制論理体系を提案し,プロセスによる充足可能性に関して健全かつ完全な証明システムを与えた.さらに,この論理体系に基づいて,検証システムなどを備えた記述言語を設計し,並行プロセス記述支援システムを完成させた.従来,並行プロセスための計算システムとしてCCS,CSP,LOTOS,CHOCSなどが有名である.上記システムを開発する際これらのシステムの機能を十分に反映させた.研究項目2については,タブロ-法のような反駁による方法と帰納推論による方法を有機的に統合させ,並行プロセスの代表的表現を自動的に合成する方法を開発した.反駁による方法は,研究項目1によるプロセス記述言語によって記述された並行プロセスの時間的な要求仕様から,プロセスの基本的な骨格を形成する方法である.帰納推論による方法は,プロセスの動作的振舞いに関する具体的な性質からプロセスの局所的な細部を確定していく方法である.両方法ともプロセスの同定基準である等価性を何に設定するかに大きく依存する.本研究では,等価性として最も代表的かつ重要な強等価性,弱等価性,合同等価性を主に検討した.

This study is aimed at developing a methodology for the automatic synthesis of high-order timing logic, global time constraints, algebraic parallel programming, and real-time parallel programming. This year, the second research project was completed. Research Project 1: Development of Parallel System Description Support System Research Project 2: Development of Parallel System Automatic Synthesis Method Research Project 1: Design of Logic Structure for μ Calculation and Time Restriction of Overall Situation; Design of High Order Timing Logic System; Sufficient Possibility of System Description; Complete Proof of System Design; In this paper, the logic system is based on the design of the test system, the preparation of the test system, the design of the test system, and the completion of the test system. CCS,CSP,LOTOS,CHOCS, etc. The function of the above system is fully reflected when it is opened. Research project 2: The development of methods for organic integration, parallel representation and automatic synthesis. The method of refuting this question is to study the method of forming the basic framework of the language description and the time requirement of the language description. The method of inference is to determine the specific nature of the motion of the object and the details of the object. How to set the equivalence of the method and the method? In this study, the most important representative of isotropy is discussed.

项目成果

Togashi,Atsushi: "On the relationship between Concurrent Process Calculi and Logic" Proc. of 6th Karuizawa Workshop on Circuits and Systems. 537-542 (1993)

Togashi，Atsushi：“论并发过程演算与逻辑之间的关系”Proc。

白井伸幸: "プロセス合成のための支援環境に関する研究" 電子情報通信学会コンピュテーション研究会技術報告. COMP93-84. 57-64 (1994)

Nobuyuki Shirai：“过程综合支持环境的研究”IEICE 计算研究组技术报告 57-64 (1994)。

B.B.Bista: "A new approach for protocol synthesis based on LOTOS" IEICE Trans on Fundamentals of Electronics,Communications and Computer Science. E77-A. 1646-1655 (1994)

B.B.Bista：“基于 LOTOS 的协议综合新方法”IEICE Trans 电子、通信和计算机科学基础知识。

Atsushi Togashi: "An Intelligent LOTOS interpreter in AMLOG" Proc.of Workshop on Logic Programming in Software Engineering. 70-80 (1994)

Atsushi Togashi：“AMLOG 中的智能 LOTOS 解释器”Proc.of 软件工程逻辑编程研讨会。

Atsushi Togashi: "Inductive Inference of Algebraic Process based on Henessy-Milner Logic" IEICE Trans on Fundamentals of Electronics,Communications and Computer Science. E77-A. 1594-1601 (1994)

Atsushi Togashi：“基于 Henessy-Milner 逻辑的代数过程的归纳推理”IEICE Trans 电子、通信和计算机科学基础知识。