差境界行列

コンピュータサイエンスの一分野であるモデル検査において、差分境界行列 (DBM)は、ゾーンと呼ばれる凸多面体を表すために使用されるデータ構造です。この構造は、空、包含、等価性のテストや、2つのゾーンの交差と和の計算など、ゾーンに対するいくつかの幾何学的操作を効率的に実装するために使用できます。たとえば、Uppaal モデルチェッカーで使用されており、独立したライブラリとしても配布されています。^[1]

より正確には、標準 DBM の概念があります。標準 DBM とゾーンの間には 1 対 1 の関係があり、各 DBM から標準の同等の DBM を効率的に計算できます。したがって、ゾーンの等価性は、標準 DBM の等価性をチェックすることによってテストできます。

差分境界行列は、ある種の凸多面体を表すために使用されます。これらの多面体はゾーンと呼ばれます。これらは定義されています。正式には、ゾーンは、、、および という形式の方程式によって定義され、いくつかの変数と定数を持ちます。 ${\displaystyle x\leq c}$${\displaystyle x\geq c}$${\displaystyle x_{1}\leq x_{2}+c}$${\displaystyle x_{1}\geq x_{2}+c}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle c}$

ゾーンはもともと領域と呼ばれていましたが[ ^2]、現在ではこの名前は通常、特別な種類のゾーンである領域を表します。直感的には、領域は制約で使用される定数が制限される、空でない最小限のゾーンと考えることができます。

変数が与えられると、1 つの変数と上限を使用する制約 、 1 つの変数と下限を使用する制約 、および変数 の順序付きペアのそれぞれに対して の上限 という、まったく異なる非冗長制約が考えられます。ただし、 の任意の凸多面体では、任意の数の制約が必要になる場合があります。 の場合でも、一部の定数に対して、任意の数の非冗長制約 が存在する可能性があります。これが、DBM をゾーンから凸多面体に拡張できない理由です。 ${\displaystyle n}$${\displaystyle n(n+1)}$${\displaystyle n}$${\displaystyle n}$${\displaystyle n^{2}}$${\displaystyle (x,y)}$${\displaystyle x-y}$${\displaystyle \mathbb {R} ^{n}}$${\displaystyle n=2}$${\displaystyle (x<iy+c_{i})_{i\in \mathbb {N} }}$${\displaystyle c_{i}}$

はじめに述べたように、、、およびという形式のステートメントの集合によって定義されるゾーンを考えます。このステートメントには、いくつかの変数と定数が含まれます。ただし、これらの制約の一部は矛盾しているか冗長です。ここでは、そのような例を示します。 ${\displaystyle x_{1}\leq c}$${\displaystyle x_{1}\geq c}$${\displaystyle x_{1}\leq x_{2}+c}$${\displaystyle x_{1}\geq x_{2}+c}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle c}$

• 制約と は矛盾しています。したがって、このような制約が 2 つ見つかった場合、定義されたゾーンは空になります。${\displaystyle x_{1}\leq 3}$${\displaystyle x_{1}\geq 4}$

  

• 制約と は冗長です。2 番目の制約は最初の制約によって暗黙的に指定されます。したがって、ゾーンの定義にこのような制約が 2 つ見つかった場合、2 番目の制約は削除できます。${\displaystyle x_{1}\leq 3}$${\displaystyle x_{1}\leq 4}$

  

また、既存の制約から新しい制約を生成する方法を示す例も示します。 と の各クロックのペアに対して、DBM には という形式の制約があり、 は< または ≤ のいずれかです。 このような制約が見つからない場合は、一般性を失うことなく制約をゾーン定義に追加できます。 ただし、場合によっては、より正確な制約が見つかることがあります。 ここでは、そのような例を示します。 ${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle x_{1}\prec x_{2}+c}$${\displaystyle \prec }$${\displaystyle x_{1}\prec x_{2}+\infty }$

