部分順序削減

コンピュータサイエンスにおいて、部分順序削減とは、モデル検査や自動計画・スケジューリングアルゴリズムによって探索される状態空間のサイズを削減するための手法である。これは、異なる順序で実行されても同じ状態になる、並行して実行される遷移の可換性を利用する。

明示的な状態空間探索では、部分順序削減は通常、有効なすべての遷移の代表部分集合を拡張する特定の手法を指します。この手法は、代表者によるモデル検査としても説明されています。^{[ 1 ]}この手法には、いわゆる頑固セット法^{[ 2 ]}、十分なセット法^{[ 1 ]} 、および永続セット法^{[ 3 ]など、さまざまなバージョンがあります。}

豊富集合は、代表者を用いたモデル検査の一例です。その定式化は、依存性という独自の概念に基づいています。2つの遷移は、互いに有効になっているときに他方を無効にできない場合にのみ独立しているとみなされます。両方の遷移を実行すると、実行順序に関係なく、一意の状態になります。独立していない遷移は、依存しています。実際には、依存性は静的解析を用いて近似されます。

さまざまな目的のための十分な集合は、ある状態において遷移の集合が「十分」である条件を与えることによって定義できる。

C0${\displaystyle {ample(s)=\varnothing }\iff {enabled(s)=\varnothing }}$

C1遷移の場合${\displaystyle \alpha }$遷移関係に依存する${\displaystyle アンプル(s)}$この遷移は、十分集合内のいずれかの遷移が実行されるまで呼び出すことはできません。

条件C0とC1は、状態空間におけるすべてのデッドロックを維持するのに十分である。より微妙な特性を維持するには、さらなる制約が必要である。例えば、線形時相論理の特性を維持するには、次の2つの条件が必要である。

C2もし${\displaystyle enabled(s)\neq ample(s)}$十分集合内の各遷移は不可視である。

C3遷移を含む状態が存在する場合、サイクルは許可されません${\displaystyle \alpha }$ は有効になっていますが、サイクル上のどの状態 s に対しても、アンプルには含まれません。

これらの条件は十分な集合の条件ではあるが、必要条件ではない。^{[ 4 ]}

頑固な集合は、明示的な独立関係を利用しません。代わりに、アクションのシーケンスに対する可換性のみによって定義されます。${\displaystyle T(s)}$以下の条件が満たされる場合、s は（弱く）頑固である。

D0${\displaystyle \forall a\in T(s)\forall b_{1},...,b_{n}\notin T(s)}$シーケンスの実行${\displaystyle b_{1},...,b_{n},a}$可能であり、状態につながる${\displaystyle s'}$続いてシーケンスの実行${\displaystyle a,b_{1},...,b_{n}}$可能であり、州につながる${\displaystyle s'}$。

D1どちらか${\displaystyle s}$デッドロック、または${\displaystyle \exists a\in T(s)}$そのため${\displaystyle \forall b_{1},...,b_{n}\notin T(s)}$実行${\displaystyle b_{1},...,b_{n},a}$可能です。

これらの条件は、アンプリルセット法におけるC0とC1と同様に、すべてのデッドロックを保持するのに十分です。ただし、これらの条件はやや弱く、結果としてより小さなセットになる可能性があります。条件C2とC3もアンプリルセット法における条件よりもさらに弱くすることができますが、スタボーンセット法はC2とC3と互換性があります。

部分順序削減のための他の表記法も存在する。よく使われるものの1つは、パーシステントセット/スリープセットアルゴリズムである。詳細については、パトリス・ゴデフロワの論文を参照されたい。^{[ 3 ]}

記号モデル検査では、制約条件を追加することで（ガード強化によって）、部分順序削減を実現できる。部分順序削減のさらなる応用例としては、自動計画が挙げられる。

• クラーク、エドモンド M. ;グランバーグ、オルナ;ペレド、ドロン A. (1999).モデル検査. MIT Press.
• Flanagan, Cormac; Godefroid, Patrice (2005). "ソフトウェアのモデル検査のための動的部分順序削減" . POPL '05、第32回ACMプログラミング言語原理シンポジウム議事録. pp. 110–121 . 
• Godefroid, Patrice (1994).並行システムの検証のための部分順序法 ― 状態爆発問題へのアプローチ(PostScript) (博士論文). リエージュ大学、コンピュータサイエンス学科。
• Holzmann, Gerard J (1993).スピンモデルチェッカー：入門とリファレンスマニュアル. Addison-Wesley. ISBN 978-0-321-22862-8。
• Peled, Doron A. (1993). "All from One, One for All: Model Checking Using Representatives". Proceedings of CAV '93, LNCS 697, Springer 1993. pp. 409–423 . doi : 10.1007/3-540-56922-7_34 . 
• Valmari, Antti ( 1990). 「状態空間縮小生成のための頑固なセット」。Advances in Petri Nets 1990、LNCS 483、Springer 1991。pp. 491–515。doi : 10.1007 /3-540-53863-1_36。