(57)【要約】コンピュータシステムの並行プログラムにおいてデータフローを計算するシステムおよび方法であって、並行プログラムについて、スレッドのファミリ（Ｕ１，…，Ｕｍ）および線形時相論理（ＬＴＬ）プロパティｆが与えられると、前記ＬＴＬプロパティｆについてカットオフを計算すること（１２）を含み、ｃ以上の全てのｎについて、Ｕｎがｆを満たし、Ｕｃがｆを満たす場合、ｃがカットオフと呼ばれる。カットオフは、スレッドの内部遷移について重み付きマルチオートマトンを使用して計算される（１４）。カットオフ数のプロセスをモデルチェックすること（１６）は、並行プログラム内の競合無し状態を検証するために実施される。
2010506309.tif 000002
【特許請求の範囲】
【請求項１】
コンピュータシステムの並行プログラムにおいてデータフローを計算する方法であって、
並行プログラムについて、スレッドのファミリ（Ｕ１，…，Ｕｍ）および線形時相論理（ＬＴＬ）プロパティｆが与えられると、前記ＬＴＬプロパティｆについてカットオフを計算すること（１２）であって、ｃ以上の全てのｎについて、Ｕｎがｆを満たし、Ｕｃがｆを満たす場合、ｃがカットオフと呼ばれ、前記カットオフは、前記スレッドの内部遷移について重み付きマルチオートマトンを使用して計算すること（１４）と、
前記並行プログラム内の競合無し状態を検証するために、カットオフ数のプロセスをモデルチェックすること（１６）とを有する方法。
【請求項２】
モデルチェックするステップ（１６）は、各スレッドの複数のコピーを含むパラメータ化されたシステム内で競合無し状態を確立することによって、それぞれが各スレッドを実行する少なくとも２つの別個のドライバに関する並行プログラム内の競合無し状態を確立することを有する請求項１に記載の方法。
【請求項３】
モデルチェックするステップ（１６）は、決定不可能な並行プログラムを含むパラメータ化されたシステム内で競合無し状態を確立することによって、前記決定不可能な並行プログラム内の競合無し状態を確立することを有する請求項１に記載の方法。
【請求項４】
前記スレッドは、プシュダウンシステム（ＰＤＳ）としてモデル化される（１２）請求項１に記載の方法。
【請求項５】
前記スレッドは、同期化プリミティブを使用して互いに相互作用する請求項１に記載の方法。
【請求項６】
同期化プリミティブは、対ランデブー、非同期ランデブー、選言ガード、ブロードキャスト、入れ子ロック、および非入れ子ロックのうちの少なくとも１つを含む請求項１に記載の方法。
【請求項７】
ｆは、２重インデックスＬＴＬ式である請求項１に記載の方法。
【請求項８】
前記スレッドの内部遷移について重み付きマルチオートマトンを使用すること（１４）は、２つのコントロール状態間の移行中に発火する遷移の数に関する限界を推定することを含む請求項１に記載の方法。
【請求項９】
並行プログラムにおいてデータフローを計算するコンピュータ媒体であって、コンピュータ読取可能プログラムを含み、前記コンピュータ読取可能プログラムは、コンピュータ上で実行されると、
並行プログラムについて、スレッドのファミリ（Ｕ１，…，Ｕｍ）および線形時相論理（ＬＴＬ）プロパティｆが与えられると、前記ＬＴＬプロパティｆについてカットオフを計算するステップ（１２）であって、ｃ以上の全てのｎについて、Ｕｎがｆを満たし、Ｕｃがｆを満たす場合、ｃがカットオフと呼ばれ、前記カットオフは、前記スレッドの内部遷移について重み付きマルチオートマトンを使用して計算するステップ（１４）と、
前記並行プログラム内の競合無し状態を検証するために、カットオフ数のプロセスをモデルチェックするステップ（１６）とを、
前記コンピュータに実行させるコンピュータ媒体。
【請求項１０】
コンピュータシステムのコンピュータプログラムにおいてデータフローを計算する方法であって、
並行プログラムについて、同期化プリミティブによって相互作用するプッシュダウンシステムとしてモデル化されたスレッドのファミリ（Ｕ１，…，Ｕｍ）および線形時相論理（ＬＴＬ）プロパティｆが与えられると、前記並行プログラムの到達可能コントロール状態間でのスレッドの計算に沿って発火する遷移の数に関する限界を計算することによってＬＴＬプロパティについてカットオフを計算すること（１２）であって、前記限界は、前記スレッドの内部遷移について重み付きマルチオートマトンを使用して計算すること（１４）と、
前記並行プログラム内の競合無し状態を検証するパラメータ化によるモデルチェッキングによって、カットオフ数のプロセスをモデルチェックすること（１６）とを有する方法。
【請求項１１】
モデルチェックするステップ（１６）は、各スレッドの複数のコピーを含むパラメータ化されたシステム内で競合無し状態を確立することによって、それぞれが各スレッドを実行する少なくとも２つの別個のドライバに関する並行プログラム内の競合無し状態を確立することを含む請求項１０に記載の方法。
【請求項１２】
モデルチェックするステップ（１６）は、決定不可能な並行プログラムを含むパラメータ化されたシステム内で競合無し状態を確立することによって、前記決定不可能な並行プログラム内の競合無し状態を確立することを含む請求項１０に記載の方法。
【請求項１３】
同期化プリミティブは、対ランデブー、非同期ランデブー、選言ガード、ブロードキャスト、入れ子ロック、および非入れ子ロックのうちの少なくとも１つを含む請求項１０に記載の方法。
【請求項１４】
ｆは、２重インデックスＬＴＬ式である請求項１に記載の方法。
【請求項１５】
並行プログラムにおいてデータフローを計算するコンピュータ媒体であって、コンピュータ読取可能プログラムを含み、前記コンピュータ読取可能プログラムは、コンピュータ上で実行されると、請求項１０に記載のステップを、前記コンピュータに実行させるコンピュータ媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、コンピュータシステム検証に関し、より詳細には、同じハードウェアまたはソフトウェアコンポーネントの多くのコピーを含むコンピュータシステムのパラメータ化された品質を利用する並行プログラムの検証に関する。
【背景技術】
【０００２】
コンピュータ検証は、コンピュータシステムが適切に動作すること、および、得られる結果が信頼できることを保証するのに必要とされる。検証の一形態は、試験である。試験において、システムの実際の振舞いは、入力の集合に関して調べられ、予想結果に対して照合される。考えられる入力の数が大きいかまたは無数であるため、システムが、全ての状況において正しく振舞うことを確認することは不可能になる。
【０００３】
検証は、これらの問題に対処しようと試みる。検証は、システムの振舞いをシミュレートするための数学的またはモデル的基礎を提供する。モデルとその意図される振舞いが定義される。マシンは、通常、その状態が経時的に進化するシステムとしてモデル化され、モデルは、状態空間の仕様およびシステムが状態空間を横切ることができる方法を含む。時相論理は、反応性システムの振舞いを表現するのに有用であることが示された。検証に対するモデルチェッキング手法は、検討中のシステムの数学的モデルを取得すること、および、モデル内で時相論理式の妥当性をチェックすることを含む。
【０００４】
全ての方法が直面する主要な問題は、状態爆発として知られる。状態爆発は、検討中のシステムの状態空間が、使用されるメモリ（たとえば、レジスタまたはプログラム変数、ポインタなど）の量に伴って急速に（たとえば、指数関数的に）増大することを意味する。これは、検証方法を制限する。
【０００５】
マルチスレッディングは、コンピュータシステムの異なるコンポーネントの間での並列性を利用する標準的な方法である。結果として、並行マルチスレッドプログラムの使用が、普及しつつある。例は、オペレーティングシステム、データベース、埋め込みシステム（携帯電話、マルチメディア消費者製品）などを含む。検証は、通常、大規模並行プログラムについてスケーリングしないため、マルチスレッドプログラムをデバッグするためのプロシジャ間データフロー解析のような静的解析技法を活用することに大きな関心が存在する。プロシジャ間データフロー解析は、シーケンシャルプログラムについてバグを見つけるのに非常に有効な技法であることが示されているが、こうしたデータフロー解析を並行ドメインに拡張することに関しての研究がこれまで非常に少なかった。
【発明の開示】
【０００６】
多くのレプリケーテッドスレッドを有する、たとえば、同じコード部分を実行する並行プログラムは、多くの重要なアプリケーションで発生する。これらは、とりわけ、ネットワーキング用のプロトコル、キャッシュコヒーレンス、同期化、およびマルチスレッドソフトウェアを実行するマルチコアアーキテクチャの実装を含む。具体的な例として、Ｌｉｎｕｘ（登録商標）デバイスドライバを考える。ドライバコードは、ドライバコードを実行するスレッドの数にかかわりなく、正しく働くようにサポートされる。こうしたアプリケーションの場合、目標は、ドライバＵｉについて、コードを実行する数ｎｉのスレッドによって測定されるプログラムサイズにかかわりなく、形式
【０００７】
【数１】
2010506309.tif 000003
【０００８】
のプログラムの正しさを確立することである。当技術分野では、これは、パラメータ化によるモデルチェッキング問題（ＰＭＣＰ）と呼ばれることが多い。疑いもなく、固定数のスレッドを有するシステムの正しさは、一般に、任意の数についての正しさを確立しないため、このことは重要である。
【０００９】
しかし、実際に、ＰＭＣＰを決定することは、難しい問題と考えられる。したがって、通常、結果として起こる手法は、固定した数の（通常、２つの）レプリケーテッドスレッドを有するプログラムについての正しさを確立することを試みようとする一見して単純な問題にまず取り組むことである。しかし、固定した数の（さらに２つの）レプリケーテッドコンポーネントについて正しさを確立することは、多くの重要な場合に、パラメータ化された正しさを確立することに比べて、立証可能なことには、扱いにくいという多少意外な結果が得られる。
【００１０】
これは、少なくとも２つの意味を有する。第１に、パラメータ化された再帰プログラムについて推論するとき、固定した少数のレプリケーテッドスレッドを含み、コピー数を連続して増加させる特別な場合について正しさを確立しようと試みるのではなく、パラメータ化された正しさについて直接推論しようと試みることが重要である。第２の、また、より重要な、実用的な関心のある結論を示すために、目標が、パラメータ化された推論ではなく、固定した数の、おそらく別個のスレッドを有するプログラムの正しさを確立することであるシナリオが考えられる。
【００１１】
２つのおそらく別個のデバイスドライバを動作させるスレッドＵ１とＵ２を含むプログラムＵ１‖Ｕ２においてデータ競合が存在しないことを確立しようとすることを仮定する。次に、Ｕ１とＵ２の任意に多くのコピーを含むパラメータ化されたシステム
【００１２】
【数２】
2010506309.tif 000004
【００１３】
内でデータ競合が存在しないことが確立される場合、Ｕ１‖Ｕ２についてデータ競合無し状態を自動的に確立する。１つの重要な点は、関心のある多くの事例において、Ｕ１‖Ｕ２について推論することは決定不可能であり、一方、ＰＭＣＰは効率的に決定可能であることがわかることを示すことである。
【００１４】
対と非同期のランデブー、ロック、ブロードキャスト、および選言ガードのような標準的な同期化プリミティブを使用して互いに相互作用するテンプレートスレッドＵｉの任意の数ｎｉのコピーを含む、形式
【００１５】
【数３】
2010506309.tif 000005
【００１６】
の並行プログラムについてのＰＭＣＰを考える。再帰プログラムを解析するための自然でかつ強力なフレームワークとして現れたプッシュダウンシステム（ＰＤＳ）として、スレッドをモデル化する。正しさプロパティは、マルチインデックスＬＴＬ／Ｘを使用して表現される。「次の」演算子Ｘが存在しないことは、ロジックスタッタリングを鈍感にし、それは、パラメータ化されたシステムについて推論するときは普通であることに留意されたい。説明を容易にするために、単一テンプレートＰＤＳを有するシステムについて、また、２重インデックスＬＴＬ／Ｘプロパティについての結果が定式化される。複数のテンプレートおよびｋインデックスプロパティ（ｋ＞２）を有するシステムへの拡張は、当業者に理解されるであろう。
【００１７】
本発明者等の新しい結果が示すところでは、ＰＭＣＰの決定可能性は、正しさプロパティにおいて受容される時相演算子の集合次第で変わり、それにより、ＰＭＣＰがそれについて決定可能である２重インデックスＬＴＬのフラグメントを特徴付ける自然な方法を提供するということである。形式Ｅｆの式を含むフラグメントを指定するために、Ｌ（Ｏｐ１，…，Ｏｐｋ）（Ｏｐｉ∈｛Ｆ，Ｕ，Ｇ｝）を使用する。ここで、ｆは、時相演算子Ｏｐ１，…，Ｏｐｋおよびブール結合記号∨および∧を使用して構築された、正標準形（ＰＮＦ）の２重インデックスＬＴＬ／Ｘ式である（すなわち、原子命題だけが否定される）。ここで、Ｆ「ｓｏｍｅｔｉｍｅｓ」、Ｕ「ｕｎｔｉｌ」、およびＧ「ａｌｗａｙｓ」は、標準的な時相演算子を指定し、Ｅは、「ｅｘｉｓｔｅｎｔｉａｌ  ｐａｔｈ  ｑｕａｎｔｉｆｉｅｒ」である。Ｌ（Ｕ，Ｇ）は、フルブラウン２重インデックスＬＴＬ／Ｘである。
【００１８】
本開示では、標準的な同期化プリミティブのそれぞれについて、２重インデックスＬＴＬ／Ｘ用のＰＭＣＰの決定可能性／決定不可能性境界を正確に記述する。具体的には、以下の通りとなる。
【００１９】
（ａ）Ｌ（Ｆ，Ｇ）およびＬ（Ｕ）についてのＰＭＣＰは、一般に、ＰＤＳが、互いに全く相互作用しないシステムについてさえも決定不可能である。上記結果は、相互作用してもしなくても、ＰＤＳについてのＰＭＣＰの決定可能性を得るために、サブ論理Ｌ（Ｆ）か、サブ論理Ｌ（Ｇ）のいずれかに制限しなければならないことを意味する。これらのサブ論理の場合、ＰＭＣＰの決定可能性は、ＰＤＳによって使用される同期化プリミティブに依存する。
【００２０】
（ｂ）サブ論理Ｌ（Ｆ）の場合、ＰＭＣＰは、対か、非同期のランデブー、選言ガード、および入れ子ロックによって相互作用するＰＤＳについて効率的に決定可能であるが、ブロードキャストおよび非入れ子ロックについて決定不可能であることが示される。対ランデブーについての（また、実際には、非同期のランデブーおよび選言ガードについての）決定可能性は、到達可能性のために対ランデブーによって相互作用する２つのＰＤＳ（２つのＰＤＳが、互いに同型であるときでさえも）を含むシステムをモデルチェックすることの決定不可能性−相互作用するＰＤＳをモデルチェックすることについて検出不可能性結果が与えられると、意外である。本発明者等の新しい結果によると、ＰＭＣＰは対ランデブーによって相互作用するＰＤＳについて決定可能であるが、それも効果的に決定可能である。これは、対ランデブー（および非同期ランデブーおよび選言ガード）について、問題のパラメータ化されたバージョンへの切換えが、ＰＭＣＰをより扱い易くすることを示すため、特に興味深い。
【００２１】
（ｃ）フラグメントＬ（Ｇ）の場合、ＰＭＣＰが、対と非同期のランデブー、選言ガード、およびロック（たとえ非入れ子ロックでも）について決定可能であることが示される。これは、全ての標準的な同期化プリミティブについてＰＭＣＰを解決する。
【００２２】
｛Ｕｎ｝が、対ランデブーによって相互作用するテンプレートＰＤＳＵによって定義されるシステムパラメータ化されたファミリであるとする。Ｌ（Ｆ）についての決定可能性を得るために、パラメータ化により到達可能である、たとえば、あるｎについてＵｎ内で到達可能であるＵのコントロール状態の集合を計算するための、新しい有効なプロシジャを定式化することによって始める。これは、Ｕの初期状態を含む集合Ｒ０で始まり、ｉ番目の反復において、Ｒｉ内の全ての状態がパラメータ化により到達可能であると仮定すると、パラメータ化により到達可能になるコントロール状態の集合Ｒｉ＋１を構築する固定点計算によって達成される。重要な点は、新しいコントロール状態ｃをＲｉに追加するときに、ランデブーから生じる同期化制約が満たされることを確保するだけでなく、新しく追加された状態が、パラメータ化により到達可能な既存の状態から、文脈自由に到達可能であることも確保されなければならないことである。２つの制約のチェックは、ピッタリ合わされる、すなわち、新しい状態が全く発見されない固定点に達するまで、インタリーブ方式で実施される。次に、Ｌ（Ｆ）の式ｆについてのＰＭＣＰが、ＰＤＳ  ＵＲの２つの非相互作用コピーを有するシステムについての標準的なモデルチェッキングに帰着することが、フラッディング議論によって示される。ここで、ＵＲは、パラメータ化により到達可能なＵのコントロール状態だけを保持し、こうした状態間の全ての対ランデブーを内部遷移に変換することによってＵから得られるテンプレートである。最後の問題は、効率的に決定可能であることが知られており、決定可能性結果をもたらす。非同期ランデブーおよび選言ガードを有するＰＤＳについての決定可能性は、同様のプロシジャによって次の通りである。
【００２３】
Ｌ（Ｇ）についての決定可能性を得るために、カットオフ結果が最初に示される。ｍ≧ｃについてＵｍ｜＝ｆであり、Ｕｃ｜＝ｆである場合、ｃは、式ｆについてのカットオフであると呼ぶ。重み付きマルチオートマトンを活用することによって、対ランデブーと非同期のランデブーによって相互作用するＰＤＳの場合、Ｌ（Ｆ）およびＬ（Ｇ）の式についてのカットオフを計算する新しいプロシジャが示される。ロックによって相互作用するＰＤＳの場合、このカットオフは、ｋインデックスプロパティについてｋであることが知られている。カットオフの存在は、選言および（非入れ子）ロックについて決定可能であることが示され、また、対ランデブーと非同期のランデブーによって相互作用するＰＤＳについて決定可能であることが既に知られている有限の多くのＰＤＳを有するシステムをモデルチェックすることに帰着させる。選言ガードによって相互作用するＰＤＳの場合、Ｌ（Ｇ）の式ｆについてのＰＭＣＰが、単純なＰＤＳ  ＵＲの２つの（非相互作用）コピーを有するシステムについての標準的なモデルチェッキングに帰着することが、フラッディング議論によって示される。最後の問題は、最後の問題は、効率的に決定可能であることが知られており、決定可能性結果をもたらす。
【００２４】
コンピュータシステムの並行プログラムにおいてデータフローを計算するシステムおよび方法は、並行プログラムについて、スレッドのファミリ（Ｕ１，…，Ｕｍ）および線形時相論理（ＬＴＬ）プロパティｆが与えられると、ＬＴＬプロパティｆについてカットオフを計算することを含み、ｃ以上の全てのｎについて、Ｕｎがｆを満たし、Ｕｃがｆを満たす場合、ｃがカットオフと呼ばれる。カットオフは、スレッドの内部遷移について重み付きマルチオートマトンを使用して計算される。並行プログラム内の競合無し状態を検証するために、カットオフ数のプロセスをモデルチェックすることが実施される。
【００２５】
これらのまた他の特徴および利点は、添付図面に関連して読まれる、例証的な実施形態の以下の詳細な説明から明らかになるであろう。
【発明を実施するための最良の形態】
【００２６】
本開示は、以下の図を参照して、好ましい実施形態の以下の説明において詳細を提供するであろう。
【００２７】
本実施形態は、コンピュータシステム検証に関し、より詳細には、ディスクドライブ、音声スピーカなどのようなハードウェアコンポーネントを制御するのに使用される、たとえば、デバイスドライバなどの並行プログラムの検証に関する。特に有益な実施形態では、並行プログラムが、同じハードウェアまたはソフトウェアコンポーネントの多くのコピーを含む点で、コンピュータシステムのパラメータ化された品質が利用される。さらに、本実施形態は、たとえば、携帯電話、携帯情報端末（ＰＤＡ）のような移動体デバイスで使用される埋め込み式ソフトウェア、データベースソフトウェア、ＳＱＬサーバ、アプリケーションレベルソフトウェア、ウェブブラウザのようなもの（Ｆｉｒｅｆｏｘ（登録商標）、Ｅｘｐｌｏｒｅ（登録商標））、または並行性を使用する任意のアプリケーションなどの他のアプリケーションに適用可能である。
【００２８】
相互作用するプッシュダウンシステムのモデルチェッキングは、並行プログラム用のデータフロー解析の基礎をなす核心の問題である。しかし、モデルチェッキングは、非常に制限された時間論理フラグメントについてだけ決定可能である。基本的な障害は、２つの文脈自由な言語の積集合の非空性をチェックすることの決定不可能性である。プッシュダウンシステム（ＰＤＳ）によって受容される文脈自由な言語の積集合を的確に受容するほどに十分に、同期化プリミティブを表現的にするか、または、プロパティが強力にモデルチェックされることによって、２つの異なるＰＤＳを結合させることは難しくない。これは、モデルチェッキング問題の決定不可能性をもたらす。しかし、本発明の原理によれば、並行システムの多くの重要なクラスがパラメータ化されることが利用される、すなわち、クラスは、コンポーネントの種数の基本型の多くのレプリケーテッドコピーを含む。
【００２９】
本発明の原理によれば、全体的に困難な問題は解決される必要がない。多くの並行システムが、パラメータされる、すなわち、同じ基本コンポーネントの多くのレプリケーテッドコピーを含むということが利用される。実際に、ネットワーク、キャッシュコヒーレンス、同期化用のほとんどの分散プロトコルの場合、プロトコルを実装する、まさにその同じコード部分は、異なるマシン上で実行され、そのため、プロトコルがパラメータ化される。インターネットは、それぞれがＴＣＰ／ＩＰプロトコルを実行するコンピュータのネットワークと考えられることができる。他の例は、マルチスレッディングを有するマルチコアアーキテクチャを含む。実際に、デバイスドライバは、デバイスドライバを実施するスレッドの数にかかわりなく、正しく動作すると仮定される。
【００３０】
新しくかつ有効なプロシジャ間データフロー解析システムおよび方法が、パラメータ化されたマルチスレッドプログラムについて提供される。問題は、全てのＰＤＳが互いのコピーであるような、相互作用するＰＤＳをモデルチェックするという問題に帰着する。パラメータ化されたプログラムを解析することに関する従来の研究は、スレッド（ＰＤＳ）間に有効な通信が全く存在しないモデルに制限されており、そのため、実用的な価値がほとんどない。本開示では、ＰＤＳが、ロック、ランデブー（たとえば、ＷａｉｔＮｏｔｉｆｙ（）ｆｒｏｍ  Ｊａｖａ（登録商標））、またはブロードキャスト（たとえば、Ｗａｉｔ  ＮｏｔｉｆｙＡｌｌ（）ｆｒｏｍ  Ｊａｖａ（登録商標））によって相互作用することができる、強力でかつ現実的なモデルを考えた。そのため、プロシジャ間解析は、現実的な通信モデルのためのパラメータ化された並行ドメインに拡張される。
【００３１】
パラメータ化によるモデルチェッキング問題（ＰＭＣＰ）と呼ばれることが多い、スレッドの固定集合の、有限であるが任意に多くのコピーを含む並行プログラムについてのモデルチェッキング問題を考える。それぞれのスレッドをＰＤＳとしてモデル化して、標準的な同期化プリミティブのそれぞれについて、インデックス線形時相論理（ＬＴＬ）用のＰＭＣＰの決定可能性境界を記述する。本発明者等の結果は、対象となる多くの場合に、ＰＭＣＰは、たとえ一見して難しい問題であっても、個定数のＰＤＳをモデルチェックする問題に比べて、より扱い易いという意外な結論をもたらす。たとえば、対ランデブーによって相互作用するＰＤＳの場合、到達可能性（データ競合の存在）についてのＰＭＣＰは、効率的に決定可能であり、一方、こうした２つの（さらに同型である）ＰＤＳを有するシステムをモデルチェックすることは決定不可能である。ＰＭＣＰを効率的に決定することは、たとえば、Ｌｉｎｕｘ（登録商標）デバイスドライバのようなパラメータ化されたアプリケーションについて非常に重要である。しかし、本発明者等の結果の実用的なより広い意味は、パラメータ化された推論にではなく、固定数のおそらくは別個のスレッドＵ１，…，Ｕｍを有するシステムＵ１‖…‖Ｕｍをモデルチェックすることにだけ興味があっても、多くの場合、Ｕ１，…，Ｕｍの任意に多くのコピーを有する、対応するパラメータ化されたシステム
【００３２】
【数４】
2010506309.tif 000006
【００３３】
についてＰＭＣＰを考えることがより有益であるということである。
【００３４】
本発明の原理による実用的なアプリケーションは、並行マルチスレッドソフトウェアをデバッグする場合、問題のパラメータ化されたバージョンを考えることがより扱い易いということを含む。たとえば、２つのＬｉｎｕｘ（登録商標）デバイスドライバＴ１およびＴ２を有する並行プログラムＴ１‖Ｔ２内のデータ競合を検出したいと思う場合、Ｔ１およびＴ２の任意の数のコピーを有するシステムＴ１ｎ‖Ｔ２ｍについて同じ問題を考えることが効率的でかつ扱い易い。これは、一見して難しい問題であるが、実際には、ずっと扱い易いため、意外である。
【００３５】
図に示す要素が、ハードウェア、ソフトウェア、または、それらの組合せの種々の形態で実装されてもよいことが理解されるべきである。好ましくは、これらの要素は、コンピュータ媒体上に記憶され、プロセッサとメモリと入力／出力インタフェースを有する適切にプログラムされた１つまたは複数の汎用デジタルコンピュータ上で、ソフトウェアで実装されてもよい。ソフトウェアは、ファームウェア、常駐ソフトウェア、マイクロコードなどを含むが、それに限定されない。
【００３６】
本発明の実施形態は、全てのハードウェアの実施形態、全てのソフトウェアの実施形態、または、ハードウェアとソフトウェア要素を共に含む実施形態の形態をとることができる。好ましい実施形態では、本発明は、ファームウェア、常駐ソフトウェア、マイクロコードなどを含むが、それに限定されないソフトウェアで実装される。
【００３７】
実施形態は、コンピュータまたは任意の命令実行システムによって、または、それに関連して使用するためのプログラムコードを提供するコンピュータ使用可能またはコンピュータ読取可能媒体からアクセス可能なコンピュータプログラム製品の形態をとることができる。コンピュータ使用可能またはコンピュータ読取可能媒体は、命令実行システム、装置、またはデバイスによって、または、それに関連して使用するためのプログラムを、記憶し、通信し、伝播させ、または輸送する任意の装置を含んでもよい。媒体は、電子システム、磁気システム、光学システム、電磁システム、赤外システム、または、半導体システム（または装置またはデバイス）、あるいは、伝播媒体であることができる。たとえば、媒体は、半導体または固体メモリ、磁気テープ、取り外し可能コンピュータディスケット、ランダムアクセスメモリ（ＲＡＭ）、読取専用メモリ（ＲＯＭ）、固定磁気ディスク、および光ディスクなどのようなコンピュータ読取可能媒体を含んでもよい。
【００３８】
ここで、同じ数字が同じかまたは同様の要素を表す図面、最初に、図１を参照すると、並行プログラムを検証するシステム／方法を示すブロック図／フロー図が、例証的に示される。テンプレートスレッドＵｉの任意の数ｎｉのコピーを含む形式
【００３９】
【数５】
2010506309.tif 000007
【００４０】
のシステムのファミリを考える。それぞれのテンプレートＵｉは、プッシュダウンシステム（ＰＤＳ）としてモデル化されてもよい。ＰＤＳは、有限のコントロール部と再帰をモデル化するスタックを有する。正式には、ＰＤＳは、５タプルＰ＝（Ｐ，Ａｃｔ，Γ，ｃ０，Δ）であり、ここで、Ｐはコントロール状態の有限集合であり、Ａｃｔは、空アクションｅを含むアクションの有限集合であり、Γは、有限スタックアルファベットであり、Δ⊆（Ｐ×Γ）×Ａｃｔ×（Ｐ×Γ＊）は、遷移ルールの有限集合である。（（ｐ，γ），ａ，（ｐ’，ｗ））∈Δである場合、
【００４１】
【数６】
2010506309.tif 000008
【００４２】
と書く。Ｐの構成は、対（ｐ，ｗ）であり、ここで、ｐ∈Ｐは、コントロールロケーションを指定し、ｗ∈Γ＊はスタックコンテンツを指定する。ｃ０をＰの初期構成と呼ぶ。Ｐの全ての構成の集合は、Ｃで指定される。それぞれのアクションａについて、
【００４３】
【数７】
2010506309.tif 000009
【００４４】
である場合、
全てのν∈Γ＊について
【００４５】
【数８】
2010506309.tif 000010
【００４６】
であるような、関係
【００４７】
【数９】
2010506309.tif 000011
【００４８】
が定義される。
【００４９】
テンプレートＵｉのｎｉのコピーのインタリーブド並列合成によって形成される並行プログラム（またはスレッド）のファミリ
【００５０】
【数１０】
2010506309.tif 000012
【００５１】
を指定するために、｛Ｕ１，…，Ｕｍ｝を使用する。Ｕｊ［ｉ］によって指定されるＵｉのｊ番目のコピーは、標準的な同期化プリミティブ−ロック、対または非同期のランデブー、ブロードキャスト、および選言ブールガードによって、他のスレッドと通信する。対ランデブーは、通信システムの算法（ＣＣＳ）（たとえば、並行プログラムを書くための言語）によって励起され、一方、非同期ランデブーおよびブロードキャストを使用して、Ｊａｖａ（登録商標）のＷａｉｔ／ＮｏｔｉｆｙおよびＷａｉｔ／ＮｏｔｉｆｙＡｌｌプリミティブがモデル化される。
【００５２】
【数１１】
2010506309.tif 000013
【００５３】
のセマンティックは、通常の方法で定義され、したがって、省略される。簡単にするために、単一テンプレートを有するパラメータ化されたシステムについて、また、２重インデックスプロパティについて、本発明者等の結果を定式化する。Ｕｎの大域的計算ｘが与えられると、ｘ［ｉ，ｊ］を使用して、スレッドＵ［ｉ］およびＵ［ｊ］の局所計算シーケンス上にｘを投影することによって得られるシーケンスが指定される。
【００５４】
正しさプロパティ  テンプレートＵが与えられると、形式Λｉ，ｊＥｇ（ｉ，ｊ）の２重インデックスプロパティを考える。ここで、ｇ（ｉ，ｊ）は、コピーＵ［ｉ］およびＵ［ｊ］の局所ローカル状態にわたって解釈されたＬＴＬ／Ｘプロパティである。対称性のために、Ｕｎ｜＝Ｅｇ（１，２）である場合、Ｕｎ｜＝Λｉ，ｊＥｇ（ｉ，ｊ）であることに留意されたい。そのため、Ｅｇ（１，２）のプロパティに制限する。この論理の場合、先に定式化した正しさプロパティにおいて受容された時相演算子に基づく分類Ｌ（Ｏｐ１，，Ｏｐｋ）に従う。２重インデックスＬＴＬ／Ｘは、対象となる多くのプロパティをエンコードすることができる非常にリッチな論理であることが観測される。たとえば、データ競合の存在は、２重インデックス式ＥＦ（ｃ１∧ｄ２）として定式化されることができる。
【００５５】
多くの同様のコンポーネント、たとえば、ディスクドライブ、音声スピーカなどのようなハードウェアを動作させるデバイスドライバを含む並行プログラムについて、ＰＤＳのファミリおよび時間論理プロパティｆ（先に述べた）が与えられると、ブロック１２にて、ｆについてのカットオフを計算する。全てのｎ≧ｃについて、Ｕｎがｆを満たし、Ｕｃがｆを満たす場合、ｃがカットオフと呼ばれる。これは、問題を、カットオフ数までのプロセスを有するシステムをデバッグすることに帰着させる。
【００５６】
ブロック１４にて、これらのカットオフを計算するために、重み付きマルチオートマトンを使用する。これらのカットオフの計算は、ソースコードのサイズにおける多項式時間で効率的に実施されることができる重み付きオートマンのｐｒｅ＊−ｃｌｏｓｕｒｅ計算に帰着する。カットオフが計算されると、ブロック１６にて、結果得られるカットオフサイズのシステムをモデルチェックする。使用される技法は、スレッドによって使用される通信プリミティブに依存し、また、技法は、わかっていてもよい。
【００５７】
本実施形態は、スレッド間の現実的な通信モデルについて、プロシジャ間データフロー解析をパラメータ化された並行ドメインに拡張する。全ての標準的なＪａｖａ（登録商標）通信プリミティブがモデル化されてもよい。本実施形態は、よりスケーラブルである、すなわち、既存の技法に比べて大規模なプログラムを検証することができる可能性があり、また、これを、所与のプログラムの大域的状態空間の構築を回避することによって達成し、したがって、状態爆発問題がバイパスされる。解析は、並行マルチスレッドプログラムから個々のスレッドに帰着する。
【００５８】
方法は、健全でかつ完璧であり、したがって、精確でない技法によって生成される可能性がある偽のエラートレースが回避される。実際の検証で費やされる資源のほとんどが、偽のエラートレースを検出すること／回避することに従事するため、これは、商業的観点から重要である。
【００５９】
決定不可能性障壁：互いに相互作用しないＰＤＳを含むシステムのためのＰＭＣＰについて２つの決定不可能性結果を示すことで始める。
【００６０】
ＰＭＣＰの決定可能性は、正しさプロパティにおいて受容される時相演算子の集合次第で変わり、それにより、ＰＭＣＰがそれについて決定可能である２重インデックスＬＴＬのフラグメントを特徴付ける自然な方法を提供する。一例では、形式Ｅｆの式を含むフラグメントを指定するために、Ｌ（Ｏｐ１，…，Ｏｐｋ）（Ｏｐｉ∈｛Ｆ，Ｕ，Ｇ｝）を使用する。ここで、ｆは、時相演算子Ｏｐ１，…，Ｏｐｋおよびブール結合記号∨および∧を使用して構築された、正標準形（ＰＮＦ）の２重インデックスＬＴＬ／Ｘ式である（すなわち、原子命題だけが否定される）。ここで、Ｆ「ｓｏｍｅｔｉｍｅｓ」、Ｕ「ｕｎｔｉｌ」、およびＧ「ａｌｗａｙｓ」は、標準的な時相演算子を指定し、Ｅは、「ｅｘｉｓｔｅｎｔｉａｌ  ｐａｔｈ  ｑｕａｎｔｉｆｉｅｒ」である。Ｌ（Ｕ，Ｇ）は、フルブラウン２重インデックスＬＴＬ／Ｘである。
【００６１】
Ｌ（Ｕ）およびＬ（Ｇ，Ｆ）についてのＰＭＣＰは、非相互作用ＰＤＳを含むシステムについて決定不可能である。これの重要な帰結は、ある同期化メカニズムを使用してＰＤＳが相互作用する、より表現的なシステムの場合、残りのフラグメント、たとえば、Ｌ（Ｆ）およびＬ（Ｇ）にだけ焦点を当てることが必要になることである。
【００６２】
対ランデブーと非同期ランデブー：｛Ｕ｝が、対ランデブーによって同期化するＰＤＳとしてモデル化されたテンプレートプロセスＵによって定義されたパラメータ化されたファミリであるとする。ここで、      
【００６３】
【数１２】
2010506309.tif 000014
【００６４】
、Ｕのアクションシンボルの集合は、内部遷移ラベルの集合
【００６５】
【数１３】
2010506309.tif 000015
【００６６】
、ならびに、それぞれ、ｓｅｎｄおよびｒｅｃｅｉｖｅ対ランデブー遷移の集合
【００６７】
【数１４】
2010506309.tif 000016
【００６８】
を含む。同期化遷移、すなわち、
【００６９】
【数１５】
2010506309.tif 000017
【００７０】
のアクションによってラベル付けされる同期化遷移は、遷移を実施するＰＤＳのスタックを修正しない。アクション
【００７１】
【数１６】
2010506309.tif 000018
【００７２】
の場合、ｌ！およびｌ？のラベルを付けられる遷移対は、整合と呼ばれる。
【００７３】
【数１７】
2010506309.tif 000019
【００７４】
の場合、局所状態ｃにおいて、ＵnのプロセスＵ［ｊ］（ｊ≠ｉ）が存在する場合、ＵnのプロセスＵ［ｉ］の遷移
【００７５】
【数１８】
2010506309.tif 000020
【００７６】
が、大域状態において有効にされ、それにより、形式
【００７７】
【数１９】
2010506309.tif 000021
【００７８】
の整合遷移が存在することを思い起こす。ランデブーを実施するために、対ｓｅｎｄ遷移と対ｒｅｃｅｉｖｅ遷移ｔｒ１とｔｒ２が共に、１つの原子ステップで同期して発火されなければならない。
【００７９】
対と非同期のランデブーによって相互作用するＰＤＳの場合、Ｌ（Ｆ）およびＬ（Ｇ）についてのＰＭＣＰのための決定プロシジャが提示される。Ｕのパラメータ化による到達可能な全てのコントロールロケーションの集合を計算する、立証可能に効率的なプロシジャを提示することによって始める。これは、Ｌ（Ｆ）およびＬ（Ｇ）についてのプロシジャを定式化するだけのために必要とされるのではなく、データ競合の存在を検出することが、パラメータ化による到達可能性を決定することに帰着されることができるため、単独で重要である。
【００８０】
パラメータ化による到達可能性：テンプレートプロセスＵのコントロール状態ｃ（構成ｃ）は、コントロール状態ｃ（構成ｃ）のプロセスに関して、あるｎについてＵｎの到達可能な大域状態ｓが存在する場合、パラメータ化により到達可能であると言える。
【００８１】
Ｕの構成ｃがパラメータ化により到達可能である場合、あるｋについてｌが与えられると、ｃの少なくともｌのコピーを有するＵｋの到達可能な大域状態ｓが存在することが示されることができる。換言すれば、Ｕのパラメータ化により到達可能なそれぞれの構成の重複度が、任意の大きな値に増大されることができる。これは、Ｕのそれぞれの構成の重複度に追従するという負担から解放する。
【００８２】
無限の重複度：Ｒを、Ｕのパラメータ化により到達可能な全ての構成の集合とし、Ｒ’を、Ｒの有限な部分集合とする。あるｍについてｌが与えられると、Ｒ’において、それぞれの構成の少なくともｌのコピーを有する大域状態ｓをもたらすＵｍの有限な計算が存在する。
【００８３】
上記結果は、ＥＦ（ｃ１∧…∧ｃｋ）、すなわち、データ競合の存在についてのＰＭＣＰをＥＦｃ（ｃはＵのコントロール状態である）についてのＰＭＣＰに帰着させる。それぞれのｉ∈［１…ｋ］について、ｃｉがパラメータ化により到達可能である場合、∃ｎ，Ｕｎ｜＝ＥＦ（ｃ１∧…∧ｃｋ）である。
【００８４】
Ｕが、有限状態ラベル付け遷移システムである場合に、パラメータ化により到達可能なコントロール状態を計算することは、簡単な固定点計算によって達成されることができるが、ＰＤＳの場合、スタックによって導入される同期化プリミティブと文脈自由な到達可能性の両方から生じる制約を同時に満たすという要件によって複雑になる。
【００８５】
図２を参照すると、到達可能性を判定するための例のテンプレートプロセスが示される。テンプレートプロセスＵを考える。あるｎについて、Ｕｎ｜＝ＥＦｃ１かどうかを決定することを仮定する。Ｕの初期状態ｃ０だけを含む集合Ｒ０＝｛ｃ０｝で始める。次に、一連の集合Ｒ０，…，Ｒｎを構築する。Ｒｉ＋１は、Ｒｉ内の全ての状態が、パラメータ化により到達可能であると仮定すると、パラメータ化により到達可能になる新しいコントロール状態を追加することによって、Ｒｉから得られる。ＲｉからＲｉ＋１を構築するために、両方の制約、すなわち、（i）同期化プリミティブによって課される制約と（ii）文脈自由な到達可能性によって課される制約が満たされることを確実にすることが必要である。これは、ダブテイル方式で達成される。
【００８６】
最初に、同期化制約を満たすために、形式
【００８７】
【数２０】
2010506309.tif 000022
【００８８】
の遷移が存在するように、形式
【００８９】
【数２１】
2010506309.tif 000023
【００９０】
の全ての遷移（ｐおよびｐ’は、ｃ∈Ｒｉに整合する、ｓｅｎｄおよびｒｅｃｅｉｖｅランデブーアクションである）が、形式
【００９１】
【数２２】
2010506309.tif 000024
【００９２】
の内部遷移（rは、
【００９３】
【数２３】
2010506309.tif 000025
【００９４】
内の新しく導入された特別な内部アクションシンボルである）に変換される。これは、ｃがパラメータ化により到達可能であるので、ａが、（今、または、ある将来の反復で）パラメータ化により到達可能になる場合、あるｍについて、Ｕｍの到達可能な大域状態が存在し、プロセスが、それぞれ局所状態ａおよびｃ内にあることを確保することができるということによって動機付けられる。換言すれば、ａが到達可能になる場合、ランデブー遷移
【００９５】
【数２４】
2010506309.tif 000026
【００９６】
が、常に有効にされ、実施される。そのため、ランデブー遷移は、内部遷移のように扱われることができる。こうして、Ｒｉの全てのコントロール状態をフラッディングさせることによって、Ｒｉ内のコントロール状態から出る対ｓｅｎｄまたは対ｒｅｃｅｉｖｅ遷移から生じる全ての同期化制約を除去することができる。これは、Ｒｉ内のコントロール状態で開始する整合ｓｅｎｄ／ｒｅｃｅｉｖｅを有する全てのランデブー遷移を有効にするであろう。したがって、こうした遷移は、内部遷移と置き換えられることができる。これによって動機付けされて、Ｕｉ＋1が、上述した適切な対ランデブーｓｅｎｄ／ｒｅｃｅｉｖｅ遷移を内部遷移と置き換え、残りのランデブーｓｅｎｄおよびｒｅｃｅｉｖｅ遷移を除去することによって、元のテンプレートＵから得られるテンプレートであると定義する。
【００９７】
第２の制約、すなわち、文脈自由な到達可能性が満たされることをチェックするために、ここで、個々のＰＤＳ  Ｕｉ内で到達可能である、Ｕのコントロール状態の集合
【００９８】
【数２５】
2010506309.tif 000027
【００９９】
を判定するために、単一ＰＤＳをモデルチェックする任意のプロシジャが使用されることができる。これは、Ｕｉ内の全ての文脈自由な到達可能状態の集合
【０１００】
【数２６】
2010506309.tif 000028
【０１０１】
を与える。新しいコントロール状態は、前の集合内での一部の同期化制約の除去によって到達可能になる場合、Ｒｉ＋１に追加され、そうでなければ、固定点に達し、プロシジャが終了する。
【０１０２】
図３を参照すると、例において、Ｒ０が、｛ｃ０｝に初期化される。これは、両方の遷移
【０１０３】
【数２７】
2010506309.tif 000029
【０１０４】
および
【０１０５】
【数２８】
2010506309.tif 000030
【０１０６】
を有効にし、したがって、遷移は共に、内部遷移に変換されることができ、テンプレートＵ１をもたらす。第２反復（Ｕ２）では、ｃ５、ｃ６、ｃ８、およびｃ９は、全てテンプレートＵ１の到達可能なコントロール状態であるため、Ｒ１＝｛ｃ０，ｃ５，ｃ６，ｃ８，ｃ９｝であることに留意する。ここで、ｃ０およびｃ５はＲｌ内にあるため、ランデブー遷移
【０１０７】
【数２９】
2010506309.tif 000031
【０１０８】
および
【０１０９】
【数３０】
2010506309.tif 000032
【０１１０】
は、有効にされ、内部遷移に変換されることができ、テンプレートＵ２をもたらす。Ｕ２では、コントロール状態ｃ２、ｃ４、およびｃ７が到達可能になり、したがって、Ｒ２に追加され、Ｒ３＝｛ｃ０，ｃ２，ｃ４，ｃ５，ｃ６，ｃ７，ｃ８，ｃ９｝をもたらす。最後に、両方のコントロール状態ｃ４およびｃ６∈Ｒ３であるため、ランデブー遷移
【０１１１】
【数３１】
2010506309.tif 000033
【０１１２】
および
【０１１３】
【数３２】
2010506309.tif 000034
【０１１４】
は、内部遷移に変換され、テンプレートＵ３をもたらす。ｃ１およびｃ３は、Ｕ３の到達可能なコントロールロケーションであるため、これらのコントロールロケーションは、Ｒ４に含まれ、それにより、固定点に達し、プロシジャの終了をもたらす。ｃ１∈Ｒ４であるため、ｃ１はパラメータ化により到達可能であると結論付けられる。方法Ａの形式記述は、以下に示される。方法Ａは、Ｕのパラメータ化により到達可能なコントロール状態の集合を戻す。
【０１１５】
方法Ａ：ｉ＝０およびＲ０＝｛ｃ０｝に初期化する。ここで、ｃ０はＵの初期状態である。次に、ｉ＝ｉ＋１である。形式
【０１１６】
【数３３】
2010506309.tif 000035
【０１１７】
の整合ｒｅｃｅｉｖｅ（ｓｅｎｄ）遷移（ｃ∈Ｒｉ−１）が存在するように、形式
【０１１８】
【数３４】
2010506309.tif 000036
【０１１９】
のテンプレートＵのそれぞれの対ｓｅｎｄ（ｒｅｃｅｉｖｅ）遷移を、内部遷移
【０１２０】
【数３５】
2010506309.tif 000037
【０１２１】
で置き換え、残りの対ｓｅｎｄまたはｒｅｃｅｉｖｅランデブー遷移を除去することによって、ＰＤＳ  Ｕｉを構築する。単一ＰＤＳをモデルチェックするプロシジャを使用して、Ｕｉの文脈自由な到達可能コントロールロケーションの集合
【０１２２】
【数３６】
2010506309.tif 000038
【０１２３】
を計算する。
【０１２４】
【数３７】
2010506309.tif 000039
【０１２５】
に設定する。初期化ステップを除いて、
【０１２６】
【数３８】
2010506309.tif 000040
【０１２７】
になるまで、これらのステップを実施する。Ｒｉを戻す。
【０１２８】
複雑さ解析：方法Ａの各反復において、Ｒｉに、少なくとも１つの新しいコントロール状態が追加されることに注目して始める。そのため、方法は、せいぜい｜Ｑ｜回で終了する。ここで、Ｑは、Ｕのコントロール状態の集合である。ｉ番目の反復中に、Ｑ、Ｒｉ内のそれぞれのコントロール状態について、コントロール状態が、Ｕｉ＋１内で文脈自由に到達可能であるかどうかを決定する必要があり、これは、ＰＤＳについてのモデルチェッキングプロシジャを使用することによって、Ｏ（｜Ｕ｜３）時間で達成されることができる。ここで、｜Ｕ｜はＵのサイズである。したがって、各ステップは、せいぜいＯ（｜Ｕ｜４）時間かかる。そのため、方法全体は、Ｏ（｜Ｕ｜５）で実行される。対ランデブーによって相互作用するテンプレートＰＤＳ  Ｕで構成されるシステムの場合の、コントロール状態達成可能性、したがって、ＥＦ（ｃ１∧…∧ｃｋ）（データ競合）についてのパラメータ化によるモデルチェッキング問題は、Ｏ（｜Ｕ｜５）時間で決定されることができる。ここで、｜Ｕ｜はＵのサイズである。
【０１２９】
非同期ランデブー：非同期ランデブーによって相互作用するＰＤＳについてのＰＭＣＰを決定するプロシジャ（対ランデブーに比べて費用がかかる）は、本質的に方法Ａと同じである。非同期ランデブーの少し異なるセマンティックを反映させるのにわずかな修正が必要とされる。唯一の差は、非同期ｓｅｎｄ遷移
【０１３０】
【数３９】
2010506309.tif 000041
【０１３１】
は、整合ｒｅｃｅｉｖｅ
【０１３２】
【数４０】
2010506309.tif 000042
【０１３３】
が存在するか否かにかかわりなく実施されることができることである。一方、ｒｅｃｅｉｖｅ遷移は、整合ｓｅｎｄがその時有効にされることを必要とせず、ｓｅｎｄ遷移とｒｅｃｅｉｖｅ遷移は共に、そして、自動的に発火する。ここで、方法Ａにおいて、ＰＤＳ  Ｕｉを構築することが、以下のように修正される。形式
【０１３４】
【数４１】
2010506309.tif 000043
【０１３５】
のテンプレートＵのそれぞれの非同期ｓｅｎｄ遷移を、内部遷移
【０１３６】
【数４２】
2010506309.tif 000044
【０１３７】
と置き換える。一方、形式
【０１３８】
【数４３】
2010506309.tif 000045
【０１３９】
のｒｅｃｅｉｖｅ遷移を、内部遷移
【０１４０】
【数４４】
2010506309.tif 000046
【０１４１】
と置き換えるために、ｃ∈Ｒｉ−１に関して、形式
【０１４２】
【数４５】
2010506309.tif 000047
【０１４３】
の整合ｓｅｎｄ遷移が存在するかどうかを試験する必要がある。残りのｒｅｃｅｉｖｅ非同期ランデブー遷移は除去される。方法の時間計算量は同じままである。
【０１４４】
複数テンプレートへの拡張：まず初めに、Ｒ０は、テンプレートＵ１，…，Ｕｍのそれぞれの初期コントロール状態を含む。集合Ｒｉは、テンプレートのうちの任意のテンプレートにおいて、ｉ番目の反復まで検出されるパラメータ化により到達可能なコントロール状態の和集合に追従する。最後に、方法Ａにおいて、それぞれの１≦ｊ≦ｍについて、テンプレートのうちの任意のテンプレート内で、形式
【０１４５】
【数４６】
2010506309.tif 000048
【０１４６】
の有効にされた整合ｒｅｃｅｉｖｅ／ｓｅｎｄ遷移（ｃ∈Ｒｉ−１）を有するテンプレートＵｊ内のそれぞれのランデブーｓｅｎｄ／ｒｅｃｅｉｖｅ遷移
【０１４７】
【数４７】
2010506309.tif 000049
【０１４８】
を、内部遷移
【０１４９】
【数４８】
2010506309.tif 000050
【０１５０】
と置き換えることによって、ＰＤＳ  Ｕｊｉを構築する。
【０１５１】
Ｌ（Ｆ）についてのモデルチェッキングプロシジャ：所与のテンプレートＵ＝（Ｐ，Ａｃｔ，Γ，ｃ０，Δ）から、新しいテンプレートＲ＝（ＰＲ，Ａｃｔ，Γ，ｃ０，ΔＲ）を定義する。ここで、ＰＲは、Ｕのパラメータ化により達成可能なコントロール状態の集合であり、ΔＲは、それぞれの対ランデブーｓｅｎｄまたはｒｅｃｅｉｖｅ遷移が内部遷移に変換された状態での、ＰＲの状態間でのＵの遷移の集合である。ｆを、形式Ｅｇ（１，２）の式であるとする。ここで、ｇ（１，２）は、Ｕ［１］およびＵ［２］にわたる原子命題を有する２重インデックスＬＴＬ／Ｘである。そして、ｆについての推論が、有限計算経路に制限される場合、
【０１５２】
【数４９】
2010506309.tif 000051
【０１５３】
であり、ここで、Ｅｆｉｎは、有限経路にわったてだけ定量化する。
【０１５４】
ＰＭＣＰの２プロセスインスタンスへの低減の背景にある直感は、無限の重複度結果から得られるフラッディング議論である。ｆが、モデルとして、たとえば、長さｌの有限計算ｘを有する場合、せいぜいｌの対ｓｅｎｄまたはｒｅｃｅｉｖｅ遷移が、ｘに沿って発火される。無限の重複度補助定理によって、あるｍについて、ＵＲのそれぞれのコントロール状態の少なくともｌのコピーを有する、Ｕｍの到達可能状態をもたらす計算ｙが存在する。Ｕｍ＋２プロセスを有するシステムにおいて、最初に、プロセスＵ３，…，Ｕｍ＋２が、少なくともｌの重複度を有するＵＲの全てのコントロール状態をフラッディングさせるように、ｙを実施するようにさせる。そして、多くてｌの長さのＵ［１，２］の任意の計算ｘにおいて、ランデブー遷移が、プロセスＵ３，…，Ｕｍ＋１のうちの１つに関する同期化によって常に発火され、したがって、内部遷移として扱われることができることが保証される。
【０１５５】
そのため、（バイナリ低減結果）が得られる。Ｕｎ（ｎ≧２）の任意の有限の計算ｘの場合、ｙが、ｘ［１，２］に対してスタッタリング的に等価であるような
【０１５６】
【数５０】
2010506309.tif 000052
【０１５７】
の有限な計算ｙが存在する。即時の系として、ｆが、あるｍについて、Ｕｍの有限な計算であるモデルを有する場合、当然、あるｋについて、
【０１５８】
【数５１】
2010506309.tif 000053
【０１５９】
である場合、Ｕｋ｜＝ｆであることになる。特に、
系：Ｌ（Ｆ）の任意の式ｆの場合、あるｍについて、
【０１６０】
【数５２】
2010506309.tif 000054
【０１６１】
の場合、
【０１６２】
【数５３】
2010506309.tif 000055
【０１６３】
である。
【０１６４】
上記結果は、対ランデブーまたは非同期ランデブーによって相互作用するＰＤＳの場合のＬ（Ｆ）についてのＰＭＣＰを、効率的に決定可能であることがわかっている、２つだけの非相互作用ＰＤＳを含むシステムの（標準的な）モデルチェッキングに帰着させることに留意されたい。系として、Ｌ（Ｆ）についてのＰＭＣＰは、Ｕのサイズにおける多項式時間で決定可能であるということが得られる。
【０１６５】
カットオフを計算すること：ｃｕｔは、時間論理式ｆについてのカットオフであり、パラメータ化されたファミリは、ｍ≧ｃｕｔについて、Ｕｍ｜＝ｆであり、Ｕｃｕｔ｜＝ｆである場合、テンプテートＵによって定義されると言える。式ｆについてのカットオフの存在は、ｆについてのＰＭＣＰを、Ｕのカットオフ数までのコピーを有するシステムについての有限数の標準的なモデルチェッキング問題に帰着させるということから有用である。Ｂ（Ｆ）が、時相演算子ＡＦ、ブール演算子∨および∧、ならびに原子命題を使用して構築された分岐時間式の集合であるとする。Ｌ（Ｆ）式についてカットオフを計算し、次に、これを、Ｂ（Ｆ）式に拡張する方法を示す。カットオフを計算する１つの動機は、それが、Ｌ（Ｇ）の場合のＰＭＣＰについての決定プロシジャのステップであることである。もちろん、Ｌ（Ｆ）式をモデルチェックするカットオフ手法を使用することもできる。
【０１６６】
Ｌ（Ｆ）式についてカットオフ：Ｌ（Ｆ）の式ｆについてのカットオフｃｕｔは、ｆを満たす有限な計算に沿って発火するランデブー遷移の数に関連することを観測することによって始める。ｘが、ｆを満たす、あるｎについての、Ｕｎの有限な計算であるとする。Ｕのそれぞれのランデブー遷移ｔｒについて、ｎｔｒは、ｘ［１，２］に沿ってｔｒが発火する回数であるとする。一般性を失うことなく、それぞれのランデブーｓｅｎｄ／ｒｅｃｅｉｖｅ遷移ｔｒは、Ｕ内で、
【０１６７】
【数５４】
2010506309.tif 000056
【０１６８】
によって指定される一意の整合ｒｅｃｅｉｖｅ／ｓｅｎｄ遷移を有すると仮定する。それぞれのコントロール状態ｃについて、Ｔｒｃは、
【０１６９】
【数５５】
2010506309.tif 000057
【０１７０】
が、ｘ［１，２］に沿って発火するような、形式ｃ→ｄの対ランデブーｓｅｎｄまたはｒｅｃｅｉｖｅ遷移ｔｒの集合であるとする。同様に、Ｕのそれぞれのコントロール状態ｃについて、
【０１７１】
【数５６】
2010506309.tif 000058
【０１７２】
であるとする。そのとき、ｎｃの値によってｆについてのカットオフが与えられることができる。
【０１７３】
その方向への第１ステップとして、ｃｕｔが、それぞれのコントロール状態ｃの少なくともｎｃのコピーを有する、Ｕｃｕｔの到達可能な大域状態が存在するようなものである場合、フラッディング議論を使用して、ｃｕｔ’＋２が、ｆについてのカットオフであることを示す。次に、ｎｃからｃｕｔについての上限を推定する。Ｕのコントロール状態ｃが、最初に、Ｒｉに追加された方法Ａについての第１反復をｉｃで指定する。そして、Ｕｍ｜＝ＥＦｃ
が得られ、ここで、
【０１７４】
【数５７】
2010506309.tif 000059
【０１７５】
である。Ｕのそれぞれのコントロール状態ｃについて、Ｎｃは、ＥＦｃについてのカットオフであるとする。そして、
【０１７６】
【数５８】
2010506309.tif 000060
【０１７７】
である。
【０１７８】
そのため、ｃｕｔを計算する問題は、ｎｔｒおよびＮｃについて限界を計算することに帰着する。所与のＬ（Ｆ）式を満たす、あるｍについての、Ｕｍの計算に沿って発火する対ランデブー遷移の数、ｎｔｒで始める。Ｌ（Ｆ）式が、単一インデックスである、すなわち、原子命題が、１つのプロセスにわたってだけ解釈される場合を最初に考える。このため、一般性を失うことなく、Ｕのそれぞれのコントロール状態は、パラメータ化により到達可能であり、さもないと、到達不可能な状態および関連する遷移が除去されるだけであることが仮定される。さらに、同じフラッディング議論を使用して、Ｕのそれぞれのコントロール状態は、任意の重複度でフラッディングされることができる。そのため、有限計算について推論するとき、それぞれのランデブー遷移が内部遷移として扱われることができる。これは、パラメータ化されたファミリ｛Ｕ｝について推論する代わりに、単一テンプレートＵについてだけ推論することで十分であるため、解析を容易にする。
【０１７９】
ＰＤＳについてのこれらの限界の計算は、スタックによって導入される文脈自由な到達可能性によって複雑になる。その問題を処理するために、重み付きマルチオートマトン（ＷＭＡ）の概念を活用する。重み付きマルチオートマトン（ＷＭＡ）は、その遷移がそれぞれ、非負整数のラベルを付けされるマルチオートマトン（ＭＡ）である。ＷＭＡは、データフロー解析のために以前から使用されてきた。しかし、ＷＭＡは、ここでは、異なる目的のために、たとえば、２つのコントロール状態間で遷移するときに発火する対ランデブー遷移の数に関する限界を推定するために使用される。直感的に、ＷＭＡの遷移ｓ→ｔに付けられる重みは、ｓからｔに達するために発火する必要があるランデブー遷移の数に関する上限を指示する。
【０１８０】
重み付きマルチオートマトン（ＷＭＡ）は、以下のように定義されてもよい。ＰＤＳ  Ｐ＝（Ｐ，Γ，ｃ０，Δ）が与えられると、重み付きマルチオートマトンは、タプルＭ＝（Γ，Ｑ，δ，ｗ，Ｉ，Ｆ）であり、ここで、Ｍ’＝（Γ，Ｑ，δ，Ｉ，Ｆ）は、マルチオートマトンであり、ｗ：δ→Ｚは、Ｍのそれぞれの遷移を非負整数にマッピングする関数である。Ｍの有限経路ｘの重みは、ｘに沿って現れる全ての遷移の重みの和であるとして定義される。Ｍの状態ｓとｔが与えられると、ｕのラベルを付けられ、かつ、重みｂを有する、ｓからｔへのＭの経路が存在することを示すために、
【０１８１】
【数５９】
2010506309.tif 000061
【０１８２】
が使用される。ｆを満たす計算に沿って発火するランデブー遷移の数についての限界を評価するために、ｆを満たすＵの全ての構成の（正則な）集合を捕捉する、ｆについてのＷＭＡ  Ｍｆを構築することにする。そして、ｂが、Ｍｆ内の（ｃ０，⊥）についての受容される経路の重みである場合、せいぜいｂの対ランデブー遷移が、それに沿って発火するＵの経路が存在することを示す。
【０１８３】
Ｌ（Ｆ）式は、演算子Ｆ、∨、および∧を使用して構築されるため、Ｍｆを構築するために、ｇおよびｈについてＷＭＡが与えられると、Ｆｇ、ｇ∧ｈ、およびｇ∨ｈについてＷＭＡを構築する方法を示すことで十分である。そして、Ｌ（Ｆ）式ｆが与えられると、ｆの原子命題について、ＷＭＡで始めてこれらの構築を繰り返し完全に適用することによって、Ｍｆが与えられる。
【０１８４】
定義：
マルチオートマトン：Ｐ＝（Ｐ，Ａｃｔ，Γ，ｃ０，Δ）が、プッシュダウンシステムであり、Ｐ＝｛ｐ１，…，ｐｍ｝であるとする。Ｐ−マルチオートマトン（短縮してＰ−ＭＡ）は、タプルＡ＝（Γ，Ｑ，δ，Ｉ，Ｆ）であり、ここで、Ｑは状態の有限集合であり、δ⊆Ｑ×Γ×Ｑは遷移集合であり、Ｉ＝｛ｓ１，…，ｓｍ｝⊆Ｑは初期状態の集合であり、Ｆ⊆Ｑは最終状態の集合である。それぞれの初期状態ｓｉは、Ｐのコントロール状態ｐｉに相当する。
【０１８５】
遷移関係→⊆Ｑ×Γ＊×Ｑを、
【０１８６】
【数６０】
2010506309.tif 000062
【０１８７】
を満たす最小関係として定義する。
【０１８８】
マルチオートマトンは、所与のＰＤＳの構成の（おそらくは無限の）正則な集合を簡潔に表現するのに使用されるデータ構造として考えられることができる。その結果、マルチオートマトンＡは、あるｑ∈Ｆについて
【０１８９】
【数６１】
2010506309.tif 000063
【０１９０】
である場合、構成（ｐｉ，ｗ）を受容すると言える。Ａによって認識される構成の集合は、Ｃｏｎｆ（Ａ）によって指定される。構成の集合は、あるＭＡによって認識される場合、正則である。
【０１９１】
交替性プッシュダウンシステム：Ｐ＝（Ｐ，Ａｃｔ，Γ，ｃ０，Δ）が、プッシュダウンシステムであるとする。ＡＰＤＳは、５タプルＰ＝（Ｐ，Γ，Δ）であり、ここで、Ｐはコントロールロケーションの有限集合であり、Γは、有限スタックアルファベットであり、
【０１９２】
【数６２】
2010506309.tif 000064
【０１９３】
は、遷移ルールの有限集合である。（ｐ，γ，Ｓ）∈Δの場合、それぞれのサクセサ集合は、形式｛（ｐ１，ｗ１），…，（ｐｎ，ｗｎ）｝∈Ｓであり、Ｐの遷移は、（ｐ，γ）｛（ｐ１，ｗ１），…，（ｐｎ，ｗｎ）｝によって指定される。非決定論によって、その全てが、集合Ｓによって捕捉される、コントロール状態ｐとスタックアルファベットγの各対について複数のサクセサ集合が存在してもよい。Ｐの構成は、対（ｐ，ｗ）であり、ここで、ｐ∈Ｐはコントロールロケーションを指定し、ｗ∈Γ＊はスタックコンテンツを指定する。Ｐの全ての構成の集合は、Ｃで指定される。（ｐ，γ）｛（ｐ１，ｗ１），…，（ｐｎ，ｗｎ）｝である場合、全てのｗ∈Γ’について、構成（ｐ，γｗ）は、集合（ｐ１，ｗ１ｗ，…，ｐｎ，ｗｎｗ）のイミディエイトプリデセサであり、この集合は、（ｐ，γｗ）のイミディエイトサクセサと呼ばれる。イミディエイトサクセサ関係を指定するために、→が使用される。構成（ｐ，γｗ）から、遷移（ｐ，γ）｛（ｐ１，ｗ１），…，（ｐｎ，ｗｎ）｝を発火させることは、ＡＰＤＳを構成（ｐ１，ｗ１ｗ，…，ｐｎ，ｗｎｗ）に分岐させることに留意されたい。
【０１９４】
初期構成ｃについてのＰのランは、ルートｃを有する構成木であり、それにより、ノードｃ’の子は、初期構成ｃのイミディエイトサクセサのうちの１つに属する構成である。構成と構成の集合との間で、達成可能性関係
【０１９５】
【数６３】
2010506309.tif 000065
【０１９６】
を定義する。非公式に、Ｃが、ｃから始まるＰのランの有限フロンティアである場合でかつその場合にだけ、ｃ⇒Ｃである。公式に、⇒は、
【０１９７】
【数６４】
2010506309.tif 000066
【０１９８】
の最小部分集合であるため、
・全てのｃ∈Ｐ×Γ＊について、ｃ⇒ｃ｛ｃ｝であり、
・ｃが、Ｃのイミディエイトプリデセサである場合、ｃ⇒Ｃであり、
・それぞれの１≦ｉ≦ｎについてｃ⇒｛ｃ１，…，ｃｎ｝でかつｃｉ⇒Ｃｉである場合、ｃ⇒（Ｃ１∪…∪Ｃｎ）である。
【０１９９】
交替性マルチオートマトン：Ｐ＝（Ｐ，Γ，Δ）が、ＡＰＤＳシステムであり、Ｐ＝｛ｐ１，…，ｐｍ｝であるとする。交替性Ｐ−マルチオートマトン（短縮してＰ−ＡＭＡ）は、タプルＡ＝（Γ，Ｑ，δ，Ｉ，Ｆ）であり、ここで、Ｑは状態の有限集合であり、δ⊆Ｑ×Γ×２Ｑは遷移集合であり、Ｉ＝｛ｓ１，…，ｓｍ｝⊆Ｑは初期状態の集合であり、Ｆ⊆Ｑは最終状態の集合である。遷移関係→⊆Ｑ×Γ＊×２Ｑを、
【０２００】
【数６５】
2010506309.tif 000067
【０２０１】
を満たす最小関係として定義する。
【０２０２】
ＡＭＡ  Ａは、あるＱ⊆Ｆについて、
【０２０３】
【数６６】
2010506309.tif 000068
【０２０４】
である場合、構成（ｐｉ，ｗ）を受容する。Ａによって認識される構成の集合は、Ｃｏｎｆ（Ａ）によって指定される。有限シーケンスｗ∈Γ＊および状態ｑ∈Ｑが与えられると、ｑから始まるｗにわたるＡのランは、そのノードがＱ内で状態によってラベル付けされ、そのエッジがΓ内でシンボルによってラベル付けされる有限木であるため、根がｑによってラベル付けされ、他のノードのラベル付けは、δと一貫性がある。こうした木において、根から葉に進むエッジのそれぞれのシーケンスは、ｗのラベルを付けられることが遵守される。構成の集合は、あるＡＭＡによって認識される場合、正則である。
【０２０５】
∨についての重み付きオートマトン：Ｍ１＝（Γ，Ｑ１，δ１，ｗ１，Ｉ１，Ｆ１）とＭ２＝（Γ，Ｑ２，δ２，ｗ２，Ｉ２，Ｆ２）が２つのＷＭＡであるとする。そして、最初に、Ｍ１の各初期状態ｓをｓ’として、Ｍ２の各初期状態ｓをｓ’’としてそれぞれリネームすることによって、Ｍ１およびＭ２によって受容される構成の和集合を受容するＷＭＡ  Ｍを構築することができる。そして、標準的な和集合構築Ｍ＝（Γ，Ｑ１∪Ｑ２，δ１∪δ２∪δ１２，ｗ，Ｉ，Ｆ１∪Ｆ２）によってマルチオートマトンＭ＝Ｍ１∨Ｍ２を定義する。ここで、遷移ｔｒ∈Ｒｉについて、δ（ｔｒ）＝δｉ（ｔｒ）であり、かつ、
【０２０６】
【数６７】
2010506309.tif 000069
【０２０７】
あり、かつ、
【０２０８】
【数６８】
2010506309.tif 000070
【０２０９】
であり、Ｉは、テンプレートＵのコントロール状態ｐ１，…，ｐｍに相当する、新しく導入された初期状態ｓ１，…，ｓｍの集合であり、δ１２は、ゼロ重み遷移
【０２１０】
【数６９】
2010506309.tif 000071
【０２１１】
の集合である。
【０２１２】
∧についての重み付きオートマトン：Ｍ１＝（Γ，Ｑ１，δ１，ｗ１，Ｉ１，Ｆ１）とＭ２＝（Γ，Ｑ２，δ２，ｗ２，Ｉ２，Ｆ２）が２つのＷＭＡであるとする。標準的な積構築Ｍ＝（Γ，Ｑ１×Ｑ２，δ，ｗ，Ｉ１×Ｉ２，Ｆ１×Ｆ２）によって、Ｍ１とＭ２の積集合を受容するＷＭＡ  Ｍを構築することができる。ここで、
【０２１３】
【数７０】
2010506309.tif 000072
【０２１４】
であり、かつ、
【０２１５】
【数７１】
2010506309.tif 000073
【０２１６】
である場合、
【０２１７】
【数７２】
2010506309.tif 000074
【０２１８】
であり、ｗは、ｗ１とｗ２の最大である。状態（ｓｉ，ｓｉ）は、ｓｉとしてリネームされて、Ｕのそれぞれのコントロール状態ｐｉについて、Ｍの初期状態が存在することが確保される。
【０２１９】
Ｆｇについての重み付きマルチオートマトン：Ｍ０が、ｇを満たすＵの正則構成の集合を受容する所与のＷＭＡであるとする。Ｍ０で始めると、一連のＷＭＡ  Ｍ０，…，Ｍｍを構築し、ＷＭＡ  Ｍｍが得られる。Ｕのそれぞれのコントロール状態ｐｉについて、Ｍ０の初期状態ｓｉが存在することが、ＭＡの定義から思い起こされる。→ｋによって、Ｍｋの遷移関係を指定する。そして、全てのｋ≧０について、状態の集合を保存し、以下の３項のように新しい遷移を追加することによって、ＭｋからＭｋ＋１が得られる。３項とは、（ｉ）それぞれの内部遷移ｐｉ→ｐｊについて、
【０２２０】
【数７３】
2010506309.tif 000075
【０２２１】
に重み０を追加する。（ｉｉ）それぞれの対ランデブーｓｅｎｄまたはｒｅｃｅｉｖｅ遷移ｐｉ→ｐｊについて、遷移
【０２２２】
【数７４】
2010506309.tif 000076
【０２２３】
に重み１を追加する。（ｉｉｉ）Ｕのそれぞれのスタック遷移
【０２２４】
【数７５】
2010506309.tif 000077
【０２２５】
について、ｕのラベルを付けられた、ｓｊからｔへのＭｋ内の経路ｘが存在する場合、遷移
【０２２６】
【数７６】
2010506309.tif 000078
【０２２７】
が追加される。ここで、ｗｕは、ｘに沿って起こる遷移の重みの和である。１を超えるこうした経路が存在する場合、全てのこうした経路にわたって最小重みであるようにｗｕを選択してもよいことに留意されたい。
【０２２８】
Ｕの構成ｓおよびｔについて、ｓ⇒≦ｂｔが、せいぜいｂの対ランデブー遷移が、それに沿って発火する、ｓからｔへの経路が存在することを指定するとする。そして、
【０２２９】
【数７７】
2010506309.tif 000079
【０２３０】
である場合、あるｐｋおよびνについて、（ｐｊ，ｗ）⇒≦ｂ（ｐｋ，ν）であるため、
【０２３１】
【数７８】
2010506309.tif 000080
【０２３２】
である。ここで、ｂ＝ｂ１＋ｂ２である。さらに、ｑが初期状態ｓｉである場合、ｐｋ＝ｐｉであり、かつ、ν＝εである。ｆ∨ｇおよびｆ∧ｇについてのＷＭＡの構築は、オートマンについての標準的な和集合および積集合構築と同様である。
【０２３３】
Ｌ（Ｆ）式ｆが与えられると、原子命題用のＭＡを構築し、全てのその遷移の重みを０に設定することによって、ｆのそれぞれの原子命題についてＷＭＡを最初に構築する。次に、原子命題から始めて式ｆを完全にトラバースすることによって、上記演算を実施する。Ｍｆが得られるＷＭＡであるとする。上記結果を使用して、Ｕの構成（ｑ，ｕ）が、Ｍｆによって受容され、ｂが、ｑから始まりかつｕのラベルを付けられたＭの受容経路の重みであるとする。そして、（ｑ，ｕ）から始まりかつｆを満たすＵの有限経路が存在するため、せいぜいｂの対ランデブー遷移が、その経路に沿って発火する。
【０２３４】
２重インデックス式：２重インデックスＬ（Ｆ）式ｆについてカットオフを計算する問題を単一インデックスの問題に帰着させる。一般性を失うことなく、ｆのそれぞれの原子命題は、形式ｃまたは¬ｃであると仮定されることができる。ここで、ｃは、Ｕのコントロールロケーションである。¬ｃを、ｃ以外のＵの全ての（有限に多くの）コントロール状態の積集合として書き直して、ｆから全ての否定を除去することができる。ｆ＝Ｅｇであるとする。そして、ｇ内の∨演算子をできる限り遠くへ押しやることによって、ｇ＝ｇ１∨…∨ｇｋと書くことができる。ここで、それぞれのｉについて、ｇｉは、∨演算子を含まない。そして、Ｅｇ１，…，Ｅｇｋについてのカットオフの最小が、Ｅｇについてのカットオフである。そのため、Ｅｇ（１，２）についてカットオフを計算することで十分である。ここで、ｇ（１，２）は、¬は無いが、Ｆ、∧、ならびにＵｎ内のＵ［１］およびＵ［２］のコントロール状態である原子命題を使用して構築された式である。
【０２３５】
ｇ（１，２）に関して、形式（ｃｉ，ｄｊ）の順序付き対の有限シーケンスの集合Ｓｅｑを関連付けることができることに留意されたい。ｃｉ（ｄｊ）は、真であるか、または、ｇ（１，２）で起こるＵ［１］（それぞれＵ［２］など）のコントロール状態であり、ｃｉ∧ｄｊを満たす大域状態が、ｇ（１，２）を満たす計算経路に沿って現れる可能性がある、考えられる全ての順序を捕捉する。たとえば、Ｕ［ｊ］が、そのとき、局所コントロール状態ｃｉにある場合に、
【０２３６】
【数７９】
2010506309.tif 000081
【０２３７】
が真であるような、
【０２３８】
【数８０】
2010506309.tif 000082
【０２３９】
に関して、シーケンス
【０２４０】
【数８１】
2010506309.tif 000083
【０２４１】
および
【０２４２】
【数８２】
2010506309.tif 000084
【０２４３】
を関連付けることができる。そのため、Ｓｅｑ内にシーケンスπ：（ｃ１，ｄ１），…，（ｃｋ，ｄｋ）が存在し、かつ、挙げた順序でｃ１∧ｄ１，…，ｃｋ∧ｄｋを満たす大域状態が、それに沿って存在する計算経路ｘ、すなわち、ｘ：ｇｋ＝ｃ１∧ｄ１∧Ｆ（ｃ２∧ｄ２∧Ｆ（…））が存在する場合、Ｕｎ｜＝Ｅｇ（１，２）である。そして、ｆπ（π∈Ｓｅｑ）についてのカットオフ限界の最小は、所望のカットオフを与える。最後に、ｆπについてのカットオフ限界の計算は、以下の結果によって、単一インデックスＬ（Ｇ）式の計算に帰着されることができる。式ｆ＝ｃ１∧ｄ１∧Ｆ（ｃ２∧ｄ２∧Ｆ（…））が与えられると、ｆ１＝ｃ１∧Ｆ（ｃ２∧Ｆ（…））およびｆ２＝ｄ１∧Ｆ（ｄ２∧Ｆ（…））についてのカットオフの和は、ｆについてのカットオフ限界である。
【０２４４】
Ｎｃの計算：Ｕのコントロール状態ｃが与えられると、Ｎｃ、すなわち、ＥＦｃについてのカットオフを計算する方法をここで示す。ｃが、方法Ａのｉ番目の反復においてＲｌに最初に含まれるとする。Ｎｃの計算は、ｉに関する帰納法による。ｉ＝０、すなわち、ｃがＵの初期状態である場合、Ｎｃ＝１である。ここで、Ｎｃは、それぞれのｃ∈Ｒｉ（ｉ＞０）についてわかっていると仮定する。ｃ∈Ｒｉ＋１，Ｒｉであるとする。そして、ｃをもたらすＲｉの状態を含むＵｉ＋１の経路が存在する。ＷＭＡを使用して、それぞれのランデブー遷移ｔｒについて、ｎｔｒに関する限界、ＥＦｃを満たすＵｉ＋１の経路に沿ってｔｒが発火する回数を計算することができる。同様に、帰納的憶測によって、Ｒｉのそれぞれのｃについて、Ｎｃの値がわかり、ＥＦｃについてのカットオフが決定され、帰納的ステップが終了する。
【０２４５】
カットオフを計算する例：ｃｕｔ＋２は、ｆについてのカットオフである。全てのコントロール状態ｃが、プロセスＵ３，…，Ｕｋ＋２を使用してフラッディングされると、プロセスＵ１およびＵ２は、ｘ［１，２］を実行することができ、Ｕ１またはＵ２によって発火されるそれぞれのランデブー遷移は、プロセスＵ３，…，Ｕｋ＋２のうちの１つと同期する。Ｕのコントロール状態ｃについて、ＮｃがＥＦｃについてのカットオフであるとすると、
【０２４６】
【数８３】
2010506309.tif 000085
【０２４７】
となる。ＮｃがＥＦｃについてのカットオフであるため、プロセスが局所状態ｃにある状態で、大域状態をもたらす
【０２４８】
【数８４】
2010506309.tif 000086
【０２４９】
の計算ｘｃが存在する。ｃの少なくともｎｃのコピーを有する大域状態を得るために、
【０２５０】
【数８５】
2010506309.tif 000087
【０２５１】
のプロセスＵ［１］，…，Ｕ［Ｎｃ］が、ｃの少なくとも１つのコピーを有する大域状態ｓｌに達するようにｘｃを実行させる。次に、ｓｌから始めて、プロセスＵ［Ｎｃ＋１］，…，Ｕ［Ｎｃ＋ｎｃ］が、ｃの少なくとも２つのコピーを有する大域状態ｓ２に達するようにｘｃを実行させる。このプロセスをｎｃ回繰り返すことによって、ｃの少なくともｎｃのコピーを有する大域状態
【０２５２】
【数８６】
2010506309.tif 000088
【０２５３】
がもたらされる。このプロセスをそれぞれのコントロール状態ｃについて繰り返すことによって、所望の結果が得られる。
【０２５４】
Ｂ（Ｆ）についてのカットオフ：Ｂ（Ｆ）式についてのカットオフを生成するために、ｍｕ−ｃａｌｃｕｌｕｓ式についてＰＤＳをモデルチェックする標準的なプロシジャを思い起こすことによって始める。所与のＰＤＳ  Ｕと、所与の式ｆについての交替性オートマトン／タブローとの積を最初にとる。こうした積は、交替性プッシュダウンシステム（ＡＰＤＳ）としてモデル化される。そして、ｆについてのモデルチェッキングは、得られるＡＰＤＳの構成の正則集合についてのｐｒｅ＊−ｃｌｏｓｕｒｅ計算に帰着する。これらの正則集合は、交替性マルチオートマトン（ＡＭＡ）としてモデル化されることができる。
【０２５５】
Ｂ（Ｆ）式についてカットオフを計算するプロシジャは、Ｌ（Ｆ）式についてのプロシジャと同様である。唯一の差は、重み付き交替性マルチオートマトン（ＷＡＭＡ）を使用して、式の分岐性質が捕捉され、一方、状態が、たった１つのサクセサの代わりにサクセサの集合を有することができることである。そのため、標準的なＡＭＡでは、それぞれの遷移は、集合（Ｑ×）Γ×２Ｑのメンバである。ｆは、分岐時間プロパティであるため、ｆについてのモデルは、Ｕの計算木であることに留意されたい。こうして、ｐｒｅ＊−ｃｌｏｓｕｒｅ計算を実施しながら、これまでに遭遇した計算木の各枝に沿って発火した対ランデブーの数に追従する必要がある。しかし、計算木の異なる枝に沿って発火する対ランデブーの数は、一般に、異なり、したがって、各状態について、進行中の遷移は、異なる重みを割当てられる必要がある。そのため、各遷移は、今や、集合（Ｑ×）Γ×２Ｑ×Ｚのメンバである。
【０２５６】
重み付き交替性マルチオートマトン（ＷＡＭＡ）：ＰＤＳ  Ｐ＝（Ｐ，Γ，ｃ０，Δ）が与えられると、ＷＡＭＡはタプルＭ＝（Γ，Ｑ，δ，Ｉ，Ｆ）（δ⊆（Ｑ×Γ）×２Ｑ×Ｚ）であり、Ｍ’＝（Γ，Ｑ，δ’，Ｉ，Ｆ）はＡＭＡ（δ’＝｛（ｓ，｛ｔ１，…，ｔｍ｝｜（ｓ，｛（ｔ１，ｗ１），…，（ｔｍ，ｗｍ）｝）∈δ｝）である。
【０２５７】
ｇについてのＷＡＭＡが与えられた場合に、ＡＦｇについてのＷＡＭＡを計算するために、ｐｒｅ＊−ｃｌｏｓｕｒｅ中に重みを更新することが、Ｌ（Ｆ）式について同様な方法で実施されることができる。唯一の差は、重みが、それぞれのサクセサについて更新される必要があることである。Ｍ０が、正則構成の集合を受容する所与のＷＡＭＡであるとする。Ｍ０で始めて、一連のＷＡＭＡ  Ｍ０，…，Ｍｐが構築され、ＷＡＭＡ  Ｍｐがもたらされる。→ｋによって、Ｍｋの遷移関係が指定される。そして、全てのｋ≧０について、状態の集合を保存し、以下の３項のように新しい遷移を追加することによって、ＭｋからＭｋ＋１が得られる。３項とは、（ｉ）それぞれの内部遷移
【０２５８】
【数８７】
2010506309.tif 000089
【０２５９】
について、遷移
【０２６０】
【数８８】
2010506309.tif 000090
【０２６１】
に重み０を追加する。（ｉｉ）それぞれの対ランデブーｓｅｎｄまたはｒｅｃｅｉｖｅ遷移
【０２６２】
【数８９】
2010506309.tif 000091
【０２６３】
について、遷移
【０２６４】
【数９０】
2010506309.tif 000092
【０２６５】
に重み１を追加する。（ｉｉｉ）それぞれの遷移
【０２６６】
【数９１】
2010506309.tif 000093
【０２６７】
および全ての集合
【０２６８】
【数９２】
2010506309.tif 000094
【０２６９】
について、新しい遷移
【０２７０】
【数９３】
2010506309.tif 000095
【０２７１】
を追加する。ここで、それぞれのｊについて、ｂｊは、全てのｂｒｊの最大であり、ここで、ｐｒｊ＝ｑｊである。
【０２７２】
Ｌ（Ｇ）についてのモデルチェッキングプロシジャ：無限モデルを有する２重インデックスＬＴＬ式について推論することは、一般に、有限モデルを有する２重インデックスＬＴＬ式について推論することより難しい。これは、あるｍについて、Ｕｍの無限計算が存在し、その計算に沿って、ランデブー遷移が、しばしば無限に再利用されることができるだけでなく、文脈自由な達成可能性を維持しながら、そうすることができることを確保しなければならないからである。しかし、Ｌ（Ｇ）式の双対性は、形式Ａｇであり、ここで、ｇは、時相演算子Ｆおよびブール結合記号∧および∨を使用して構築されることを利用する。こうした式は、有限木に似たモデルを有する。しかし、∀ｎ：Ｕｎ｜＝¬ｆである場合、∃ｎ：Ｕｎ｜＝ｆであることに留意されたい。そのため、ｆの双対性に頼る場合、得られる問題は、もはやＰＭＣＰではない。Ｌ（Ｇ）の場合のＰＭＣＰについての方法は、以下のようになる。
１．Ｌ（Ｇ）式ｆが与えられると、¬ｆに等価なＢ（Ｆ）式ｇを構築する、すなわち、Ｕｍ｜＝ｇである場合、Ｕｎ｜＝¬ｆである。
２．ｇについてカットオフｃｕｔを計算する。
３．それぞれのｍ≦ｃｕｔについて、Ｕｍ｜＝ｇであるかどうかをチェックする。
【０２７３】
Ｂ（Ｆ）式についてのカットオフを計算するプロシジャが、先に示された。ステップ３の場合、それぞれのｍ≦ｃｕｔについて、Ｕｍ｜＝¬ｇであるかどうかをチェックすることで十分である。ここで、ｆ＝¬ｇは、Ｌ（Ｇ）式である。しかし、対または非同期ランデブーによって相互作用する有限数のＰＤＳを有するシステムの場合のＬ（Ｇ）式についてのモデルチェッキング問題は、決定可能であることが既に知られている。そのため、ｆに等価なＢ（Ｆ）式ｇを構築する方法が示されることができる。
【０２７４】
選言ガード：選言ガードによって相互作用するＰＤＳについてのＰＭＣＰを考える。ここで、Ｕの遷移は、ｃ１，…，ｃｋがＵのコントロール状態である形式∨（ｃ１∨…∨ｃｋ）のブール表現であるガードのラベルを付けられる。Ｕｎ内のテンプレートＵのコピーＵ［ｉ］において、Ｕの遷移
【０２７５】
【数９４】
2010506309.tif 000096
【０２７６】
は、形式
【０２７７】
【数９５】
2010506309.tif 000097
【０２７８】
の遷移として書き直される。Ｕｎにおいて、ｓ内の局所状態ｃ１，…，ｃｋのうちの少なくとも１つの中に、Ｕ［ｉ］以外のプロセスＵ［ｊ］が存在する場合、Ｕ［ｉ］のこうした遷移は、Ｕｎの大域状態ｓ内で有効にされる。ブールガードによって通信するプロセスを有する並行システムは、ダイクストラのガード付きコマンドモデルによって動機付けされる。選言ガードによって相互作用する有限状態プロセスについてのＰＭＣＰは、効率的に決定可能であることが示された。対ランデブーについて、無限の重複度結果が有効である。そして、前と同様に、パラメータ化により到達可能なコントロール状態の集合が、効率的に計算されることができる。同期制約を扱うために、ＲｉからＲｉ＋１を構築するときに、形式
【０２７９】
【数９６】
2010506309.tif 000098
【０２８０】
の全ての遷移（あるｊ∈［１，ｋ］についてｃｊ∈Ｒｉ）を、形式
【０２８１】
【数９７】
2010506309.tif 000099
【０２８２】
の内部遷移に変換することを除いて、プロシジャは、対ランデブーによって相互作用するＰＤＳについてのプロシジャと同様である。これは、ｃｊが、パラメータ化により到達可能であるため、あるｊについて、局所状態ｃｊのプロセスが存在することを、無限の重複度結果およびフラッディング議論により保証することによって、遷移
【０２８３】
【数９８】
2010506309.tif 000100
【０２８４】
が常に有効にされることができることによって動機付けされる。選言ガードによって相互作用するテンプレートＰＤＳ  Ｕから構成されるシステムの場合の、コントロール状態到達可能性についてのパラメータ化によるモデルチェッキング問題は、Ｏ（｜Ｕ｜５）回で決定されることができる。ここで、｜Ｕ｜は、Ｕのサイズである。
【０２８５】
線形時間式についてのＰＭＣＰ：ＵＲを、パラメータ化により到達可能なコントロール状態だけ、および、内部であるか、または、パラメータ化により到達可能なコントロール状態のうちの少なくとも１つを選言肢として有する選言ガードをラベル付けされる、コントロール状態間の全ての遷移を保持することによって、Ｕから得られるＰＤＳであるとする。しかし、選言ガードをラベル付けされるそれぞれのこうした遷移を、ＵＲを非相互作用的にする内部遷移で置き換える。任意の２重インデックスＬＴＬ＼Ｘ式ｇの場合、あるｎについて、
【０２８６】
【数９９】
2010506309.tif 000101
【０２８７】
である場合、Ｕｎ｜＝Ｅｇであることを、フラッディング議論によって、最初に示す。無限の重複度プロパティによって、あるｍについて、Ｕのパラメータ化により到達可能なそれぞれのコントロール状態のうちの少なくとも１つのコピーを有するＵｍの大域状態をもたらす計算ｙが存在する。Ｕｍ＋２のプロセスを有するシステムにおいて、最初に、Ｕの全てのコントロール状態を重複度で少なくとも１回フラッディングさせるように、プロセスＵ３，…，Ｕｍ＋２にｙを実行させる。そして、Ｕ３，…，Ｕｍ＋１の中のプロセスが、到達可能なコントロール状態のそれぞれの中に存在するため、Ｕ［１，２］の任意の計算ｘ（有限または無限）において、選言ガードをラベル付けされた遷移が、常に発火されることができることが保証される。したがって、全てのこうした遷移は、内部遷移として扱われることができる。
【０２８８】
バイナリ低減結果：Ｕｎ（ｎ≧２）の任意の計算ｘについて、ｙが、ｘ［１，２］とスタッタリング的に等価であるような、
【０２８９】
【数１００】
2010506309.tif 000102
【０２９０】
の計算ｙが存在する。上記結果は、任意の２重インデックスＬＴＬ＼Ｘ式ｆについてのＰＭＣＰを、ｆについての２つの非相互作用ＰＤＳを有するシステムについてのモデルチェッキングに帰着させることに留意されたい。結果として、フラグメントＬ（Ｆ）およびＬ（Ｇ）だけを考える必要があることになる。これらのフラグメントの場合、非相互作用ＰＤＳを有するシステムをモデルチェックする問題は、効率的に決定可能であることが既にわかっている。そのため、選言ガードによって相互作用するＰＤＳについてのＰＭＣＰは、フラグメントＬ（Ｆ）およびＬ（Ｇ）については効率的に決定可能であり、フラグメントＬ（Ｕ）およびＬ（Ｆ，Ｇ）については決定不可能である。
【０２９１】
ロック：ロックによって相互作用するＰＤＳについてのＰＭＣＰを考える。先に求めたカットオフ結果を活用して、Ｕ２｜＝ｆ（ｆは２重インデックスＬＴＬ＼Ｘ式である）である場合、ｎ≧２について、Ｕｎ｜＝ｆである。これは、ｆについてＰＭＣＰを決定する問題を、ロックによって相互作用する２つのＰＤＳを含むシステムについての（標準的な）モデルチェッキング問題に帰着させる。
【０２９２】
ここで、入れ子ロックと非入れ子ロックとを区別する。ＰＤＳは、ＰＤＳが取得し、まだ解放していない最後のロックを解放することができるだけである場合、入れ子方式でロックにアクセスする。入れ子ロックによって相互作用する２つのＰＤＳを有するシステムの場合、２つのＰＤＳを有するシステムのモデルチェッキング問題は、対象となる両方のフラグメント、すなわち、Ｌ（Ｆ）およびＬ（Ｇ）について、効率的に決定可能であることがわかっている。そのため、入れ子ロックによって相互作用するＰＤＳの場合のＬ（Ｆ）およびＬ（Ｇ）についてのＰＭＣＰは、所与のテンプレートＵのコントロール状態の数の多項式時間で、Ｕのロックの数の指数関数時間で決定可能である。
【０２９３】
非入れ子ロックの場合、ＰＭＣＰは、Ｌ（Ｇ）については決定可能であるが、Ｌ（Ｆ）については決定不可能であることを示す。Ｌ（Ｆ）の場合、決定不可能であることがわかっている式ＥＦ（ｃ１∧ｃ２）の場合に、非入れ子ロックによって相互作用する２つのＰＤＳ  Ｐ１およびＰ２を含むシステムをモデルチェックする問題からの帰着によって、決定不可能性結果がもたらされる。
【０２９４】
ＥＦ（ｃ１∧ｃ２）、したがって、Ｌ（Ｆ）についてのＰＭＣＰは、非入れ子ロックによって相互作用するＰＤＳについて決定不可能である。Ｌ（Ｇ）の場合、Ｌ（Ｇ）式ｆの場合に、ロックによって相互作用するＰＤＳを有するシステムをモデルチェックする問題は、２つの非相互作用ＰＤＳについての代替式ｆ’をモデルチェックすることに帰着されることができることが示される。ロックｌ１，…，ｌｋによって相互作用するテンプレートＵが与えられる場合、形式（ｃ，ｍ１，…，ｍｋ）のコントロール状態を有する新しいテンプレートＶを構築する。考え方は、Ｕのコピーが、そのときロックｌｉの占有下にあるかどうかをビットｍｉに記憶することである。ビットｍｉは、それぞれ、Ｕｉが、ｌｉの占有下にあるか否かに応じて、１または０をセットされる。そして、全てのロックをＶから除去し、代わりにＶのそれぞれの遷移にｌｉを取得させる／解放させ、ｍｉを１／０にセットすることによって、Ｖを非相互作用ＰＤＳに変換することができる。しかし、ロックを除去することは、Ｕ２において互いに排他的であったコントロール状態を、Ｖ２において同時に到達可能にする。形式ＥｇのＬ（Ｇ）プロパティについてモデルチェックしている間に、ロックセマンティックを回復するために、代わりに、修正Ｌ（Ｇ）プロパティＥ（ｇ∧ｇ’）をチェックする。ここで、
【０２９５】
【数１０１】
2010506309.tif 000103
【０２９６】
は、大域状態ｓにおいて真であることを評価する原子命題
【０２９７】
【数１０２】
2010506309.tif 000104
【０２９８】
を有し、局所コントロール状態
【０２９９】
【数１０３】
2010506309.tif 000105
【０３００】
においてプロセスＶｊがｓにある場合、
【０３０１】
【数１０４】
2010506309.tif 000106
【０３０２】
である。Ｖ１およびＶ２のコントロール状態において、それぞれのｉについて、ロックｌｉに相当するｍｉエントリが、Ｖ［１］とＶ［２］の両方について、同時に１であることができないことを、ｇ’が保証する、すなわち、Ｕ［１］とＵ［２］は共に、同じロックｌｉを保持することができないことに留意されたい。そして、問題は、決定可能であることがわかっているＬ（Ｇ）式について、２つの非相互作用ＰＤＳをモデルチェックすることに帰着する。これは、Ｌ（Ｇ）についてのＰＭＣＰが、非入れ子ロックによって相互作用するＰＤＳについて効率的に決定可能であることを与える。
【０３０３】
ブロードキャスト：ブロードキャストによって通信するＰＤＳについてのＰＭＣＰを考える。ここで、
【０３０４】
【数１０５】
2010506309.tif 000107
【０３０５】
、Ｕのアクションシンボルの集合は、それぞれ、内部遷移ラベルの集合
【０３０６】
【数１０６】
2010506309.tif 000108
【０３０７】
、ならびに、ｓｅｎｄおよびｒｅｃｅｉｖｅブロードキャスト遷移の集合
【０３０８】
【数１０７】
2010506309.tif 000109
【０３０９】
を含む。非同期ランデブーのように、有効にされるブロードキャストｓｅｎｄ遷移は、常に発火されることができる。ブロードキャストｒｅｃｅｉｖｅ遷移は、有効にされた整合ブロードキャストｓｅｎｄ遷移が存在する場合に発火されることができるだけである。ブロードキャストｓｅｎｄ遷移を実行することは、整合ｒｅｃｅｉｖｅを有する１つだけでなく全ての他のプロセスが発火することを強制する点で、ブロードキャストは、非同期ランデブーと異なる。ブロードキャストによって相互作用するＰＤＳの場合、対到達可能性についてのＰＭＣＰ、すなわち、ＥＦ（ｃ１∧ｃ２）は、決定不可能であることが示されることができる。そして、Ｌ（Ｆ）についての決定不可能性結果は、即時の系としてもたらされる。Ｌ（Ｆ）についてのＰＭＣＰは、ブロードキャストによって相互作用するＰＤＳについて決定不可能である。
【０３１０】
時相プロパティの幅広いクラス用の標準的な同期プリミティブのそれぞれによって相互作用するＰＤＳについてのＰＭＣＰを考える。具体的に、２重インデックスＬＴＬ用の標準的な同期プリミティブのそれぞれによって相互作用するＰＤＳについてのＰＭＣＰの決定可能性境界を記述した。対象となる多くの重要な場合に、ＰＭＣＰは、標準的なモデルチェッキング問題に比べて扱い易いことも実証した。新しい結果の実用的な意味は、Ｌｉｎｕｘ（登録商標）デバイスドライバのような多くのアプリケーションにおいて、標準的なモデルチェッキング問題よりもＰＭＣＰを考えることがより有用である可能性があることである。
【０３１１】
パラメータ化された並行ソフトウェアのプロシジャ間データフロー解析のためのシステムおよび方法の好ましい実施形態（例証的であり、制限的でないことが意図される）を述べたが、上記教示に照らして、修正および変形が、当業者によって行われることができることが留意される。したがって、開示された特定の実施形態において、添付特許請求の範囲によって概説される本発明の範囲および精神内にある変更が行われてもよいことが理解される。特許法によって要求される詳細および特殊性と共に、本発明の態様を述べたが、特許状によって保護される、請求され、所望されることは、添付特許請求の範囲において述べられる。
関連出願情報
本出願は、参照により本明細書に組み込まれる２００７年１月９日に出願された仮出願第６０／８８４，０４８号に対する優先権を主張する。本出願はまた、参照により本明細書に組み込まれる２００６年１０月５日に出願された仮出願第６０／８２８，２４６号に対する優先権も主張する。
【０３１２】
本出願は、「ＭＯＤＥＬ  ＣＨＥＣＫＩＮＧ  ＰＡＲＡＭＥＴＥＲＩＺＥＤ  ＴＨＲＥＡＤＳ  ＦＯＲ  ＳＡＦＥＴＹ」という名称の前記出願と同時出願された米国出願番号（未定）（代理人書類番号第０６０４９（４４９−４）号）に関連し、参照により本明細書に組み込まれる。
【図面の簡単な説明】
【０３１３】
【図１】図１は、例証的な実施形態による、並行プログラムにおけるデータフロー計算を解決するシステム／方法を示すブロック図／フロー図である。
【図２】図２は、コントロール状態ｃを有するテンプレートプロセスＵ、および、本発明の原理による動作を示すための！および？による遷移指定を示す図である。
【図３】図３は、数回の反復による進行を示す本発明の原理による固定点計算を示す図である。
【図１】
2010506309.tif 000110
【図２】
2010506309.tif 000111
【図３】
2010506309.tif 000112
【手続補正書】
【提出日】平成21年7月15日(2009.7.15)
【手続補正１】
【補正対象書類名】特許請求の範囲
【補正対象項目名】請求項１４
【補正方法】変更
【補正の内容】
【請求項１４】
ｆは、２重インデックスＬＴＬ式である請求項１０に記載の方法。
【国際調査報告】
2010506309.tif 000113
2010506309.tif 000114