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

点击翻译按钮获取中文摘要

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