• 制約 は、を意味します。したがって、 や などの他の制約が定義に属していないと仮定すると、制約 がゾーン定義に追加されます。${\displaystyle x_{1}\leq 3}$${\displaystyle x_{2}\geq -3}$${\displaystyle x_{1}\leq x_{2}+6}$${\displaystyle x_{1}\leq x_{2}+5}$${\displaystyle x_{1}<x_{2}+6}$${\displaystyle x_{1}\leq x_{2}+6}$

  

• 制約 は、を意味します。したがって、 や などの他の制約が定義に属していないと仮定すると、制約 がゾーン定義に追加されます。${\displaystyle x_{2}\leq 3}$${\displaystyle x_{1}\leq x_{2}+3}$${\displaystyle x_{1}\leq 6}$${\displaystyle x_{1}\leq 5}$${\displaystyle x_{1}<6}$${\displaystyle x_{1}\leq 6}$

  

• 制約 は、を意味します。したがって、 や などの他の制約が定義に属していないと仮定すると、制約 がゾーン定義に追加されます。${\displaystyle x_{1}\leq x_{2}+3}$${\displaystyle x_{2}\leq x_{3}+3}$${\displaystyle x_{1}\leq x_{3}+6}$${\displaystyle x_{1}\leq x_{3}+5}$${\displaystyle x_{1}<x_{3}+6}$${\displaystyle x_{1}\leq x_{3}+6}$

実際、上記の最初の 2 つのケースは、3 番目のケースの特殊なケースです。実際、およびはそれぞれ、およびと書き直すことができます。したがって、最初の例で追加された制約は、3 番目の例で追加された制約に似ています。 ${\displaystyle x_{1}\leq 3}$${\displaystyle x_{2}\geq -3}$${\displaystyle x_{1}\leq 0+3}$${\displaystyle 0\leq x_{2}+3}$${\displaystyle x_{1}\leq x_{2}+6}$

ここで、実数直線のサブセットであるモノイドを決定します。このモノイドは、伝統的に 整数、 有理数、実数、またはそれらの非負数のサブセット の集合です。${\displaystyle (M,0,+)}$

データ構造の差境界行列を定義するには、まず原子制約をエンコードするデータ構造を与える必要があります。さらに、原子制約の代数を導入します。この代数は熱帯半環に似ていますが、次の 2 つの変更が加えられています。

• の代わりに任意の順序付きモノイドを使用することもできます。${\displaystyle \mathbb {R} }$
• 「 」と「 」を区別するために、代数の要素の集合には、順序が厳密であるかどうかを示す情報が含まれている必要があります。${\displaystyle <m}$${\displaystyle \leq m}$

満足可能な制約の集合は、次の形式のペアの集合として定義されます。

• ${\displaystyle (\leq ,m)}$であり、これは という形式の制約を表す。${\displaystyle m\in M}$${\displaystyle \leq m}$
• ${\displaystyle (<,m)}$であり、 はの最小元ではなく、 という形式の制約を表す。${\displaystyle m\in M}$${\displaystyle m}$${\displaystyle M}$${\displaystyle <m}$
• ${\displaystyle (<,\infty )}$制約がないことを表します。

制約セットには、すべての満たせる制約が含まれており、次の満たせない制約も含まれています。

• ${\displaystyle (<,-\infty )}$。

この種の制約を使用してサブセットを定義することはできません。より一般的には、定義内の各制約が最大 2 つの変数を使用する場合でも、順序付きモノイドが最小上限プロパティを持たない場合、一部の凸多面体は定義できません。 ${\displaystyle \{q\in \mathbb {Q} \mid q\leq {\sqrt {2}}\}}$

同じ変数に適用された制約のペアから単一の制約を生成するために、制約の交差と制約の順序の概念を形式化します。同様に、既存の制約から新しい制約を定義するには、制約の合計の概念も定義する必要があります。

ここで、制約に対する順序関係を定義します。この順序は包含関係を表します。

