(57)【特許請求の範囲】
【請求項１】
入力プロパティを、複数の遷移ラベルを用いて表現される複数の遷移関数から構成される状態遷移機械に変換する状態遷移機械変換部と、
縮約ルールを記憶する記憶手段と、
無視する信号を表す縮約指示情報に従って、前記状態遷移機械において前記無視する信号に相当する遷移ラベルを無入力遷移に変換し、該無入力遷移を除去可能な縮約ルールを適用して遷移関数の書き換えを行うことにより該状態遷移機械を縮約する状態遷移機械縮約部と、
前記縮約処理後の状態遷移機械を出力プロパティに変換するプロパティ変換部と、を具備するプロパティ抽出装置。
【請求項２】
新たな縮約ルールを入力し、前記記憶手段に追加する縮約ルール入力部と、
前記記憶手段が記憶する縮約ルールの妥当性を検証するルール検証部とをさらに具備する請求項１に記載のプロパティ抽出装置。
【請求項３】
前記ルール検証部は、前記状態遷移機械縮約部による前記縮約ルールを用いた前記縮約前の状態遷移機械が有する遷移関数を第１の方程式に変形し、前記状態遷移機械縮約部による前記縮約ルールを用いた前記縮約後の状態遷移機械が有する遷移関数を第２の方程式に変形し、前記第１の方程式を前記第２の方程式に変形可能であるか否かを判定することにより、前記縮約ルールが妥当であるか否かを判定する請求項２記載のプロパティ抽出装置。
【請求項４】
着目する信号の入出力属性情報を前記縮約指示情報として用いて縮約を行い、該縮約により得られた状態遷移機械から特定のパターンに合致するプロパティを抽出し、該プロパティの集合からタイミング図を生成するタイミング図生成部をさらに具備する請求項１乃至３のいずれかに記載のプロパティ抽出装置。
【請求項５】
入力プロパティを、複数の遷移ラベルを用いて表現される複数の遷移関数から構成される状態遷移機械に状態遷移機械変換部が変換するステップと、
縮約ルールを記憶手段が記憶するステップと、
無視する信号を表す縮約指示情報に従って、前記状態遷移機械において前記無視する信号に相当する遷移ラベルを無入力遷移に変換し、該無入力遷移を除去可能な縮約ルールを適用して遷移関数の書き換えを行うことにより状態遷移機械縮約部が該状態遷移機械を縮約するステップと、
前記縮約処理後の状態遷移機械をプロパティ変換部が出力プロパティに変換するステップと、を有するプロパティ抽出方法。
【請求項６】
縮約ルール入力部が新たな縮約ルールを入力し、前記記憶手段に追加するステップと、
前記記憶手段が記憶する縮約ルールの妥当性をルール検証部が検証するステップとをさらに有する請求項５に記載のプロパティ抽出方法。
【請求項７】
前記ルール検証部は、前記状態遷移機械縮約部による前記縮約ルールを用いた前記縮約前の状態遷移機械が有する遷移関数を第１の方程式に変形し、前記状態遷移機械縮約部による前記縮約ルールを用いた前記縮約後の状態遷移機械が有する遷移関数を第２の方程式に変形し、前記第１の方程式を前記第２の方程式に変形可能であるか否かを判定することにより、前記縮約ルールが妥当であるか否かを判定する請求項６記載のプロパティ抽出方法。
【請求項８】
タイミング図生成部が、着目する信号の入出力属性情報を前記縮約指示情報として用いて縮約を行い、該縮約により得られた状態遷移機械から特定のパターンに合致するプロパティを抽出し、該プロパティの集合からタイミング図を生成するステップをさらに有する請求項５乃至７のいずれかに記載のプロパティ抽出方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウエア、ＬＳＩ等のハードウエア、ソフトウエアとハードウエアを組み合わせたシステム等を対象とするアサーションベース設計に用いられるプロパティ抽出装置及び方法に関する。
【背景技術】
【０００２】
ＬＳＩ設計や組込ソフトウエア設計において短時間開発を実現する１つの手段として、時相論理（ＬＴＬ，ＰＳＬ等）に代表される制約をアサーションとして仕様内に記述し、これを利用して設計や検証を行うアサーションベース設計／検証手法が着目されている（例えば下記「非特許文献１」を参照。）。アサーションベース設計では、アサーションはシステムの構成部品毎の性質（プロパティ）として定義され、この部品付属のプロパティをシステムに埋め込み、設計過程で部品のプロパティに違反しないかどうかを検証しながら設計を行っている。
【０００３】
設計問題とは、部分を適切に組み合わせて全体を作成する過程であるから、部品を組み合わせて初めて発生する性質（例えば部品をまたがる性質や、組み上がったシステム全体としての性質）を検証する要求があるが、これらの性質を個々の部品プロパティから得る手段はこれまで提供されていない。このため、プロパティを合併したり、必要な部分を抽出したりする技術が必要とされている。
【０００４】
一方、ソフトウエアの形式的な検証理論においては、ＬＴＬ（線形時相論理）に代表される論理式で記述されたプロパティをつかって、モデル検査等の検証技術が研究されてきた。例えばモデル検査では、ＬＴＬをいったん状態遷移機械（オートマトン）に変換し、これと検証対象のモデル（これも状態遷移機械で記述）を合わせてＬＴＬで記述される性質が成立するかどうかを検証するようにしている。
【０００５】
したがって、時相論理を状態遷移機械に変換する技術をベースにして、状態遷移機械を操作する技術を適用することにより、プロパティを合併したり必要な部分を抽出したりする技術を具体的に実現することが考えられる。
【０００６】
時相論理の一種である線形時相論理（ＬＴＬ：Ｌｉｎｅａｒ  Ｔｅｍｐｏｒａｌ  Ｌｏｇｉｃ）については、これを状態遷移機械の一種である交替性オートマトン（Ａｌｔｅｒｎａｔｉｎｇ  Ａｕｔｏｍａｔａ）に変化する技術（例えば、下記「非特許文献２」を参照。）が確立されている。さらに、交替性オートマトンを線形時相論理に変換する技術（例えば下記「非特許文献３」を参照。）も確立されている。
【非特許文献１】「アサーションベース設計」原書2版，Harry D.Foster・Adam C.Krolnik・David J. Lacey著，東野  輝夫・岡野  浩三・中田  明夫  監訳，丸善書店
【非特許文献２】"An Automata-Theoretic Approach to Linear Temporal Logic", MY Vardi - Logics for Concurrency: Structure Versus Automata, 1996,Springer-Verlag Inc.
【非特許文献３】"Deeper Connections between LTL and Alternating Automata", Pelanek, R. and Strejcek, J.,Proc. of Conference on Implementation and Application of Automata (CIAA 2005)
【発明の開示】
【発明が解決しようとする課題】
【０００７】
上述したように、従来の技術では、アサーションは、個別の部品や関数毎に与えられ、システム全体の制約としての把握および活用が困難である。例えば複数の部品にまたがる制約を、設計者が活用できる形で抽出することができない。
【０００８】
したがって、アサーションとして定義されるシステムの構成部品毎の性質（プロパティ）から所望の部分を抽出できることが好ましい。
【０００９】
本発明はかかる事情を考慮してなされたものであり、オートマトンを対象に操作演算を施すことにより、所望プロパティの抽出を実現することを目的とする。
【課題を解決するための手段】
【００１０】
本発明の一観点に係るプロパティ抽出装置は、入力プロパティを、複数の遷移ラベルを用いて表現される複数の遷移関数から構成される状態遷移機械に変換する状態遷移機械変換部と、縮約ルールを記憶する記憶手段と、無視する信号を表す縮約指示情報に従って、前記状態遷移機械において前記無視する信号に相当する遷移ラベルを無入力遷移に変換し、該無入力遷移を除去可能な縮約ルールを適用して遷移関数の書き換えを行うことにより該状態遷移機械を縮約する状態遷移機械縮約部と、縮約処理後の状態遷移機械を出力プロパティに変換するプロパティ変換部と、を具備する。
【００１１】
本発明の一観点に係るプロパティ抽出方法は、入力プロパティを、複数の遷移ラベルを用いて表現される複数の遷移関数から構成される状態遷移機械に状態遷移機械変換部が変換するステップと、縮約ルールを記憶手段が記憶するステップと、無視する信号を表す縮約指示情報に従って、前記状態遷移機械において前記無視する信号に相当する遷移ラベルを無入力遷移に変換し、該無入力遷移を除去可能な縮約ルールを適用して遷移関数の書き換えを行うことにより状態遷移機械縮約部が該状態遷移機械を縮約するステップと、縮約処理後の状態遷移機械をプロパティ変換部が出力プロパティに変換するステップと、を有する。
【発明の効果】
【００１２】
本発明によれば、縮約指示情報に従い、オートマトンを対象に操作演算を施すことにより、所望プロパティを抽出するプロパティ抽出装置及び方法を提供できる。
【発明を実施するための最良の形態】
【００１３】
以下、図面を参照しながら本発明の実施形態を説明する。
【００１４】
図１は本発明の一実施形態に係るプロパティ抽出装置を示すブロック図である。同図に示すようにプロパティ抽出装置２は、入力プロパティ１を状態遷移機械４に変換する状態遷移機械変換部３と、縮約指示情報５に従って縮約ルール７を適用し、状態遷移機械４を縮約する状態遷移機械縮約部６と、縮約ルール７を入力し、追加し、あるいは削除することが可能なルール入力部８と、縮約ルール７の妥当性を検証するルール検証部９と、縮約処理後の状態遷移機械４を出力プロパティ１１に変換するプロパティ変換部１０と、入出力属性情報１３に従って出力プロパティ１１からタイミング図を生成するタイミング図生成部１２とを有する。なお、上記構成において、縮約ルール７は、縮約ルールを表す情報を記憶するメモリやハードディスク等の記憶手段を構成する。また、ルール検証部９及び／又はタイミング図生成部１２を含まない構成とすることも可能である。また、本実施形態のプロパティ抽出装置２は、汎用的なコンピュータのハードウェアを用いて情報処理を行うソフトウェアとして実現することができる。
【００１５】
最初に、本実施形態で取り扱うプロパティの代表的な記述方法である線形時相論理ＬＴＬ（Ｌｉｎｅａｒ  Ｔｅｍｐｏｒａｌ  Ｌｏｇｉｃ）について説明する。ＬＴＬは、項ｐ１，ｐ２，・・・と、論理作用素である「¬」（否定）、「∨」（論理和）、「∧」（論理積）、「→」（含意）と、「ｔｒｕｅ」（真）、「ｆａｌｓｅ」（偽）と、様相作用素とで構成される。様相作用素は、Ｘ（ｎｅｘｔ）、Ｇ（ｇｌｏｂａｌｌｙ）、Ｆ（ｉｎ  ｔｈｅ  ｆｕｔｕｒｅ）、Ｕ（ｕｎｔｉｌ）、Ｒ（ｒｅｌｅａｓｅ）である。
【００１６】
ここで、Ｘ，Ｇ，Ｆ作用素は単項演算である。Ｕ，Ｒは二項演算である。ψとφが論理式であるとすると、様相作用素は次の意味を持つ。すなわち、“Ｘψ”は「次の状態でψが真である」性質を表し、“Ｇψ”は「今後常にψが真である」性質を表し、“Ｆψ”は「今後いつかψが真になる」性質を表し、“φＵψ”は「ψは現在または将来に真であり、かつその時点までφが真である」性質を表し、“φＲψ”は「φが真になる時点までψが真でありつづける」性質を表す。
【００１７】
様相作用素間は互いに関係があり、例えば、Ｆψ＝ｔｒｕｅ  Ｕψ、Ｇψ＝¬Ｆ¬ψ＝¬（ｔｒｕｅ  Ｕ¬ψ）＝ｆａｌｓｅ  Ｒψ、ψＲφ＝¬（¬ψＵ¬φ）のように、ある作用素を別の作用素で置き換えることも可能である。
【００１８】
（状態遷移機械変換部３）
まず状態遷移機械の定義について説明する。本実施形態における状態遷移機械は、例えば交替性オートマトン（Ａｌｔｅｒｎａｔｉｎｇ  Ａｕｔｏｍａｔａ）であるとする。交替性オートマトンＡは（Σ，Ｑ，ｑ０，δ，Ｆ）のタプルで構成される。ただし、Σは有限のアルファベット及びｔｒｕｅであり、Ｑは有限の状態の集合であり、ｑ０∈Ｑは初期状態であり、ｔｒｕｅ∈Qは受理状態、ｆａｌｓｅ∈Qは不受理状態である。δは遷移関数であり、δ：Ｑ×Σ→β＋（Ｑ）と定義される。ここで、β＋（Ｑ）は状態Ｑ上の正のブール式を表している。Ｆ⊆Ｑは受理状態である。
【００１９】
（プロパティ例）
プロパティ抽出装置２への入力として、例えば「ψ＝Ｇ（ａ→Ｆｂ）」のような入力プロパティ１が与えられる。このψは「今後常に、信号ａが成立するならば、いつかは信号ｂが成立する」ことを意味する。状態遷移機械変換部３は、以下に説明するように、入力プロパティ１を交替性オートマトン（状態遷移機械４）に変換する。プロパティを交替性オートマトンにどのようにして変換するかについては、非特許文献２の記載を参考にすることもできる。
【００２０】
（１）状態Ｑ＝｛ｑ＿＜φ＞，ｑ＿＜¬φ＞｜φはψの部分式｝とする。ここで、ｑ＿＜φ＞とはφを代表する状態である。
【００２１】
（２）遷移関数δはａ，ｂ∈Σとすると、以下の書換により帰納的に定義される。
【００２２】
（遷移関数の帰納的定義）
δ（ｑ＿＜Ｔ＞，ａ）＝ｔｒｕｅ  
δ（ｑ＿＜ａ＞，ｂ）＝ｔｒｕｅ    ．．．ａ＝ｂである場合  
δ（ｑ＿＜ａ＞，ｂ）＝ｆａｌｓｅ  ．．．ａ≠ｂである場合  
δ（ｑ＿＜¬φ＞，ａ）＝ｄｕａｌ（δ（ｑ＿＜φ＞，ａ））  
δ（ｑ＿＜φ∧ρ＞，ａ）＝δ（ｑ＿＜φ＞，ａ）∧δ（ｑ＿＜ρ＞，ａ）  
δ（ｑ＿＜Ｘφ＞，ａ）＝ｑ＿＜φ＞  
δ（ｑ＿＜φＵρ＞，ａ）＝δ（ｑ＿＜ρ＞，ａ）∨（δ（ｑ＿＜φ＞，ａ）∧（ｑ＿＜φＵρ＞））
ここで、ｄｕａｌ（α）は、項αに対する双対項であり以下のように定義される。
【００２３】
（双対項（ｄｕａｌ）の定義）
ｄｕａｌ（ｔｒｕｅ）＝ｆａｌｓｅ，ｄｕａｌ（ｆａｌｓｅ）＝ｔｒｕｅ  
ｄｕａｌ（ｑ＿＜¬φ＞）＝ｑ＿＜φ＞  
ｄｕａｌ（ｑ＿＜φ＞）＝ｑ＿＜¬φ＞  
ｄｕａｌ（β∧γ）＝ｄｕａｌ（β）∨ｄｕａｌ（γ）  
ｄｕａｌ（β∨γ）＝ｄｕａｌ（β）∧ｄｕａｌ（γ）  
以上の定義を使えば、例えば、δ（ｑ＿＜φ＞Ｒρ，ａ）を以下のように展開できる。
【００２４】
δ（ｑ＿＜φＲρ＞，ａ）  
＝δ（ｑ＿＜¬（¬φ  Ｕ  ¬ρ）＞，ａ）  
＝ｄｕａｌ（δ（ｑ＿＜¬φ  Ｕ  ¬ρ＞，ａ））  
＝ｄｕａｌ（δ（ｑ＿＜¬ρ＞，ａ）∨（δ（ｑ＿＜¬φ＞，ａ）∧（ｑ＿＜¬φＵ¬ρ＞））  
＝ｄｕａｌ（ｄｕａｌ（δ（ｑ＿＜ρ＞，ａ）））∨（ｄｕａｌ（δ（ｑ＿＜φ＞，ａ））∧（ｑ＿＜¬φＵ¬ρ＞）））  
＝δ（ｑ＿＜ρ＞，ａ）∧（ｄｕａｌ（ｄｕａｌ（δ（ｑ＿＜φ＞，ａ））∧（ｑ＿＜¬φＵ¬ρ＞）））  
＝δ（ｑ＿＜ρ＞，ａ）∧（δ（ｑ＿＜φ＞，ａ）∨（ｑ＿＜φ＞Ｒρ））
＜例１＞
ここで、遷移関数の計算により入力プロパティ１を交替性オートマトンに変換する手順を説明する。
【００２５】
入力プロパティ１であるψ＝Ｇ（ａ→Ｆｂ）は、ψ１＝¬ａ∨（ｔｒｕｅ  Ｕ  ｂ）、ψ２＝（ｔｒｕｅ  Ｕ  ｂ）であるとすると、ψ＝Ｇ（ａ→Ｆｂ）＝¬Ｆ¬（¬ａ∨（ｔｒｕｅ  Ｕ  ｂ））＝¬（ｔｒｕｅ  Ｕ  ¬（¬ａ∨（ｔｒｕｅ  Ｕ  ｂ）））＝ｆａｌｓｅ  Ｒ  ψ１と置き換えることができる。従って、以下のように遷移関数を計算できる。
【００２６】
（遷移の計算）
δ（ψ，ａ）＝δ（ψ１，ａ）∧（δ（ｆａｌｓｅ，ａ）∨ψ）  
＝（δ（¬ａ，ａ）∨δ（ψ２，ａ））∧（ｆａｌｓｅ∨ψ）  
＝（δ（¬ａ，ａ）∨（δ（ｂ，ａ）∨（δ（ｔｒｕｅ，ａ）∧ψ２））∧（ｆａｌｓｅ∨ψ）  
＝（ｆａｌｓｅ∨（ｆａｌｓｅ∨（ｔｒｕｅ∧ψ２））∧（ｆａｌｓｅ∨ψ）  
＝ψ２∧ψ
δ（ψ，ｂ）＝（δ（¬ａ，ｂ）∨（δ（ｂ，ｂ）∨（δ（ｔｒｕｅ，ｂ）∧ψ２））∧（ｆａｌｓｅ∨ψ）  
＝（ｔｒｕｅ∨（ｔｒｕｅ∨（ｔｒｕｅ∧ψ２））∧（ｆａｌｓｅ∨ψ）  
＝ｔｒｕｅ  ∧ψ＝ψ
δ（ψ１，ａ）＝（δ（¬ａ，ａ）∨δ（ψ２，ａ））  
＝（δ（¬ａ，ａ）∨（δ（ｂ，ａ）∨（δ（ｔｒｕｅ，ａ）∧ψ２））  
＝（ｆａｌｓｅ∨（ｆａｌｓｅ∨（ｔｒｕｅ∧ψ２））  
＝ψ２
δ（ψ２，ａ）＝（δ（ｂ，ａ）∨（δ（ｔｒｕｅ，ａ）∧ψ２）  
＝（ｆａｌｓｅ∨（ｔｒｕｅ∧ψ２）  
＝ψ２
δ（ψ２，ｂ）＝（δ（ｂ，ｂ）∨（δ（ｔｒｕｅ，ｂ）∧ψ２）  
＝（ｔｒｕｅ∨（ｔｒｕｅ∧ψ２）  
＝ｔｒｕｅ
ψ１は初期状態ψから到達可能でないことを考慮すると、ψに相当する交替性オートマトンＡ＝（Σ，ｑ０，δ，Ｆ）は次のようになる。
【００２７】
交替性オートマトンＡ＝（Σ，ｑ０，δ，Ｆ）  
Σ＝｛ｑ＿｛ψ｝，ｑ＿｛ψ１｝｝，  
ｑ０＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ｝，ａ）＝ｑ＿｛ψ｝∧ｑ＿｛ψ２｝  
δ（ｑ＿｛ψ］，ｂ）＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ２｝，ａ）＝ｑ＿｛ψ２｝  
δ（ｑ＿｛ψ２｝，ｂ）＝ｔｒｕｅ  
この＜例１＞の場合において、上記の交替性オートマトンをグラフ形式で表したものを図２に示す。
【００２８】
＜例２＞
上記＜例１＞と同様に、入力プロパティ１の別の例であるψ＝Ｇ（（ａ→Ｆｂ）∧（ｂ→Ｆｃ））を状態遷移機械変換部３により交替性オートマトンに変換する場合を以下に示す。
【００２９】
Ｇ（（ａ→Ｆｂ）∧（ｂ→Ｆｃ））  
＝ｆａｌｓｅ  Ｒ  （（ａ→Ｆｂ）∧（ｂ→Ｆｃ））  
＝ｆａｌｓｅ  Ｒ  ψ１  
＝ｆａｌｓｅ  Ｒ  （ψ２∧ψ３）  
となるので、遷移関数の計算は次のようになる。
【００３０】
δ（ψ，ａ）＝δ（ψ１，ａ）∧（δ（ｆａｌｓｅ，ａ）∨ψ）  
＝（δ（ψ２，ａ）∧δ（ψ３，ａ））∧（ψ）  
＝（（δ（¬ａ，ａ）∨δ（ｔｒｕｅ  Ｕ  ｂ，ａ））∧（δ（¬ｂ，ａ）∨δ（ｔｒｕｅ  Ｕ  ｃ，ａ）））∧ψ  
＝（（δ（¬ａ，ａ）∨（δ（ｂ，ａ）∨（δ（ｔｒｕｅ，ａ）∧（ψ２’））∧（δ（¬ｂ，ａ）∨（δ（ｃ，ａ）∨（δ（ｔｒｕｅ，ａ）∧（ψ３’）））∧ψ  
＝（（ｆａｌｓｅ∨（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ２’）））∧（ｔｒｕｅ∨（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ３’））））∧ψ  
＝（ψ２’∧ｔｒｕｅ）∧ψ  
＝ψ２’∧ψ
δ（ψ，ｂ）＝（（δ（¬ａ，ｂ）∨（δ（ｂ，ｂ）∨（δ（ｔｒｕｅ，ｂ）∧（ψ２’））∧（δ（¬ｂ，ｂ）∨（δ（ｃ，ｂ）∨（δ（ｔｒｕｅ，ｂ）∧（ψ３’）））∧ψ  
＝（（ｔｒｕｅ∨（ｔｒｕｅ∨（ｔｒｕｅ∧（ψ２’））∧（ｆａｌｓｅ∨（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ３’）））∧ψ  
＝ψ３’∧ψ
δ（ψ，ｃ）＝（（δ（¬ａ，ｃ）∨（δ（ｂ，ｃ）∨（δ（ｔｒｕｅ，ｃ）∧（ψ２’））∧（δ（¬ｂ，ｃ）∨（δ（ｃ，ｃ）∨（δ（ｔｒｕｅ，ｃ）∧（ψ３’）））∧ψ  
＝（（ｔｒｕｅ∨（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ２’））∧（ｔｒｕｅ∨（ｔｒｕｅ∨（ｔｒｕｅ∧（ψ３’）））∧ψ  
＝（ｔｒｕｅ  ∧  ｔｒｕｅ）∧ψ  
＝ψ
δ（ψ２’，ａ）＝δ（ｔｒｕｅ  Ｕ  ｂ，ａ）  
＝（δ（ｂ，ａ）∨（δ（ｔｒｕｅ，ａ）∧（ψ２’））  
＝（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ２’））  
＝ψ２’
δ（ψ２’，ｂ）＝δ（ｔｒｕｅ  Ｕ  ｂ，ｂ）  
＝（δ（ｂ，ｂ）∨（δ（ｔｒｕｅ，ｂ）∧（ψ２’））  
＝（ｔｒｕｅ∨（ｔｒｕｅ∧（ψ２’））  
＝ｔｒｕｅ
δ（ψ２’，ｃ）＝δ（ｔｒｕｅ  Ｕ  ｂ，ｃ）  
＝（δ（ｂ，ｃ）∨（δ（ｔｒｕｅ，ｃ）∧（ψ２’））  
＝（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ２’））  
＝ψ２’
δ（ψ３’，ａ）＝δ（ｔｒｕｅ  Ｕ  ｃ，ａ）  
＝（δ（ｃ，ａ）∨（δ（ｔｒｕｅ，ａ）∧（ψ３’））  
＝（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ３’））  
＝ψ３’
δ（ψ３’，ｂ）＝δ（ｔｒｕｅ  Ｕ  ｃ，ｂ）  
＝（δ（ｃ，ｂ）∨（δ（ｔｒｕｅ，ｂ）∧（ψ３’））  
＝（ｆａｌｓｅ∨（ｔｒｕｅ∧（ψ３’））  
＝ψ３’
δ（ψ３’，ｃ）＝δ（ｔｒｕｅ  Ｕ  ｃ，ｃ）  
＝（δ（ｃ，ｃ）∨（δ（ｔｒｕｅ，ｃ）∧（ψ３’））  
＝（ｔｒｕｅ∨（ｔｒｕｅ∧（ψ３’））  
＝ｔｒｕｅ
ψに相当する交替性オートマトンＡ＝（Σ，ｑ０，δ，Ｆ）は次のようになる。
【００３１】
交替性オートマトンＡ＝（Σ，ｑ０，δ，Ｆ）  
Σ＝｛ｑ＿｛ψ｝，ｑ＿｛ψ２’｝，ｑ＿｛ψ２’｝｝  
ｑ０＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ｝，ａ）＝ｑ＿｛ψ｝∧ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ｝，ｂ）＝ｑ＿｛ψ｝∧ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ］，ｃ）＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ２’｝，ａ）＝ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ２’｝，ｂ）＝ｔｒｕｅ  
δ（ｑ＿｛ψ２’｝，ｃ）＝ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ３’｝，ａ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｂ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｃ）＝ｔｒｕｅ
この＜例２＞の場合において、上記の交替性オートマトンをグラフ形式で表したものを図３に示す。
【００３２】
（状態遷移機械縮約部６）
プロパティψ＝Ｇ（（ａ→Ｆｂ）∧（ｂ→Ｆｃ））に対して、縮約指示情報５として｛ａ，ｃ｝すなわち「信号ａ，ｃのみに着目する」という縮約指示があるとする。これは信号ｂを無視することに相当する。信号を無視することは、オートマトンとしては、無視する信号に関わる遷移ラベルをすべて無入力遷移（以下、「ε」と表記する。）に変換することになる。本例では、次に示す通り、状態遷移機械縮約部６が交替性オートマトン（状態遷移機械４）における信号ｂのラベルを全てεに変換する。
【００３３】
Σ＝｛ｑ＿｛ψ｝，ｑ＿｛ψ２’｝，ｑ＿｛ψ２’｝｝  
ｑ０＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ｝，ａ）＝ｑ＿｛ψ｝∧ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ｝，ε）＝ｑ＿｛ψ｝∧ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ］，ｃ）＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ２’｝，ａ）＝ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ２’｝，ε）＝ｔｒｕｅ  
δ（ｑ＿｛ψ２’｝，ｃ）＝ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ３’｝，ａ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ε）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｃ）＝ｔｒｕｅ  
Ｆ＝｛ψ｝
（縮約ルールの適用）
「縮約」とはオートマトンにおけるε遷移を、受理言語を変更することなく削除することに相当する。以下、本実施形態における「縮約ルール」を例示する。「縮約」は遷移関数を部分的に書き換えることにより実現され、これを記憶する縮約ルール７は書換ルールとして記述される。以下、縮約ルール７に記憶される縮約ルールを例示する。また図４に、各々の縮約ルールにより遷移関数がどのように縮約されるかをグラフにより示す。
【００３４】
＜縮約ルール１＞  
［縮約前の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿２  
δ（ｑ＿２，ε）＝ｑ＿３  
δ（ｑ＿３，ｃ）＝ｑ＿４｝  
［縮約後の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２３  
δ（ｑ＿２３，ｂ）＝ｑ＿２３  
δ（ｑ＿２３，ｃ）＝ｑ＿４｝  
＜縮約ルール２＞  
［縮約前の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿２  
δ（ｑ＿２，ε）＝ｔｒｕｅ｝  
Ｆ＝Ｆ０  
［縮約後の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２Ｔ  
δ（ｑ＿２Ｔ，ｂ）＝ｑ＿２Ｔ｝  
Ｆ＝Ｆ０∪｛ｑ＿２Ｔ｝  
＜縮約ルール３＞  
［縮約前の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿２  
δ（ｑ＿２，ε）＝ｑ＿３  
δ（ｑ＿３，ｂ）＝ｑ＿４｝  
［縮約後の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２３  
δ（ｑ＿２３，ｂ）＝ｑ＿２３  
δ（ｑ＿２３，ｂ）＝ｑ＿４｝  
＜縮約ルール４＞  
［縮約前の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿１，ε）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿３｝  
［縮約後の遷移関数］  
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿３  
δ（ｑ＿１，ｂ）＝ｑ＿３｝
状態遷移機械縮約部６は、以上のような縮約ルールを適宜、交替性オートマトン（状態遷移機械４）に適用することにより遷移関数の書換を行う。具体的な縮約の手順は例えば以下の通りである。
【００３５】
［手順１］：縮約ルール７において、適用できる縮約ルールを検索する。
【００３６】
［手順１ａ］：手順１において適用できる縮約ルールが見つかったならば手順２に移る。
【００３７】
［手順１ｂ］：手順１において適用できる縮約ルールが見つかったならば手順４に移る。
【００３８】
［手順２］：手順１において見つかった縮約ルールを適用することにより遷移関数の書き換えを行う。これによりε遷移を除去する。
【００３９】
［手順３］：手順１以降を繰り返す。
【００４０】
［手順４］：交替性オートマトンにε遷移が残っていなければ正常終了し、そうでない場合は異常終了とする。
【００４１】
まず＜縮約ルール４＞を  
δ（ｑ＿｛ψ３’｝，ａ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ε）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｃ）＝ｔｒｕｅ  
においてψ３’に関する遷移関数の部分に適用すると、上記は、ε遷移を含まない  
δ（ｑ＿｛ψ３’｝，ａ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｃ）＝ｔｒｕｅ  
に書き換えられる。
【００４２】
また、＜縮約ルール２＞を  
δ（ｑ＿｛ψ２’｝，ａ）＝ｑ＿｛ψ２’｝  
δ（ｑ＿｛ψ２’｝，ε）＝ｔｒｕｅ  
δ（ｑ＿｛ψ２’｝，ｃ）＝ｑ＿｛ψ２’｝  
においてψ２’に関する遷移関数の部分に適用すると、上記は、ε遷移を含まない  
δ（ｑ＿｛ψ２’Ｔ｝，ａ）＝ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ２’Ｔ｝，ｃ）＝ｑ＿｛ψ２’Ｔ｝  
Ｆ＝Ｆ０∪｛ψ２’Ｔ｝  
に書き換えられる。
【００４３】
ここまでの交替性オートマトンの縮約結果は以下の通りである。
【００４４】
Σ＝｛ｑ＿｛ψ｝，ｑ＿｛ψ２’Ｔ｝，ｑ＿｛ψ３’｝｝  
ｑ０＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ｝，ａ）＝ｑ＿｛ψ｝∧ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ｝，ε）＝ｑ＿｛ψ｝∧ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ］，ｃ）＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ２’Ｔ｝，ａ）＝ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ２’Ｔ｝，ｃ）＝ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ３’｝，ａ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｃ）＝ｔｒｕｅ
さらに、ψに関する遷移関数、すなわち
δ（ｑ＿｛ψ｝，ａ）＝ｑ＿｛ψ｝∧ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ｝，ε）＝ｑ＿｛ψ｝∧ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ］，ｃ）＝ｑ＿｛ψ｝  
δ（ｑ＿｛ψ３’｝，ａ）＝ｑ＿｛ψ３’｝  
δ（ｑ＿｛ψ３’｝，ｃ）＝ｔｒｕｅ
には＜縮約ルール３＞を適用することができる。
【００４５】
ψとψ３’を１状態＝ψ４に融合して、以下を得る。
【００４６】
δ（ｑ＿｛ψ４｝，ａ）＝ｑ＿｛ψ４｝∧ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ４］，ｃ）＝ｑ＿｛ψ４｝  
δ（ｑ＿｛ψ４｝，ａ）＝ｑ＿｛ψ４｝  
δ（ｑ＿｛ψ４｝，ｃ）＝ｔｒｕｅ
最終的には、ε遷移が除去されたオートマトンは以下のようになる。  
（縮約後の交替性オートマトン）  
Σ＝｛ｑ＿｛ψ４｝，ｑ＿｛ψ２’Ｔ｝｝  
ｑ０＝ｑ＿｛ψ４｝  
δ（ｑ＿｛ψ２’Ｔ｝，ａ）＝ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ２’Ｔ｝，ｃ）＝ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ４｝，ａ）＝ｑ＿｛ψ４｝∧ｑ＿｛ψ２’Ｔ｝  
δ（ｑ＿｛ψ４］，ｃ）＝ｑ＿｛ψ４｝  
δ（ｑ＿｛ψ４｝，ａ）＝ｑ＿｛ψ４｝  
δ（ｑ＿｛ψ４｝，ｃ）＝ｔｒｕｅ  
Ｆ＝｛ψ２’Ｔ｝  
図５に、上記の交替性オートマトンをグラフ形式で示す。
【００４７】
（プロパティ変換部１０）
プロパティ変換部１０は、状態遷移機械縮約部６により処理された交替性オートマトン（状態遷移機械４）を、受理言語が等しい線形時相論理の出力プロパティ１１に変換する。オートマトンで表現されたプロパティを論理式に展開する方法として、ここでは非特許文献３に記載の手順に従って説明する。この方法では、オートマトンの状態変数毎に論理式を変換できる。初期状態に対する論理式がオートマトン全体の論理式である。
【００４８】
まずオートマトンＡにおける状態変数ｐに対応する論理式、すなわち
ψ＿｛ｐ｝＝ψ１  Ｕ  ψ２
が求められる。
【００４９】
ただし、ψ＿｛ｎ｝とは状態＝ｎに対応する論理式を表している。
【００５０】
ψ１は自己ループを含む遷移に関する部分式、すなわち（ａ∧Ｘψ＿｛ｑ｝）の遷移分の論理和である。ただし、ψ＿｛ｑ｝はラベルａの自己遷移以外の遷移先の状態に対応する論理式である。
【００５１】
ψ２は自己ループを含まない遷移に関する部分式、すなわち（ｂ∧Ｘψ＿｛ｒ｝）の遷移分の論理和である。ただし、ψ＿｛ｒ｝はラベルｂの遷移先の状態に対応する論理式である。
【００５２】
上記縮約後の交替性オートマトンの例では、  
ψ＿｛ｑ０｝＝（（ａ∧Ｘψ＿｛ｑ１｝）∨ａ∨ｃ）Ｕ（ｃ）  
ψ＿｛ｑ１｝＝（ａ∨ｃ）  
すなわち、
ψ＿｛ｑ０｝＝（（ａ∧Ｘ（ａ∨ｃ））∨ａ∨ｃ）Ｕ（ｃ）  
となる。
【００５３】
（ルール検証部９）
ルール検証部９は、縮約ルール７の適用により縮約前の遷移関数を縮約後の遷移関数に書き換えることの妥当性を検証する。最初に、ルール検証部９は遷移関数を連立方程式に変形する。次に、ルール検証部９は、この連立方程式を対象に代入・書換等の演算を行い、縮約前の方程式から縮約後の方程式に変形ができるかどうかを調べることにより上記妥当性の有無を判定する。以下、縮約ルール４を例として具体的に説明する。
【００５４】
＜縮約ルール４＞は、上記の通り、［縮約前の遷移関数］を
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿１，ε）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿３｝  
とするものであり、［縮約後の遷移関数］を
｛δ（ｑ＿１，ａ）＝ｑ＿２  
δ（ｑ＿２，ｂ）＝ｑ＿３  
δ（ｑ＿１，ｂ）＝ｑ＿３｝  
とするものである。
【００５５】
ルール検証部９によるルール検証は具体的には以下の手順に従って行われる。
【００５６】
［手順１］：状態関数定義を式形式に変換する。
【００５７】
［手順２］：同一再帰変数を左辺に持つ式を１つにまとめる。
【００５８】
［手順３］：（連立）方程式を解く。
【００５９】
［手順４］：縮約前後の遷移関数に対して手順１〜手順３を実行する。
【００６０】
［手順５］：手順４の結果が同値ならば、当該縮約ルールは正しいと判定する。
【００６１】
ここで、本実施形態における「（連立）方程式」とは、  
再帰変数（V＿ｉ：ｉはｎ以下の自然数）と、ラベル記号（ａ，ｂ，．．等）と、ラベル記号を再帰変数の係数として用いるための記号（．）と、ラベル記号間の演算子（｜）と、再帰変数間の演算子（｜）と、再帰変数の時間発展を表す（＝）演算子とにより構成され、Ｖ＿ｉ＝Σｊ≦ｎ［ラベルあるいは（｜）演算されたラベル］．Ｖ＿ｊという形式で表される式の集合であるとする。
【００６２】
以下は「（連立）方程式」の例である。Ｘ，Ｙ，Ｚが再帰変数、ａ，ｂ，ｃ，ｔｒｕｅがラベル記号である。  
Ｘ＝ａ．Ｙ＋ｃ．Ｘ  
Ｙ＝ｂ．Ｚ  
Ｚ＝ｔｒｕｅ．Ｚ  
方程式における再帰変数は状態変数に対応する。また、式は、状態遷移関数に対応している。例えば、以下の再帰変数（Ｘ，Ｙ）とラベル（ａ，ｃ）を使った式、すなわちＸ＝ａ．Ｙ＋ｃ．Ｘは、  
δ（Ｘに対応する状態変数，ａ）＝Ｙに対応する状態変数  
δ（Ｘに対応する状態変数，ｃ）＝Ｘに対応する状態変数  
という２行にわたる遷移関数に対応する。
【００６３】
交替制オートマトンの特徴であるＡＮＤ分岐例δ（ｑ＿ｘ，ａ）＝ｑ＿ｙ∧ｑ＿ｚは、Ｘ＝ａ．（Ｙ｜Ｚ）として表される。（Ｙ｜Ｚ）は状態ＹとＺが同時に成立する組合せ状態である。
【００６４】
方程式係数に現れる（｜）演算により結合されたラベルは、ラベルが同時に成立することを表す。例えば式、Ｘ＝（ａ｜ｂ）．Ｙは、ａとｂが同時に成立する時にＹに遷移する遷移関数、すなわち「δ（Ｘに対応する状態変数，ａ＆ｂ）＝Ｙに対応する状態変数」に対応している。
【００６５】
以下、［手順１］〜［手順５］の各々を詳細に説明する。
【００６６】
［手順１］について説明する。上述したように［手順１］では、状態関数定義を式形式に変換する。これは、以下の［手順１−１］及び［手順１−２］から構成される。
【００６７】
［手順１−１］：状態変数を方程式上の再帰変数に置き換える。例えば、状態変数ｑ＿１，ｑ＿２，ｑ＿３を、それぞれ再帰変数Ｘ，Ｙ，Ｚに置き換える。
【００６８】
［手順１−２］：遷移関数定義を式に変換する。具体的には、遷移関数の定義の１行、すなわち「δ（状態変数１，ラベル）＝状態変数２」を「再帰変数１＝ラベル．状態変数２」という形式の式に変換する。このときε遷移はτという記号に変換する。
【００６９】
例えば、＜縮約ルール４＞の縮約前の遷移関数は、  
Ｘ＝ａ．Ｘ  
Ｘ＝τ．Ｙ  
Ｙ＝ｂ．Ｚ  
のような式形式に変換される。
【００７０】
［手順２］について説明する。上述したように［手順２］では、同一再帰変数を左辺にもつ式を１つにまとめる。これは、以下の［手順２−１］及び［手順２−２］から構成される。
【００７１】
［手順２−１］：左辺が同一変数である式を集める。  
［手順２−２］：集めた式（複数）の右辺を演算子（＋）により結合する。  
このように、左辺が同一変数である式を集めて、右辺を演算子（＋）により結合することにより１つの式としてまとめることができる。
【００７２】
縮約ルール４は以下の方程式、すなわち  
Ｘ＝ａ．Ｙ＋τ．Ｙ  
Ｙ＝ｂ．Ｚ  
にまとめることができる。
【００７３】
［手順３］について説明する。上述したように、［手順３］は、（連立）方程式を解くというものである。これは、以下の［手順３−１］及び［手順３−２］から構成される。
【００７４】
［手順３−１］：式の右辺に現れるτを係数にもつ状態変数に対し、これを右辺にもつ式を代入する。例えば、以下の方程式、すなわち  
Ｘ＝ａ．Ｙ＋τ．Ｙ  
Ｙ＝ｂ．Ｚ  
においては、Ｘ＝ａ．Ｙ＋τ．Ｙに対して、右辺の２番目の項（τ．Ｙ）がτを係数に持つ状態変数であることから、この２番目の項の状態変数Ｙに対して（Ｙ＝ｂ．Ｚ）を代入する。これによりＸ＝ａ．Ｙ＋τ．（ｂ．Ｚ）が得られる。
【００７５】
［手順３−２］：式の簡略化を行う。τはε遷移に相当する遷移ラベルであり、ラベル間の演算として以下のルール（ｒｕｌｅ１，ｒｕｌｅ２）が成り立つとする。
【００７６】
（ｒｕｌｅ１）：ｘ．τ＝τ．ｘ＝ｘ（ｘは任意のラベル）
（ｒｕｌｅ２）：代入を行いｒｕｌｅ１でτを消去する演算を繰り返した後でかつτに関するラベルが残る右辺の項は削除する。
【００７７】
上記の式のτを含む項について上記処理を施した結果、  
Ｘ＝ａ．Ｙ＋τ．（ｂ．Ｚ）  
＝ａ．Ｙ＋（τ．ｂ）．Ｚ，  
＝ａ．Ｙ＋ｂ．Ｚ  
が得られる。
【００７８】
最後に、［手順４］及び［手順５］について説明する。上述したように、縮約前の遷移関数に対して［手順１］〜［手順３］を実行した結果、＜縮約ルール４＞の［縮約前の遷移関数］に相当する、以下の方程式、すなわち  
Ｘ＝ａ．Ｙ＋ｂ．Ｚ  
Ｙ＝ｂ．Ｚ  
が得られる。
【００７９】
一方、＜縮約ルール４＞の［縮約後の遷移関数］に相当する遷移関数に対して［手順１］〜［手順３］を実行した結果、上記と同一の方程式を得ることができる。従って、ルール検証部９は、＜縮約ルール４＞は妥当である（正しい）旨の判定結果を出力する。このような出力は、ルール入力部８を通じて縮約ルールの入力を行うユーザ等に対して提示される。
【００８０】
（タイミング図生成部１２）
タイミング図生成部１２は、プロパティから得られた交替性オートマトンと、システムの分割仕様とが与えられた際に、以下に説明するようにタイミング図を生成する。ここで、「分割仕様」とは、対象とするシステムを分割した場合に、どの信号が、分割された２つのサブシステム間のインターフェイス信号になるかを記述するものである。
【００８１】
具体的には、タイミング図生成部１２は例えば以下の手順に従ってタイミングを生成する。ここでは、ＩＮを入力信号、ＯＵＴを出力信号の集合とし、分割仕様の一例として、ＯＵＴ＝｛ａ，ｃ，ｅ｝、ＩＮ＝｛ｂ，ｄ，ｆ｝が与えられるとする。これは、図１に示した入出力属性情報１３に相当する。  
［手順１］分割仕様に従いオートマトンを縮約する。
【００８２】
［手順２］オートマトンの特定パターンに合致する部分を検索する。
【００８３】
［手順３］互いに接続するパターン列を計算する。
【００８４】
［手順４］パターンをプロパティに変換する。
【００８５】
［手順５］プロパティをタイミング図に変換する。
【００８６】
先ず［手順１］では、分割仕様に従いオートマトンを縮約する。具体的には、まず、分割仕様に現れる信号（ＩＮ∪ＯＵＴ）を縮約指示情報として、オートマトンを縮約する。すなわち、入出力属性情報１がタイミング図生成部１２に入力され、該入出力属性情報１に基づく縮約指示情報がタイミング図生成部１２から状態遷移機械縮約部６に与えられることによりオートマトンの縮約指示がなされる。本実施形態では、これにより得られた縮約後のオートマトンは以下の構造であるとする。
【００８７】
縮約後のオートマトンの例（遷移関数をソートしたもの）  
Σ＝｛ｑ＿０，ｑ＿１，ｑ＿２，ｑ＿３，ｑ＿４，ｑ＿５｝  
ｑ０＝ｑ＿０  
δ（ｑ＿０，ａ）＝ｑ＿０  
δ（ｑ＿０，ｂ）＝ｑ＿１  
δ（ｑ＿１，ｔｒｕｅ）＝ｑ＿２  
δ（ｑ＿２，ｔｒｕｅ）＝ｑ＿３  
δ（ｑ＿３，ｃ）＝ｑ＿４  
δ（ｑ＿４，ｄ）＝ｑ＿４  
δ（ｑ＿４，ｅ）＝ｑ＿５  
δ（ｑ＿５，ｅ）＝ｑ＿５  
δ（ｑ＿５，ｆ）＝ｔｒｕｅ
次に［手順２］では、オートマトンの特定パターンに合致する部分を検索する。すなわち、［手順１］で得られたオートマトンの中で、特定のパターンと合致する部分構造を得る。特定のパターンは、以下のような遷移関数のテーブルとして実現される。
【００８８】
例えば“ｘ→ｙ  Ｕ  ｚ”に相当するパターンは、  
δ（ｑ＿ｉｎ，ｘ）＝ｑ１  
δ（ｑ１，ｙ）＝ｑ１  
δ（ｑ１，ｚ）＝ｑ＿ｏｕｔ  
のように表現される。ただし、ｑ＿ｉｎはパターン外からの入力状態、ｑ＿ｏｕｔはパターン外への出力状態を示している。
【００８９】
同様に、例えば“ｘ→Ｆ  ｙ”に相当するパターンは、  
δ（ｑ１，ｘ）＝ｑ１，  
δ（ｑ１，ｙ）＝ｑ＿ｏｕｔ  
のように表現される。
【００９０】
同様に、例えば“ｘ→Ｘ２ｙ”に相当するパターンは、  
δ（ｑ＿ｉｎ，ｘ）＝ｑ１  
δ（ｑ１，ｔｒｕｅ）＝ｑ１  
δ（ｑ２，ｔｒｕｅ）＝ｑ３  
δ（ｑ３，ｙ）＝ｑ＿ｏｕｔ  
のように表現される。
【００９１】
以下、オートマトンにおいて特定パターンに合致する部分を検索する手順を詳細に説明する。
【００９２】
最初にオートマトンの遷移関数の最初の２行、すなわち
δ（ｑ０，ａ）＝ｑ０  
δ（ｑ０，ｂ）＝ｑ１  
に対し、ｑ０をｑ＿１，ｑ１をｑ＿２，ｑ＿ａをｘ，ｂをｙに読み替えると“ｘ→Ｆ  ｙ”のパターン、すなわち
δ（ｑ＿１，ｘ）＝ｑ＿１  
δ（ｑ＿１，ｙ）＝ｑ＿ｏｕｔ  
にマッチすることから、このパターンにおけるｘ，ｙ，ｑ＿１を置き換えて、以下の部分項、すなわち  
部分項１＝“ａ→Ｆ  ｂ”  
δ（ｑ＿０，ａ）＝ｑ＿０  
δ（ｑ＿０，ｂ）＝ｑ＿１
が得られる。
【００９３】
次に、変換した最後の行からのオートマトンの次の４行、すなわち  
δ（ｑ＿０，ｂ）＝ｑ＿１  
δ（ｑ＿１，ｔｒｕｅ）＝ｑ＿２  
δ（ｑ＿２，ｔｒｕｅ）＝ｑ＿３  
δ（ｑ＿３，ｃ）＝ｑ＿４  
に対し、同様に状態変数と変数名を置き換えると、“ｘ→Ｘ２ｙ”のパターン、すなわち  
δ（ｑ＿ｉｎ，ｘ）＝ｑ１  
δ（ｑ１，ｔｒｕｅ）＝ｑ１  
δ（ｑ２，ｔｒｕｅ）＝ｑ３  
δ（ｑ３，ｙ）＝ｑ＿ｏｕｔ  
に合致する。このパターンの状態と変数を置き換えて以下の部分項、すなわち
部分項２＝“ｂ→Ｘ２ｃ”  
δ（ｑ＿０，ｂ）＝ｑ＿１  
δ（ｑ＿１，ｔｒｕｅ）＝ｑ１  
δ（ｑ＿２，ｔｒｕｅ）＝ｑ３  
δ（ｑ＿３，ｃ）＝ｑ＿４
が得られる。
【００９４】
次に、変換した最後の行からのオートマトンの次の３行、すなわち  
δ（ｑ＿３，ｃ）＝ｑ＿４  
δ（ｑ＿４，ｄ）＝ｑ＿４  
δ（ｑ＿４，ｅ）＝ｑ＿５  
に対し、同様に状態変数と変数名を置き換えると、“ｘ→ｙ  Ｕ  ｚ”のパターン、すなわち  
δ（ｑ＿ｉｎ，ｘ）＝ｑ１  
δ（ｑ１，ｙ）＝ｑ１  
δ（ｑ１，ｚ）＝ｑ＿ｏｕｔ  
に合致する。このパターンの状態と変数を置き換えて以下の部分項、すなわち  
部分項３＝“ｃ→ｄ  Ｕ  ｅ”  
δ（ｑ＿３，ｃ）＝ｑ＿４  
δ（ｑ＿４，ｄ）＝ｑ＿４  
δ（ｑ＿４，ｅ）＝ｑ＿５
が得られる。
【００９５】
次に、変換した次行からのオートマトンの次の２行、すなわち  
δ（ｑ＿５，ｅ）＝ｑ＿５  
δ（ｑ＿５，ｆ）＝ｔｒｕｅ  
に対し、同様に状態変数と変数名を置き換えると、“ｘ→Ｆ  ｙ”のパターン、すなわち  
δ（ｑ＿１，ｘ）＝ｑ＿１  
δ（ｑ＿１，ｙ）＝ｑ＿ｏｕｔ  
に合致する。このパターンの状態と変数を置き換えて以下の部分項、すなわち  
部分項４＝“ｅ→Ｆ  ｆ”
δ（ｑ＿５，ｅ）＝ｑ＿５，
δ（ｑ＿５，ｆ）＝ｔｒｕｅ
が得られる。
【００９６】
以上の手順により、元々のオートマトンの遷移関数にマッチする部分項が４つ得られる。上記特定のパターンは時相論理式に対応しており、得られた部分構造は後ほどプロパティに変換される。図６は、状態遷移のパターンと、対応する論理式の例を図に示したものである。
【００９７】
次に［手順３］では、互いに接続するパターン列を計算する。すなわち、部分項の間の近接関係を元々の全体（縮約の結果得られたオートマトン）の構造を参照して決定する。先ほどの例で得られた部分項は以下の４つ、すなわち  
部分項１：ａ→Ｆ  ｂ  
部分項２：ｂ→Ｘ２  ｃ  
部分項３：ｃ→ｄ  Ｕ  ｅ  
部分項４：ｅ→Ｆ  ｆ  
である。
【００９８】
さらに、部分項１と部分項２は状態変数＝ｑ＿１を介して接続され、部分項２と部分項３は状態変数＝ｑ＿３，ｑ＿４を介して接続され、部分項３と部分項４は状態変数＝ｑ＿５を介して接続される、という状態変数を介した近接関係がある。このような、状態変数を介した部分項の連鎖を「シナリオ」と呼ぶ。
【００９９】
例えば本実施形態で得られたものをシナリオ１と呼ぶ。シナリオ１は、「部分項１→（ｑ＿１）→部分項２→（ｑ＿３，ｑ＿４）→部分項３→（ｑ＿５）→部分項４」である。本実施形態では、状態変数を介した直列のシナリオが得られたが、状態変数を介して近接する部分項が複数ある場合（ＯＲ分岐）は、分岐を考慮した場合の数分だけシナリオを得ることができる。
【０１００】
次に［手順４］では、パターンをプロパティに変換する。パターンはタイミング図に対応する。図７はパターンに対応するタイミング図片を表している。タイミング図は、変数種別を縦軸に、単位時間（サイクル）で区切られた時間軸を横軸にして、変数に対する値の時間的な変化と、変数間で値の変化の間に成立する依存関係を表している。ここで、依存関係には、順序依存関係（ｘの後にｙが起きる）、時間順序関係（ｘの２サイクル後にｙが起きる）がある。
【０１０１】
最後に、［手順５］では、プロパティをタイミング図に変換する。図７に示した対応関係に従い、シナリオ１をタイミング図に変換したものを図８に示す。タイミング図は、分割された部分構造においては、外部環境に対するプロパティになる。特に、「入力変数→出力変数」というパターンのものを「Ｇｕａｒａｎｔｅｅプロパティ」と称し、「出力変数→入力変数」というパターンのものを「Ａｓｓｕｍｅプロパティ」と呼ぶ。
【０１０２】
システムが例えばソフトウェアとハードウェアのように分割された場合に、タイミング図はインターフェイスの仕様を規定し、片方（例：ハードウェア（ＨＷ））におけるＡｓｓｕｍｅはもう一方（例：ソフトウェア（ＳＷ））のＧｕａｒａｎｔｅｅになる。同様に、ＧｕａｒａｎｔｅｅはＡｓｓｕｍｅに対応する。プロパティをＡｓｓｕｍｅとＧｕａｒａｎｔｅｅに分別することは、モデル検査等の形式検証を行うときの前提条件（Ａｓｓｕｍｅ）、守らなければならない性質（Ｇｕａｒａｎｔｅｅ）を明らかにすることになる。このように、タイミング図を介してソフトウェアとハードウェアとの間のプロパティのすり合わせが容易になるという効果がある。
【０１０３】
以上説明した実施形態を利用すれば、信号値を表す論理変数と、該論理変数を原子項とする論理式又は時相論理式により設計対象の制約に係るプロパティが表現される場合に、与えられたプロパティの集合から、複数のプロパティにまたがる任意の論理変数のみに関わる部分制約を選択し、該部分制約が論理式又は時相論理式により表現される新たなプロパティを抽出することができる。すなわち、全体のアサーションの集合から有効な任意の部分を絞り込んで検証に用いることにより、効率的な検証を行うことが可能になる。またハードウェア（ＨＷ）とソフトウェア（ＳＷ）が組み合わさったシステムにおいては、ハードウェアとソフトウェアの互いに関連のある制約をタイミング図として得ることができる。したがって、ハードウェアとソフトウェアの間のすり合わせを効率的に行える。
【０１０４】
なお、本発明は上記実施形態そのままに限定されるものではなく、実施段階ではその要旨を逸脱しない範囲で構成要素を変形して具体化できる。また、上記実施形態に開示されている複数の構成要素の適宜な組み合わせにより、種々の発明を形成できる。例えば、実施形態に示される全構成要素から幾つかの構成要素を削除してもよい。さらに、異なる実施形態にわたる構成要素を適宜組み合わせてもよい。
【図面の簡単な説明】
【０１０５】
【図１】本発明の一実施形態に係るプロパティ抽出装置を示すブロック図
【図２】交替性オートマトンのグラフを示す図
【図３】交替性オートマトンのグラフを示す図
【図４】縮約ルールの一覧を示す図
【図５】交替性オートマトンのグラフを示す図
【図６】パターンと対応する論理式の例を示す図
【図７】パターンとタイミング図の対応を示す図
【図８】タイミング図の生成を示す図
【符号の説明】
【０１０６】
１…入力プロパティ；
２…プロパティ抽出装置；
３…状態遷移機械変換部；
４…状態遷移機械（オートマトン）；
５…縮約指示情報；
６…状態遷移機械縮約部；
７…縮約ルール；
８…ルール入力部；
９…ルール検証部；
１０…プロパティ変換部；
１１…出力プロパティ；
１２…タイミング図生成部；
１３…入出力属性情報
【図１】
0005025542.tif 000002
【図２】
0005025542.tif 000003
【図３】
0005025542.tif 000004
【図４】
0005025542.tif 000005
【図５】
0005025542.tif 000006
【図６】
0005025542.tif 000007
【図７】
0005025542.tif 000008
【図８】
0005025542.tif 000009