領域（モデルチェック）

コンピュータサイエンスの一分野であるモデル検査において、領域とは、ある次元における凸多面体であり、より正確には、ある最小性特性を満たすゾーンです。領域は に分割されます。 ${\displaystyle \mathbb {R} ^{d}}$${\displaystyle d}$${\displaystyle \mathbb {R} ^{d}}$

ゾーンの集合は、、、および という形式の制約の集合に依存し、 およびいくつかの変数と定数があります。 領域は、2 つのベクトルと が同じ領域に属する場合、それらが の同じ制約を満たすように定義されます。 さらに、これらのベクトルをクロックの組と見なすと、両方のベクトルに同じ可能な未来の集合があります。 直感的には、これは、 の制約のみを使用する時間付き命題時相論理-式、または時間付きオートマトンやシグナル オートマトンでは、両方のベクトルを区別できないことを意味します。 ${\displaystyle K}$${\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}$${\displaystyle {\vec {x}}}$${\displaystyle {\vec {x}}'}$${\displaystyle K}$${\displaystyle K}$

領域の集合により、各ノードが領域である有向グラフである領域オートマトン を作成することができ、各エッジはが の可能な未来であることを保証する。この領域オートマトンと言語を受け入れる時間付きオートマトンの積を取ると、有限オートマトンまたは時間なし を受け入れるBüchi オートマトンが作成されます。特に、 の空の問題を有限または Büchi オートマトン の空の問題に簡略化することができます。この手法は、たとえばソフトウェアUPPAALで使用されています。^[1]${\displaystyle r\to r'}$${\displaystyle r'}$${\displaystyle r}$ ${\displaystyle {\mathcal {A}}}$${\displaystyle L}$ ${\displaystyle L}$${\displaystyle {\mathcal {A}}}$

時計の集合を とします。それぞれについてとします。直感的に、この数は時計を比較できる値の上限を表します。 の時計上の領域の定義には、これらの数 を使用します。これで、同等の定義が 3 つ与えられます。 ${\displaystyle C=\{x_{1},\dots ,x_{d}\}}$${\displaystyle x\in \mathbb {N} }$${\displaystyle c_{x}\in \mathbb {N} }$${\displaystyle x}$${\displaystyle C}$${\displaystyle c_{x}}$

クロック割り当て が与えられた場合、 は が属する領域を表します 。領域の集合は で表されます。 ${\displaystyle \nu }$${\displaystyle [\nu ]}$${\displaystyle \nu }$${\displaystyle {\mathcal {R}}}$

最初の定義により、2 つの割り当てが同じ領域に属しているかどうかを簡単にテストできます。

領域は、何らかの同値関係の同値類として定義されることがある。2つのクロック割り当てとが同等であるとは、次の制約を満たす場合である。^{[2] : 202}${\displaystyle \nu _{1}}$${\displaystyle \nu _{2}}$

• ${\displaystyle \nu _{1}(x)\sim c}$かつ整数それぞれに対して、かつ ~ が=、<、≤のいずれかの関係である場合に限ります。${\displaystyle \nu _{2}(x)\sim c}$${\displaystyle x\in C}$${\displaystyle 0\leq c\leq c_{x}}$
• ${\displaystyle \{\nu _{1}(x)\}\sim \{\nu _{1}(y)\}}$それぞれの に対して、、、は実数の小数部であり、 ~ は=、<、≤のいずれかの関係です。${\displaystyle \{\nu _{2}(x)\}\sim \{\nu _{2}(y)\}}$${\displaystyle x,y\in C}$${\displaystyle \nu _{1}(x)\leq c_{x}}$${\displaystyle \nu _{1}(y)\leq c_{y}}$${\displaystyle \{r\}}$${\displaystyle r}$

最初の種類の制約は、 と が同じ制約を満たすことを保証します。実際、 およびの場合、 2 番目の割り当てのみが を満たします。一方、およびの場合、制約では整数定数のみが使用されるため、両方の割り当てがまったく同じ制約セットを満たします。 ${\displaystyle \nu _{1}}$${\displaystyle \nu _{2}}$${\displaystyle \nu _{1}(x)=0.5}$${\displaystyle \nu _{2}(x)=1}$${\displaystyle x=1}$${\displaystyle \nu _{1}(x)=0.5}$${\displaystyle \nu _{2}(x)=0.6}$

2 番目の種類の制約は、2 つの割り当ての将来が同じ制約を満たすことを保証します。たとえば、letと です。すると、制約は最終的にクロック リセットなしの の将来によって満たされますが、クロック リセットなしの の将来では満たされません。 ${\displaystyle \nu _{1}=\{x\mapsto 0.5,y\mapsto 0.6\}}$${\displaystyle \nu _{2}=\{x\mapsto 0.5,y\mapsto 0.4\}}$${\displaystyle y=1\land x<1}$${\displaystyle \nu _{1}}$${\displaystyle \nu _{2}}$

前の定義では、2 つの割り当てが同じ領域に属しているかどうかをテストできますが、領域をデータ構造として簡単に表現することはできません。以下に示す 3 番目の定義では、領域の標準的なエンコードを指定できます。

領域は、次の制約を満たす 一連の方程式と不等式を使用して、ゾーンとして明示的に定義できます。${\displaystyle S}$

• 各 について、次のいずれかが含まれます。 ${\displaystyle x\in C}$${\displaystyle S}$
  • ${\displaystyle x=c}$ある整数に対して${\displaystyle 0\leq c\leq c_{x}}$
  • ${\displaystyle x\in (c,c+1)}$ある整数に対して、${\displaystyle 0\leq c<c_{x}}$
  • ${\displaystyle x>c_{x}}$、
• さらに、各時計のペアについて、および の形式の制約が含まれる場合、 が=、<、または≤のいずれかである形式の (不変の) 等式が含まれます 。${\displaystyle x,y\in C}$${\displaystyle S}$${\displaystyle x\in (c,c+1)}$${\displaystyle y\in (c',c'+1)}$${\displaystyle S}$${\displaystyle \{x\}\sim \{y\}}$${\displaystyle \sim }$

とが固定されている場合、最後の制約は と同等です。 ${\displaystyle c}$${\displaystyle c'}$${\displaystyle x\sim y+c-c'}$

この定義により、領域をデータ構造としてエンコードできます。各クロックについて、それがどの間隔に属するかを示し、長さ 1 の開間隔に属するクロックの小数部の順序を思い出すだけで十分です。したがって、この構造のサイズはクロックの数 に比例します。${\displaystyle O\left(\sum \log(c_{k})+|C|\log(|C|)\right)}$${\displaystyle |C|}$

ここで、領域の 3 番目の定義を示します。この定義はより抽象的ですが、モデル チェックで領域が使用される理由でもあります。直感的には、この定義は、2 つのクロック割り当ての違いが、どの時間オートマトンも気付かないほどである場合、それらの割り当ては同じ領域に属していると述べています。クロック割り当て で始まる実行が与えられた場合、同じ領域内の他の割り当てに対して、同じ場所を通過し、同じ文字を読み取る実行が存在します。唯一の違いは、2 つの連続する遷移間の待機時間が異なる可能性があることであり、したがって、連続するクロックの変化は異なります。 ${\displaystyle r}$${\displaystyle \nu }$${\displaystyle \nu '}$${\displaystyle r'}$

正式な定義が与えられました。 1 組のクロック、2 つの割り当て 、2 つのクロック割り当て、および が、ガードがより大きい数とクロックを決して比較しない各時間指定オートマトンについて、の任意の位置が与えられたときに、拡張状態との間に時間指定バイシミュレーションが存在する場合、同じ領域に属します。より正確には、このバイシミュレーションは文字と位置を保存しますが、正確なクロック割り当ては保存しません。^{[1] : 7}${\displaystyle C}$${\displaystyle \nu _{1}}$${\displaystyle \nu _{2}}$ ${\displaystyle {\mathcal {A}}}$${\displaystyle x}$${\displaystyle c_{x}}$${\displaystyle \ell }$${\displaystyle {\mathcal {A}}}$${\displaystyle (\ell ,\nu _{1})}$${\displaystyle (\ell ,\nu _{2})}$

いくつかの操作が領域に対して定義されるようになりました: クロックの一部をリセットし、時間を経過させます。

一連の (不) 方程式と一連の時計によって定義される領域が与えられた場合、の時計が再開される に類似した領域が定義されます。この領域は で表され、次の制約によって定義されます。 ${\displaystyle \alpha }$${\displaystyle S}$${\displaystyle C'\subseteq C}$${\displaystyle \alpha }$${\displaystyle C'}$${\displaystyle \alpha [C'\mapsto 0]}$

• 時計を含まないというそれぞれの制約、${\displaystyle S}$${\displaystyle x}$
• の制約。${\displaystyle x=0}$${\displaystyle x\in C'}$

によって定義される割り当ての集合は、の割り当ての集合とまったく同じです。 ${\displaystyle \alpha [C'\mapsto 0]}$${\displaystyle \nu [C'\mapsto 0]}$${\displaystyle \nu \in \alpha }$

領域 が与えられたとき、時計をリセットせずに到達できる領域は の時間後続領域と呼ばれます。ここで、2 つの同等の定義が与えられます。 ${\displaystyle \alpha }$${\displaystyle \alpha }$

各割り当て に対して、となる正の実数が存在する場合、クロック領域は別のクロック領域の時間的後続となります。 ${\displaystyle \alpha '}$${\displaystyle \alpha }$${\displaystyle \nu \in \alpha }$${\displaystyle t_{\nu ,\alpha '}>0}$${\displaystyle \nu +t_{\nu ,\alpha '}\in \alpha '}$

これは を意味するわけではないことに注意してください。たとえば、制約 のセットによって定義される領域には、制約 のセットによって定義される時間後続領域があります。実際、各 に対して、 を取れば十分です。ただし、となる実数や となる実数は存在しません。実際、は三角形を定義し、 は線分を定義します。 ${\displaystyle \alpha +t_{\nu ,\alpha '}=\alpha '}$${\displaystyle \alpha }$${\displaystyle \{0<x<1,0<y<1,x<y\}}$${\displaystyle \alpha '}$${\displaystyle \{0<x<1,y=1\}}$${\displaystyle \nu \in \alpha }$${\displaystyle t_{\nu ,\alpha '}=1-\nu (y)}$${\displaystyle t}$${\displaystyle \alpha +t=\alpha '}$${\displaystyle \alpha +t\subseteq \alpha '}$${\displaystyle \alpha }$${\displaystyle \alpha '}$

ここで与えられた 2 番目の定義により、制約セットによって指定された領域の時間後続セットを明示的に計算できるようになります。

制約 のセットとして定義された領域が与えられた場合、その時間後続のセットを定義しましょう。そのためには、次の変数が必要です。 の制約のセットが形式であるとします。制約 を含むような時計のセットがあるとします。に形式の制約が存在しないような時計のセットがあるとします。 ${\displaystyle \alpha }$${\displaystyle S}$${\displaystyle T\subseteq S}$${\displaystyle S}$${\displaystyle x_{i}=c_{i}}$${\displaystyle Y\subseteq C}$${\displaystyle y}$${\displaystyle S}$${\displaystyle y>c_{y}}$${\displaystyle Z\subseteq C\setminus Y}$${\displaystyle \{z\}}$${\displaystyle \{x\}<\{z\}}$${\displaystyle S}$

が空の場合、はそれ自身の時間後続です。 の場合、 はの唯一の時間後続です。 それ以外の場合、と等しくないの最小の時間後続が存在します。が空でない 場合、最小の時間後続には以下が含まれます。${\displaystyle T}$${\displaystyle \alpha }$${\displaystyle Y=C}$${\displaystyle \alpha }$${\displaystyle \alpha }$${\displaystyle \alpha }$${\displaystyle \alpha }$${\displaystyle T}$

• の制約${\displaystyle S\setminus T}$
• ${\displaystyle x_{i}>c_{i}}$、
• ${\displaystyle \{x_{i}\}=\{x_{j}\}}$、 そして
• がに属さない各 に対して、制約。${\displaystyle y}$${\displaystyle y>c_{y}}$${\displaystyle S}$${\displaystyle x_{i}<y}$

が空の場合、最小の時間後継者は次の制約によって定義されます。 ${\displaystyle T}$

• のクロックを使用しないという制約、${\displaystyle S}$${\displaystyle Z}$
• 制約、内の各制約について、。${\displaystyle z=c+1}$${\displaystyle c<z<c+1}$${\displaystyle S}$${\displaystyle z\in Z}$

領域は最大で 個あり、その数は時計の数である。^{[2] : 203}${\displaystyle |C|!2^{|C|}\prod _{x\in C}(2c_{x}+2)}$${\displaystyle |C|}$

時間付きオートマトン が与えられた場合、その領域オートマトンは有限オートマトン、または時間なしを受け入れるBüchi オートマトンです。このオートマトン は に似ていますが、クロックが領域 に置き換えられています。直感的には、領域オートマトン は領域グラフ と の 積として構築されます。この領域グラフが最初に定義されます。${\displaystyle {\mathcal {A}}}$ ${\displaystyle L}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}}$

領域グラフは、タイムドオートマトンの実行中に可能なクロック値のセットをモデル化するルート付き有向グラフです。次のように定義されます。

• そのノードは地域であり、
• そのルートは、制約の集合によって定義される初期領域であり、${\displaystyle \alpha _{0}}$${\displaystyle \{x=0\mid x\in C\}}$
• エッジの集合は、の時間後続に対して です。${\displaystyle (\alpha ,\alpha '[C'\mapsto 0])}$${\displaystyle \alpha '}$${\displaystyle \alpha }$

時間付きオートマトンとします。各クロック に対して、内に の形式のガードが存在するような最大の数をとします。で示される の領域オートマトンは、本質的には と 上記で定義した領域グラフ の積である有限オートマトンまたは Büchi オートマトンです。つまり、領域オートマトンの各状態は、 の場所と領域を含むペアです。同じ領域に属する 2 つのクロックの割り当ては同じガードを満たすため、各領域には、どの遷移を実行できるかを決定するのに十分な情報が含まれています。 ${\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle }$${\displaystyle x\in C}$${\displaystyle c_{x}}$${\displaystyle c}$${\displaystyle x\sim c}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}}$${\displaystyle R({\mathcal {A}})}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}}$

