(57)【要約】【課題】検証対象となるシステムに対する検証パフォーマンスを向上させる。【解決手段】複数の状態間の遷移を表現した状態遷移モデルを記憶したリレーショナルデータベースと、CTL式により記述した、前記状態遷移モデルの検証条件の入力を受け付ける検証条件受付手段と、前記検証条件を解析することにより、それぞれ論理式が対応付けられた複数のノードを含む構文木を生成し、親ノードの論理式は、子ノードに対応する論理式と、前記親ノードに割り当てられた演算子とに基づいて定義される、構文解析手段と、前記構文木の各ノードに対応する論理式を充足する状態を検索する検索文を生成する検索文生成手段と、前記リレーショナルデータベースに対して各検索文を、前記構文木における葉ノードからルートノードへ向けて階層の深いノード順に実行することにより、各前記検索文に対応する状態をそれぞれ取得する検索実行手段とを備える。【選択図】図１
2009265996.tif 000002
【特許請求の範囲】
【請求項１】
複数の状態間の遷移を表現した状態遷移モデルを記憶した第１のリレーショナルデータベースと、
計算木論理（CTL：Computational Tree Logic）式により記述した、前記状態遷移モデルの検証条件の入力を受け付ける検証条件受付手段と、
前記検証条件受付手段に入力された前記検証条件を解析することにより、それぞれ論理式が対応付けられた複数のノードを含む構文木を生成し、親ノードの論理式は、子ノードに対応する論理式と、前記親ノードに割り当てられた演算子とに基づいて定義される、構文解析手段と、
前記構文木の各ノードに対応する論理式を充足する状態を検索する検索文を、前記親ノードの検索文が、前記親ノードの前記子ノードに対応する論理式の出力を引数とするように生成する検索文生成手段と、
前記第１のリレーショナルデータベースに対して、前記検索文生成手段により生成された各検索文を、前記構文木における葉ノードからルートノードへ向けて階層の深いノード順に実行することにより、各前記検索文に対応する状態をそれぞれ検索結果として取得する検索実行手段と、
少なくとも前記構文木のルートノードに対応する検索結果を出力する検索結果出力手段と、
を備えた検証装置。
【請求項２】
各前記検索文に対する検索結果を、各前記検索文に対応する論理式または前記論理式の識別子と関連づけて記憶する第２のリレーショナルデータベースをさらに備え、
前記検索文生成手段は、
前記構文木のノードをルートから葉へ向けて階層が浅い順番に読み取り、読み取ったノードに対応する対象論理式またはその識別子が前記第２のリレーショナルデータベースに記憶されているか否かを検査し、
記憶されているときは、前記読み取ったノードの子孫を削除し、前記読み取ったノードに対応する前記対象論理式を、前記対象論理式に関連づけられた前記検索結果への参照に更新し、
前記検索実行手段は、前記検索結果への参照へ更新されたノードについては、前記第２のリレーショナルデータベースを参照することにより前記検索結果を取得する、
ことを特徴とする請求項１に記載の検証装置。
【請求項３】
前記論理式をドモルガンの法則に基づく書き換え規則により書き換えることにより前記論理式の第１等価式および前記論理式の否定の第２等価式を生成する論理式生成手段をさらに備え、
前記検索文生成手段は、前記対象論理式またはその識別子が記憶されていないとき
（１）前記対象論理式の第１等価式が前記第２のリレーショナルデータベースに記憶されているときは、前記読み取ったノードの子孫を削除しかつ前記対象論理式を前記対象論理式の第１等価式の検索結果への参照に置換し、
（２）前記対象論理式の第１等価式が記憶されておらずかつ前記対象論理式の第２等価式が記憶されているときは、前記読み取ったノードの子孫を削除し、前記読み取ったノードに対応する前記対象論理式を前記第１等価式に置換しかつ前記読み取ったノードの子として前記対象論理式の第２等価式の検索結果への参照を示す第２ノードを追加する、
ことを特徴とする請求項２に記載の検証装置。
【請求項４】
前記検索文生成手段は、前記読み取ったノードに割り当てられた演算子が否定演算子と異なるときのみ前記（２）の処理を行うことを特徴とする請求項３に記載の検証装置。
【請求項５】
再帰制御手段をさらに備え、
前記検索文生成手段は、前記（１）および（２）のいずれの条件も満たされないときは、
前記対象論理式に含まれる部分論理式が前記第２のリレーショナルデータベースに記憶されているかどうかを検査し、記憶されているときは前記部分論理式に対応する検索結果を参照することにより前記部分論理式を満たす状態数を取得し、前記読み取ったノードに割り当てられた演算子と、取得した状態数とに基づいて前記対象論理式の処理コストを計算し、
前記第１等価式または前記第２等価式についてもその部分論理式が前記第２のリレーショナルデータベースに記憶されているときは前記対象論理式と同様にしてその処理コストを計算し、
前記第１等価式または第２等価式の処理コストの方が前記対象論理式の処理コストよりも小さいときは、前記（１）または（２）と同様にして、前記構文木を更新し、
前記再帰制御手段は、前記対象論理式、第１等価式および第２等価式のうち、前記第２のリレーショナルデータベースに記憶されていないために処理コストが計算されなかった第２の対象論理式については、前記第２の対象論理式の部分論理式をルートに割り当てた構文木を取得し、取得した構文木に対して再帰的に前記検索文生成手段による処理を行うように制御し、
前記検索文生成手段は、再帰処理の後、前記第２のリレーショナルデータベースにアクセスして前記第２の対象論理式に対応する検索結果を参照することにより前記第２の対象論理式を満たす状態数を取得する
ことを特徴とする請求項３または４に記載の検証装置。
【請求項６】
複数の状態間の遷移を表現した状態遷移モデルを記憶した第１のリレーショナルデータベースを準備する準備ステップと、
計算木論理（CTL：Computational Tree Logic）式により記述した、前記状態遷移モデルの検証条件の入力を受け付ける検証条件受付ステップと、
前記検証条件受付ステップで入力された前記検証条件を解析することにより、それぞれ論理式が対応付けられた複数のノードを含む構文木を生成し、親ノードの論理式は、子ノードに対応する論理式と、前記親ノードに割り当てられた演算子とに基づいて定義される、構文解析ステップと、
前記構文木の各ノードに対応する論理式を充足する状態を検索する検索文を、前記親ノードの検索文が、前記親ノードの前記子ノードに対応する論理式の出力を引数とするように生成する検索文生成ステップと、
前記第１のリレーショナルデータベースに対して、前記検索文生成ステップにより生成された各検索文を、前記構文木における葉ノードからルートノードへ向けて階層の深いノード順に実行することにより、各前記検索文に対応する状態をそれぞれ検索結果として取得する検索実行ステップと、
少なくとも前記構文木のルートノードに対応する検索結果を出力する検索結果出力ステップと
を備えた検証方法。
【請求項７】
各前記検索文に対する検索結果を、各前記検索文に対応する論理式または前記論理式の識別子と関連づけて第２のリレーショナルデータベースに記憶する記憶ステップと、をさらに備え、
前記検索文生成ステップは、
前記構文木のノードをルートから葉へ向けて階層が浅い順番に読み取り、読み取ったノードに対応する対象論理式またはその識別子が前記第２のリレーショナルデータベースに記憶されているか否かを検査し、
記憶されているときは、前記読み取ったノードの子孫を削除し、前記読み取ったノードに対応する前記対象論理式を、前記対象論理式に関連づけられた前記検索結果への参照に更新し、
前記検索実行ステップは、前記検索結果への参照へ更新されたノードについては、前記第２のリレーショナルデータベースを参照することにより前記検索結果を取得する、
ことを特徴とする請求項６に記載の検証方法。
【請求項８】
前記論理式をドモルガンの法則に基づく書き換え規則により書き換えることにより前記論理式の第１等価式および前記論理式の否定の第２等価式を生成する論理式生成ステップをさらに備え、
前記検索文生成ステップは、前記対象論理式またはその識別子が記憶されていないとき
（１）前記対象論理式の第１等価式が前記第２のリレーショナルデータベースに記憶されているときは、前記読み取ったノードの子孫を削除しかつ前記対象論理式を前記対象論理式の第１等価式の検索結果への参照に置換し、
（２）前記対象論理式の第１等価式が記憶されておらずかつ前記対象論理式の第２等価式が記憶されているときは、前記読み取ったノードの子孫を削除し、前記読み取ったノードに対応する前記対象論理式を前記第１等価式に置換しかつ前記読み取ったノードの子として前記対象論理式の第２等価式の検索結果への参照を示す第２ノードを追加する、
ことを特徴とする請求項７に記載の検証方法。
【請求項９】
前記検索文生成ステップは、前記読み取ったノードに割り当てられた演算子が否定演算子と異なるときのみ前記（２）の処理を行うことを特徴とする請求項８に記載の検証方法。
【請求項１０】
再帰制御ステップをさらに備え、
前記検索文生成ステップは、前記（１）および（２）のいずれの条件も満たされないときは、
前記対象論理式に含まれる部分論理式が前記第２のリレーショナルデータベースに記憶されているかどうかを検査し、記憶されているときは前記部分論理式に対応する検索結果を参照することにより前記部分論理式を満たす状態数を取得し、前記読み取ったノードに割り当てられた演算子と、取得した状態数とに基づいて前記対象論理式の処理コストを計算し、
前記第１等価式または前記第２等価式についてもその部分論理式が前記第２のリレーショナルデータベースに記憶されているときは前記対象論理式と同様にしてその処理コストを計算し、
前記第１等価式または第２等価式の処理コストの方が前記対象論理式の処理コストよりも小さいときは、前記（１）または（２）と同様にして、前記構文木を更新し、
前記再帰制御ステップは、前記対象論理式、第１等価式および第２等価式のうち、前記第２のリレーショナルデータベースに記憶されていないために処理コストが計算されなかった第２の対象論理式については、前記第２の対象論理式の部分論理式をルートに割り当てた構文木を取得し、取得した構文木に対して再帰的に前記検索文生成ステップによる処理を行うように制御し、
前記検索文生成ステップは、再帰処理の後、前記第２のリレーショナルデータベースにアクセスして前記第２の対象論理式に対応する検索結果を参照することにより前記第２の対象論理式を満たす状態数を取得する
ことを特徴とする請求項８または９に記載の検証方法。
【請求項１１】
請求項６ないし１０のいずれか一項に記載の各ステップをコンピュータに実行させるための検証プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検査装置、検証方法および検証プログラムに関し、たとえばソフトウェアを始めとするシステム開発において、仕様の正しさを検証する手法の一つであるモデル検査に関する。
【背景技術】
【０００２】
モデル検査は、システムがある一定条件下でとり得る全状態及び状態遷移に関して、検証条件の充足性を網羅的に検証する手法である。モデル検査は、仕様から有限状態遷移系を生成する段階と、計算木論理式(CTL)で記述された検証条件を検証する段階から構成される。従来のモデル検査では、検証対象システムの規模が大規模化すると状態爆発が発生し、その検証が困難化若しくはパフォーマンスが著しく低下する問題があった。
【発明の開示】
【発明が解決しようとする課題】
【０００３】
本発明は、検証パフォーマンスを向上させることを可能とした検証装置、検証方法および検証プログラムを提供する。
【課題を解決するための手段】
【０００４】
本発明の一態様としての検証装置は、
複数の状態間の遷移を表現した状態遷移モデルを記憶した第１のリレーショナルデータベースと、
計算木論理（CTL：Computational Tree Logic）式により記述した、前記状態遷移モデルの検証条件の入力を受け付ける検証条件受付手段と、
前記検証条件受付手段に入力された前記検証条件を解析することにより、それぞれ論理式が対応付けられた複数のノードを含む構文木を生成し、親ノードの論理式は、子ノードに対応する論理式と、前記親ノードに割り当てられた演算子とに基づいて定義される、構文解析手段と、
前記構文木の各ノードに対応する論理式を充足する状態を検索する検索文を、前記親ノードの検索文が、前記親ノードの前記子ノードに対応する論理式の出力を引数とするように生成する検索文生成手段と、
前記第１のリレーショナルデータベースに対して、前記検索文生成手段により生成された各検索文を、前記構文木における葉ノードからルートノードへ向けて階層の深いノード順に実行することにより、各前記検索文に対応する状態をそれぞれ検索結果として取得する検索実行手段と、
少なくとも前記構文木のルートノードに対応する検索結果を出力する検索結果出力手段と、
を備える。
本発明の一態様としての検証方法は、
複数の状態間の遷移を表現した状態遷移モデルを記憶した第１のリレーショナルデータベースを準備する準備ステップと、
計算木論理（CTL：Computational Tree Logic）式により記述した、前記状態遷移モデルの検証条件の入力を受け付ける検証条件受付ステップと、
前記検証条件受付ステップで入力された前記検証条件を解析することにより、それぞれ論理式が対応付けられた複数のノードを含む構文木を生成し、親ノードの論理式は、子ノードに対応する論理式と、前記親ノードに割り当てられた演算子とに基づいて定義される、構文解析ステップと、
前記構文木の各ノードに対応する論理式を充足する状態を検索する検索文を、前記親ノードの検索文が、前記親ノードの前記子ノードに対応する論理式の出力を引数とするように生成する検索文生成ステップと、
前記第１のリレーショナルデータベースに対して、前記検索文生成ステップにより生成された各検索文を、前記構文木における葉ノードからルートノードへ向けて階層の深いノード順に実行することにより、各前記検索文に対応する状態をそれぞれ検索結果として取得する検索実行ステップと、
少なくとも前記構文木のルートノードに対応する検索結果を出力する検索結果出力ステップと
を備える。
本発明の一態様としての検証プログラムは、上記検証方法の各ステップをコンピュータに実行させることを特徴とする。
【発明の効果】
【０００５】
本発明により、検証パフォーマンスを向上させることができる。
【発明を実施するための最良の形態】
【０００６】
まず本実施の形態の説明で用いる用語について定義する。
（１）RDB（Relational DataBase：リレーショナルデータベース）：関係モデルに基づくデータベースのことである。関係モデルでは、複数のデータ集合（ドメイン）の直積部分集合として、ドメイン間に関係を定義する。具体的には関係は表形式で表現され、各列は１つのドメインを表し、各行は各ドメインの要素の組合せ（即ち関係）を表す。リレーショナルデータベースは、この関係モデルに対して関係代数演算（和集合、射影）を適用することで、データの検索を可能にする。
【０００７】
（２）FSM (Finite State Machine：有限状態遷移系)：有限個の状態と状態遷移とからなる、ふるまいのモデルのことである。図２に、OSのタスク管理機能を題材にしたFSMの一例を示す。個々の円形が一つの「状態」を、状態間を結ぶ有向曲線が一つの「状態遷移」を表す。円形の中のS1、S2などの「1」「2」は、状態識別子である。有向曲線のT1,T2などの「1」「2」は状態遷移識別子である。
【０００８】
図2には、３つのタスク１、２、３の場合のFSMが示されており、各タスクは、実行（RUN）状態と、実行可能（RDY）状態と、実行待ち（WAI）状態の３つの状態を有する。"RUN", "RDY", "WAI"は状態を構成する変数名に相当する。各タスクには、自発的なCPU譲り渡し（yield）操作と、自発的な実行待ち状態への遷移（sleep）操作と、実行待ち状態のタスクの実行可能状態への変更（wakeup）操作の三つのAPI（Application Programming Interface）関数が提供されている。実行（RUN）状態にあるタスクが、yield,sleep,wakeupを選択的に実行する。
【０００９】
（３）CTL（Computational Tree Logic）式 (計算木論理式):  時間経過と共に真偽値が変化しえる文を記述する論理体系のことであり、システムの振る舞いに関する要求仕様(システム検証条件となる)を記述することが出来る。信号機システムの場合におけるCTL式の一例を以下に示す。
CTL式: "押しボタンが点灯" -> AF("歩行者信号が青")
意味: "押しボタンが点灯"したら、いずれ必ず"歩行者信号が青"
ただし AF = "いずれ必ず"
定義
（A）Φ ::= T | F | p | ¬Φ | Φ∨Φ | Φ∧Φ | Φ⇒Φ | Φ⇔Φ
| AXΦ | EXΦ | AGΦ | EGΦ | AFΦ | EFΦ | A(ΦUΦ) | E(ΦUΦ)
| A(ΦWΦ) | E(ΦWΦ)
ただし T: 真(True)
F: 偽(False)
p: 原子項
（B）原子項
部分論理式を持たないCTL式 (構文上分解不可能)
（C）論理演算子
¬ : not
∨ : or
∧ : and
⇒ : ならば
⇔ : 同値
（D）時相演算子
経路演算子 (Path Operators)
A （All: 現在状態から分岐する全ての経路で真である。）
E （Exists: 現在状態から分岐する経路のうち、少なくとも1つの経路で真である。）
状態演算子 (State Operators)
X Φ （Next: 経路上、次の状態でΦは真である。）
G Φ （Globally: 経路上、全ての状態でΦは常に真である。）
F Φ （Finally: 経路上、いずれかの時点でΦは真となる。）
Φ U Ψ （Until: 経路上、ある時点でΨは真になり、それまでは常にΦが真である。）
Φ W Ψ （Weak until(unless): 経路上(Φ U Ψ) ∨ ¬F(Ψ)）
【００１０】
以降の説明において「演算子」と言えば、論理演算子か時相演算子を表すものとする。
【００１１】
以下、CTL式の定義を理解するため、具体例（OSのタスク管理機能）をいくつか示す。
【００１２】
図2のFSMにおいて、以下の検証条件1 (原子項)を満たす状態は、図3における太線の丸で示すようになる。
p := "Task1 ∈ RDY"
この意味は、タスク1が実行可能状態にあるというものである
【００１３】
また、図2のFSMにおいて、下記の検証条件2を満たす状態の一例は図4のようになる。
p ⇒ AF(q)
但し q := "Task1 ∈ RUN"
この意味は、タスク1が実行可能状態ならば、全ての経路の、ある時点で(必ずいつか)、タスク1が実行状態になるというものである。
【００１４】
また、図2のFSMにおいて、下記の検証条件3を満たす状態の一例は図5のようになる。
p ⇒ A(p U q)
この意味は、タスク1が実行待ち状態ならば、
全ての経路の、ある時点で(必ずいつか)タスク1が実行状態になり、
且つ、タスク1が実行状態になるまで、タスク1は実行可能状態である、というものである。
【００１５】
（４）構文木とは、CTL式を構文解析により木構造で表現したもののことである(図8左側参照)。構文木は、複数のノードと、ノード間を結ぶ枝とを含む。葉ノードには、T, F, または原子項が割り当てられ、葉ノード以外のノード（非葉ノード）には論理演算子または時相演算子が割り当てられる。
【００１６】
ノード間の親子関係は、CTL式中の各(部分)CTL式と、(論理・時相)演算子との作用関係を表現する。結果的に、元のCTL式に含まれる演算子の演算順位は、構文木の末端である葉ノードからルートノードに向けてノードを辿る順番として認識される。
【００１７】
各ノードを頂点とする部分木は、それぞれ各ノードに対応する論理式を表す。葉ノードについては、それに割り当てられたT, F, または原子項自体が論理式となる。
【００１８】
以下、本発明の実施の形態について詳細に説明する。
【実施例１】
【００１９】
図１は、本発明の一実施の形態に係るシステム状態検査装置の構成を概略的に示す。
【００２０】
このシステム状態検査装置は、予め検査対象システムの仕様書から生成されたFSMをリレーショナルデータベース（RDB）１４に保持しておき、外部から与えられた検証条件(CTL式)からリレーショナルデータベースの検索手続き(SQL(Structured Query Language)文)を生成し、リレーショナルデータベース１４の検索機能を利用して、生成した検索手続き（SQL文）を実行する事で、モデル検査を行おうするものである。なお、本実施例では検索手続きをSQLで記述するが、リレーショナルデータベースのクエリー言語形式およびその手続き型拡張形式で記述されていればよく、記述言語はSQLに限定されるものではない。
【００２１】
このシステム状態検査装置の検査対象はFSM、当該システム状態検査装置への入力は、検証条件（CTL式）、出力は、検証条件を満たす全状態の集合である。
【００２２】
以下では、本装置の処理について説明するが、その前にFSMについて詳細な説明を行う。
【００２３】
上述したように、図2はOSのタスク管理機能を題材にしたFSMの一例（タスクが３つの場合）を示している。検査対象であるFSMは本装置のRDB１４にあらかじめ格納されている。
【００２４】
FSMは、「状態表」(以降"State")と「状態遷移表」(以降"Trans")の二つのテーブルから形成される。
【００２５】
状態表はFSMの全状態を記録する。状態表は、状態を識別する「状態識別子」(以降"ID")と、状態を構成する各「変数名」を、属性として持つ。状態表の一例を以下に示す。最も左の属性"ID"が状態識別子であり、それ以外の"RUN", "RDY", "WAI"は状態を構成する変数名である。例えば一行目の状態0は、RUN={1}, RDY={2, 3}, WAI={}を意味する。
【表１】
2009265996.tif 000003
【００２６】
また、状態遷移表はFSMの全状態遷移を記録する。状態遷移表は、状態遷移を識別する「状態遷移識別子」(以降"ID")、遷移元の状態識別子「遷移元」(以降"SRC")、遷移先の状態識別子「遷移先」(以降"DST")、状態遷移を引き起こしたメソッド(引数を含む)を表す「メソッド」(以降"FUN")、そしてメソッドの戻り値を表す「戻り値」(以降"RET")を、属性として持つ。状態遷移表の一例を以下に示す。例えば、1行目の状態遷移0は、状態0から状態1への遷移であり、void型のメソッド"yield 1"により、引き起こされたものである。
【表２】
2009265996.tif 000004
【００２７】
図6は、図1のシステム状態検査装置による全体処理の流れを示すフローチャートである。
【００２８】
処理1（S101）では、検証条件入力手段１１においてCTL式で記述された検証条件を取得する。
処理2（S102）では、構文解析手段１２において、検証条件入力手段１１により取得された検証条件を解析して構文木を生成する。検証条件「p⇒A(pUq)」(p, qは共に原子項)が取得された場合、生成される構文木は、図8の左側に示すようになる。
処理3（S103）では、構文解析手段１２により生成された構文木をもとに、検証条件を検証するための、SQL形式の検索手続きを組み立てる。この処理は、検索手続き組立て手段１３、原子項に関する検索文生成手段２４、論理演算子に関する検索文生成手段２５、時相演算子に関する検索文生成手段２６において行われる。なお、手段２１〜２３、１６は、本実施例１では用いられず、後述する他の実施例で用いられる。
処理4（S104）では、検索手続き実行手段１５が、リレーショナルデータベース１４を用いて、生成した検索手続き（SQL形式）を逐次実行し、検索結果として、検証条件を満たす全状態の集合を得る。
処理5（S105）では、検査結果出力手段１７が、取得された検査結果（後述する検索結果表）を出力する。
【００２９】
以下、本実施例１の大きな特徴となる処理3（S103）の詳細について説明する。
【００３０】
図7は、図6の処理3（S103）(検索手続きの組み立て)の詳細な流れを示すフローチャートである。
【００３１】
処理3-1（S201）では、検索手続き組立て手段１３が、構文木を用いて、検索計画を作成する。構文木のノードを葉からルートへ向けて階層が深いノードから順番に読み取り、各ノードに対応する論理式に関して演算子と引数情報(構文木の子ノード)とから構成される検索処理情報を、順番付きリスト(検索計画)の形で生成する。検索計画の一例を以下に示す。
【表３】
2009265996.tif 000005
【００３２】
上記の検索計画は表形式で記述されている。表は「SRCHID」「論理式」「演算子」「引数」の属性から構成される。一つの検索処理が一行で表現され、検索処理ID（SRCHID）が若い順番(表の上部)に、SRCHIDに対応する検索処理が実行される。
「SRCHID」は各検索処理を識別する一意的な番号である。
「論理式」は検索処理で検証したい論理式を表す。
「演算子」は論理式に含まれる最も外側の演算子を表す。
「引数」は演算子の引数となる論理式のSRCHIDを表す。例えば、3行目の検索処理2（SRCHID2）は、引数p, qを取る演算子AUに関するものであり、引数として検索処理0, 1（SRCHID1,2）の結果を参照する。但し、論理式が原子項の場合は、引数として原子項自身が記述される。
【００３３】
処理3-2（S202）では、検索手続き組立て手段１３が、検索計画の重複処理を削除する。 検索計画において検索処理情報を上から順番に読み取り、論理式が重複する検索処理（IDが大きい方）を削除する。これと同時に、削除した検索処理を引数にしていた検索処理の引数を、削除した検索処理と重複する、IDが若い検索処理のIDで置換する。これは一般的なソーティングアルゴリズムを利用する事で実現可能である。重複処理削除後の検索計画の一例を以下に示す。SRCHID0,3の論理式が重複しているため、番号の高いSRCHID3の行が削除されている。
【表４】
2009265996.tif 000006
【００３４】
処理3-3（S203〜S211）では、検索手続き組立て手段１３、原子項に関する検索文生成手段２４、論理演算子に関する検索文生成手段２５、時相演算子に関する検索文生成手段２６により、重複処理削除後の検索計画から、検索手続き(SQL形式)を作成する。重複処理削除後の検索計画において検索処理情報を上から順番に読み取り、各検索処理情報に関してSQL文を生成し、それらのSQL文を検索計画の順番に並べて検索手続きを生成する。生成されたSQL文は、検索処理情報で指定された論理式を充足する全状態を検索し、検索した状態を検索結果として検索結果表に出力するものである。
【００３５】
より詳細に、検索計画において検索処理情報を読み取り、読み取った検索処理情報における論理式が原子項のときは（S204のYES）原子項に関する検索文生成手段２４においてSQL文を生成し（処理3-3-1：S207）、論理演算子のときは（S205のYES）論理演算子に関する検索文生成手段２５においてSQL文を生成し（処理3-3-2：S208）、時相演算子のときは（S206のYES）時相演算子に関する検索文生成手段２６においてSQL文を生成する（処理3-3-3：S209）。各検索処理情報から生成されたSQL文は、生成順に先頭から並べられることにより検索手続き（SQL形式）が作成される（処理3-3-4：S210）。S204〜S210の処理は以下のように記述することができる。
for (検索処理情報 : 検索計画)
if (検索処理 == 原子項)
処理3-3-1: 原子項に関する検索文生成
if else (検索処理 == 論理演算子)
処理3-3-2: 論理演算子に関する検索文生成
if else (検索処理 == 時相演算子)
処理3-3-3: 時相演算子に関する検索文生成
処理3-3-4 検索手続きの末尾にSQL文を追加する。
【００３６】
以下処理3-3-1（S207）、処理3-3-2（S208）、処理3-3-3（S209）の詳細について説明する。
【００３７】
処理3-3-1（S207）では、原子項に関する検索文生成手段２４が、検証条件である「原子項」と、「出力先情報（RDB１４の検索結果表の「SRCHID」を表す）」とを入力とし、原子項を充足する全状態を検索し、検索した状態を検索結果としてSRCHIID（検索結果ID）とともに検索結果表に書き込むための、SQL文を生成する。検索結果表はあらかじめRDB１４内に用意されている。検索結果表における検索結果IDあるいはSRCHIDは、たとえば検索計画において当該検索処理情報に割り当てられていたSRCHIDである。SQL文は、以下の生成規則によって生成される。s.idは検索された状態のIDを表す。
入力
原子項: p
出力先情報: OutID(検索結果表のSRCHID)
出力:
### SQL文開始 ### ※ p, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE p;
### SQL文終了 ###
【００３８】
ここで検索結果表(以降"Result"と記述することもある)は、検索結果を保持するテーブルである。Resultは、各検索処理を識別する「検索処理ID」("SRCHID")と検索結果の「状態識別子」("STATE"。StateのIDを示す)を属性として持つ。検索処理の結果複数の状態が該当した場合、その状態数分の行数が追加される。例えば下記のResultでは、検索処理"SRCHID=0"の検索結果は、状態{0, 2, 3}である。
【表５】
2009265996.tif 000007
【００３９】
処理3-3-2（S208）では、論理演算子に関する検索文生成手段２５が、論理演算の入力を示す「参照元情報（引数）」と、論理演算結果の出力先を示す「出力先情報（検索結果IDあるいはSRCHID）」とを入力とし、参照元情報を参照しながら、論理演算子による論理式を充足する全状態を検索し、検索した状態を検索結果としてSRCHIID（検索結果ID）とともに検索結果表に出力するための、SQL文を生成する。SQL文は、論理演算子種別毎に決められた生成規則によって生成される。以下に、その生成規則を説明する。Φ、Ψは論理演算子が作用する論理式とする。
論理演算子1: ¬Φ (否定)
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID);
### SQL文終了 ###
論理演算子2: Φ∨Ψ (または)
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID1)
OR
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID2);
### SQL文終了 ###
論理演算子3: Φ∧Ψ (かつ)
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID1)
AND
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID2);
### SQL文終了 ###
論理演算子4: Φ⇒Ψ (ならば)
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE
s.id NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID1)
OR
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID2);
### SQL文終了 ###
論理演算子5: Φ⇔Ψ (⇔)
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE
(      s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID1)
OR
s.id NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID2))
AND
(      s.id NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID1)
AND
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID2))
### SQL文終了 ###
【００４０】
処理3-3-3（S209）では、時相演算子に関する検索文生成手段２６が、参照元情報（引数）を参照しながら、時相演算子により論理式を充足する全状態を検索し、検索した状態を検索結果としてSRCHID（検索結果ID）とともに検索結果表に出力するための、SQL文を生成する。時相演算子も論理演算子同様に、時相演算子種別毎に決められた生成規則によって生成される。以下に、その生成規則を説明する。入力や出力に関する規則は論理演算子の規則と同様である。
【００４１】
ただし、次のことに注意する。 不動点計算を含む処理(AX, EX以外全て)は、検索処理のループを含む。SQLをベースとした手続きの記述体系は、PL/SQL等を代表に幾つか存在する。以下の例はPL/SQLで記述しているが、それに依存しない。ループと条件によるループの終了が記述可能な体系であれば何でも良い。
時相演算子1: AXΦ
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE
EXISTS (
SELECT * FROM Trans t
WHERE s.id = t.src
) AND (
NOT EXISTS (
SELECT * FROM Trans t
WHERE
s.id = t.src
AND
t.dst NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID
)
);
### SQL文終了 ###
時相演算子2: EXΦ
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE EXISTS (
SELECT * FROM Trans t
WHERE
s.id = t.src
AND
t.dst IN (
SELECT r.state FROM Result r
WHERE r.srchid = InID)
);
### SQL文終了 ###
時相演算子3: AGΦ (最大不動点)
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID);
## 最大不動点計算 (削除される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 削除操作
DELETE FROM Result r
WHERE
r.srchid = OutID
AND
EXISTS (
SELECT * FROM Trans t
WHERE (
r.state = t.src
) AND (
t.dst NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = OutID
)
);
# 削除後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 削除前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子4: EGΦ : 最大不動点
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID);
## 最大不動点計算 (削除される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 削除操作
DELETE FROM Result r
WHERE
r.srchid = OutID
AND
EXISTS (
SELECT * FROM Trans t
WHERE r.state = t.src
) AND (
NOT EXISTS (
SELECT * FROM Trans t
WHERE (
r.state = t.src
) AND (
t.dst in (
SELECT r.state FROM Result r
WHERE r.srchid = OutID
)
)
)
);
# 削除後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 削除前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子5: AFΦ : 最小不動点
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID);
## 最小不動点計算 (追加される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 追加操作
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE (
EXISTS (
SELECT * FROM Trans t
WHERE s.id = t.src)
) AND (
NOT EXISTS (
SELECT * FROM Trans t
WHERE
s.id = t.src
AND
t.dst NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = OutID
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子6: EFΦ : 最小不動点
入力
参照元情報: InID (Φに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID);
## 最小不動点計算 (追加される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 追加操作
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE EXISTS (
SELECT * FROM Trans t
WHERE (
t.src=s.id
) AND (
t.dst in (
SELECT r.state FROM Result r
WHERE r.srchid = OutID
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子7: A(Φ U Ψ) : 最小不動点
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID2);
## 最小不動点計算 (追加される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 追加操作
INSERT INTO Result
SELECT OutID, s.state FROM Result s
WHERE (
s.id = InID1
) AND (
EXISTS (
SELECT * FROM Trans t
WHERE s.id = t.src)
) AND (
NOT EXISTS (
SELECT * FROM Trans t
WHERE
s.id = t.src
AND
t.dst NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = OutID
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子8: E(Φ U Ψ) : 最小不動点
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID2);
## 最小不動点計算 (追加される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 追加操作
INSERT INTO Result
SELECT OutID, s.state FROM Result s
WHERE (
s.id = InID1
) AND (
EXISTS (
SELECT * FROM Trans t
WHERE (
t.src=s.state
) AND (
t.dst in (
SELECT r.state FROM Result r
WHERE r.srchid = OutID
)
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子9: A(Φ W Ψ) : 最大不動点
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID1);
## 最大不動点計算 (削除される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 削除操作
DELETE FROM Result r
WHERE
r.srchid = OutID
AND
EXISTS (
SELECT * FROM Trans t
WHERE (
r.state = t.src
) AND (
t.dst NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = OutID OR r.srchid = InID1
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
時相演算子10: E(Φ W Ψ) : 最大不動点
入力
参照元情報: InID1, InID2 (それぞれΦとΨに対応する)
出力先情報: OutID
出力: 
### SQL文開始 ### ※ InID1, InID2, OutIDを入力値で置換して出力する。
INSERT INTO Result
SELECT OutID, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = InID1);
## 最大不動点計算 (削除される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 削除操作
DELETE FROM Result r
WHERE
r.srchid = OutID
AND
NOT EXISTS (
SELECT * FROM Trans t
WHERE (
r.state = t.src
) AND (
t.dst IN (
SELECT r.state FROM Result r
WHERE r.srchid = OutID OR r.srchid = InID1
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = OutID;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
以上、図6の処理3（S103）の詳細について説明した。
【００４２】
以下、具体例として、検証条件「p⇒A(pUq)」(p, qは共に原子項)が与えられた場合を想定して、本実施例１の処理の流れを示す。
【００４３】
Step1：図6の処理1（S101）により、検証条件(CTL式)として、以下を取得する。
検証条件"p⇒A(pUq)" (但しp, qは共に原子項)
【００４４】
Step2 ：図6の処理2（S102）により、検証条件を解析して構文木を生成する。ここでは図8の左側に示す構文木が生成される。
【００４５】
以下、図6の処理3（S103）により、検索手続きを組み立てる
【００４６】
Step3：処理3-1（図7のS201）により検索計画を作成すると以下のようになる。
【表６】
2009265996.tif 000008
【００４７】
Step4：処理3-2（図7のS202）により検索計画における重複処理を削除すると以下のようになる。処理3-1（S201）で得られた検索計画における３行目が削除されている。
【表７】
2009265996.tif 000009
【００４８】
以下、Step4で得られた重複処理削除後の検索計画を用いて、処理3-3（図7のS203〜S211）により、検索手続きの作成を行う。図8の右側に、構文木と、本処理3-3で生成される検索手続き（SQL手続き）との対応関係を表す。以下、本処理3-3の詳細を示す。
【００４９】
Step5：処理3-3-1（図7のS207）により、原子項pに関する検索文を生成する。出力先情報は、"SRCHID 0"とする。以下に生成された検索文（SQL手続１）を示す。
### SQL文開始 ###
INSERT INTO Result
SELECT 0, s.id FROM State s
WHERE p;
### SQL文終了 ###
【００５０】
Step6：処理3-3-1（図7のS207）により、原子項qに関する検索文を生成する。出力先情報は、"SRCHID 1"とする。以下に、生成された検索文（SQL手続き2）を示す。
### SQL文開始 ###
INSERT INTO Result
SELECT 1, s.id FROM State s
WHERE q;
### SQL文終了 ###
【００５１】
Step7：処理3-3-3（図7のS209）により、時相演算子AUに関する検索文を生成する。出力先情報は、"SRCHID 2"とする。以下に、生成された検索文（SQL手続き3）を示す。
### SQL文開始 ###
INSERT INTO Result
SELECT 2, s.id FROM State s
WHERE s.id in (
SELECT r.state FROM Result r
WHERE r.srchid = 1);
## 最小不動点計算 (追加される状態が無くなるまで繰り返す)
# 現在のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = 2;
# 一つ前のサイズ
size_prev;
LOOP # ループ開始
# 一つ前のサイズへ代入
size_prev = size;
# 追加操作
INSERT INTO Result
SELECT 2, s.state FROM Result s
WHERE (
s.id = 0
) AND (
EXISTS (
SELECT * FROM Trans t
WHERE s.id = t.src)
) AND (
NOT EXISTS (
SELECT * FROM Trans t
WHERE
s.id = t.src
AND
t.dst NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = 2
)
)
);
# 追加後のサイズ
size = SELECT COUNT(*) FROM Result WHERE id = 2;
# 追加前後でサイズが同じ時、ループ終了
EXIT WHEN size == size_prev;
# ループ終了
END LOOP;
### SQL文終了 ###
【００５２】
Step8 ：処理3-3-2（図7のS208）により論理演算子⇒に関する検索文を生成する。出力先情報は、"SRCHID 4"とする。以下に、生成された検索文（SQL手続き4）を示す。
### SQL文開始 ###
INSERT INTO Result
SELECT 4, s.id FROM State s
WHERE
s.id NOT IN (
SELECT r.state FROM Result r
WHERE r.srchid = 0)
OR
s.id IN (
SELECT r.state FROM Result r
WHERE r.srchid = 2);
### SQL文終了 ###
【００５３】
Step9：処理4（図6のS104）により、処理3（図6のS103）で生成した検索手続きをリレーショナルデータベース１４で逐次実行することにより検索結果表を取得する。取得された検索結果表を以下に示す。
【表８】
2009265996.tif 000010
【００５４】
Step10：処理5（図6のS105）により、検索結果表を出力する。検証条件を満たす状態は、FSMの全状態(状態0-15)を含むため、システムは検証条件を充足することが分かる。
【００５５】
これまでの説明では、構文木から検索結果表を得る処理(図6の処理3および処理4)を、マルチパス方式で実装した例を示した。即ち、実施例１では、構文木における各ノードのSQL文を全て生成した後、各生成したSQL文を順次実行した。これに対し、構文木のノードの１つ１つごとに、検索手続き生成（SQL文の生成）と検索処理（SQL文の実行）を繰り返すような1パス方式を行うことも可能である。マルチパス方式であるか１パス方式であるかは本発明の本質ではなく、本発明は、いずれの方式によっても実施可能である。
【００５６】
以上のように、本実施例１によれば、検証条件を木構造により表現し、各ノードの検索文を生成し、葉ノードからルートノードに向けてリレーショナルデータベースを活用して順次各検索文を検索するようにしたことにより、検証パフォーマンスに優れたシステム検証が可能となる。すなわち、産業界で長く実績を積んできたリレーショナルデータベースは検索性能や信頼性が優れており、このようなリレーショナルデータベースを活用することで、検証パフォーマンスや、検証対象規模に関するスケーラビリティの向上が期待できる。
【実施例２】
【００５７】
本実施例２では、検索履歴をリレーショナルデータベース１４に保持・検索可能し、また検証条件に含まれる論理式について、その等価論理式（第１等価式）を書換え候補として生成する。または、その論理式の等価論理式（第１等価式）と、当該論理式の否定の等価論理式（第２の等価式）とを書き換え候補として生成する。論理式およびその書換え候補のうち、どれかが過去において既に検索処理されている場合、その過去の検索処理結果を再利用することで、その論理式についての検索処理を省略し、これにより処理の高速化を図ることができる。以下本実施例２について詳細に説明する。
本実施例２におけるリレーショナルデータベース（RDB）１４は、実施例１の状態表および状態遷移表、検索結果表に加え、「検索履歴表」(以下"History")を持つ。
【００５８】
Historyは「SRCHID」と「FORMULA」を属性として持ち、これまでRDB１４で実行された検索履歴(構文木上中間段階の検索処理も含む)を保有する。SRCHIDは検索処理の識別子で、ResultのSRCHIDと同じである。またFORMULAは、SRCHIDに対応する検索処理の元となった論理式を表す。つまり、Historyには、過去に検索済みの論理式とそのSRCHIDとが格納されている。Historyの一例を以下に示す。例えば、検索処理"SRCHID=4"の元となった論理式は"E(¬q W ¬q)"である。
【表９】
2009265996.tif 000011
【００５９】
図9は、本実施例２による全体処理の流れを示すフローチャートである。
【００６０】
本実施例２の大半の処理は実施例１と同じである。本実施例２が実施例１と異なる点は、処理3(S303)おいて「検索履歴の分析」と「論理式の書換え候補生成」が追加実行され、また、処理4（S304）の次に追加された処理5（S305）において、「検索履歴を保存」を行うことである。処理１（S301）、処理２（S302）、処理４（S304）、処理６（S306）は、図6の処理１（S101）、処理２（S102）、処理４（S104）、処理５（S105）と同様である。
【００６１】
まず処理5（S305）で行う「検索履歴を保存」について説明する。処理４（S304）では、図1の検索履歴保存手段１６が、検索手続き実行手段１５で実行された検索手続き(SQL形式)について、その識別子(SRCHID)と、当該検索手続に対応する論理式とを、リレーショナルデータベース１４のHistoryに保存する。
「検索履歴を保存」は少なくとも、一つの検索手続きが実行される度に履歴を保存するように、処理4（S304）のサブルーチンとして組み込む方法と、処理4と独立に検索手続きから一括でリレーショナルデータベース１４に保存する方法とがあり得るが、これらのどちらの方法を用いてもかまわない。
【００６２】
次に、処理3（S303）で行う検索手続きの組み立てについて説明する。
【００６３】
図10は、処理3（S303）で行う検索手続きの組み立ての処理の流れを示すフローチャートである。実施例１（図7）と異なる点は、処理3-0（S212）が、処理3-1（S201）の前に先頭に追加されたことにある。したがって、以下では、この差分点に着目して説明を行う。その他の処理3-1、処理3-2、処理3-3については実施例１と同様であるため重複する説明を省略する。
【００６４】
図11は、処理3-0(S212)で行う、再利用可能性の反映処理の流れを示すフローチャートである。
【００６５】
検索手続き組立て手段１３は、構文木のノードをルートから葉へ向けて順番に読み取り（S401）、検索履歴分析手段２２を用いて各ノードに対応する論理式が既に検索されているかを分析する（処理3-0-0：S402）。
【００６６】
処理3-0-0（S402）において、検索履歴分析手段２２は、論理式を入力として、検索履歴においてその論理式の存在有無を分析する。具体的には、RDB１４のHistoryのFORMULAで、入力された論理式を検索する。既に履歴が存在した場合（Historyにおいて該当行が見つかった場合）は、対応するSRCHID（ResultのSRCHID）を取得する。
【００６７】
論理式が過去において検索済みであったときは（S403のYES）、構文木において該当ノードの子孫からなる部分を削除し（処理3-0-1：S404）、該当ノードについて既に実施された検索結果を参照するようにする当該ノードを更新する（処理3-0-2：S405）（後述する図１２参照）。ループ終了条件“走査すべきノードが無い”を満たす場合は処理を終了し、そうでない場合はS401へ戻る。
【００６８】
一方、論理式の検索が過去において行われていないとき（S403のNO）、当該論理式が演算子か否かを判断する。演算子でないとき（S406のNO）、すなわち原子項であるときは、S410へ進む。ループ終了条件“走査すべきノードが無い”を満たす場合は処理を終了し、そうでない場合はS401へ戻る。一方、当該論理式が演算子のとき（S406のYES）、検索手続き組立手段１３は、論理式の書換え候補生成手段（論理式生成手段）２１を用いて、論理式の書換え候補を生成する（処理3-0-3：S407）。
【００６９】
この処理3-0-3（S407）において、論理式の書換え候補生成手段２１は、論理式（ここでは原子項を除く）を入力とし、入力された論理式から、ドモルガンの法則に基づく書換え規則を用いて、等価論理式（第１等価式）および否定の等価論理式（第２等価式）を生成する。否定の等価論理式（第２等価式）は、演算子が否定演算子と異なるときのみ生成するようにしてもよい。書換え規則の詳細については、巻末「補足説明2: 論理演算の等価書換え規則」に記述したので、ここを参照されたい。
【００７０】
処理3-0-4（S408）において、検索履歴分析手段２２を用いて、その等価論理式または否定の等価論理式が過去において既に検索されているかを分析する
【００７１】
既に検索済みの等価論理式または否定の等価論理式がある場合には（S409のYES）、該当ノードについて既に実施された検索結果を参照するように構文木を更新する（処理3-0-1：S404、処理3-0-2：S405）（後述する図１２参照）。構文木の更新方法は、等価論理式および否定の等価論理式のいずれが検索済みであるかによって異なり、この詳細は後述する。ループ終了条件“走査すべきノードが無い”を満たす場合は処理を終了し、そうでない場合はS401へ戻る。
【００７２】
以上に説明したS401〜S10の処理は以下のように記述することができる。
loop (ノード <構文木のトップから葉に向けて全ノードを走査) {
処理3-0-0: 検索履歴を分析
if (ノードの論理式が既に検索されている場合) {
処理3-0-1: 構文木上の全子孫を削除
処理3-0-2: ノード論理式を、処理3-0-0で見つけた"SRCHID"への参照で置換
exit loop
} else {
if (ノード == 演算子) {
処理3-0-3: 等価な論理式を生成
処理3-0-4: (生成した論理式に関して)検索履歴を分析
if (生成した論理式の内、既に検索されたものが存在する場合) {
処理3-0-5: 構文木上の全子孫を削除
処理3-0-6: ノード論理式を、処理3-0-0で見つけた"SRCHID"への参照で置換
exit loop
}
}
}
}
【００７３】
以下、具体例として、実施例１と同様に、検証条件「p⇒A(pUq)」(p, qは共に原子項)が与えられた場合を想定して、本実施例２に係わる動作（特に処理3-0)を示す。本実施例２の動作は、Historyに蓄積された検査結果の状況により異なる。ここでは、以下の2つの場合を挙げる。
場合1: A(pUq)が既に検索済みの場合
場合2: E(¬pW¬q)が既に検索済みの場合 (A(pUq)は未検索)
なお、以下の説明において、便宜上、A(pUq)およびE(¬pW¬q)に関連するSRCHIDは共に「xx」とする。
【００７４】
場合1 : A(pUq)が検索済み
Step1：図9の処理1（S301）および処理2（S302）は、実施例１と同じであるため説明を省略する。
以下では処理３（S303）で検索手続きの組み立て行う。
Step2：図10の処理3-0（S212：再利用可能性の反映）における処理3-0-0（図11のS402）で、検索履歴を分析する。"A(pUq)"は検索済みであるため、SRCHIDxxを出力する（図12の左側参照）。
Step3：図11の処理3-0-1（S404）で、構文木において"A(pUq)"に対応するノードの全子孫を削除する（図12の右側参照）
Step4：図11の処理3-0-2(S405)で、ノード論理式を、Step3の検索結果(SRCHIDxx)を参照するように置換する（図12の右側参照）。
Step5：図10の処理3-1（S201）以降は実施例１と同じであるため説明を省略する。
【００７５】
場合2 : E(¬pW¬q)が検索済み
Step1：図9の処理1（S301）および処理2（S302）は、実施例１と同じであるため説明を省略する。
以下では処理３（S303）で検索手続きの組み立て行う。
Step2：図10の処理3-0（S212：再利用可能性の反映）における処理3-0-0（図11のS402）で、検索履歴を分析する。上記仮定の下、"A(pUq)"は未検索であることが判明する。
Step3：図11の処理3-0-3（S407）で、当該論理式の等価論理式（第１等価式）として、¬E(¬pW¬q)が生成され、さらに当該論理式の否定の等価論理式（第２等価式）として、E(¬pW¬q)が生成される（図13右側参照）。
Step4：図11の処理3-0-4（S408）で、生成した論理式に関して、検索履歴を分析すると、"¬E(¬pW¬q)"は検索済みでないが、"E(¬pW¬q)"は検索済みであるため、SRCHIDxxを出力する。
Step5：図11の処理3-0-1（S404）で、構文木において"A(pUq)"に対応するノードの全子孫を削除し、当該ノードを"¬E(¬pW¬q)"に置換し、当該ノードの子ノードとして"E(¬pW¬q)"のノードを追加する。なお、もし"¬E(¬pW¬q)"が検索済みであれば子ノードの追加は不要である。
Step6：図11の処理3-0-2(S405)で、ノード論理式"E(¬pW¬q)"を、Step4の検索結果(SRCHIDxx)を参照するように置換する（図12の右側参照）。
Step7：図10の処理3-1（S201）以降は実施例１と同じであるため説明を省略する。
【００７６】
以上のように、本実施例によれば、過去における検索結果を可能な限り再利用するようにしたことにより、更なるパフォーマンス向上を図ることができる。
【実施例３】
【００７７】
本実施例３は、実施例２において論理式およびその書き換え候補のいずれも検索済みでないとき（図14のS409参照）、論理式および書き換え候補の処理コストを、それらの部分論理式を満たす状態数（サイズ）に基づいて分析する。部分論理式を満たす状態数は検索履歴表および検索結果表を利用して取得する。部分論理式が検索済みでないときは、部分論理式をルートとする構文木を生成し、再帰的に処理を行い、以降これを繰り返す。これにより、論理式および書き換え候補の部分論理式を満たす状態数（サイズ）が得られるため、論理式および書き換え候補の処理コストを計算する。そして処理コストが最小になるような論理式または書き換え候補を選択して構文木を更新する。以下、本実施例３について詳細に説明する。
【００７８】
本実施例３では図1の検索処理コスト分析手段２３を用いる。リレーショナルデータべースは、実施例２と同様に、状態表、状態遷移表、検索結果表に加え、検索履歴表を持つ。
【００７９】
以下、本実施例３に係る処理の流れについて説明する。
本実施例３における大半の処理は実施例２と同じであり、図10の処理3-0(S212)において「処理コスト分析」が追加的に行われる点が実施例２と異なる。したがって、ここでは処理3-0を、実施例２との差分に着目して説明する。
【００８０】
図14は、本実施例３に係る処理3-0の詳細なフローを示したフローチャートである。ハッチングが施されたステップ（S411〜S417）が、実施例２との差分に相当する。ステップS414の処理は再帰制御手段の処理に相当する。本フローチャートの処理は詳細には以下のように記述できる。
【００８１】
なおステップＳ４１１で時相演算子のときのみ本実施例の処理を行うとしているのは、論理演算子の場合、書き換えを行ったとしても処理コストの差は非常に小さく、演算量の違いにさほど差がでないためである。これに対し、時相演算子の場合、繰り返し処理があるため、書き換えによって演算量に大きな違いがでる場合がある。
【００８２】
また下記の処理の記述においてステップS414で行う部分論理式の構文木の生成は、構文解析手段１２を用いて行ってもよいし、生成済みの構文木の一部を利用して生成してもよい。
処理3-0: 再利用可能性の反映 <<"★"は実施例２との差分>>
loop (ノード <構文木のトップから葉に向けて全ノードを走査) {
処理3-0-0: 検索履歴を分析
if (ノードの論理式が既に検索されている場合) {
処理3-0-1: 構文木上の全子孫を削除
処理3-0-2: ノード論理式を、処理3-0-0で見つけた"SRCHID"への参照で置換
exit loop
} else {
if (ノード == 演算子) {
処理3-0-3: 等価な論理式を生成
処理3-0-4: (生成した論理式に関して)検索履歴を分析
if (生成した論理式の内、既に検索されたものが存在する場合) {
処理3-0-5: 構文木上の全子孫を削除
処理3-0-6: ノード論理式を、処理3-0-0で見つけた"SRCHID"への参照で置換
exit loop
}
★                 else {
★                       if (ノード == 時相演算子) {
★                             処理3-0-7: (対象ノードの論理式の部分論理式の)検索履歴を分析
★                             if (論理式が検索されていない場合) {
★                                   処理3-0-8: 部分論理式に関する検索を実施
★                             }
★                             処理3-0-9: RDBのResultを用いて、部分論理式を満たす集合のサイズを計算
★                             処理3-0-10: 時相演算子の種別と、入力される論理式(部分論理式)の充足集合のサイズを元に、検索対象集合のサイズに基づいて処理コストを分析する。 (検索処理コスト分析)
★                             処理3-0-11: 対象ノードを、全書き換え候補の中で、処理コストが最小である書き換え候補に書き換える。
★                             exit loop
★                       }
★                 }
}
}
}
処理3-0-8
入力: 構文木 (部分論理式をルートとする構文木)
出力: 部分論理式の検索結果を参照するSRCHID
副作用: RDBのResult, History
処理説明: 部分論理式をルートとする構文木に関して、再帰的に処理3-0、図9の処理4および処理5を呼び出す。結果として、部分論理式の検索結果がRDBのResultに保存され、またそれを参照するSRCHIDを返す。
処理3-0-10 (検索処理コスト分析)
入力: 時相演算子、演算子への入力となる論理式(部分論理式)の充足集合のサイズ
出力: 処理コスト
担当手段: 「検索処理コスト分析」
処理説明: 検索対象集合のサイズに基づいて、処理コストを分析する。算出規則は巻末の「補足説明1: 時相演算子の計算方法」を参照されたい。
【００８３】
以下、具体例として、実施例１と同様に、検証条件「p⇒A(pUq)」(p, qは共に原子項)が与えられた場合を想定して、本実施例３の動作 (特に処理3-0)について示す。
【００８４】
実施例２と同様に、本装置の振る舞いはFSMや検証条件、そしてHistory（検証履歴）の蓄積状況により異なる。本具体例では、FSM、検証条件および検証履歴について、以下を仮定する。
FSM(検査対象)
状態数: 16
状態遷移数: 42
検証履歴
"A(pUq)": 未検査
"E( ¬p W ¬q )": 未検査
"p", "q": 共に検査済み
"¬p", "¬q": 共に検査済み
【００８５】
Step1：図9の処理1（S301）および処理2（S302）は、実施例１と同じであるため説明を省略する。
【００８６】
以下では処理３（S303）で検索手続きの組み立て行う。
【００８７】
Step2：図10の処理3-0（S212：再利用可能性の反映）における図14の処理3-0-0（S402）、3-0-3（S407）、3-0-4（S408）は、実施例２と同じであるため説明を省略する。
【００８８】
Step3：図14の処理3-0-7（S412）で、 部分論理式の検索履歴を分析する。
【００８９】
上記した仮定により、"E(¬pW¬q)"の部分論理式である"¬p", "¬q"が共に検査済みであるためこれらの部分論理式を取得する。また"A(pUq)"の部分論理式である"p", "q"が共に検査済みであるためこれらの部分論理式を取得する。
【００９０】
Step4：図14の処理3-0-9（S415）では、部分論理式の集合サイズを計算する。
【００９１】
部分論理式"¬p"および"¬q"のサイズをたとえばResultに基づき計算すると、"¬p"の方は1個、"¬q"の方は、4個となったとする。また部分論理式"p"および"q"のサイズをたとえばResultに基づき計算すると、"p"の方は15個、"¬q"の方は、12個となったとする。なお、（"¬p"の状態数）は、全状態数−（pを充足する状態数）に等しく、また（"¬q"の状態数）は、 全状態数−（qを充足する状態数）に等しい。
【００９２】
Step5：図14の処理3-0-10（S416）では、検索処理コストを分析する。"A(pUq) "および"E( ¬p W ¬q ) "のコストはそれぞれ以下のように計算される。
A(pUq) : 7560 (= pを充足する状態数(=15) * 状態遷移数(=42) * qを充足する状態数(=12)
E( ¬p W ¬q ) : 210 (= ¬pを充足する状態数(=1) * 状態遷移数(=42) * [¬pを充足する状態数 + ¬qを充足する状態数](=5))
【００９３】
両コストを比較して、"E( ¬p W ¬q )"の処理コストの方が小さいことを判定する。なお、"¬E( ¬p W ¬q )"の処理コストを求め、"¬E( ¬p W ¬q )"と"A(pUq) "との処理コストを比較してもよいが、論理演算子（ここでは"¬"）の演算量は、時相演算子の演算量に比べてきわめて小さいため、実際上、"E( ¬p W ¬q ) "の処理コストとの比較でも十分である。このため本実施例では"E( ¬p W ¬q ) "の処理コストとの比較を行っている。
【００９４】
Step6：図14の処理3-0-11（S417）では、ノード論理式を、処理コストが最小のものを参照するように置換する（図15の右側参照）。置換方法の詳細は第２の実施例で説明したとおりである。
【００９５】
Step7：図10の処理3-1（S201）以降は実施例１と同じであるため説明を省略する。
以上のように本実施例によれば、過去に取得された検索結果を利用し、処理コストが最小になるような論理式の書き換えを行うようにしたことにより、よりパフォーマンス特性に優れた検証を行うことができる。
【００９６】
なお、以上に説明した本発明の実施形態におけるシステム状態検証装置は、例えば、汎用のコンピュータ装置を基本ハードウェアとして用いることでも実現することが可能である。すなわち、図1のシステム状態検証装置における各手段１１〜１７、２１〜２６は、上記のコンピュータ装置に搭載されたプロセッサにプログラムを実行させることにより実現することができる。このとき、検証装置は、上記のプログラムをコンピュータ装置にあらかじめインストールすることで実現してもよいし、ＣＤ−ＲＯＭなどの記憶媒体に記憶して、あるいはネットワークを介して上記のプログラムを配布して、このプログラムをコンピュータ装置に適宜インストールすることで実現してもよい。
【００９７】
[補足説明1: 時相演算子の計算方法]
時相演算子の数学的計算方法と不動点計算コストを説明する。
○記号定義
State: 状態集合
Trans: 状態遷移集合
s: 状態 (∈State)
t: 状態遷移 (∈Trans)
t.src: 状態遷移tの遷移元
t.dst: 状態遷移tの遷移先
Φ、Ψ: CTL式
"s |= Φ" : 状態sでCTL式Φが真
#S: 集合Sのサイズ(要素の個数)
○ AX Φ
数学的定義
S := {s ∈ State | ∀t (∈ Trans, t.src=s) t.dst|=Φ}
○ EX Φ
数学的定義
S := {s ∈ State | ∃t (∈ Trans, t.src=s) ST t.dst|=Φ}
○ AG Φ (最大不動点)
数学的定義
# 集合S0 := 論理式Φを満たす全状態
S0 := {s ∈ State | s|=Φ }
# 集合Sn+1 := 全ての遷移で集合Snへ至る、集合Snの全状態。
Sn+1 := {s ∈ Sn | ∀t (∈ Trans, t.src=s) t.dst ∈ Sn}
※ Sn: 任意のパス上nステップ以内の任意の状態がΦを満たす状態集合 (単調減少)
# 最大不動点計算
S := ∩Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #Sn-1 * #Trans * #Sn-1
=> コスト計算式: (#S0)^2 * #Trans
○ EG Φ (最大不動点)
数学的定義
# 集合S0 := 論理式Φを満たす全状態
S0 := {s ∈ State | s|=Φ }
# 集合Sn+1 := 集合Snへ至る遷移が存在する、若しくは遷移が存在しない、集合Snの全状態
Sn+1 := {s ∈ Sn | (∃t (∈ Trans) ST (t.src=s ∧ t.dst ∈ Sn)) ∨ (¬∃t (∈ Trans) ST t.src=s)}
※ Sn: あるパスで、nステップ以内の任意の状態がΦを満たす、状態集合。 (単調減少)
# 最大不動点計算
S := ∩Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #Sn * ((#Trans * #Sn) + #Trans)
=> コスト計算式: #S0 * #Trans * (#S0 + 1)
○ AF Φ (最小不動点)
数学的定義
# 集合S0 := 論理式Φを満たす全状態
S0 := {s ∈ State | s|=Φ }
# 集合Sn+1 := 任意の遷移でSnの元に写る状態の集合、若しく集合Snの全状態
Sn+1 := {s ∈ State | ∀t(∈ Trans, t.src=s) t.dst ∈ Sn} ∪ Sn
※ Sn : 任意のパスでnステップ以内にΦを満たす状態の集合 (単調増加)
# 最小不動点計算
S := ∪Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #State * #Trans * #Sn
=> コスト計算式: #State * #Trans * #S0
○ EF Φ (最小不動点)
数学的定義
# 集合S0 := 論理式Φを満たす全状態
S0 := {s ∈ State | s|=Φ }
# 集合Sn+1 := ある遷移でSnの元に写る状態の集合、若しく集合Snの全状態
Sn+1 := {s ∈ State | ∃t(∈ Trans, t.src=s) t.dst ∈ Sn} ∪ Sn
※ Sn : あるパスでnステップ以内にΦを満たす状態の集合 (単調増加)
# 最小不動点計算
S := ∪Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #State * #Trans * #Sn
=> コスト計算式: #State * #Trans * #S0
○ A(Φ U Ψ) : 最小不動点
数学的定義
T := {s ∈ State | s|=Φ }
# 集合S0 := 論理式Ψを満たす全状態
S0 := {s ∈ State | s|=Ψ }
# 集合Sn+1 := 任意の遷移でSnへ至るTの要素、若しくはSnの全要素。
Sn+1 := {s ∈ T | ∀t(∈ Trans, t.src=s) t.dst ∈ Sn } ∪ Sn
※ Sn : あるパスでnステップ以内にΦを満たす状態の集合 (単調増加)
# 最小不動点計算
S := ∪Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #T * #Trans * #Sn
=> コスト計算式: #T * #Trans * #S0
○ E(Φ U Ψ) : 最小不動点
数学的定義
T := {s ∈ State | s|=Φ }
# 集合S0 := 論理式Ψを満たす全状態
S0 := {s ∈ State | s|=Ψ }
# 集合Sn+1 := ある遷移でSnへ至るTの要素、若しくはSnの全要素。
Sn+1 := {s ∈ T | ∃t(∈ Trans, t.src=s) t.dst ∈ Sn } ∪ Sn
※ Sn : あるパスで、nステップ以内にΨが成り立ち、それまではΦが成り立つ集合 (単調増加)
# 最小不動点計算
S := ∪Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #T * #Trans * #Sn
=> コスト計算式: #T * #Trans * #S0
○ A(Φ W Ψ) : 最大不動点
数学的定義
T := {s ∈ State | s|=Ψ }
# 集合S0 := 論理式Φを満たす全状態
S0 := {s ∈ State | s|=Φ }
# 集合Sn+1 := 任意の遷移でSnかTへ至る、Snの要素。
Sn+1 := {s ∈ Sn | ∀t(∈ Trans, t.src=s) (t.dst ∈ Sn) or (t.dst ∈ T)}
※ Sn : 任意のパスでnステップ以内に、
Ψが成り立ち、それまではΦが成り立つ or
Ψが成り立たず、全ての状態でΦが成り立つ
状態集合。 (単調減少)
# 最大不動点計算
S := ∩Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #Sn * #Trans * (#Sn + #T)
=> コスト計算式: #S0 * #Trans * (#S0 + #T)
○ E(Φ W Ψ) : 最大不動点
数学的定義
T := {s ∈ State | s|=Ψ }
# 集合S0 := 論理式Φを満たす全状態
S0 := {s ∈ State | s|=Φ }
# 集合Sn+1 := ある遷移でSnかTへ至る、Snの要素。
Sn+1 := {s ∈ Sn | ∃t(∈ Trans, t.src=s) (t.dst ∈ Sn) or (t.dst ∈ T)}
※ Sn : あるパスでnステップ以内に、
Ψが成り立ち、それまではΦが成り立つ or
Ψが成り立たず、全ての状態でΦが成り立つ
状態集合。(単調減少)
# 最大不動点計算
S := ∩Sn (nは全ての自然数)
処理コスト(検索対象の大きさ)
Snの場合: #Sn * #Trans * (#Sn + #T)
=> コスト計算式: #S0 * #Trans * (#S0 + #T)
【００９８】
[補足説明2: 論理演算の等価書換え規則]
○ 時相演算の同値関係
AFΦ = ¬EG¬Φ
EFΦ = ¬AG¬Φ
AXΦ = ¬EX¬Φ
A(Φ U Ψ) = ¬E(Φ V Ψ)
E(Φ U Ψ) = ¬A(Φ V Ψ)
○ 時相演算の書換え規則
※ 書換え候補は「検索履歴分析手段」で検索する論理式のテンプレートである。一般的に否定を含めて、2つの候補が存在する。また、右側に書かれた書換え規則は、その書換え候補で元の論理式を等価性を保ちながら置換する場合の置換規則である。
Next
AX
=> 書換え候補: ¬EX¬ (書換え規則 "¬EX¬")
=> 書換え候補: EX¬ (書換え規則 "¬EX¬")
EX
=> 書換え候補: ¬AX¬ (書換え規則 "¬AX¬")
=> 書換え候補: AX¬ (書換え規則 "¬AX¬")
Finally
AF
=> 書換え候補: ¬EG¬ (書換え規則 "¬EG¬")
=> 書換え候補: EG¬ (書換え規則 "¬EG¬")
EF
=> 書換え候補: ¬AG¬ (書換え規則 "¬AG¬")
=> 書換え候補: AG¬ (書換え規則 "¬AG¬")
Globally
AG
=> 書換え候補: ¬EF¬ (書換え規則 "¬EF¬")
=> 書換え候補: EF¬ (書換え規則 "¬EF¬")
EG
=> 書換え候補: ¬AF¬ (書換え規則 "¬AF¬")
=> 書換え候補: AF¬ (書換え規則 "¬AF¬")
Until
A(Φ U Ψ)
=> 書換え候補: ¬E(¬Φ W ¬Ψ) (書換え規則 "¬E(¬Φ W ¬Ψ)")
=> 書換え候補: E(¬Φ W ¬Ψ) (書換え規則 "¬E(¬Φ W ¬Ψ)")
E(Φ U Ψ)
=> 書換え候補: ¬A(¬Φ W ¬Ψ) (書換え規則 "¬A(¬Φ W ¬Ψ)")
=> 書換え候補: A(¬Φ W ¬Ψ) (書換え規則 "¬A(¬Φ W ¬Ψ)")
Weak Until
A(Φ W Ψ)
=> 書換え候補: ¬E(¬Φ U ¬Ψ) (書換え規則 "¬E(¬Φ U ¬Ψ)")
=> 書換え候補: E(¬Φ U ¬Ψ) (書換え規則 "¬E(¬Φ U ¬Ψ)")
E(Φ W Ψ)
=> 書換え候補: ¬A(¬Φ U ¬Ψ) (書換え規則 "¬A(¬Φ U ¬Ψ)")
=> 書換え候補: A(¬Φ U ¬Ψ) (書換え規則 "¬A(¬Φ U ¬Ψ)")
【図面の簡単な説明】
【００９９】
【図１】本発明の一実施の形態としてのシステム状態検証装置のブロック図。
【図２】FSMの一例を示す図。
【図３】検証条件1を満たす状態の例を示す図。
【図４】検証条件2を満たす状態の例を示す図。
【図５】検証条件3を満たす状態の例を示す図。
【図６】実施例１の全体の処理の流れを示すフローチャート。
【図７】実施例１における検索手続きの組み立て処理の流れを示すフローチャート。
【図８】実施例１の具体例を説明する図。
【図９】実施例２における全体の処理の流れを示すフローチャート。
【図１０】実施例２における検索手続きの組み立て処理の流れを示すフローチャート。
【図１１】実施例２における再利用可能性の反映処理の流れを示すフローチャート。
【図１２】実施例２の具体例を説明する図。
【図１３】実施例２の他の具体例を説明する図。
【図１４】実施例３の再利用可能性の反映処理の流れを示すフローチャート。
【図１５】実施例３の具体例を説明する図。
【符号の説明】
【０１００】
１１：検証条件入力手段
１２：構文解析手段
１３：検索手続き組立て手段
１４：リレーショナルデータベース（第１および第２のリレーショナルデータベース）
１５：検索手続き実行手段
１６：検索履歴保存手段
１７：検査結果出力手段
２１：論理式の書き換え候補生成手段
２２：検索履歴分析手段
２３：検索処理コスト分析手段
２４：原子項に関する検索文生成手段
２５：論理演算子に関する検索文生成手段
２６：時相演算子に関する検索文生成手段
【図１】
2009265996.tif 000012
【図２】
2009265996.tif 000013
【図３】
2009265996.tif 000014
【図４】
2009265996.tif 000015
【図５】
2009265996.tif 000016
【図６】
2009265996.tif 000017
【図７】
2009265996.tif 000018
【図８】
2009265996.tif 000019
【図９】
2009265996.tif 000020
【図１０】
2009265996.tif 000021
【図１１】
2009265996.tif 000022
【図１２】
2009265996.tif 000023
【図１３】
2009265996.tif 000024
【図１４】
2009265996.tif 000025
【図１５】
2009265996.tif 000026