まず、集合 は順序付き集合とみなされ、< は ≤ より劣っています。直感的に、 によって定義される集合はによって定義される集合に厳密に含まれるため、この順序が選択されます。次に 、または (かつより小さい)の場合、制約 はより小さいと 述べます。つまり、制約 の順序は、右から左に適用される辞書式順序です。この順序は全順序であることに注意してください。 に最小上限特性(または最大下限特性)がある場合、制約の集合にもそれがあります。 ${\displaystyle \{<,\leq \}}$${\displaystyle x<c}$${\displaystyle x\leq c}$${\displaystyle (\prec _{1},m_{1})}$${\displaystyle (\prec _{2},m_{2})}$${\displaystyle m_{1}<m_{2}}$${\displaystyle m_{1}=m_{2}}$${\displaystyle \prec _{1}}$${\displaystyle \prec _{2}}$${\displaystyle M}$

と表記される 2 つの制約の交差は、単に 2 つの制約の最小値として定義されます。 が最大下限プロパティを持つ場合、無限数の制約の交差も定義されます。 ${\displaystyle (\prec _{1},m_{1})\sqcap (\prec _{2},m_{2})}$${\displaystyle M}$

制約 および が適用されている2つの変数 および が与えられた場合、が満たす制約 を生成する方法を説明します。 この制約は、上記の 2 つの制約の合計と呼ばれ、 と表され、 と定義されます。 ${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle (\prec _{1},m_{1})}$${\displaystyle (\prec _{2},m_{2})}$${\displaystyle x_{1}+x_{2}}$${\displaystyle (\prec _{1},m_{1})+(\prec _{2},m_{2})}$${\displaystyle (\min(\prec _{1},\prec _{2}),m_{1}+m_{2})}$

以下は制約セットによって満たされる代数的特性のリストです。

• どちらの演算も結合的かつ交換的であり、
• 和は交差に対して分配的である。つまり、任意の3つの制約に対して、和は、${\displaystyle ((\prec _{1},m_{1})\sqcap (\prec _{2},m_{2}))+(\prec _{3},m_{3})}$${\displaystyle ((\prec _{1},m_{1})+(\prec _{3},m_{3}))\sqcap ((\prec _{2},m_{2})+(\prec _{3},m_{3}))}$
• 交差演算は冪等であり、
• 制約は交差演算の恒等式であり、${\displaystyle (<,\infty )}$
• 制約は和演算の恒等式であり、${\displaystyle (\leq ,0)}$

さらに、次の代数的性質は満足可能な制約に対して成り立ちます。

• 制約は合計演算ではゼロである。${\displaystyle (<,\infty )}$
• したがって、満足可能な制約の集合は、がゼロで が1 である冪等半環であることがわかります。${\displaystyle (<,\infty )}$${\displaystyle (\leq ,0)}$
• 0 が の最小要素である場合、充足可能な制約上の交差制約に対して はゼロになります。${\displaystyle M}$${\displaystyle (\leq ,0)}$

充足不可能な制約では、両方の演算は同じ零点、つまり を持ちます。したがって、共通部分の恒等式は和の零点とは異なるため、制約集合は半環を形成しません。 ${\displaystyle (<,-\infty )}$

変数の集合 が与えられると、DBM は によってインデックス付けされた列 と行 を持つ行列となり、エントリは制約となります。直感的には、列と行の場合、位置 の値はを表します。したがって、で表される行列 によって定義されるゾーンはです。 ${\displaystyle n}$${\displaystyle x_{1},\dots ,x_{n}}$${\displaystyle 0,x_{1},\dots ,x_{n}}$${\displaystyle C}$${\displaystyle R}$${\displaystyle m}$${\displaystyle (C,R)}$${\displaystyle C\prec R+m}$${\displaystyle D((\prec _{C,R},m_{C,R}))_{C,R\in \{0,x_{1},\dots ,x_{n}}\}}$${\displaystyle {\mathcal {R}}(D)}$${\displaystyle \{(x_{1},\dots ,x_{n})\in \mathbb {R} \mid \bigwedge _{C,R\in \{0,x_{1},\dots ,x_{n}\}}C\prec _{C,R}R+m_{C,R}\}}$

