並行システムを解析するための逐次化と状態削減機能の実装－仕様の自動生成を目指して

摘要

並行システムは逐次システムに比べてその全体の動作を把握することが難しい．そこで，並行システムが仕様を満たすことを判定するためのツールが利用されている．しかし，実際にはそのような仕様を記述することは，並行システムのモデル化よりも難しいことが多い．本報告書では，並行システムのモデルから仕様を自動生成するために，記号処理によって並行動作の逐次化と状態数削減をする手法を提案し，本手法を実装したツールについて報告する．