(57)【要約】【課題】ブルームフィルタを使用する訪問管理装置において、メモリ容量を増加せずに、探索のカバー率を向上させる。【解決手段】訪問管理装置は、状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成し、前記状態に対して所定の処理を実行し、初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持し、前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとし、所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする。【選択図】図１
2011107822.tif 000002
【特許請求の範囲】
【請求項１】
とりうる各状態を訪問して処理を実行する訪問管理装置であって、
状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成する状態生成手段と、
前記状態生成手段により生成された前記状態に対して所定の処理を実行する処理手段と、
初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持しており、前記状態生成手段により生成された前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとする訪問手段と、
所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする確率的クリア手段と、
を有する訪問管理装置。
【請求項２】
前記確率的クリア手段は、
所定の確率に基づいて、前記訪問手段によりオンとされたビットを削除するか否かを判断するとともに、該訪問手段により１つの状態が訪問済みとされたときにオンとされたビット数に応じて、オフにするビットの数を決定する状態削除判定手段と、
前記状態削除判定手段により削除すると判断されたならば、前記ブルームフィルタのオンのビットのうち、該削除判定手段により決定された数のビットをオフにする既訪状態削除手段と、
を有する、請求項１に記載の訪問管理装置。
【請求項３】
前記状態削除判定手段は、前記訪問手段により１つの状態が訪問済みとされるたびに、所定の確率に基づいて、前記訪問手段によりオンとされたビットを削除するか否かを判断する、請求項２に記載の訪問状態管理装置。
【請求項４】
前記既訪状態削除手段は、該削除判定手段により決定された数のビットを１ビットずつオフにし、
前記状態削除判定手段は、前記既訪状態削除手段により１ビットがオフにされるたびに、所定の確率に基づいて、前記訪問手段によりオンとされたビットを削除するか否かを判断する、請求項２に記載の訪問状態管理装置。
【請求項５】
前記訪問手段によりオンにされたビットの数を計数するオンビット数計数手段を更に有し、
前記確率的クリア手段は、前記オンビット数計数手段により計数された前記ビットの数が第１の閾値以上であれば、所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする、請求項１乃至４のいずれか１項に記載の訪問管理装置。
【請求項６】
前記訪問手段は、前記状態が未訪問の場合、該状態に対応するビットを所定の確率でオンにする、請求項１乃至５のいずれか１項に記載の訪問管理装置。
【請求項７】
前記訪問手段によりオンにされたビットの、前記ブルームフィルタにおける位置を保持する保持手段を更に有し、
前記確率的クリア手段は、所定の確率で、前記指標値取得手段により保持された前記位置にある、１つ以上のビットをクリアする、請求項１乃至６のいずれか１項に記載の既訪状態管理装置。
【請求項８】
状態生成手段が、状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成し、
処理手段が、前記状態生成手段により生成された前記状態に対して所定の処理を実行し、
訪問手段が、初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持しており、前記状態生成手段により生成された前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとし、
確率的クリア手段が、所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする、訪問管理方法。
【請求項９】
コンピュータに、
状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成する状態生成手順、
前記状態生成手順で生成された前記状態に対して所定の処理を実行する処理手順、
初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持しておき、前記状態生成手順で生成された前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとする訪問手順、
所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする確率的クリア手順、
を実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、システムのとりうる状態を抽出し、抽出された各状態を訪問するための技術に関する。
【背景技術】
【０００２】
分散システムやハードウェアの設計段階におけるシステムの検証手法の一つとしてモデル検査の手法が広く用いられている。この手法では、システムを有限状態の状態遷移グラフとしてモデルを記述しておき、その状態遷移グラフにおいて、モデル検査器は、各状態が、不変条件や時相論理式によって記述された形式仕様を満たすかどうかを検査する。
【０００３】
モデル検査の手法における課題の１つとして、状態爆発問題が挙げられる。この種のモデル検査は、状態を抽出しながら、抽出された状態を訪問し、検査を行う。システムが複雑になると探索すべき状態数は指数的に増加する。状態数の増加に伴い、検査に必要なメモリ量も増加する。そのため、検査するシステムの規模が大きくなると、検査の途中でメモリ不足となって探索が打ち切られることがある。その場合、モデル検査器は、検査において、ごく一部の探索空間しかカバーできないことになる。
【０００４】
このような状態爆発によるメモリ不足に対する対処法として様々な手法が考えられている。例えば、モデル検査ツールＳＰＩＮ（Simple Promela Interpreter）では、Ｂｉｔｓｔａｔｅ  Ｈａｓｈｉｎｇと呼ばれる手法で十分なメモリが確保できない状態での状態空間のカバー率向上を実現している。
【０００５】
ＳＰＩＮについて説明する。状態空間の網羅的探索を行うモデル検査では、遷移先の状態に既に訪問したかどうか、すなわち、探索において、その状態に到達したかどうかを確認するために、各状態の既訪状態を保存する必要がある。データ操作の効率を考えると、既訪状態を保存するためには、ハッシュテーブルを用いるのが一般的であるが、Ｂｉｔｓｔａｔｅ  Ｈａｓｈｉｎｇではブルームフィルタを用いて既訪状態を管理する。
【０００６】
ブルームフィルタは、ある要素が集合のメンバーであるか否かを判定するために使用されるデータ構造である。但し、ブルームフィルタは確率的データ構造であり、確率的に擬陽性による誤検出が生じる可能性がある。言い換えれば、既訪状態を確認するためにブルームフィルタを利用する場合において、未だ訪問していないにも関わらず、既に訪問済みと判断される可能性がある。
【０００７】
しかしながら、ブルームフィルタを使用すれば、訪問済みの状態を保存するために必要なデータ量は、ハッシュテーブルを用いる場合に比べ少なくて済む。このため、メモリが十分確保できない状況では、ハッシュテーブルよりも、ブルームフィルタを使用する方が、状態空間のカバー率が向上する。
【０００８】
図１２に、ブルームフィルタを使用する場合の、一般的なモデル検査器の動作手順を疑似コードとして示す。この動作手順は、初期状態ｓ０、状態遷移規則、および形式仕様を与えられ、検査開始が指示されたときに開始する。検査が開始されると、モデル検査器は、関数ｃｈｅｃｋ（ｓ）の再帰呼び出しによる深さ優先探索を用いて、初期状態ｓ０と状態遷移規則とから生成される各状態のうち、形式仕様に違反する状態を探索する。
【０００９】
ｃｈｅｃｋ（ｓ）は、与えられた状態ｓの遷移先状態の列Ｓを、状態遷移規則を利用して生成し（Ｌ０２）、列Ｓに属する、それぞれの要素（状態ｔ）について以下の処理を行う（Ｌ０３〜Ｌ１０）。
【００１０】
まず、モデル検査器は、状態ｔが形式仕様に違反しているかをチェックし（Ｌ０４）、違反している場合は、反例を報告し（Ｌ０５）、検査を終了する（Ｌ０６）。違反していない場合、次に状態ｔが訪問済みであるかどうかを判定する（Ｌ０７）。未訪問（未登録）と判定された場合（Ｌ０７：ＮＯ）、状態ｔを既訪状態判定部に登録し（Ｌ０８）、再帰的にｃｈｅｃｋ（ｔ）を実行する（Ｌ０９）。
【００１１】
簡単のため、ここでは、深さ優先探索を利用する場合の手順について説明したが、このほか、幅優先探索などのその他の探索アルゴリズムを用いる場合や、特許文献１に記載された検証処理装置のように、ＬＴＬ（Linear Temporal Logic）式を用いた検査を行う場合もある。
【先行技術文献】
【特許文献】
【００１２】
【特許文献１】特開２００８−７１１３５号公報
【発明の概要】
【発明が解決しようとする課題】
【００１３】
しかしながら、図１２で説明した手順などで、探索において、各状態を訪問したか否かをブルームフィルタで管理するモデル検査器においては、システムの規模がさらに大きくなると、探索におけるカバー率を十分に向上させることが困難になるという問題があった。
【００１４】
これは、システムが更に大規模化し、とりうる状態の数が多くなると、ブルームフィルタを用いてもメモリ不足が生じ、検査が途中で打ち切られるためである。
【００１５】
メモリを大きくすれば、カバー率は向上するが、コストや物理的制約から、大容量のメモリを設けることができない場合がある。ブルームフィルタを用いるモデル検査器では、メモリ容量を増加せずに、カバー率を向上させることが困難であった。
【００１６】
本発明は、各状態が訪問済みか否かを、ブルームフィルタを使用して管理する装置において、メモリ容量を増加せずに、探索のカバー率を向上させる技術を提供することを目的とする。
【課題を解決するための手段】
【００１７】
上記目的を達成するために、本発明の訪問管理装置は、とりうる各状態を訪問して処理を実行する訪問管理装置であって、状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成する状態生成手段と、前記状態生成手段により生成された前記状態に対して所定の処理を実行する処理手段と、初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持しており、前記状態生成手段により生成された前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとする訪問手段と、所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする確率的クリア手段と、を有する。
【００１８】
本発明の訪問管理方法は、状態生成手段が、状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成し、処理手段が、前記状態生成手段により生成された前記状態に対して所定の処理を実行し、訪問手段が、初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持しており、前記状態生成手段により生成された前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとし、確率的クリア手段が、所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする、訪問管理方法である。
【００１９】
本発明のプログラムは、コンピュータに、状態遷移規則に従って、未訪問の状態の遷移先の状態を回帰的に生成する状態生成手順、前記状態生成手順で生成された前記状態に対して所定の処理を実行する処理手順、初期値がオフの複数のビットのうち、状態に対応するビットをオンにして該状態が訪問済みであることを確率的に示すブルームフィルタを保持しておき、前記状態生成手順で生成された前記状態に対応するビットがオンであるか否かに基づいて、該状態が訪問済みであるか否かを判断し、未訪問の場合、該状態に対応するビットをオンにすることで、該状態を訪問済みとする訪問手順、所定の確率で、前記訪問手段によりオンとされた前記ビットのうち、１つ以上のビットをオフにする確率的クリア手順、を実行させるためのプログラムである。
【発明の効果】
【００２０】
本発明によれば、訪問管理装置は、ブルームフィルタのオンのビットのうち、１つ以上のビットを確率的にオフにするので、従来手法ではハッシュ値の衝突により探索が行われなかった状態を訪問できる確率が上がるため、探索のカバー率が向上する。
【図面の簡単な説明】
【００２１】
【図１】本発明の第１の実施形態のモデル検査器の一構成例を示すブロック図である。
【図２】本発明の第１の実施形態の既訪状態判定処理を示すフローチャートである。
【図３】本発明の第１の実施形態の状態削除判定処理を示すフローチャートである。
【図４】本発明の第１の実施形態のランダムクリア処理を示すフローチャートである。
【図５】本発明の変形例の状態削除判定処理を示すフローチャートである。
【図６】本発明の第２の実施形態のモデル検査器の一構成例を示すブロック図である。
【図７】本発明の第２の実施形態の既訪状態判定処理を示すフローチャートである。
【図８】本発明の第２の実施形態の状態追加判定処理を示すフローチャートである。
【図９】本発明の第３の実施形態のモデル検査器の一構成例を示すブロック図である。
【図１０】本発明の第３の実施形態の既訪状態判定処理を示すフローチャートである。
【図１１】本発明の第３の実施形態の状態削除判定処理を示すフローチャートである。
【図１２】一般的なモデル検査器の動作手順を示す疑似コードである。
【発明を実施するための形態】
【００２２】
（第１の実施形態）
本発明を実施するための第１の実施形態について図面を参照して詳細に説明する。図１は、本実施形態のモデル検査器１の一構成例を示すブロック図である。モデル検査器１は、ブルームフィルタを使用して、システムの各状態が形式仕様に違反しないか否かを検査するための装置である。
【００２３】
モデル検査器１は、遷移状態生成部１０、遷移状態検査部２０、および既訪状態判定部３０を有する。そして、既訪状態判定部３０は、ブルームフィルタ登録部３０１、既訪状態カウンタ３０２、状態削除判定部３０３、および既訪状態削除部３０４を有する。ブルームフィルタ登録部３０１は、ブルームフィルタを保持している。
【００２４】
遷移状態生成部１０は、所定の遷移生成規則を用いて、状態ｓが入力されたとき、その状態ｓの遷移先状態の列Ｓを生成する。この遷移先状態の列Ｓは、入力された状態ｓに対して、ある特定の順序に整列されていてもよいし、生成毎にランダムに順序が異なっていてもよい。
【００２５】
そして、遷移状態検査部２０は、生成された各状態について、形式仕様に違反するか否かを判断（検査）する。形式仕様に違反する状態があれば、遷移状態検査部２０は、反例を出力する。遷移状態生成部１０は、形式仕様に違反しない状態について、その状態が訪問済みであるか否かを判定する。
【００２６】
ここで、「訪問」とは、生成された遷移先の状態の集合の探索において、ある状態に到達したことを意味する。訪問された状態は、ブルームフィルタ登録部３０１でブルームフィルタに登録される。
【００２７】
より具体的に説明すると、遷移状態生成部１０は、ブルームフィルタ登録部３０１へ状態を出力し、ブルームフィルタ登録部３０１に、状態がブルームフィルタに登録（追加）されているか否かを判断させる。そして、遷移状態生成部１０は、その結果から、状態が訪問済みであるか否かを判定する。
【００２８】
訪問済みでなければ、遷移状態生成部１０は、ブルームフィルタ登録部３０１に、その状態を登録させ、更にその遷移先の状態を生成する。訪問済みであれば、遷移状態生成部１０は、その状態の遷移先を生成しない。
【００２９】
遷移状態生成部１０、遷移状態検査部２０は、未訪問の遷移先状態が生成されなくなるまで上記の動作を繰り返す。
【００３０】
つまり、遷移状態生成部１０、遷移状態検査部２０は、深さ優先探索のアルゴリズムを使用して、形式仕様に違反する状態を検索する。
【００３１】
なお、遷移状態生成部１０、遷移状態検査部２０は、深さ優先探索に限らず、幅優先探索やＤＤＦＳ（Double Depth First Search）などのその他の探索アルゴリズムを利用して、形式仕様に違反する状態を検索してもよい。
【００３２】
ブルームフィルタ登録部３０１は、ブルームフィルタを保持し、遷移状態生成部１０の制御に従って、ブルームフィルタを操作する。
【００３３】
ここで、ブルームフィルタの構成、および操作について説明する。ブルームフィルタのデータ構造は長さがｍビットのビット列である。また、ブルームフィルタ登録部３０１は、出力する値の範囲が０からｍ−１であるｋ個のハッシュ関数、すなわち配列の添え字を出力するハッシュ関数を予め定義しておく。
【００３４】
ブルームフィルタ登録部３０１は、ブルームフィルタに対して、初期化、要素の追加、要素の検索の三つの操作を行う。本実施形態では、要素として、システムの各状態が入力される。ブルームフィルタを初期化する場合、ブルームフィルタ登録部３０１は、ｍビットのビット列をすべてオフにする。
【００３５】
状態をブルームフィルタに追加する場合、ブルームフィルタ登録部３０１は、追加する状態をｋ個のハッシュ関数に入力し、ｋ個のインデックスを得た後、それらのインデックスで特定される位置のビットを全てオンにする。
【００３６】
ここで、ビットのオンとは、ある要素がブルームフィルタの表す集合に含まれるときに、その要素のハッシュ値をインデックスとしたビットを初期状態から移行させた状態をいう。ビットのオフとは、初期のビットの状態をいう。例えば、ビットのオンを１、オフを０とする。
【００３７】
状態を検索する場合、ブルームフィルタ登録部３０１は、追加と同様に、検索する状態をｋ個のハッシュ関数に入力し、ｋ個のインデックスを得た後、それらで特定されるビットがすべてオン（１）であるかどうかを調べる。もし一つでもオフ（０）のビットがある場合、その状態はこれまで追加されていないことを意味する。一方、すべてのビットがオンである場合、その状態が追加された可能性がある。
【００３８】
これらの３つの操作の実行順番について説明する。ブルームフィルタ登録部３０１は、まず、ブルームフィルタを初期化する。状態が入力されたとき、ブルームフィルタ登録部３０１は、ブルームフィルタを検索し、その状態が登録されているか否かを判断する。
【００３９】
登録済でない場合、ブルームフィルタ登録部３０１は、その状態をブルームフィルタに登録する。
【００４０】
次に、既訪状態カウンタ３０２、および既訪状態削除部３０４について説明する。既訪状態カウンタ３０２は、ブルームフィルタのビット列のうち、オンのビット数を計数する。
【００４１】
状態削除判定部３０３は、既訪状態カウンタ３０２の値を監視し、その値が閾値α以上であるとき、ブルームフィルタ登録部３０１に登録されている状態を削除するか否かを確率に基づいて判断する。また、状態削除判定部３０３は、ブルームフィルタに状態が１つ登録されたときにオンとなったビットの数に応じて、クリアするオンビットの数を決定する。
【００４２】
状態削除判定部３０３が状態を削除すると判断したならば、既訪状態削除部３０４は、ブルームフィルタのうち、状態削除判定部３０３が決定した数のオンビットをクリアする。
【００４３】
ここで、閾値αの値は、ブルームフィルタのクリアの効率の観点から適切に選択する必要がある。ブルームフィルタのサイズがｍ（ビット）である場合、１ビットのクリアにかかる乱数の生成回数は、平均でｍ／α回となる。そのため、ｍ／αの値が２〜１００となるようにαを設定し、計算時間の増加を抑制することが望ましい。
【００４４】
続いて、図２を参照してモデル検査器１の動作について説明する。本実施形態のモデル検査器１の動作は、図１６のモデル検査器の動作手順のうち、Ｌ０７（if 状態ｔは未訪問）およびＬ０８（ｔを既訪状態として登録）の処理が異なる。この異なる部分について詳細に説明し、共通する部分については、説明を省略する。Ｌ０７,Ｌ０８の処理は、図２のフロ−チャートで示す既訪状態判定処理に置き換えられる。
【００４５】
図２を参照すると、既訪状態判定部３０は、ブルームフィルタを検索し、入力された状態が既に訪問済み、すなわち、ブルームフィルタに登録済であるか否かを判断する（ステップＳ１）。
【００４６】
状態が未訪問であれば（ステップＳ１：ＹＥＳ）、既訪状態判定部３０は、その状態をブルームフィルタに追加し、追加時にオンにしたビット数を変数Ｂに保持する（ステップＳ２）。
【００４７】
既訪状態判定部３０は、オンとなったビット数で既訪状態カウンタ３０２の値を更新する（ステップＳ３）。既訪状態判定部３０は、更新後の既訪状態カウンタ３０２の値が、閾値α以上であるか否かを判断する（ステップＳ４）。
【００４８】
既訪状態カウンタ３０２の値が、閾値αより大きければ（ステップＳ４：ＹＥＳ）、既訪状態判定部３０は、状態削除判定処理を実行する（ステップＳ５）。
【００４９】
状態が訪問済みである場合（ステップＳ１：ＮＯ）、または既訪状態カウンタ３０２の値が、閾値α未満である場合（ステップＳ４：ＮＯ）、或いはステップＳ５の後、既訪状態判定部３０は、既訪状態判定処理を終了する。
【００５０】
図３は、状態削除判定処理を示すフローチャートである。同図を参照すると、既訪状態判定部３０は、０以上、且つ１未満の乱数を生成し、Ｒｐに設定する（ステップＳ５１）。既訪状態判定部３０は、Ｒｐが、予め定めておいた値Ｐ未満であるか否かを判断する（ステップＳ５２）。
【００５１】
ＲｐがＰ未満であれば（ステップＳ５２：ＹＥＳ）、既訪状態判定部３０は、ブルームフィルタのオンビットを１ビットだけランダムにクリアするランダムクリア処理を実行する（ステップＳ５３）。
【００５２】
ランダムクリア処理実行後、既訪状態判定部３０は、既訪問状態カウンタ３０２、および変数Ｂの値をデクリメントする（ステップＳ５４）。
【００５３】
既訪状態判定部３０は、変数Ｂの値が０であるか否かを判断する（ステップＳ５５）。変数Ｂの値が０でなければ（ステップＳ５５：ＮＯ）、既訪状態判定部３０は、ステップＳ５３に戻る。
【００５４】
ＲｐがＰ以上である場合（ステップＳ５２：ＮＯ）、または、変数Ｂの値が０である場合（ステップＳ５５：ＹＥＳ）、既訪状態判定部３０は、状態削除判定処理を終了する。
【００５５】
図４は、ランダムクリア処理を示すフローチャートである。同図を参照すると、既訪状態判定部３０は、０〜ｍ−１のうち、いずれかの値をとる乱数を生成し、Ｒに代入する（ステップＳ５３１）。
【００５６】
既訪状態判定部３０は、ブルームフィルタのビット列のうち、Ｒビット目がオンであるか否かを判断する（ステップＳ５３２）。Ｒビット目がオンでなければ（ステップＳ５３２：ＮＯ）、既訪状態判定部３０は、ステップＳ５３１に戻る。
【００５７】
Ｒビット目がオンであれば（ステップＳ５３２：ＹＥＳ）、既訪状態判定部３０は、そのビットをオフにする（ステップＳ５３３）。ステップＳ５３３の後、既訪状態判定部３０は、ランダムクリア処理を終了する。
【００５８】
なお、本実施形態では、システムの各状態を訪問したか否かをブルームフィルタで管理するモデル検査器に本発明を適用している。しかし、状態に相当する要素がある条件を満たすか否かの探索において、各要素を訪問したか否かをブルームフィルタで管理する装置であれば、モデル検査器以外の訪問管理装置にも本発明を適用できる。
【００５９】
本実施形態では、遷移状態検査部２０が各状態を検査する構成としているが、各状態について、状態の初期化など、検査の代わりに他の処理を行う構成としてもよい。
【００６０】
また、本実施形態では、図３のステップＳ５１、Ｓ５２で示したように、１回の確率的判断によって、オンビットをクリアしているが、図５に示すように、１ビット毎に、乱数を生成し、クリアするか否かを判断する構成としてもよい。
【００６１】
本実施形態では、モデル検査器１に既訪状態カウンタ３０２を設けているが、第３の実施形態で後述するように、モデル検査器１に、既訪状態カウンタ３０２を設けない構成とすることもできる。
【００６２】
本実施形態の遷移状態生成部１０が本発明の状態生成手段に該当し、本実施形態の遷移状態検査部２０が本発明の処理手段に該当する。また、本実施形態のブルームフィルタ登録部３０１が本発明の訪問手段に該当する。本実施形態のオンビット数は、本発明の指標値の一例である。本実施形態の状態削除判定部３０３及び既訪状態削除部３０４が本発明の確率的クリア手段に該当する。
【００６３】
以上説明したように、本実施形態によれば、モデル検査器１（訪問管理装置）は、ブルームフィルタのオンのビットのうち、１つ以上のビット確率的にオフにするので、従来手法ではハッシュ値の衝突により探索が行われなかった状態を訪問できる確率が上がるため、探索のカバー率が向上する。
【００６４】
モデル検査器１は、状態の登録で立てたブルームフィルタのビットを、確率Ｐでクリアする。このため、ブルームフィルタに１つの状態を追加するときのオンビット数をＢとすると、ブルームフィルタのオンビット数は、１つの状態を追加するたびに、Ｂ（１−Ｐ）ビットだけ増加する。Ｐが１のときビット数の増加は０になるが、その場合ブルームフィルタが訪問済みと判断する確率が一定になってしまうため、探索が長時間に及び、最悪の場合停止しない可能性がある。Ｐを１未満の値とすることで、訪問済みと判断する確率は、ある状態をブルームフィルタが未訪問と判断するたびに確率的に増加していくため、このリスクを抑えることができる。
【００６５】
また、モデル検査器１は、ブルームフィルタに登録された状態をランダムに削除するので、従来手法では、ハッシュ値の衝突によって訪問済みと見なされ探索が行われなかった状態とその遷移先の状態について、確率的に訪問することができる。この結果、状態探索のカバー率が向上する。
【００６６】
更に、ランダムな既訪状態の削除によって、個々の検査における既訪状態か否かの判定は必ずしも同一ではなくなる。そのため、複数回の検査により以前の検査で訪問できなかった状態に訪問する可能性が生じ、結果として複数回の検査によってカバー率を向上できる。また、複数のモデル検査器を並列実行する場合は、いずれかひとつのモデル検査器が反例を返した時点で検査を終了するように構成することで、反例が存在する場合の応答性を高めることができる。
【００６７】
（第２の実施形態）
本発明の第２の実施形態について図６〜図８を参照して詳細に説明する。本実施形態のモデル検査器１ａは、状態をブルームフィルタに追加する場合に、確率的に追加する点で、第１の実施形態のモデル検査器１と異なる。なお、本実施形態のモデル検査器１ａについて、図１〜図４で説明した構成と同様の処理の詳細な説明を省略し、第１の実施形態と異なる点について詳しく説明する。
【００６８】
図６は、モデル検査器１ａの一構成例を示すブロック図である。同図を参照すると、モデル検査器１ａは、状態追加判定部３０５を更に有する以外は、第１の実施形態のモデル検査器１と同様である。
【００６９】
状態追加判定部３０５は、遷移状態生成部１０により状態が未訪問であると判定されたとき、その状態をブルームフィルタに追加するか否かを確率に基づいて判断する。
【００７０】
状態追加判定部３０５により状態を追加すると判断されたのであれば、遷移状態生成部１０は、ブルームフィルタ登録部３０１に、その状態を登録させ、更にその遷移先の状態を生成する。
【００７１】
図７は、本実施形態の既訪状態判定処理を示すフローチャートである。同図を参照すると、本実施形態の既訪状態判定処理は、ステップＳ２、Ｓ３の代わりにステップＳ２ａを実行する点以外は、図２で示した第１の実施形態の既訪状態判定処理と同様である。
【００７２】
状態が未訪問であれば（ステップＳ１：ＮＯ）、既訪状態判定部３０は、その状態をブルームフィルタに追加するか否かを判定するための状態追加判定処理（ステップＳ２ａ）を実行し、ステップＳ４を実行する。
【００７３】
図８は、状態追加判定処理を示すフローチャートである。既訪状態判定部３０は、０以上、且つ１未満の乱数を生成し、Ｒｑに設定する（ステップＳ２１）。状態追加判定部３０５は、Ｒｑが、予め定めておいた値Ｑ未満であるか否かを判断する（ステップＳ２２）。
【００７４】
ここで、Ｑは、０以上、且つ１未満の値であり、モデル検査器１ａは、Ｑをモデル検査の開始時に指定してもよいし、動的に変更してもよい。
【００７５】
ＲｑがＱ未満であれば（ステップＳ２２：ＹＥＳ）、既訪状態判定部３０は、未訪問の状態をブルームフィルタに追加し、追加時にオンにしたビット数を変数Ｂに保持する（ステップＳ２３）。
【００７６】
既訪状態判定部３０は、オンとなったビット数で既訪状態カウンタ３０２の値を更新する（ステップＳ２４）。
【００７７】
ＲｑがＱ以上である場合（ステップＳ２２：ＮＯ）、またはステップＳ２４の後、既訪状態判定部３０は、状態追加判定処理を終了する。
【００７８】
以上説明したように、本実施形態によれば、モデル検査器１ａは、状態が未訪問であれば、その状態をブルームフィルタに確率的に登録するので、オンビット数の増加数を抑えることができる。これにより、モデル検査器１ａは、探索序盤における未訪問の状態を訪問済みと判断する確率を下げることができ、結果的にカバー率を向上することができる。
【００７９】
（第３の実施形態）
本発明の第３の実施形態について図９〜図１２を参照して詳細に説明する。本実施形態のモデル検査器１ｂは、生成したハッシュ値の一部をキャッシュに保持しておき、要素の削除時に、キャッシュからハッシュ値を選択し、選択した値に対応する要素を削除する点で、第１の実施形態のモデル検査器１と異なる。なお、本実施形態のモデル検査器１ｂについて、図１〜図４で説明した構成と同様の処理の詳細な説明を省略し、第１の実施形態と異なる点について詳しく説明する。
【００８０】
図９は、モデル検査器１ｂの一構成例を示すブロック図である。同図を参照すると、モデル検査器１ａは、既訪状態カウンタ３０２の代わりに既訪状態キャッシュ３０２ｂを有する以外は、第１の実施形態のモデル検査器１と同様である。
【００８１】
既訪状態キャッシュ３０２ｂは、ブルームフィルタのオンビットの一部に対応するハッシュ値を保持する。既訪状態キャッシュ３０２ｂは、最大値以下の数の個数のハッシュ値しか保持しないように置換アルゴリズムにより管理される。メモリの利用を抑えるため、キャッシュに保持する、ハッシュ値の個数の最大値は、ブルームフィルタのサイズよりも小さな値に設定される。
【００８２】
既訪状態削除部３０４は、状態削除判定部３０３が状態を削除すると判断したとき、既訪状態キャッシュ３０２ｂに保持されたハッシュ値の中から、いずれか１つのハッシュ値をランダムに選択する。既訪状態削除部３０４は、ブルームフィルタのオンビットのうち、選択したハッシュ値に対応するオンビットをクリアする。既訪状態削除部３０４は、これらの処理を状態削除判定部３０３が決定した数のオンビットがクリアされるまで繰り返す。
【００８３】
図１０および図１１を参照して、モデル検査器１ｂの動作について説明する。図１０は、本実施形態の既訪状態判定処理の構成を示すフローチャートである。同図を参照すると、本実施形態の既訪状態判定処理は、ステップＳ３、Ｓ４、およびＳ５の代わりに、ステップＳ４ｂ、およびＳ５ｂを実行する以外は、図２で示した第１の実施形態の既訪状態判定処理と同様である。
【００８４】
既訪状態判定部３０は、未訪問の状態をブルームフィルタに追加し、追加時にオンにしたビット数を変数Ｂに保持する（ステップＳ２）。そして、既訪状態判定部３０は、要素の登録のために生成したハッシュ値を既訪状態キャッシュ３０２ｂに保持する（ステップＳ４ｂ）。そして、既訪状態判定部３０は、状態削除判定処理を実行する（ステップＳ５ｂ）。
【００８５】
図１１は、本実施形態の状態削除判定処理を示すフローチャートである。同図を参照すると、本実施形態の状態削除判定処理は、ステップＳ５３の代わりに、ステップＳ５３１、Ｓ５３２、およびＳ５３３を実行する点以外は、図３で説明した第１の実施形態の状態削除判定処理と同様である。
【００８６】
ＲｐがＰ未満であれば（ステップＳ５２：ＹＥＳ）、既訪状態判定部３０は、既訪状態キャッシュ３０２ｂに保持されたハッシュ値の中から、いずれか１つをランダムに選択する（ステップＳ５３１）。
【００８７】
既訪状態判定部３０は、ステップＳ５３ｂで選択したハッシュ値に対応するオンのビットを、ブルームフィルタから削除する（ステップＳ５３２）。
【００８８】
既訪状態判定部３０は、ステップＳ５３ｂで選択したハッシュ値を、既訪状態キャッシュ３０２ｂから削除する（ステップＳ５３３）。
【００８９】
そして、既訪状態判定部３０は、既訪問状態カウンタ３０２、および変数Ｂの値をデクリメントする（ステップＳ５４）。
【００９０】
オンビットの数を閾値α以下とする効果について説明する。本実施形態では、前述したように、既訪状態キャッシュ３０２ｂが保持するハッシュ値の数は、ブルームフィルタのビット数より小さくしている。このため、ブルームフィルタにおいて、既訪状態キャッシュ３０２ｂに保持されないオンビットが生じ、このオンビットがクリアされなくなってしまう問題が生じる可能性がある。しかし、オンビットの数が閾値α以下となるように、ブルームフィルタへの登録を制限することにより、この問題を防ぐことができる。
【００９１】
以上説明したように、本実施形態によれば、モデル検査器１ｂは、既訪状態キャッシュ３０２ｂを利用して、クリアするオンビットを選択する。この構成によれば、既訪状態キャッシュ３０２ｂのためにメモリを消費するというデメリットはあるが、クリアするオンビットを効率的に選択することができ、処理速度が向上する。
【００９２】
なお、ＣＰＵ（Central Processing Unit）、メモリ、およびコンピュータプログラムを格納した記憶装置を備えたコンピュータをモデル検査器として使用することができる。その場合、図２〜図５、図７、図８、図１０、図１１、および図１２に示したフローチャートは、モデル検査器がコンピュータプログラムを実行することにより実現される。しかし、これらのフローチャートの全部または一部は、モデル検査器内部に、制御回路を設け、その制御回路により実現することもできる。
【符号の説明】
【００９３】
１、１ａ、１ｂ    モデル検査器
１０    遷移状態生成部
２０    遷移状態検査部
３０    既訪状態判定部
３０１    ブルームフィルタ登録部
３０２    既訪状態カウンタ
３０３    状態削除判定部
３０４    既訪状態削除部
３０５    状態追加判定部
【図１】
2011107822.tif 000003
【図２】
2011107822.tif 000004
【図３】
2011107822.tif 000005
【図４】
2011107822.tif 000006
【図５】
2011107822.tif 000007
【図６】
2011107822.tif 000008
【図７】
2011107822.tif 000009
【図８】
2011107822.tif 000010
【図９】
2011107822.tif 000011
【図１０】
2011107822.tif 000012
【図１１】
2011107822.tif 000013
【図１２】
2011107822.tif 000014