(57)【特許請求の範囲】
【請求項１】
イベントログの集合から特定のイベント発生順序を含むイベントログを検索する方法であって、
入力装置と、SeqBDD形式で表されたイベントログの集合を記憶する記憶装置と、出力装置と、検索制御手段と、イベントログ追加手段と、マップ関数生成手段と、観点列集合変換手段と、検索手段とを用いて、
検索制御手段が、入力装置から特定のイベント発生順序を表す条件を記述した時相論理式が入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出すステップと、
検索制御手段の制御に応じてマップ関数生成手段が、イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数を作成するステップと、
検索制御手段の制御に応じて観点列集合変換手段が、記憶装置から取り出したイベントログの集合を表すSeqBDDを前記マップ関数に基づいて等価な観点列の集合を表すSeqBDDに変換するステップと、
検索制御手段の制御に応じて検索手段が、観点列の集合を表すSeqBDDから前記入力された時相論理式を満たす観点列を抽出するステップと、
検索制御手段が、前記抽出させた観点列をマップ関数の逆関数によりイベントログに変換するステップと、
検索制御手段が、前記変換したイベントログが記憶装置から取り出したイベントログの集合を表すSeqBDDに含まれているか判定し、含まれているイベントログのみ出力装置に出力するステップと、を具備する
ことを特徴とするイベントログの検索方法。
【請求項２】
記憶装置から取り出したイベントログの集合を表すSeqBDDをマップ関数に基づいて等価な観点列の集合を表すSeqBDDに変換するステップにあっては、
検索制御手段の制御に応じて観点列集合変換手段が、
イベントログの集合を表すSeqBDDの中間ノードのラベルをマップ関数によりイベントから対応する観点に置き換える第１のステップと、
ラベルを観点に変換したSeqBDDにおける頂点ノードである基準ノードがシンクノードか判定する第２のステップと、
シンクノードでない場合に基準ノードから０エッジのみで到達可能な中間ノードである比較ノードにラベルが等しいノードがあるか判定する第３のステップと、
基準ノードとラベルが等しい比較ノードが存在しない場合に、基準ノードの０子ノード及び１子ノードをそれぞれ基準ノードとして第２のステップ以降を再帰的に繰り返す第４のステップと、
基準ノードとラベルが等しい比較ノードが存在する場合に、当該比較ノードへの０エッジを０シンクノードに張り替える第５のステップと、
基準ノードを頂点とするSeqBDDと比較ノードを頂点とするSeqBDDとの和集合を表すSeqBDDを求める第６のステップと、
求めた和集合のSeqBDDの頂点ノードに対して基準ノードへのエッジを張り替える第７のステップと、
求めた和集合のSeqBDDの頂点ノードの０子ノード及び１子ノードをそれぞれ基準ノードとして第２のステップ以降を再帰的に繰り返す第８のステップと、を実行する
ことを特徴とする請求項１に記載のイベントログの検索方法。
【請求項３】
請求項１または２に記載のイベントログの検索方法における記憶装置を更新する方法であって、
さらに、イベントログ追加手段を用いて、
検索制御手段が、入力装置から検索対象となるイベントログが入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出すステップと、
検索制御手段の制御に応じてイベントログ追加手段が、前記入力されたイベントログのみを要素とする集合を表すSeqBDDを作成するステップと、
検索制御手段の制御に応じてイベントログ追加手段が、前記作成した入力イベントログのみを要素とする集合を表すSeqBDDと記憶装置から取り出したイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求めるステップと、
検索制御手段が、前記求めさせた和集合を表すSeqBDDを記憶装置に記憶するステップと、を具備する
ことを特徴とする請求項１または２に記載のイベントログの検索方法。
【請求項４】
イベントログの集合から特定のイベント発生順序を含むイベントログを検索する装置であって、
入力装置と、
SeqBDD形式で表されたイベントログの集合を記憶する記憶装置と、
出力装置と、
イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数を作成するマップ関数生成手段と、
イベントログの集合を表すSeqBDDをマップ関数ｍに基づいて等価な観点列の集合を表すSeqBDDに変換する観点列集合変換手段と、
観点列の集合を表すSeqBDDから時相論理式を満たす観点列を抽出する検索手段と、
入力装置から特定のイベント発生順序を表す条件を記述した時相論理式が入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出し、
マップ関数生成手段を制御して、イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数を作成させ、
観点列集合変換手段を制御して、記憶装置から取り出したイベントログの集合を表すSeqBDDを前記マップ関数に基づいて等価な観点列の集合を表すSeqBDDに変換させ、
検索手段を制御して、観点列の集合を表すSeqBDDから前記入力された時相論理式を満たす観点列を抽出させ、
前記抽出させた観点列をマップ関数の逆関数によりイベントログに変換し、
前記変換したイベントログが記憶装置から取り出したイベントログの集合を表すSeqBDDに含まれているか判定し、含まれているイベントログのみ出力装置に出力する検索制御手段と、を少なくとも具備する
ことを特徴とするイベントログの検索装置。
【請求項５】
さらに、
入力されたイベントログのみを要素とする集合を表すSeqBDDを作成し、これと記憶装置に記憶されているイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求めるイベントログ追加手段を備え、
検索制御手段は、さらに、
入力装置から検索対象となるイベントログが入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出し、
イベントログ追加手段を制御して、前記入力されたイベントログのみを要素とする集合を表すSeqBDDを作成させ、
イベントログ追加手段を制御して、前記作成した入力イベントログのみを要素とする集合を表すSeqBDDと記憶装置から取り出したイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求めさせ、
前記求めさせた和集合を表すSeqBDDを記憶装置に記憶する
ことを特徴とする請求項４に記載のイベントログの検索装置。
【請求項６】
コンピュータを、請求項４または５に記載のイベントログの検索装置の各手段として機能させるためのプログラム。                                                                                
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアにおけるイベントログを検索する技術に関する。
【背景技術】
【０００２】
コンピュータ上で動作するソフトウェアによって実現される、企業における業務システム等の情報処理システム向けのソリューションとして、近年、イベントログを活用した技術が数多く提案されている。通常、業務の案件を完了させるには、情報処理システムのサーバやクライアントの機能を活用し、様々な処理を順次実行する必要がある。イベントログとは、案件の完了までの過程で実施される処理や操作、システムの状態変化の内容（ここではこれらを総称して単にイベントと呼ぶ。）を、処理時刻（タイムスタンプ）とともに記録したものである。各案件のイベントログは記憶装置に蓄積され、例えば業務監査で不正な処理や必要な処理が抜けた案件がないかの検査や、エラーの発生した状態がどのような案件に多いのか等の業務改善のための分析に活用される。
【０００３】
イベントログを用いた検査や分析ではイベントログの集合に対して条件を与え、その条件に合致するイベントログを検索する技術が必須となる。一般的なイベントログの検索技術は、検索キーワードを含む文書を抽出するＷｅｂ検索などと同様に、条件として記述されたイベントが出現するイベントログを抽出する。しかし、実際のイベントログの検査や分析では、２以上の特定のイベントが特定の順序で出現するイベントログ、すなわち特定のイベント発生順序を含むイベントログを抽出したい場合があり、イベント発生順序に関する検索技術の確立が必要となっている。
【０００４】
［従来技術］
特定のイベント発生順序の検索技術として、非特許文献１に提案の技術がある。非特許文献１提案の技術では、特定のイベント発生順序を表す条件を線形時相論理で記述し、記憶装置に蓄積されている各イベントログがその条件を満たすか判定する。以下、非特許文献１提案の技術について説明する。
【０００５】
記憶装置に蓄積されているイベントログの集合をＳとし、案件に対するイベントログをπ∈Ｓとしたとき、イベントログπはその案件を処理する過程で発生したイベントをタイムスタンプの昇順に並べた列で表現することができる。すなわちイベントログの集合Ｓに含まれるすべてのイベントの集合をＡとし、イベントログπで発生するイベントをタイムスタンプの昇順にｅ1，ｅ2，・・・，ｅnとすると、π＝ｅ1ｅ2ｅ3・・・ｅnとなる。但し、ｅ1，ｅ2，・・・，ｅn∈Ａである。なおイベントログπの長さを|π|と表記する。
【０００６】
検索条件として記述する線形時相論理式では、命題論理における否定（¬）や連言（∧）、選言（∨）などの論理演算子に加えて、Next（○）、Until（Ｕ）といった様相演算子を使用することができる。図１にＢＮＦ記法で記した線形時相論理の文法を示す。
【０００７】
イベントログπが線形時相論理式Ｆを満たすかの判定は、関数Check(F，π，i)を用いてCheck(F，π，0)を実行する。Check(F，π，i)は、イベントログπのｉ番目のイベントｅiにて論理式Ｆを満たすか判定する関数である。出力はtrueもしくはfalseであり、それぞれ論理式を満たすこと、及び満たさないことを意味する。Check(F，π，0)は論理式Ｆの構造に対して再帰的に判定が実施される。図２にCheck(F，π，i)の判定処理、すなわちイベントログπが線形時相論理式Ｆを満たすかの判定処理の概要を示す。
【０００８】
このような判定方法は、イベントログを個々にCheck関数を用いて判定する必要がある。したがって集合Ｓに含まれるイベントログの数に対して、ログを検索する計算量が比例してしまうという問題点がある。
【０００９】
時相論理による判定の高速化技術としては、モデル検査技術分野において様々な提案がなされている。モデル検査とは、システムの振る舞いをオートマトンでモデル化し、その振る舞いが時相論理式で記述された仕様を満たすか判定する。オートマトンの状態数に比例して判定に必要となる計算量が増加するため、オートマトンをＢＤＤ（Binary Decision Diagram）と呼ばれるコンパクトなデータ構造で表現し、検査手続を高速化した非特許文献２や、ＳＡＴ問題に帰着することでＳＡＴソルバを利用して高速化を実現する非特許文献３などが提案されている。このような高速化技術は、検査対象がオートマトンであることを前提としている。
【００１０】
イベントログの時相論理による検索に、モデル検査などで利用されている高速化技術を適用する場合、イベントログの集合Ｓをそれと等価なオートマトンに変換する必要がある。イベントの集合に含まれる各イベントをアルファベット（ａ，ｂ，ｃ等）で表現すると、イベントログは文字列ａ，ａｂｂ，ａｃ，ｂｃ等として表現することができる。イベントログの集合Ｓと等価なオートマトンとは、Ｓに含まれる文字列のみを受理するオートマトンとなる。
【００１１】
このような有限長の文字列の集合をコンパクトに表現するデータ構造として、非特許文献４にSeqBDD（Sequence BDD）が提案されている。SeqBDDはノードとノード間を結ぶ方向つきのエッジとで表現される無閉路有向グラフの一種である。
【００１２】
前記ノードとしては他のノードへのエッジを持つ中間ノードと、他のノードへのエッジを持たないシンクノードの２種類が存在する。中間ノードはラベルを持ち、ここではアルファベット文字とする。中間ノードから他のノードへのエッジは必ず２つ存在し、ここではそれぞれを１エッジ、０エッジと呼ぶ。さらに１エッジ側に接続されるノードを１子ノード、同様に０エッジ側に接続されるノードを０子ノードと呼ぶ。
【００１３】
１子ノードが中間ノードの場合、文字列中において親ノードが示す文字の次に出現する文字を示す。０子ノードが中間ノードの場合、親ノードが示す文字は文字列に出現せず、０子ノードの文字が出現することを意味する。文字には順序が付与されており、中間ノードとその１子ノードの中間ノードのラベルに制限はない。中間ノードとその０子ノードの中間ノードのラベルは、その順序を守って文字が出現する必要がある。例えばａ→ｂという順序があるとき、中間ノードのラベルがｂである場合にその０子ノードの中間ノードのラベルがａであったり、ｂであったりすることは許されない。
【００１４】
シンクノードは１もしくは０というラベルを持ち、それぞれ１シンクノード、０シンクノードと呼ぶ。SeqBDDにおいては１シンクノードと０シンクノードはそれぞれ１つのみ存在する。SeqBDDでは中間ノードを経由する経路が文字列を表現している。経路が１シンクノードへ到達するとき、経路の示す文字列はSeqBDDの表現する文字列の集合に含まれることを意味する。もし経路が０シンクノードへ到達するとき、経路の示す文字列はSeqBDDが表現する文字列の集合に含まれないことを意味する。
【００１５】
図３に文字列ａｂｃのみで構成される文字列の集合｛ａｂｃ｝を意味するSeqBDDを示す。また図４に文字列ａａａ，ａｂａ，ｂｂｃ，ｂｃで構成される文字列の集合｛ａａａ，ａｂａ，ｂｂｃ，ｂｃ｝を意味するSeqBDDを示す。なお、図４では説明を容易にするため中間ノードから０シンクノードへのエッジ及び０シンクノードの表示を省略した。これ以降のSeqBDDの図示でも同様に表記するものとする。
【００１６】
直感的にはSeqBDDの中間ノードの１シンクノードからの１エッジに関する高さが、表現する文字列中におけるラベルの文字の出現位置を示す（高いほうが文字列中の前の位置に出現する。）。一方、中間ノードと０子ノードの中間ノードとの関係は、文字列中の同じ位置における出現文字のバリエーションを表している。例えば、図４の最も高い位置にあるａノードは、文字列の先頭においてａの文字が出現する文字列を意味している。そのａノードの０子ノードであるｂノードは、文字列の先頭においてａが出現せず、ｂが出現する文字列を意味する。
【発明の概要】
【発明が解決しようとする課題】
【００１７】
SeqBDDは近年、データマイニング領域において適用されているデータ構造である。主に文字列の集合から頻出する部分文字列を抽出するために利用する。SeqBDDを時相論理によるイベントログの検索に用いる場合、イベントログの集合からそれと等価なSeqBDDに変換することが考えられる。SeqDBBは一種のオートマトンとみなすこともできるため、SeqBDDに対してモデル検査技術の高速化技術を適用することで検索を高速化することが可能である。しかし、このようなSeqBDDを用いたイベントログの検索においては、現状の技術では下記のような課題がある。
【００１８】
一般にイベントログの検索条件の記述では、時相論理式の原子としてイベントそのものを記述するとは限らない。例えば、イベントログのイベントとしてアプリケーションのＧＵＩの画像を記録していると仮定する。もちろん、画像そのもの（それを画像ａとする。）を原子に与えて、「いつか画像ａが出現するイベントログ」などの時相論理式（true Ｕ ａ）で検索する場合もある。しかし、イベントそのものではなく、「エラーウインドウが出現している画像」という別の観点で出現順序に関する検索をしたい場合もある。この場合、イベントをイベントで成立する観点にマップする関数が必要となる。すなわちマップ関数ｍは観点の集合をＰとすると、ｍ：Ａ→２Pと表現することができる。
【００１９】
このようなマップ関数ｍのもとで、観点を原子とする時相論理式による検索を実施する場合、検索対象であるイベントログ、すなわちイベントの集合Ａ上のイベント列を観点の部分集合２P上の列（ここでは観点列と呼ぶ。）に変換しなければならない。
【００２０】
例えばイベントログとして「ａｂｃ」が存在するとき、観点の集合Ｐ＝[α，β]の部分集合に対して、マップ関数ｍがｍ(a)＝[α]，ｍ(b)＝[α]，ｍ(c)＝[β]が与えられた場合を考える（マップ関数ｍは対表現でｍ：(a，[α] )，(b，[α])，(c，[β])などと表現しても良い。）。このときイベントログ「ａｂｃ」を観点列「ααβ」（正確には[α][α][β]であるが略記する。）に変換し、原子が観点の集合Ｐの要素である時相論理式で検索することになる。
【００２１】
このようなイベントログの観点列への変換は、イベントログの集合Ｓを表すSeqBDD上で実現できることが望ましい。図４のSeqBDDが表すイベントログ（文字列）の集合｛ａａａ，ａｂａ，ｂｂｃ，ｂｃ｝を前述のマップ関数ｍによる観点列の集合｛ααα，ααβ，αβ｝に変換し、SeqBDDで表現したものを図５に示す。
【００２２】
図５のSeqBDDを得るためには、各イベントログを一度すべて観点列に変換し、観点列の集合からSeqBDDを構築する方法が考えられる。しかし、この方法では検索条件の時相論理式にて原子が変わる、すなわち観点の集合Ｐの変更やイベントと観点とのマッピングの変更のたびにSeqBDDを最初から構築し直す必要があるため、最悪、検索のたびにSeqBDDを構築することになり、検索のレスポンスの低下の一因となる。
【００２３】
イベントログの集合を表すSeqBDDから観点列の集合を表すSeqBDDへ直接変換することができれば、検索のレスポンスの低下を防止することができる。SeqBDDでは、様々な集合演算や操作をSeqBDD上で実施するためのアルゴリズムが提案されている（非特許文献５の表３に簡潔にまとめられているので参考にされたい。）。しかし、これらの提案されている演算の単純な組み合わせでは、本発明において実現したいイベントログの集合から観点列の集合への変換をSeqBDD上で実現することができなかった。
【課題を解決するための手段】
【００２４】
本発明では、イベントログの集合に対してイベントの観点を原子とする時相論理式で検索を行うとき、検索条件を変更による観点の集合やイベントと観点のマッピングの変更のたびに検索レスポンスが低下するという課題を解決するために、以下の特徴を有する。
【００２５】
本発明の第一の発明として、
イベントログの集合から特定のイベント発生順序を含むイベントログを検索する方法であって、入力装置と、SeqBDD形式で表されたイベントログの集合を記憶する記憶装置と、出力装置と、検索制御手段と、イベントログ追加手段と、マップ関数生成手段と、観点列集合変換手段と、検索手段とを用いて、検索制御手段が、入力装置から特定のイベント発生順序を表す条件を記述した時相論理式が入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出すステップと、検索制御手段の制御に応じてマップ関数生成手段が、イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数を作成するステップと、検索制御手段の制御に応じて観点列集合変換手段が、記憶装置から取り出したイベントログの集合を表すSeqBDDを前記マップ関数に基づいて等価な観点列の集合を表すSeqBDDに変換するステップと、検索制御手段の制御に応じて検索手段が、観点列の集合を表すSeqBDDから前記入力された時相論理式を満たす観点列を抽出するステップと、検索制御手段が、前記抽出させた観点列をマップ関数の逆関数によりイベントログに変換するステップと、検索制御手段が、前記変換したイベントログが記憶装置から取り出したイベントログの集合を表すSeqBDDに含まれているか判定し、含まれているイベントログのみ出力装置に出力するステップと、を具備することを特徴とする。
【００２６】
本発明の第二の発明として、
第一の発明における記憶装置から取り出したイベントログの集合を表すSeqBDDをマップ関数に基づいて等価な観点列の集合を表すSeqBDDに変換するステップにあっては、検索制御手段の制御に応じて観点列集合変換手段が、イベントログの集合を表すSeqBDDの中間ノードのラベルをマップ関数によりイベントから対応する観点に置き換える第１のステップと、ラベルを観点に変換したSeqBDDにおける頂点ノードである基準ノードがシンクノードか判定する第２のステップと、シンクノードでない場合に基準ノードから０エッジのみで到達可能な中間ノードである比較ノードにラベルが等しいノードがあるか判定する第３のステップと、基準ノードとラベルが等しい比較ノードが存在しない場合に、基準ノードの０子ノード及び１子ノードをそれぞれ基準ノードとして第２のステップ以降を再帰的に繰り返す第４のステップと、基準ノードとラベルが等しい比較ノードが存在する場合に、当該比較ノードへの０エッジを０シンクノードに張り替える第５のステップと、基準ノードを頂点とするSeqBDDと比較ノードを頂点とするSeqBDDとの和集合を表すSeqBDDを求める第６のステップと、求めた和集合のSeqBDDの頂点ノードに対して基準ノードへのエッジを張り替える第７のステップと、求めた和集合のSeqBDDの頂点ノードの０子ノード及び１子ノードをそれぞれ基準ノードとして第２のステップ以降を再帰的に繰り返す第８のステップと、を実行することを特徴とする。
【００２７】
本発明の第三の発明として、
第一または第二の発明における記憶装置を更新する方法であって、さらに、イベントログ追加手段を用いて、検索制御手段が、入力装置から検索対象となるイベントログが入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出すステップと、検索制御手段の制御に応じてイベントログ追加手段が、前記入力されたイベントログのみを要素とする集合を表すSeqBDDを作成するステップと、検索制御手段の制御に応じてイベントログ追加手段が、前記作成した入力イベントログのみを要素とする集合を表すSeqBDDと記憶装置から取り出したイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求めるステップと、検索制御手段が、前記求めさせた和集合を表すSeqBDDを記憶装置に記憶するステップと、を具備することを特徴とする。
【００２８】
本発明の第四の発明として、
イベントログの集合から特定のイベント発生順序を含むイベントログを検索する装置であって、入力装置と、SeqBDD形式で表されたイベントログの集合を記憶する記憶装置と、出力装置と、イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数を作成するマップ関数生成手段と、イベントログの集合を表すSeqBDDをマップ関数ｍに基づいて等価な観点列の集合を表すSeqBDDに変換する観点列集合変換手段と、観点列の集合を表すSeqBDDから時相論理式を満たす観点列を抽出する検索手段と、入力装置から特定のイベント発生順序を表す条件を記述した時相論理式が入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出し、マップ関数生成手段を制御して、イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数を作成させ、観点列集合変換手段を制御して、記憶装置から取り出したイベントログの集合を表すSeqBDDを前記マップ関数に基づいて等価な観点列の集合を表すSeqBDDに変換させ、検索手段を制御して、観点列の集合を表すSeqBDDから前記入力された時相論理式を満たす観点列を抽出させ、前記抽出させた観点列をマップ関数の逆関数によりイベントログに変換し、前記変換したイベントログが記憶装置から取り出したイベントログの集合を表すSeqBDDに含まれているか判定し、含まれているイベントログのみ出力装置に出力する検索制御手段と、を少なくとも具備することを特徴とする。
【００２９】
本発明の第五の発明として、
第四の発明において、さらに、入力されたイベントログのみを要素とする集合を表すSeqBDDを作成し、これと記憶装置に記憶されているイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求めるイベントログ追加手段を備え、検索制御手段は、さらに、入力装置から検索対象となるイベントログが入力されると、記憶装置からイベントログの集合を表すSeqBDDを取り出し、イベントログ追加手段を制御して、前記入力されたイベントログのみを要素とする集合を表すSeqBDDを作成させ、イベントログ追加手段を制御して、前記作成した入力イベントログのみを要素とする集合を表すSeqBDDと記憶装置から取り出したイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求めさせ、前記求めさせた和集合を表すSeqBDDを記憶装置に記憶することを特徴とする。
【００３０】
本発明の第六の発明として、
コンピュータを、第四または第五の発明の各手段として機能させるためのプログラムであることを特徴とする。
【発明の効果】
【００３１】
本発明によれば、イベントログの集合から観点列への集合の変換をSeqBDD上で実施することが可能となり、検索条件として記述される時相論理式の原子に出現する観点の集合やイベントと観点のマッピングが変更されても高速にログの検索を行うことができるようになる。
【図面の簡単な説明】
【００３２】
【図１】ＢＮＦ記法で記した線形時相論理の文法を示す説明図
【図２】イベントログπが線形時相論理式Ｆを満たすかの判定処理の概要を示す流れ図
【図３】文字列の集合｛ａｂｃ｝を表すSeqBDDを示す説明図
【図４】文字列の集合｛ａａａ，ａｂａ，ｂｂｃ，ｂｃ｝を表すSeqBDDを示す説明図
【図５】図４に示したイベントログの集合｛ａａａ，ａｂａ，ｂｂｃ，ｂｃ｝を表すSeqBDDを、ｍ(a)＝[α]，ｍ(b)＝[α]，ｍ(c)＝[β]のマップ関数ｍに基づいて変換した観点列の集合｛ααα，ααβ，αβ｝を表すSeqBDDを示す説明図
【図６】本発明のイベントログの検索方法を実施する装置の実施の形態の一例を示す構成図
【図７】本発明のイベントログの集合の更新処理を示す流れ図
【図８】本発明のイベントログの検索処理を示す流れ図
【図９】マップ関数の生成処理を示す流れ図
【図１０】SeqBDDの変換処理を示す流れ図
【図１１】図４に示したSeqBDDの各中間ノードのラベルを、ｍ(a)＝[α]，ｍ(b)＝[α]，ｍ(c)＝[β]のマップ関数ｍに基づいて書き換えた状態を示す説明図
【図１２】図１０中のステップＳ４２の詳細を示す流れ図
【図１３】図１１に示したSeqBDDの頂点ノードに図１２のステップＳ５４を実行した結果を示す説明図
【図１４】図１３に示したSeqBDDのノード１を頂点とするSeqBDDを示す説明図
【図１５】図１３に示したSeqBDDのノード２を頂点とするSeqBDDを示す説明図
【図１６】図１４及び図１５に示したSeqBDDの和集合を求めた結果を示す説明図
【図１７】図１６に示したSeqBDDのノード２’を頂点とするSeqBDDを示す説明図
【図１８】図１６に示したSeqBDDのノード３’を頂点とするSeqBDDを示す説明図
【図１９】図１７及び図１８に示したSeqBDDの和集合を求めた結果を示す説明図
【図２０】図１９に示したSeqBDDの頂点ノードに図１６に示したSeqBDDのノード２’へのエッジを張り替えた状態を示す説明図
【図２１】イベントログ「ａａａ」のみからなる集合を表現するSeqBDDを示す説明図
【図２２】イベントログ「ａｂａ」のみからなる集合を表現するSeqBDDを示す説明図
【図２３】図２１及び図２２に示したSeqBDDの和集合を求めた結果を示す説明図
【発明を実施するための形態】
【００３３】
図６は本発明のイベントログを検索する方法を実施する装置の実施の形態の一例、ここでは周知のコンピュータ上に実現した例を示すもので、図中、１１は入力装置、１２は記憶装置、１３は出力装置、１４はコンピュータである。
【００３４】
入力装置１１は、キーボード、マウス等からなり、ユーザがコンピュータ１４に所定の情報、すなわち検索対象となるイベントログや検索条件となる時相論理式を入力するためのものである。記憶装置１２は、入力装置１１より入力されたイベントログを記録し、イベントログの集合をSeqBDDの形式で記憶・保持するためのものである。出力装置１３は、ディスプレイ等で構成され、コンピュータ１４が実施する図７及び図８の手続きの途中経過や結果（抽出したイベントログ）を表示するためのものである。
【００３５】
コンピュータ１４は、検索制御部１５、イベントログ追加部１６、マップ関数生成部１７、観点列集合変換部１８及び検索部１９を構成する。
【００３６】
検索制御部１５は、コンピュータ１４に構成される各部を制御するとともに、図７及び図８の手続きを実施する。具体的には、入力装置１１から検索対象となるイベントログが入力されたときに図７の手続きを実施し、記憶装置１２のイベントログの集合に入力されたイベントログを追加し、記憶装置１２のイベントログの集合を更新する。また検索制御部１５は、入力装置１１から検索条件を表す時相論理式が入力されたときに図８の手続きを実施し、記憶装置１２のイベントログの集合から時相論理式を満たすイベントログを抽出し、出力装置１３に結果を出力する。
【００３７】
図８のＳ２１からＳ２４までのステップの実施により、入力された時相論理式ｆを満たす観点列を抽出することができる。しかしここで必要なのは、その観点列と対応する元のイベントログである。Ｓ２５のステップでは、そこで得られた観点列をマップ関数ｍの逆関数によってイベントログに変換する。例えば、図５のSeqBDDが示す観点列の集合から「ααα」という観点列を抽出したとする。マップ関数ｍがｍ(a)＝[α]，ｍ(b)＝[α]，ｍ(c)＝[β]の場合、αはイベントａもしくはｂと対応するため、Ｓ２５のステップにより観点列「ααα」に対応するイベントログとして「ａａａ」，「ａａｂ」，「ａｂａ」，「ｂａａ」，「ｂａｂ」，「ｂｂａ」，「ｂｂｂ」を得ることができる。
【００３８】
このようにして得られたイベントログには、元のイベントログの集合に含まれないイベントログが存在するため、Ｓ２６のステップでイベントログの集合にこれらのイベントログが含まれるか判定し、含まれるイベントログのみ出力装置１３に出力する。この例の場合、図５の観点列の集合と対応するイベントログの集合のSeqBDDは図４となるため、結果としてイベントログ「ａａａ」，「ａｂａ」が出力される。なお、SeqBDD上で文字列の集合に文字列が含まれるかを判定することは非特許文献４などにより公知の事項であるため、説明を割愛する。
【００３９】
イベントログ追加部１６は、検索制御部１５が実施する図７の手続きにおけるＳ１２、Ｓ１３のステップを実施し、入力されたイベントログのみを要素とする集合を表すSeqBDDを作成し、これと記憶装置に記憶されているイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求める。
【００４０】
すなわち、入力装置１１から検索対象となるイベントログ、ここではπが入力されると、検索制御部１５が、記憶装置１２からイベントログの集合を表すSeqBDDを取り出し（Ｓ１１）、イベントログ追加部１６によりＳ１２のステップにて入力されたイベントログπのみを要素とする集合を表すSeqBDDを作成し、イベントログ追加部１６によりＳ１３のステップにて前記作成した入力イベントログπのみを要素とする集合を表すSeqBDDと記憶装置１２から取り出したイベントログの集合を表すSeqBDDとの和集合を表すSeqBDDを求め、その後、前記求めた和集合を表すSeqBDDを記憶装置１２に記憶する（Ｓ１４）。
【００４１】
マップ関数生成部１７は、検索制御部１５が実施する図８の手続きにおけるＳ２２のステップを実施、具体的には図９の手続きを実施し、イベントログの集合を観点列の集合に変換するために必要となる、イベントログの集合に出現するイベントと時相論理式の原子に出現する観点の部分集合とのマップ関数ｍを生成する。
【００４２】
図９の手続では、Ｓ３１のステップにてイベントログの集合Ｓに出現するイベントの集合をＡとし、Ｓ３２のステップにて時相論理式ｆに出現する原子（観点）を抽出し、集合Ｐとする。次に、Ｓ３３のステップにて集合Ａが空集合であれば処理を終了して図８の手続きにおけるＳ２３のステップに戻る。集合Ａが空集合でなければ、Ｓ３４のステップにて集合Ａからイベントを１つ取り出してｅで表す。次に、Ｓ３５のステップにて、前記取り出したイベントとそのイベントが満たす観点の集合Ｑ⊆Ｐとの対（ｅ，Ｑ）を作成する。さらに、Ｓ３６のステップにてマップ関数ｍに前記作成した対（ｅ，Ｑ）を追加し、Ｓ３３のステップに戻り、集合Ａが空集合となるまでＳ３４〜Ｓ３６のステップを繰り返す。
【００４３】
観点列集合変換部１８は、検索制御部１５が実施する図８の手続きにおけるＳ２３のステップ、具体的には図１０の手続きを実施し、記憶装置１２から取り出したイベントログの集合を表すSeqBDDをマップ関数ｍに基づいて等価な観点列の集合を表すSeqBDDに変換する。
【００４４】
図１０の手続では、Ｓ４１のステップにて、イベントログの集合Ｓを表すSeqBDDの各中間ノードのラベルを、マップ関数ｍに基づいてイベントから観点の集合に書き換える。例えば図４のSeqBDDに対して、マップ関数ｍがｍ(a)＝[α]，ｍ(b)＝[α]，ｍ(c)＝[β]で与えられるとき、SeqBDDの中間ノードのラベルａ，ｂをαに書き換え、ラベルｃをβに書き換えて図１１のSeqBDDを得る。
【００４５】
このようにして得られたSeqBDDは、SeqBDDの条件を満たしておらず、正規化が必要になる。例えば、図１１のSeqBDDでは、中間ノードとその０子ノードのラベルが同じ観点となっているものが存在する（図１１におけるノード１とノード２、あるいはノード３とノード４など）。よって、続くＳ４２のステップでは、Ｓ４１のステップで得たSeqBDDの頂点ノード（基準ノード）ｎに対して図１２の手続きを実施し、正規化されたSeqBDDに変換する。
【００４６】
図１２の手続きでは、まずＳ５１のステップにて、与えられたノードｎがシンクノードであるか調べる。シンクノードであればこれ以上の変換はできないため、手続きを終了する。シンクノードではなく、中間ノードである場合は、Ｓ５２のステップにてノードｎから０エッジのみで到達可能な中間ノード（比較ノード）に当該ノードｎと同じラベルのノードｎ’があるかを調べる。
【００４７】
同じラベルがない場合はＳ５３のステップを実施し、ノードｎの０子ノード及び１子ノードをそれぞれノードｎとしてＳ５１以降の手続きを再帰的に実施する。同じラベルが存在する場合は以下のＳ５４からＳ５７のステップを実施する。例えば、図１１の頂点ノード１に対して図１２の手続きを実施すると、ノード１の０子ノードであるノード２が同じαというラベルを持つため、Ｓ５４からＳ５７のステップが実施されることになる。
【００４８】
Ｓ５４のステップでは、まずノードｎ’への０エッジを０シンクノードに接続する。図１１の頂点ノード１に対して、このステップを実施した結果を図１３に示す。図１３ではノード１からノード２への０エッジが削除されていることに注意されたい。このノード２への０エッジは０シンクノードに接続されているが、表記上省略している。
【００４９】
次にＳ５５のステップで、ノードｎを頂点ノードとするSeqBDDと、ノードｎ’を頂点とするSeqBDDとの和集合を求める。図１３のSeqBDDに対してこのステップを実施するとき、ノード１を頂点とするSeqBDD（図１４）とノード２を頂点とするSeqBDD（図１５）との和集合を求める。その結果のSeqBDDを図１６に示す。和集合のSeqBDDを求める方法は非特許文献１等により公知の事項であるため、説明は割愛する。
【００５０】
さらにＳ５６のステップで、ノードｎへのエッジがあれば、それをＳ５５のステップで求めたSeqBDDの頂点ノードへ張り替える。図１６の場合は、ノードｎが頂点ノード１であり、ノード１へのエッジがないため特に処理を実施しない。
【００５１】
最後にＳ５７のステップでは、Ｓ５６のステップで作成したSeqBDDの頂点ノードの０子ノード及び１子ノードをそれぞれノードｎとしてＳ５１以降の手続きを再帰的に実施する。図１６のSeqBDDにおいてＳ５７のステップを実行する場合、頂点ノード１’の０子ノードである０シンクノード（図示せず）と、１子ノードであるノード２’とをそれぞれノードｎとしてＳ５１以降の手続きを実施する。
【００５２】
０シンクノードに対してＳ５１以降の手続きを実施すると、Ｓ５１のステップのシンクノードの判定により特に処理を実施せず、終了となる。一方、ノード２’に対しては、Ｓ５１，Ｓ５２，Ｓ５４のステップが実行され、Ｓ５５のステップでノードｎであるノード２’を頂点ノードとするSeqBDD（図１７）とノードｎ’であるノード３’を頂点ノードとするSeqBDD（図１８）との和集合を求める（図１９）。
【００５３】
Ｓ５６のステップでは、Ｓ５５で求めた図１９の頂点ノード１”に、図１６におけるノードｎであるノード２’への（ノード１’からの）エッジを張り替えて、図２０のSeqBDDを得る。これ以降は図２０のノード１”の０子ノード及び１子ノードをそれぞれノードｎとしてＳ５１以降の手続きを再帰的に実施するが、結果としては特に変更は発生せず、最終的に図２０のSeqBDDに変換することができる。
【００５４】
このように、図１２の手続き及びそれを実施する観点列集合変換部１８により、イベントログの集合を表すSeqBDDから等価な観点列の集合を表すSeqBDDを直接求めることができる。これにより、検索条件が入力される度にイベントログを観点列に変換して観点列集合を表すSeqBDDを求める必要がなくなり、検索のレスポンスを大きく改善することができる。
【００５５】
検索部１９は、図８の手続きにおけるＳ２４のステップを実施し、観点列集合変換部１８にて求めたSeqBDDに対して、入力された時相論理式ｆを満たす観点列を抽出する。SeqBDDは一種のオートマトンであり、オートマトンが受理する文字列の集合に対して時相論理式満たす文字列を抽出する技術は非特許文献２や３にて公知の事項であるため、説明は割愛する。
【００５６】
なお、前述した実施の形態では、検索制御部１５、イベントログ追加部１６、マップ関数生成部１７、観点列集合変換部１８及び検索部１９をコンピュータ１４上に実現した例を示したが、ハードウェアで実現しても良い。またこれら各装置が、適切な通信路で相互に接続された複数のハードウェア上に分散して存在し、相互に通信し合いながら実行することもできる。
【実施例１】
【００５７】
ここでは、本発明の実施例として、図６の構成をとった場合におけるイベントログの検索方法を説明する。
【００５８】
例えば、記憶装置１２に記憶されているイベントログが１つも存在しない場合を考える。ここで入力装置１１からイベントログ「ａａａ」が入力された場合、コンピュータ１４に構成された検索制御部１５は図７の手続きを実施し、イベントログ追加部１６がイベントログ「ａａａ」のみからなる集合を表現する図２１のSeqBDDを作成し、記憶装置１２に記録する。さらに、入力装置１１からイベントログ「ａｂａ」が入力されると同様に図７の手続きを実施し、記憶装置１２に記憶されている図２１のSeqBDDと、イベントログ「ａｂａ」のみの集合を表す図２２のSeqBDDとの和集合（図２３）をイベントログ追加部１６が求め、記憶装置１２に記憶する。さらに入力装置１１からイベントログ「ｂｂｃ」や「ｂｃ」が入力されると、結果として記憶装置１２に記憶されるイベントログの集合｛ａａａ，ａｂａ，ｂｂｃ，ｂｃ｝を表すSeqBDDは図４となる。
【００５９】
記憶装置１２に記憶されているSeqBDDが図４であるとき、入力装置１１から時相論理式ｆとして◇β（いつかβが成立しているイベントログ）が入力された場合を考える。ここでβはイベントｃでのみ成立し、イベントａやｂでは成立しないものとする。このときコンピュータ１４に構成される検索制御部１５は図８の手続きを実施する。
【００６０】
まずＳ２１のステップで記憶装置１２に記憶されている図４のSeqBDDを取り出す。次にＳ２２のステップでマップ関数生成部１７によりイベントとイベントで成立する観点の集合とのマップ関数ｍを作成する。具体的には図９の手続きを実施する。すなわち、Ｓ３１のステップにてイベントの集合がＡ＝｛ａ，ｂ，ｃ｝となり、Ｓ３２のステップで観点の集合ＰがＰ＝[β]となる。続くＳ３３からＳ３６のステップでイベントの集合Ａからイベントを１つずつ取り出し、そのイベントで成立する観点の部分集合を求める。ここではイベントａ，イベントｂで成立する観点の部分集合は空集合となり、イベントｃで成立する観点の部分集合は[β]となる。ここで空集合をαで表現すると、マップ関数ｍは(a，α)，(b，α)，(c，β)で表現できる。
【００６１】
マップ関数ｍを求めると、検索制御部１５は図８の続くＳ２３のステップを実施し、観点列集合変換部１８が図１０の手続きを実施する。まずＳ４１のステップで図４のSeqBDDのラベルをマップ関数ｍに基づいてイベントから観点に変更する。この結果、得られるSeqBDDは図１１となる。さらにＳ４２のステップを実施し、図１１のSeqBDDを図１２の手続きにより図２０のSeqBDDに変換する。観点列の集合を表すSeqBDDが求まると、検索制御部１５は図８の手続きのＳ２４のステップを実施し、検索部１９が図２０のSeqBDDに対して時相論理式◇βを満たす観点列を求める。
【００６２】
結果として、観点列「ααβ」，「αβ」を抽出する。このように抽出された観点列に対して検索制御部１５はＳ２５のステップを実行し、関数ｍの逆関数を使って観点列をイベントログに変換する。結果としてイベントログ「ａａｃ」，「ａｂｃ」，「ｂｂｃ」，「ａｃ」，「ｂｃ」を得ることができる。最後にＳ２６のステップで検索制御部１５は、これらのイベントログが記憶装置１２から取り出した図４のSeqBDDに含まれるか判定し、含まれているもののみを出力装置１３に出力する。この場合はイベントログ「ｂｂｃ」及び「ｂｃ」が出力される。
【符号の説明】
【００６３】
１１：入力装置、１２：記憶装置、１３：出力装置、１４：コンピュータ、１５：検索制御部、１６：イベントログ追加部、１７：マップ関数生成部、１８：観点列集合変換部、１９：検索部。
【先行技術文献】
【非特許文献】
【００６４】
【非特許文献１】W. M. P. van der Aalst, H. T. de Beer and B.F. van Dongen, "Process Mining and Verification of Properties: An Approach based on Temporal Logic", Lecture Notes in Computer Science, Vol.3760, pp.130-147, Springer, 2005
【非特許文献２】J. R. Burch, E. M. Clarke and K. L. McMillan, "Symbolic Model Checking: 10２０ States and Beyond", Information and Computation, Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium one , pp.428-439, 4-7 Jun 1990
【非特許文献３】A. Biere, A. Cimatti, E. Clarke and Y. Zhu, " Symbolic Model Checking without BDDs", Lecture Notes in Computer Science, Vol.1579, pp.193-207, Springer, 1999
【非特許文献４】E. Loekito, J. Bailey and J. Pei, "A binary decision diagram based approach for mining frequent subsequences", Knowl. Inf. Syst., Vol.24, pp.235-268, Springer, 2009
【非特許文献５】湊、"ＢＤＤ／ＺＤＤを基盤とする離散構造と演算処理系の最近の展開"、IEICE Fundamentals Review、Vol.4、No.3、pp.224-230、電子情報通信学会、2011
【図１】
0005618381.tif 000002
【図２】
0005618381.tif 000003
【図３】
0005618381.tif 000004
【図４】
0005618381.tif 000005
【図５】
0005618381.tif 000006
【図６】
0005618381.tif 000007
【図７】
0005618381.tif 000008
【図８】
0005618381.tif 000009
【図９】
0005618381.tif 000010
【図１０】
0005618381.tif 000011
【図１１】
0005618381.tif 000012
【図１２】
0005618381.tif 000013
【図１３】
0005618381.tif 000014
【図１４】
0005618381.tif 000015
【図１５】
0005618381.tif 000016
【図１６】
0005618381.tif 000017
【図１７】
0005618381.tif 000018
【図１８】
0005618381.tif 000019
【図１９】
0005618381.tif 000020
【図２０】
0005618381.tif 000021
【図２１】
0005618381.tif 000022
【図２２】
0005618381.tif 000023
【図２３】
0005618381.tif 000024