モデル検査はソフトウェアシステムやハードウェアシステムの時相論理的な性 質を検証する技術であり，オートマトンを用いる手法，タブロー法などがある． オートマトンを用いる方法では，システムをオートマトンとして捉え，性質も オートマトンで表現し，それらの受理言語の共通集合が空であるか否かを判定 する．オートマトンを用いる方法は，モデル検査がオートマトンの 受理言語の空問題に帰着できるなど，オートマトン理論の成果を活用できると いう点では優れているが，システムが性質を満たすと きの検査結果は「Yes」という最低限の情報だけである． 検査結果が「No」のときはシステムが性質を満たさないという反例を返す． このことから，システムが性質を満たすという結論が 得られたとき，その証明を提示する方法が提案されている．生成された証明を 調べることにより，システムが性質を満たすことを直観的に理解でき，また， 証明は実際のシステムのオートマトンとしてのモデル化の妥当性を判断する際 の情報を提供する．一方，複雑なシステムの設計には，部分的な設計を組み合 わせて全体を設計するというモジュラーな設計手法が有効である．したがって， システムが部分の合成で設計されている場合のモジュラーな証明生成の方法を 開発することは有用である．モジュラーなシステム設計は並行合成などのシス テムの合成演算に基づいて行われる．本研究では，並行合成の特別な場合の 合成演算を定義し，証明生成の鍵となるオートマトンの極大強連結成分 を求めるアルゴリズムのモジュラー化を行う．得られたモジュラーなアルゴリ ズムは，合成後のシステムに対して証明生成を行うアルゴリズムに比べて 極大強連結成分を記憶するスタックが小さくてすむという 点で優れていることを示す．