は と同等であることに注意してください。したがって、エントリは本質的には依然として上限です。ただし、モノイド を検討しているため、 および のいくつかの値に対して、実数は実際にはモノイドに属していないことに注意してください。 ${\displaystyle C\prec R+m}$${\displaystyle C-R\prec m}$${\displaystyle (\prec ,m)}$${\displaystyle M}$${\displaystyle C}$${\displaystyle R}$${\displaystyle C-R}$

標準的な DBM の定義を紹介する前に、それらの行列の順序関係を定義して議論する必要があります。

行列の各要素が より小さい場合、その行列は より小さいとみなされます。この順序は完全ではないことに注意してください。2 つの DBM と が与えられ、がより小さいか等しい場合、 となります。 ${\displaystyle D}$${\displaystyle D'}$${\displaystyle D}$${\displaystyle D'}$${\displaystyle D}$${\displaystyle D'}$${\displaystyle {\mathcal {R}}(D)\subseteq {\mathcal {R}}(D')}$

2 つの行列およびの最大下限はと表記され、そのエントリとして値 を持ちます。は制約の半環の「和」演算であるため、演算は2 つの DBM の「和」であり、DBM の集合はモジュールとみなされることに注意してください。 ${\displaystyle D}$${\displaystyle D'}$${\displaystyle D\sqcap D'}$${\displaystyle (a,b)}$${\displaystyle (\prec _{a,b},m_{a,b})\sqcap (\prec '_{a,b},m'_{a,b})}$${\displaystyle \sqcap }$${\displaystyle \sqcap }$

上記の「制約の操作」セクションで検討した制約の場合と同様に、最大下限プロパティを満たす とすぐに、無限の数の行列の最大下限が正しく定義されます。${\displaystyle M}$

行列/ゾーンの交差は定義されています。和集合演算は定義されておらず、実際、ゾーンの和集合は一般にゾーンではありません。

すべて同じゾーン を定義する任意の行列の集合に対して、も定義します。したがって、 が最大下限特性を持つ限り、少なくとも 1 つの行列によって定義される各ゾーンには、それを定義する一意の最小行列が存在します。この行列は の標準 DBM と呼ばれます。 ${\displaystyle {\mathcal {D}}}$${\displaystyle Z}$${\displaystyle \sqcap _{D\in {\mathcal {D}}}D}$${\displaystyle Z}$${\displaystyle M}$${\displaystyle Z}$

標準差分境界行列の定義を再度述べます。これは、より小さい行列が同じセットを定義しない DBM です。以下では、行列が DBM かどうかを確認する方法と、そうでない場合は両方の行列が同じセットを表すように任意の行列から DBM を計算する方法について説明します。ただし、最初にいくつか例を示します。

まず、時計が 1 つだけある場合を考えます。 ${\displaystyle x_{1}}$

まず、 の標準的な DBM を示します。次に、集合 をエンコードする別の DBM を導入します。これにより、任意の DBM が満たす必要がある制約を見つけることができます。 ${\displaystyle \mathbb {R} }$${\displaystyle \mathbb {R} }$

実数集合の標準的な DBM は です。これは制約、、および を表します。これらの制約はすべて、 に割り当てられた値とは関係なく満たされます。以降の説明では、 という形式のエントリによる制約は体系的に満たされるため、 明示的には説明しません。${\displaystyle \left({\begin{array}{ll}(\leq ,0)&(<,\infty )\\(<,\infty )&(\leq ,0)\end{array}}\right)}$${\displaystyle 0\leq 0+0}$${\displaystyle x_{1}\leq 0+\infty }$${\displaystyle 0\leq x_{1}+\infty }$${\displaystyle 0\leq 0+0}$${\displaystyle x_{1}}$${\displaystyle (<,\infty )}$

DBM は実数の集合もエンコードします。これには、の値とは独立に満たされる制約および が含まれます。これは、標準 DBM では対角要素が より大きくなることはないことを示しています。対角要素を で置き換えることによってから得られる行列は 同じ集合を定義し、 より小さくなるためです。 ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,\infty )\\(<,\infty )&(<,\infty )\end{array}}\right)}$${\displaystyle 0<0+\infty }$${\displaystyle x_{1}<x_{1}+\infty }$${\displaystyle x_{1}}$${\displaystyle D}$${\displaystyle (\leq ,0)}$${\displaystyle D}$${\displaystyle (\leq ,0)}$${\displaystyle D}$

