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

1994 Fiscal Year Annual Research Report

• Project/Area Number: 05680262
• Research Institution: Tohoku University
• Principal Investigator: 富樫 敦 東北大学, 電気通信研究所, 助教授 (20172140)
• Keywords: 並行プロセス / 自動合成 / 帰納推論 / 時制論理 / 等価性 / μ計算 / プロセス記述 / プロセス計算

Research Abstract

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

Research Products

• [Publications] Ushio Yamamoto: "A Support Method for Specifications based on LTSs" IEICE Trans on Fundamentals of Electronics,Communications and Computer Science. E77-A. 1656-1662 (1994)
• [Publications] 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)
• [Publications] 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)
• [Publications] Atsushi Togashi: "An Intelligent LOTOS interpreter in AMLOG" Proc.of Workshop on Logic Programming in Software Engineering. 70-80 (1994)
• [Publications] Sen Yoshida: "Integrated Support Environment for Concurrent Process Calculi" Proc.of ACM13th Ann.Symposium on Principle of Distributed Computing. 395-395 (1994)
• [Publications] B.B.Bista: "A Synthesis algorithm of a protocol model from a single entity" Proc.of Seventh International Conference on Formal Description Techniques. 467-482 (1994)
• [Publications] Shigetomo Kimura: "Synthesis Algorithm for Recursive Processes by μ-calculus" Proc.of the 5th International Workshop on Algorithmic Learning Theory,Lecture Notes in Artifical Intellegence. 872. 379-394 (1994)
• [Publications] Atsushi Togashi: "ProCSuS:A Meta System for Concurrent Profcess Calculi based on SOS" Proc.of Workshop on Theory and Practive of Parallel Programming. 207-214 (1994)
• [Publications] Ushio Yamamoto: "Similarity as Criterion of Communication Software Development" Proc.of the 9th International Conference on Infomation Networking(ICOIN-9). 377-382 (1994)
• [Publications] Atsushi Togashi: "A Derivation of System Specifications based on a Partial Logical Petri Net" Proc.of ISCAS95. - (1995)