"イベントに応じて変化する状態の遷移条件を表形式であらわした状態遷移表に対応する状態遷移情報を取得する取得部と、前記状態遷移表がとりうる前記状態を各ノードとする木構造の階層ごとに、前記遷移条件を一階論理式化した論理式を前記状態遷移情報から生成する論理式生成部と、前記論理式生成部によって生成された前記論理式に基づいて充足性モジュロ理論による検査を実行する検査実行部とを備えることを特徴とするモデル検査装置。前記論理式生成部は、最初の前記階層からあらかじめ指定された前記階層までの前記階層ごとに1つの前記論理式をそれぞれ生成することを特徴とする請求項1に記載のモデル検査装置。前記状態遷移情報は、1つの前記状態遷移表から他の前記状態遷移表へ発行される外部イベントに関する情報を含んでおり、前記論理式生成部は、前記外部イベントに関する情報を含んだ前記遷移条件を前記階層ごとに一階論理式化した前記論理式を生成することを特徴とする請求項1または2に記載のモデル検査装置。前記検査実行部は、前記論理式が満たすべき性質を示す検査条件に基づいて前記検査を実行することを特徴とする請求項1、2または3に記載のモデル検査装置。イベントに応じて変化する状態の遷移条件を表形式であらわした状態遷移表に対応する状態遷移情報を取得する取得工程と、前記状態遷移表がとりうる前記状態を各ノードとする木構造の階層ごとに、前記遷移条件を一階論理式化した論理式を前記状態遷移情報から生成する論理式生成工程と、前記論理式生成工程によって生成された前記論理式に基づいて充足性モジュロ理論による検査を実行する検査実行工程とを含むことを特徴とするモデル検査方法。イベントに応じて変化する状態の遷移条件を表形式であらわした状態遷移表に対応する状態遷移情報を取得する取得手順と、前記状態遷移表がとりうる前記状態を各ノードとする木構造の階層ごとに、前記遷移条件を一階論理式化した論理式を前記状態遷移情報から生成する論理式生成手順と、前記論理式生成手順によって生成された前記論理式に基づいて充足性モジュロ理論による検査を実行する検査実行手順とをコンピュータに実行させることを特徴とするモデル検査プログラム。しかしながら、従来のモデル検査手法には、検査対象となるモデルの状態数や遷移条件項目数が増加すると、モデル検査で使用するメモリ量が爆発的に増加してしまうという問題、すなわち、状態爆発の問題があった。また、特許文献1の技術には、モデル検査の検査対象が、コンピュータプログラムに限定されてしまうという問題もあった。すなわち、特許文献1の技術は、独立した人や物をそれぞれモデル化した場合のように、非同期な振る舞いモデルについては、モデル検査の検査対象とすることができなかった。開示の技術は、上記に鑑みてなされたものであって、状態爆発の問題を回避しつつ、モデル検査の検査対象を拡大することができるモデル検査装置、モデル検査方法およびモデル検査プログラムを提供することを目的とする。本願の開示するモデル検査装置は、イベントに応じて変化する状態の遷移条件を表形式であらわした状態遷移表に対応する状態遷移情報を取得する取得部と、前記状態遷移表がとりうる前記状態を各ノードとする木構造の階層ごとに、前記遷移条件を一階論理式化した論理式を前記状態遷移情報から生成する論理式生成部と、前記論理式生成部によって生成された前記論理式に基づいて充足性モジュロ理論による検査を実行する検査実行部とを備える。本願の開示するモデル検査装置によれば、状態爆発の問題を回避しつつ、モデル検査の検査対象を拡大することができる。以下、添付図面を参照して、本願の開示するモデル検査装置、モデル検査方法およびモデル検査プログラムの実施例を詳細に説明する。なお、以下に示す実施例における例示で本発明が限定されるものではない。また、以下に示す実施例では、複数の状態遷移表をモデル検査の対象とする場合について説明するが、当然ながら、1つの状態遷移表のみをモデル検査の対象とすることもできる。まず、本実施例に係るモデル検査手法について、図1および図2を用いて説明する。図1は、本実施例に係るモデル検査手法の説明図であり、図2は、一階論理式化の説明図である。図1に示すように、本実施例に係るモデル検査手法は、複数の状態遷移表からなる状態遷移表群を入力として受け取り、各状態遷移表がとりうるすべての状態について、あらかじめ定められた検査条件を満たすか否かを網羅的に検査する。なお、状態とは、1または複数の状態遷移表に含まれる変数群の各変数値の組み合わせを指す。ここで、本実施例に係るモデル検査手法は、状態の遷移を木構造で表現した場合における、状態階層以下、単に階層と記載する場合もあるごとに、遷移条件を一階論理式化した論理式を生成する。そして、各階層に対応する論理式ごとに、上記した検査条件を満たすか否かを検査する。かかる一階論理式化について図2を用いて説明しておく。図2のAに示したのは、状態の遷移をあらわす木構造である。たとえば、この木構造としては、いわゆるクリプキ構造を用いることができる。図2のAには、各状態および状態間の遷移の例を示しており、各状態を楕円、状態から状態への遷移を矢印であらわしている。ここで、状態S0は、初期状態であり、状態S1または状態S2へ遷移する。また、状態S1は、状態S3または状態S4へ遷移する。一般的に、モデル検査では、各状態が、それぞれ検査条件を満たすか否かを検査するが、各状態に対応するデータをメモリへ記憶させる必要がある。このため、検査すべき状態に含まれる要素数や、状態自体の個数が増えると、メモリへ記憶させるべきデータ量は急激に増加する。たとえば、図2のAおよびBでは、状態S0~状態S9の10個の状態を例示しているが、実際の状態の数は、非常に大きいことが通常である。しかしながら、物理的なメモリ量を超えたモデル検査は不可能であるため、検査すべき状態に対応するメモリ量を確保できない場合には、モデル検査自体を行うことができない。また、仮にメモリ量を確保できた場合であっても、モデル検査に要する物理的なコストはかさんでしまう。そして、このような問題は、状態空間爆発問題、あるいは、単に状態爆発の問題と呼ばれる。そこで、図2のBに示すように、本実施例に係るモデル検査手法では、図2のAに示した木構造の階層ごとに、1つの階層に含まれるすべての状態に関する遷移条件を一階論理式化することで、1つの論理式としてあらわすこととした。なお、かかる論理式の詳細な内容については後述することとする。また、図2のBに示すように、本実施例に係るモデル検査手法では、階層kについて、k=0からk=bdまでの範囲で、それぞれ論理式を生成することとした。ここで、bdは、探索深度と呼ばれ、この探索深度には任意の深度階層を指定することができる。このように、本実施例に係るモデル検査手法によれば、検査すべき状態の個数が非常に多い場合であっても、有限個数の論理式を検査すれば足りるので、上記した状態爆発の問題を回避することができる。すなわち、状態空間を縮減することによって、状態爆発の問題を回避することができる。また、状態空間の縮減によって検査の高速化を図ることができる。すなわち、図1に示すように、本実施例に係るモデル検査手法は、状態遷移表群の状態階層ごとに遷移条件を一階論理式化し図1のA参照、論理式k=0から論理式k=bdまでのbd1個の論理式群を生成する。そして、本実施例に係るモデル検査手法は、生成した論理式群と、論理式群が満たすべき性質を示す検査条件とをSMTSatisfiabilityModuloTheories:充足性モジュロ理論ソルバへ入力する図1のB-1およびB-2参照。なお、SMTソルバとしては、一般的に流通している各種SMTソルバを用いることができる。さらに、本実施例に係るモデル検査手法は、SMTソルバの出力に基づいて反例情報を生成し、生成した反例情報を出力する図1のC参照。ここで、反例とは、検査条件に反する状態およびかかる状態に至る状態の履歴を指す。このように、本実施例に係るモデル検査手法は、状態遷移表をモデル検査の対象としているので、コンピュータプログラムに限らず、非同期な振る舞いモデルをもモデル検査することができる。すなわち、本実施例に係るモデル検査手法は、モデル検査の対象を拡大することができる。また、本実施例に係るモデル検査手法は、状態階層ごとに生成した論理式を用いて有限界モデル検査BMC:BoundedModelCheckedを行うので、状態爆発の問題を回避するとともに、検査の高速化を図ることができる。次に、図1および図2を用いて説明したモデル検査手法を適用したモデル検査装置の構成について図3を用いて説明する。図3は、モデル検査装置10の構成を示すブロック図である。図3に示すように、モデル検査装置10は、入力部11と、表示部12と、出力部13と、制御部14と、記憶部15とを備える。また、制御部14は、取得部14aと、変換部14bと、論理式生成部14cと、検査部14dとをさらに備えており、記憶部15は、検査条件情報15aと、状態遷移情報15bと、論理式情報15cとを記憶する。入力部11は、キーボードやマウスといった入力デバイス、可搬型記憶媒体のリーダ、他装置との通信を行う通信ボードなどで構成される。また、この入力部11は、受け取ったデータを制御部14へ渡す処理を行う。表示部12は、ディスプレイ装置などの表示デバイスである。この表示部12は、制御部14の検査部14dから渡された検査結果や、検査に用いる条件などを表示する。また、出力部13は、可搬型記憶媒体のライタ、他装置との通信を行う通信ボードなどで構成される。そして、この出力部13は、制御部14の検査部14dから渡された検査結果を可搬型記憶媒体や他装置などに対して出力する処理を行う。制御部14は、モデル検査装置10の全体制御を行う制御部である。取得部14aは、入力部11から受け取ったデータを、記憶部15へ記憶させる処理を行う。具体的には、この取得部14aは、モデル検査において検査対象が満たすべき性質を示す検査条件を、入力部11から受け取った場合には、受け取った検査条件を検査条件情報15aとして記憶部15へ記憶させる。また、取得部14aは、状態遷移表に対応する情報を、入力部11から受け取った場合には、受け取った情報を状態遷移情報15bとして記憶部15へ記憶させる。ここで、この状態遷移情報15bの具体例を説明するために、状態遷移表の例および状態遷移の例について図4および図5を用いて説明しておく。図4は、状態遷移表の例を示す図である。なお、図4のAには、状態遷移表STM1を、同じくBには、状態遷移表STM2を、それぞれ例示しているが、状態遷移表の個数には、特に、制限はない。図4のAおよびBに示すように、状態遷移表は、イベントを受け取った場合に、現在の状態がどの状態へ遷移するか、各種変数がどのように変化するか、どのようなイベントが発行されるか、を示すアクションを定義した情報である。図4のAに示す状態遷移表STM1がとりうる状態は、STS11およびSTS12である。また、状態遷移表STM1が受け取るイベントは、evt11およびevt12である。そして、所定の状態と、所定のイベントとで特定される要素は、セルと呼ばれる。たとえば、状態遷移表STM1における現在の状態がSTS11である場合に、evt11を受け取ると、状態は、STS12へ遷移する。また、変数aaは、0へ変化する。そして、現在の状態がSTS12である場合に、evt12を受け取ると、状態は、STS11へ遷移する。また、変数bbには100が加算され、変数ccから変数bbを差し引いた値があらたな変数ccの値となる。さらに、状態遷移表STM2に対してevt21が発行される。なお、このように、他の状態遷移表へ向けて発行されるイベントは、外部イベントと呼ばれる。また、図4のAにおいて/が記載されたセルは、状態とイベントとの組み合わせはありえるものの、処理を行わない無視セルをあらわしている。そして、×が記載されたセルは、状態とイベントとの組み合わせがありえない不可セルをあらわしている。なお、上記したアクションが定義されたセルは、通常セルと呼ばれる。次に、状態遷移表STM2について説明する。図4のBに示す状態遷移表STM2がとりうる状態は、STS21およびSTS22である。また、状態遷移表STM2が受け取るイベントは、evt21およびevt22である。なお、evt21は、図4のAに示した状態遷移表STM1から発行される外部イベントである。たとえば、状態遷移表STM2における現在の状態がSTS21である場合に、evt21を受け取ると、状態は、STS22へ遷移する。また、変数ccには200が加算される。そして、現在の状態がSTS22である場合に、evt22を受け取ると、状態は、STS21へ遷移する。また、変数ccは0へ変化する。このように、各状態遷移表は、状態とイベントとの組み合わせで特定されるセルにおいて、遷移先となる状態や、各種変数の変化、イベントの発行といったアクション遷移条件が定義された情報である。そして、上記した取得部14aは、このような状態遷移表に対応する情報を、あらかじめ定められた所定の形式へ変更することによって状態遷移情報15bを生成し、生成した状態遷移情報15bを記憶部15へ記憶させる。なお、図4のAおよびBには、それぞれ独立した状態遷移表を例示したが、状態遷移表におけるセルに、他の状態遷移表を挿入した入れ子形式の状態遷移表を用いることとしてもよい。また、図4のAおよびBでは、状態およびイベントの個数がそれぞれ2個の状態遷移表を例示したが、状態の個数、あるいは、イベントの個数には、特に、制限はない。次に、状態遷移の例について図5を用いて説明する。図5は、状態遷移の例を示す図である。なお、図5のAには、状態遷移の説明に用いる状態遷移表群を、図5のBには、状態遷移表における各種変数の初期値を、図5のCには、状態遷移の例を、それぞれ示している。以下、図5のAに示す3つの状態遷移表状態遷移表STM1、状態遷移表STM2および状態遷移表STM3を用いて状態遷移の説明を行う。なお、図5のAに示す各状態遷移表では、外部変数aおよび外部変数bを、イベントとして取り扱う。また、図5のAに示すように、各状態遷移表のセルに括弧付きで示したt1~t9は、状態間の遷移をあらわす。たとえば、状態遷移表STM1における現在の状態status1がs1である場合に、外部変数aが1と等しければ、状態はs2へ、外部変数bは1へ、それぞれ更新される。そして、このような遷移は、t1とあらわされる。なお、図5のAに示す3つの状態遷移表状態遷移表STM1、状態遷移表STM2および状態遷移表STM3は、それぞれ、非同期かつ並列に状態遷移を行う独立した状態遷移表である。また、図5のAに示した各状態遷移表の各種変数は、図5のBに示す初期値へ初期化される。具体的には、外部変数aは1へ、外部変数bは0へ、状態遷移表STM1の状態status1はs1へ、それぞれ初期化される。また、状態遷移表STM2の状態status2はs3へ、状態遷移表STM3の状態status3はs5へ、それぞれ初期化される。そして、図5のAおよびBに示した条件を前提とすると、状態遷移は、図5のCのようにあらわされる。すなわち、図5のCに示すように、初期状態に相当する状態S0では、外部変数a、外部変数b、状態遷移表STM1の状態status1、状態遷移表STM2の状態status2および状態遷移表STM3の状態status3は、それぞれ図5のBに示した初期値をとる。ここで、状態S0における外部変数bの値は0であるが、図5のAに示した各状態遷移表のイベントには、b==0が存在しない。一方、状態S0における外部変数aの値は1であり、状態遷移表STM1および状態遷移表STM2のイベントには、a==1が存在する。そして、状態遷移表STM1の状態status1はs1であるので、s1とa==1との組み合わせに対応するセルにおける遷移t1は可能である。また、状態遷移表STM2の状態status2はs3であるので、s3とa==1との組み合わせに対応するセルにおける遷移t4も可能である。なお、その他の遷移は不可能であるので、状態S0においては、状態S1への遷移t1と、状態S2への遷移t4とが発生しうる。そして、状態S0から状態S1への遷移t1に伴い、外部変数bは1へ、状態遷移表STM1の状態status1はs2へ、それぞれ更新される状態S1における破線の閉領域参照。また、状態S0から状態S2への遷移t4に伴い、外部変数bは2へ、状態遷移表STM2の状態status2はs4へ、それぞれ更新される状態S2における破線の閉領域参照。このように、各状態遷移表がとりうる各状態は、各状態遷移表が更新する各種変数の組み合わせとして表現される。また、現在の状態は、少なくとも1つの変数が変更されれば、他の状態へと遷移する。なお、図5のCに示すように、状態S1においては、遷移t3、遷移t4および遷移t8が発生しうる。また状態S2においては、遷移t1および遷移t6が発生しうる。なお、以下、同様に状態遷移が行われていくことになる。そして、後述する変換部14bは、モデル検査の対象となる状態遷移表非同期かつ並列に状態遷移を行う状態遷移表群に属する状態遷移表に対応する状態遷移情報15bを、記憶部15から抽出することになる。なお、図5のAには、3個の状態遷移表を例示したが、状態遷移表の個数には、特に、制限はない。図3の説明に戻り、制御部14の説明をつづける。変換部14bは、モデル検査の対象となる状態遷移表に対応する状態遷移情報15bを、記憶部15から抽出するとともに、抽出した状態遷移情報15bを論理式生成部14cへ渡す処理を行う。なお、この変換部14bは、上記した入れ子形式の複数の状態遷移表を、1つの状態遷移表へ展開する処理を併せて行う。ここで、並列に存在する状態遷移表の各単位をタスクと呼ぶこととすると、変換部14bは、並列に存在するすべてのタスクにそれぞれ対応する状態遷移情報15bを、記憶部から抽出する。なお、並列に存在するすべてのタスクは、挙動単位とも呼ばれる。論理式生成部14cは、変換部14bから受け取った状態遷移情報15bを、状態階層ごとに一階論理式化することによって、各階層に対応する論理式をそれぞれ生成する処理を行う。ここで、この論理式生成部14cが、状態遷移情報15bから論理式を生成する生成処理について具体的に説明する。なお、以下に示す論理式においては、∧はAND論理積を、∨はOR論理和を示す。また、∧を数列としてあらわす場合にはΛを、∨を数列としてあらわす場合にはVを、それぞれ用いることとする。なお、¬は否定をあらわしている。各状態遷移表をHiただし、iは1以上n以下の整数、k番目の階層図2のB参照における各状態遷移表の状態をstatusHi[k]、k番目の階層における全ての変数をVarD[k]、変数の値をvalueVarD[k]、k番目の階層に対応する論理式をstep[k]とすると、0番目の階層、すなわち、ルート階層の論理式step[0]は、であらわされる。なお、Dは、状態遷移表H1~Hnを含んだ状態遷移表デザインを指す。ここで、式1は、0番目の階層では、変数群の各変数値に初期値が設定され、すべての状態遷移表Hiにおける状態statusHiが0へ初期化されることを示している。次に、通常セルをc、k番目の階層における通常セルcの遷移条件をguardsc[k]、k番目の階層における通常セルcから発生するイベントをeventc[k]、通常セルcにおける状態の遷移前の値をsourcecとすると、k番目の階層における通常セルcの活性条件enabledc[k]は、であらわされる。なお、kは、1以上bd以下の整数である。ここで、式2は、k番目の階層の通常セルcでアクションの実行が可能となる条件が、k-1番目の階層で3つの条件をすべて満たすことである旨を示している。つまり、k-1番目の階層で、遷移条件を満たし、かつ、イベントがディスパッチされ、かつ、状態遷移表の状態が更新された場合に、k番目の階層の通常セルcにおいてアクションの実行が可能となる。次に、k番目の階層の通常セルcにおいてアクションが実行された結果について説明する。k番目の階層における通常セルcのアクション群をactionsc[k]、通常セルcにおける状態の遷移後の値をtargetcとすると、アクションの実行結果effectsc[k]は、であらわされる。ここで、式3は、アクション群が実行され、かつ、状態遷移表の状態が遷移後の値へ更新されることが、アクションの実行結果である旨を示している。次に、式3に示したactionsc[k]についてさらに詳細に説明する。k番目の階層について、アクション群を構成するm個のステートメントをstl[k]、変数をx、変数xの母集合をXとすると、actionsc[k]は、であらわされる。ここで、式4は、m個のステートメントstl[k]による操作によって変数xが変更され、かつ、stl[k]によって操作されなかった変数xについてはk-1番目の階層とk番目の階層とで変化がないことが、actionsc[k]として定義される旨を示している。そして、上記した式2、式3および式4から、k番目の階層における通常セルc[k]は、であらわされる。なお、allVarDは、状態遷移表デザインDに含まれる全ての変数であり、変数xは、allVarDに属している。ここで、式5は、k番目の階層における通常セルc[k]が、アクションの実行が可能なセル、または、アクションの実行が不可能なセルからなることをあらわしている。また、式5は、アクションの実行が可能なセルについては、アクションの実行結果が反映され、アクションの実行が不可能なセルについては、k-1番目の階層とk番目の階層とで変数xに変化がない旨を併せてあらわしている。次に、外部イベントに関する論理式について説明する。外部変数をeとすると、k番目の階層において外部変数eを操作する外部イベントによる影響exte[k]は、であらわされる。なお、\{e}は、外部変数eを除く旨をあらわしている。ここで、式6は、k-1番目の階層と、k番目の階層とで外部変数eが変化した場合には、外部変数e以外のすべての変数xが不変であり、k-1番目の階層と、k番目の階層とで外部変数eが変化しない場合には、外部変数eを含むすべての変数xが不変である旨をあらわしている。なお、式6では、外部変数eが2値変数Booleanである場合を例示しているが、外部変数は2値変数には限られない。そして、式5におけるc[k]と、式6におけるexte[k]とを用いると、k番目の階層における論理式step[k]は、であらわされる。なお、c∈Hi.Cnormalは、式7におけるc[k]が、状態遷移表Hiにおけるすべての通常セルである旨を、e∈Hi.Eexternalは、同じくexte[k]が、状態遷移表Hiにおけるすべての外部変数である旨を、それぞれあらわしている。ここで、式7は、k番目の階層における論理式step[k]が、n個の状態遷移表Hiそれぞれにおける、通常セルc[k]の内部的な遷移と、外部変数eによる外部的な遷移とで定義される旨をあらわしている。論理式生成部14cは、このようにして、変換部14bから受け取った状態遷移情報15bを、状態階層ごとに一階論理式化する。そして、論理式生成部14cは、生成した論理式を、論理式情報15cとして記憶部15へ記憶させる。検査部14dは、各階層に対応する論理式を含む論理式情報15cが、検査条件情報15aに含まれる検査条件に合致するか否かを検査する処理を行う。なお、この検査部14dとしては、一般的に流通している各種SMTソルバを用いることができる。また、検査部14dは、各階層に対応する論理式が、検査条件に反することを検出した場合には、検査条件に反する状態およびかかる状態に至る状態の履歴を反例情報として生成する。そして、検査部14dは、生成した反例情報を、表示部12や出力部13へ出力する。具体的には、検査部14dは、状態遷移表H1~Hnを含んだ状態遷移表デザインD、状態遷移表デザインDが満たすべき検査条件ρ、探索深度bdを用いた有限界モデル検査BMC検査を行う。そして、かかるBMC検査は、上記した式7に示したstep[k]を用いると、であらわされる。ここで、式8は、0番目からbd番目までの各階層kにそれぞれ対応する論理式step[k]が、各階層kに対応するいずれかの反例検査条件ρ[k]の否定に該当することを検査する旨をあらわしている。なお、検査部14dは、式8を用いて検出した反例についての反例情報、すなわち、検査条件ρ[k]に反する状態およびかかる状態に至る状態の履歴を生成する。記憶部15は、ハードディスクドライブや不揮発性メモリといった記憶デバイスである。検査条件情報15aは、取得部14aによって取得される検査条件である。なお、かかる検査条件は、たとえば、操作者の操作に基づき、入力部11を介してモデル検査装置10へ入力される。状態遷移情報15bは、取得部14aによって取得される、1または複数の状態遷移表たとえば、図4参照に対応する情報であり、たとえば、操作者の操作に基づき、入力部11を介してモデル検査装置10へ入力される。論理式情報15cは、論理式生成部14cによって生成される論理式群である。具体的には、この論理式情報15cは、並列に動作する状態遷移表群における各状態階層k0≦k≦bdにそれぞれ対応する論理式群である式7のstep[k]参照。次に、モデル検査装置10を用いたモデル検査手順の例について図6を用いて説明する。図6は、モデル検査装置10を用いたモデル検査手順の例を示す図である。なお、図6には、状態遷移表たとえば、図4参照を生成する装置である状態遷移表生成装置20を例示しているが、この状態遷移表生成装置20の機能を含んだモデル検査装置10を構成することとしてもよい。図6に示すように、状態遷移表生成装置20は、操作者の設計入力を受け付けると図6の1参照、状態遷移情報を生成する。そして、状態遷移表生成装置20は、生成した状態遷移情報をモデル検査装置10へ出力する。かかる状態遷移情報を受け取ったモデル検査装置10は、操作者の性質検査条件入力を受け付けると図6の2参照、最終的に、生成した反例情報、すなわち、設計の不具合を、操作者へ報知する図63参照。以下、設計の不具合を修正した設計入力図6の1参照、性質検査条件入力図6の2参照、設計の不具合の報知図6の3参照が繰り返されることで、最終的に、不具合のない設計を得ることが可能となる。次に、モデル検査装置10が実行する処理手順について図7を用いて説明する。図7は、モデル検査装置10が実行する処理手順を示すフローチャートである。図7に示すように、取得部14aが、すべての状態遷移情報15bを取得するとステップS101、変換部14bは、挙動単位、すなわち、並列して存在するすべてのタスクの状態遷移情報を、状態遷移情報15bから抽出するステップS102。つづいて、論理式生成部14cは、全変数の初期値を設定しステップS103、状態階層ごとに論理式を生成するステップS104。そして、検査部14dは、論理式生成部14cによって生成された論理式および取得部14aによって取得された検査条件に基づいてモデル検査を実行するステップS105。つづいて、検査部14dは、反例解析情報を、表示部12や出力部13へ出力しステップS106、処理を終了する。なお、図7では、1つの挙動単位に含まれる状態遷移表群についてモデル検査を実行する手順について示したが、複数の挙動単位についてモデル検査を行う場合には、図7に示した処理手順を、挙動単位ごとに繰り返せばよい。次に、図7のステップS105に示したモデル検査処理の処理手順について、図8を用いて説明する。図8は、モデル検査処理の処理手順を示すフローチャートである。図8に示すように、検査部14dが、論理式および検査条件の入力を受け付けるとステップS201、検査部14dは、各論理式の遷移探索において検査条件に反する状態があるか否かを検査するステップS202。そして、検査条件に反する状態がある場合にはステップS202,Yes、検出した状態および検出した状態に至る状態履歴を反例として記録しステップS203、ステップS202以降の処理を繰り返す。なお、かかる記録は、たとえば、記憶部15に対して行えばよい。ここで、検査条件に反する状態がない場合にはステップS202,No、処理を終了する。なお、図8では、すべての反例の検出が完了するまでモデル検査処理を繰り返す場合を例示したが、1つの反例を検出し、検出した反例を記録した時点で、モデル検査処理を終了することとしてもよい。上述したように、本実施例では、イベントに応じて変化する状態の遷移条件を表形式であらわした状態遷移表に対応する状態遷移情報を取得する取得部と、とりうる状態を各ノードとする木構造の階層ごとに遷移条件を一階論理式化した論理式を状態遷移情報から生成する論理式生成部とを備えるようにモデル検査装置を構成した。また、本実施例では、論理式生成部によって生成された論理式に基づいて充足性モジュロ理論による検査を実行する検査実行部を備えるようにモデル検査装置を構成した。このように、本実施例に係るモデル検査装置は、状態階層の階層ごとに遷移条件を一階論理式化するので、状態ごとにメモリ領域を用意する必要がない。したがって、本実施例に係るモデル検査装置によれば、メモリ状態爆発の問題を回避することができる。また、本実施例に係るモデル検査装置は、状態遷移表をモデル検査対象とすることとしたので、コンピュータプログラムに限らず、非同期な振る舞いモデルをもモデル検査することが可能となる。したがって、本実施例に係るモデル検査装置によれば、モデル検査の検査対象を拡大することができる。なお、上述した実施例では、1つの状態階層ごとに、1つの論理式を生成する場合について説明したが、生成した論理式を複数の論理式へ分割したうえで、モデル検査を実行することとしてもよい。また、1つの状態階層ごとに、複数の論理式を生成することとしてもよい。また、上記したモデル検査装置などの各装置は、たとえば、コンピュータで構成することができる。この場合、制御部は、CPUCentralProcessingUnitであり、記憶部は、メモリである。また、制御部の各機能は、あらかじめ作成されたプログラムを制御部へロードして実行させることによって実現することができる。さらなる効果や変形例は、当業者によって容易に導き出すことができる。このため、本発明のより広範な態様は、以上のように表しかつ記述した特定の詳細および代表的な実施例に限定されるものではない。したがって、添付の特許請求の範囲およびその均等物によって定義される総括的な発明の概念の精神または範囲から逸脱することなく、様々な変更が可能である。"