ここで、空集合をエンコードする多くの行列について考えます。まず、空集合の標準的な DBM を示します。次に、各 DBM が空集合をエンコードする理由を説明します。これにより、どの DBM でも満たさなければならない制約を見つけることができます。

1 つの変数上の空集合の標準的な DBM は です。実際、これは制約、、および を満たす集合を表します。これらの制約は満たすことができません 。${\displaystyle \left({\begin{array}{ll}(<,-\infty )&(<,-\infty )\\(<,-\infty )&(<,-\infty )\end{array}}\right)}$${\displaystyle 0<0-\infty }$${\displaystyle 0<x_{1}-\infty }$${\displaystyle x_{1}<0-\infty }$${\displaystyle x_{1}<x_{1}-\infty }$

DBM は空集合もエンコードします。実際、空集合には満たされない制約が含まれています。より一般的には、すべてのエントリが でない限り、どのエントリも にならないことを示しています。 ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,-\infty )\\(<,\infty )&(<,\infty )\end{array}}\right)}$${\displaystyle x_{1}<0-\infty }$${\displaystyle (<,-\infty )}$${\displaystyle (<,-\infty )}$

DBM は空集合もエンコードします。実際、空集合には満たされない制約が含まれています。より一般的には、これは、 でない限り、対角線のエントリが より小さくなることはないことを示しています。 ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,\infty )\\(<,\infty )&(<,-1)\end{array}}\right)}$${\displaystyle x_{1}<x_{1}-1}$${\displaystyle (\leq ,0)}$${\displaystyle (<,-\infty )}$

DBM は空集合もエンコードします。実際、空集合には矛盾する制約と が含まれます。より一般的には、各 に対しての場合、 と は両方とも ≤ に等しいことが示されます。 ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(<,1)\\(\leq ,-1)&(<,\infty )\end{array}}\right)}$${\displaystyle 0<x_{1}+1}$${\displaystyle x_{1}\leq -1}$${\displaystyle C,R\in \{0,x_{1},\dots ,x_{n}\}}$${\displaystyle m_{C,R}=-m_{R,C}}$${\displaystyle \prec _{R,C}}$${\displaystyle \prec _{C,R}}$

DBM は空集合もエンコードします。実際、空集合には矛盾する制約と が含まれます。より一般的には、これは、でない限り、各に対して であることを示します。 ${\displaystyle \left({\begin{array}{ll}(<,\infty )&(\leq ,1)\\(\leq ,-2)&(<,\infty )\end{array}}\right)}$${\displaystyle 0\leq x_{1}+1}$${\displaystyle x_{1}\leq -2}$${\displaystyle C,R\in \{0,x_{1},\dots ,x_{n}\}}$${\displaystyle -m_{C,R}\leq m_{R,C}}$${\displaystyle m_{C,R}}$${\displaystyle -\infty }$

このセクションに示されている例は、上記の例のセクションに示されている例と似ています。今回は、DBM として示されています。

DBM は、制約および を満たすセットを表します。例のセクションで述べたように、これらの制約は両方とも を意味します。これは、DBMが同じゾーンをエンコードすることを意味します。実際、これはこのゾーンの DBM です。これは、任意の DBM で、各 に対して、制約 が制約 よりも小さいことを示しています。 ${\displaystyle \left({\begin{array}{lll}(\leq ,0)&(<,\infty )&(<,\infty )\\(<,\infty )&(\leq ,0)&(\leq ,3)\\(\leq ,3)&(<,\infty )&(\leq ,0)\end{array}}\right)}$${\displaystyle x_{2}\leq 3}$${\displaystyle x_{1}\leq x_{2}+3}$${\displaystyle x_{1}\leq 6}$${\displaystyle \left({\begin{array}{lll}(\leq ,0)&(\leq ,6)&(<,\infty )\\(<,\infty )&(\leq ,0)&(\leq ,3)\\(\leq ,3)&(<,\infty )&(\leq ,0)\end{array}}\right)}$${\displaystyle ((\prec _{C,R},m_{C,R}))_{c,r\in \{0,x_{1},\dots ,x_{n}\}}}$${\displaystyle 1\leq i,j\leq n}$${\displaystyle (\prec _{x_{i},0},m_{x_{i},0})}$${\displaystyle (\prec _{x_{j},0},m_{x_{j},0})+(\prec _{x_{i},x_{j}},m_{x_{i},x_{j}})}$