正式には、領域オートマトンは次のとおり定義されます。

• そのアルファベットは、${\displaystyle \Sigma }$
• その状態の集合は、${\displaystyle L\times {\mathcal {R}}}$
• その状態集合は初期領域と同じであり、${\displaystyle L_{0}\times \{\alpha _{0}\}}$${\displaystyle \alpha _{0}}$
• その受理状態の集合は、${\displaystyle F\times {\mathcal {R}}}$
• その遷移関係には、 に対してが含まれており 、 はの時間後続子です。${\displaystyle \delta }$${\displaystyle ((\ell ,\alpha ),a,(\ell ',\alpha '[C'\mapsto 0]))}$${\displaystyle (\ell ,a,g,C',\ell ')\in E}$${\displaystyle \gamma \models \alpha '}$${\displaystyle \alpha '}$${\displaystyle \alpha }$

の任意の連続 が与えられた場合、シーケンスはと表記され、 の連続 であり、 がを受け入れる場合と同値である^{[2] : 207}。したがって、 が成り立ちます。特に、がタイムドワードを受け入れる場合と同値である。さらに、 の受け入れ連続はの受け入れ連続から計算できます。 ${\displaystyle r=(\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots }$${\displaystyle {\mathcal {A}}}$${\displaystyle (\ell _{0},[\nu _{0}]){\xrightarrow {\sigma _{1}}}(\ell _{1},[\nu _{1}])\dots }$${\displaystyle [r]}$${\displaystyle R({\mathcal {A}})}$${\displaystyle r}$${\displaystyle L(R({\mathcal {A}}))=\operatorname {Untime} (L({\mathcal {A}}))}$${\displaystyle {\mathcal {A}}}$${\displaystyle R({\mathcal {A}})}$${\displaystyle {\mathcal {A}}}$${\displaystyle R({\mathcal {A}})}$