規則性を持つ大規模な有限状態機械の形式的設計検証に関する研究

マルチ・プロセッサ・システムにおけるキャッシュ・プロトコルなどは、規則性を持つ大規模な回路ととらえることができる。こうした回路は、同一の有限状態のプロセスが多数接続されてできているとみなすことができる。本研究では、特にこのような回路を対象として、交付申請書に記載の通り、以下の研究を行った。有限状態のプロセスを任意個接続して構成されるシステムを対象として、時相論理や有限オートマトンによる仕様記述を与えた場合、検証問題は一般に決定不能になる。しかし実用的には、十分多数の有限個のプロセスを結合したシステムを考えれば十分なことが多い。この観点から、本研究では、与えられた有限状態機械を1つ接続するごとに最小化して、徐々に大規模な機械を構成してゆく手法を、二分決定グラフを用いて実装・評価を行った。この結果、多数の機械を接続した後、まとめて最小化するよりも、接続毎に最小化した場合の方が、より多数の有限状態機械を接続することができることが明らかとなった。また、このように接続を繰り返した場合、最小化が進むにつれて、有限状態機械の状態を表現するための状態変数の数が多くなり、また割り当てられた符号語がスパースになってゆく。そこで、二分決定グラフ上で符号の再割当を行って、状態変数の数を削減するアルゴリズムを考案・実装し、その結果、接続が進むにつれて、記憶量・時間量ともに改善されることを確認した。

マルチ・プロセッサ・システムにおけるキャッシュ・プロトコルなどは、規則性を持つ大規模な回路ととらえることができる。こうした回路は、同一の有限状態のプロセスが多数接続されてできているとみなすことができる。本研究では、特にこのような回路を対象として、交付申請書に記載の通り、以下の研究を行った。有限状態のプロセスを任意個接続して構成されるシステムを対象として、時相論理や有限オートマトンによる仕様記述を与えた場合、検証問題は一般に決定不能になる。しかし実用的には、十分多数の有限個のプロセスを結合したシステムを考えれば十分なことが多い。この観点から、本研究では、与えられた有限状態機械を1つ接続するごとに最小化して、徐々に大規模な機械を構成してゆく手法を、二分決定グラフを用いて実装・評価を行った。この結果、多数の機械を接続した後、まとめて最小化するよりも、接続毎に最小化した場合の方が、より多数の有限状態機械を接続することができることが明らかとなった。また、このように接続を繰り返した場合、最小化が進むにつれて、有限状態機械の状態を表現するための状態変数の数が多くなり、また割り当てられた符号語がスパースになってゆく。そこで、二分決定グラフ上で符号の再割当を行って、状態変数の数を削減するアルゴリズムを考案・実装し、その結果、接続が進むにつれて、記憶量・時間量ともに改善されることを確認した。