例のセクションで説明したように、定数 0 は任意の変数と見なすことができます。これにより、より一般的な規則が導かれます。任意の DBM では、各 に対して、制約 は制約 よりも小さくなります。 ${\displaystyle ((\prec _{C,R},m_{C,R}))_{c,r\in \{0,x_{1},\dots ,x_{n}\}}}$${\displaystyle a,b,c\in \{0,x_{1},\dots ,x_{n}\}}$${\displaystyle (\prec _{a,b},m_{a,b})}$${\displaystyle (\prec _{c,b},m_{c,b})+(\prec _{a,c},m_{a,c})}$

差分境界行列のセクションの冒頭で説明したように、標準 DBM は、行と列が でインデックス付けされ、エントリが制約である DBM です。さらに、次の同等の特性のいずれかに従います。 ${\displaystyle (0,x_{1},\dots ,x_{n})}$

• 同じゾーンを定義するより小さなDBMは存在しない。
• 各 に対して、制約は制約よりも小さい。${\displaystyle a,b,c\in \{0,x_{1},\dots ,x_{n}\}}$${\displaystyle (\prec _{a,b},m_{a,b})}$${\displaystyle (\prec _{c,b},m_{c,b})+(\prec _{a,c},m_{a,c})}$
• ラベルが付けられた辺と矢印を持つ有向グラフが ある場合、任意の辺から任意の辺への最短経路は矢印 です。このグラフはDBM のポテンシャル グラフと呼ばれます。${\displaystyle G}$${\displaystyle \{0,x_{1},\dots ,x_{n}\}}$${\displaystyle (a,b)}$${\displaystyle (\prec _{a,b},m_{a,b})}$${\displaystyle a}$${\displaystyle b}$${\displaystyle (a,b)}$

最後の定義は、DBM に関連付けられた標準 DBM を計算するために直接使用できます。グラフにFloyd-Warshall アルゴリズムを適用し、グラフ内のからへの最短パスを各エントリに関連付けるだけで十分です。このアルゴリズムが負の長さのサイクルを検出した場合、これは制約が満たされず、ゾーンが空であることを意味します。 ${\displaystyle (a,b)}$${\displaystyle a}$${\displaystyle b}$

はじめに述べたように、DBM の主な利点は、ゾーンに対する操作を簡単かつ効率的に実装できることです。

まず、上で検討した操作を思い出します。

• ゾーンがゾーンに含まれているかどうかのテストは、 の標準 DBM がの DBM 以下であるかどうかをテストすることによって行われます。${\displaystyle Z_{1}}$${\displaystyle Z_{2}}$${\displaystyle Z_{1}}$${\displaystyle Z_{2}}$
• ゾーンの集合の交差に対するDBMは、それらのゾーンのDBMの最大下限である。
• ゾーンの空性をテストするには、ゾーンの標準DBMが のみで構成されているかどうかを確認する必要があります 。${\displaystyle (<,-\infty )}$
• ゾーンが空間全体であるかどうかをテストするには、ゾーンの DBM が のみで構成されているかどうかを確認する必要があります 。${\displaystyle (<,\infty )}$

ここでは、上記で考慮しなかった操作について説明します。以下で説明する最初の操作には、明確な幾何学的意味があります。最後の操作は、クロック評価にとってより自然な操作に対応します。

2 つの DBM と によって定義される 2 つのゾーンのミンコフスキー和は、要素がであるDBM によって定義されます。は制約の半環の「積」演算であるため、DBM 上の演算は実際には DBM のモジュールの演算ではないこと に注意してください。 ${\displaystyle D}$${\displaystyle D'}$${\displaystyle D+D'}$${\displaystyle (a,b)}$${\displaystyle D_{a,b}+D'_{a,b}}$${\displaystyle +}$${\displaystyle +}$

特に、ゾーンを方向 で 変換するには、 の DBMを の DBM に追加するだけで十分であることがわかります。 ${\displaystyle Z}$${\displaystyle v}$${\displaystyle \{v\}}$${\displaystyle Z}$

定数 とします。${\displaystyle d\in M}$

ベクトルとインデックスが与えられた場合、の- 番目の要素 の への射影はベクトル です。クロックの言語では、 の場合、これは- 番目のクロックをリセットすることに相当します。 ${\displaystyle {\vec {x}}=(x_{1},\dots ,x_{n})}$${\displaystyle 1\leq i\leq n}$${\displaystyle i}$${\displaystyle {\vec {x}}}$${\displaystyle d}$${\displaystyle (x_{1},\dots ,x_{i-1},d,x_{i+1},\dots ,x_{n})}$${\displaystyle d=0}$${\displaystyle i}$

ゾーンの - 番目の成分を に投影することは、 - 番目の成分を とする のベクトルの集合に単純化されます。これは、成分を に設定し、成分を に設定することで DBM に実装されます。${\displaystyle i}$${\displaystyle Z}$${\displaystyle d}$${\displaystyle Z}$${\displaystyle i}$${\displaystyle d}$${\displaystyle (x_{i},a)}$${\displaystyle (\leq ,d)+D(0,a)}$${\displaystyle (a,x_{i})}$${\displaystyle (\leq ,-d)+D(0,a)}$

未来をゾーン、過去をゾーンと呼ぶことにします。点が与えられたとき、の未来はと定義され、の過去はと定義されます。 ${\displaystyle F=\{(t,\dots ,t)\mid t\in \mathbb {R} _{\geq 0}\}}$${\displaystyle P=\{(-t,\dots ,-t)\mid t\in \mathbb {R} _{\geq 0}\}}$${\displaystyle {\vec {x}}=(x_{1},\dots ,x_{n})\in \mathbb {R} ^{n}}$${\displaystyle {\vec {x}}}$${\displaystyle \{(x_{1}+t,\dots ,x_{n}+t)\mid t\in \mathbb {R} _{\geq 0}\}=F+\{{\vec {x}}\}}$${\displaystyle {\vec {x}}}$${\displaystyle P+\{{\vec {x}}\}}$

未来と過去という名前は、クロックの概念に由来しています。 、などの値にクロックのセットが割り当てられている場合、それらの将来において、それらに割り当てられたセットは の将来になります。 ${\displaystyle n}$${\displaystyle x_{1}}$${\displaystyle x_{2}}$${\displaystyle {\vec {x}}}$

ゾーン が与えられた場合、の未来はゾーンの各ポイントの未来の和になります。ゾーンの過去の定義も同様です。したがって、ゾーンの未来は と定義できるため、DBM の合計として簡単に実装できます。ただし、DBM に適用できるさらに簡単なアルゴリズムもあります。すべてのエントリを に変更するだけで十分です。同様に、ゾーンの過去は、すべてのエントリを に設定することで計算できます。 ${\displaystyle Z}$${\displaystyle Z}$${\displaystyle F+Z}$${\displaystyle (x_{i},0)}$${\displaystyle (<,\infty )}$${\displaystyle (0,x_{i})}$${\displaystyle (<,\infty )}$

• 領域（モデル検査） - 包含関係が最小で、いくつかの特性を満たす領域

• 差境界行列 上級モデル検査講義 #20 Joost-Pieter Katoen
• Péron, Mathias; Halbwachs, Nicolas (2008)。「不等式制約による差境界行列の抽象ドメイン拡張」(PDF)。検証、モデル検査、抽象解釈。コンピュータサイエンスの講義ノート。第 4349 巻。pp. 268–282。doi : 10.1007 / 978-3-540-69738-1_20。ISBN 978-3-540-69735-0。