クロック（モデルチェック）

コンピュータサイエンスの一分野であるモデル検査において、時計は時間をモデル化するために用いられる数学的オブジェクトである。より正確には、時計は特定のイベントが発生してからどれだけの時間が経過したかを測定するものであり、この意味では、時計はストップウォッチをより抽象化したものである。ある特定のプログラムのモデルでは、時計の値はプログラムが開始されてからの経過時間か、プログラム内で特定のイベントが発生してからの経過時間のいずれかである。これらの時計は、時間オートマトン、シグナルオートマトン、時間命題時相論理、クロック時相論理の定義に用いられる。また、時間オートマトンを実装するUPPAALなどのプログラムでも用いられる。 ^[1]

一般的に、システムのモデルでは多くのクロックが使用されます。限られた数のイベントを追跡するには、複数のクロックが必要です。これらのクロックはすべて同期されています。つまり、2 つの固定クロック間の値の差は、どちらかが再起動されるまで一定です。電子工学の用語で言えば、クロックのジッターがゼロであることを意味します。

10 階建ての建物にあるエレベーターをモデル化するとします。モデルにはクロックがあり、クロックの値は階 で誰かがエレベーターを待った時間になります。このクロックは、誰かが 階 でエレベーターを呼んだときに開始されます(そして、エレベーターは前回その階を訪れてからこの階でまだ呼ばれていません)。このクロックは、エレベーターが 階 に到着したときにオフにすることができます。この例では、10 個の独立したイベントを追跡する必要があるため、実際には 10 個の異なるクロックが必要です。別のクロックを使用して、エレベーターが特定の階で過ごした時間をチェックすることもできます。 ${\displaystyle n}$${\displaystyle c_{0},\dots ,c_{9}}$${\displaystyle c_{i}}$${\displaystyle i}$${\displaystyle i}$${\displaystyle i}$${\displaystyle s}$

このエレベーターのモデルは、これらのクロックを使用して、エレベーターのプログラムが「エレベーターが 1 階に 15 秒以上停車しないと仮定すると、誰も 3 分以上エレベーターを待つ必要はありません」などの特性を満たしているかどうかを判断できます。このステートメントが成り立つかどうかを確認するには、クロックが常に 15 秒未満であるモデルの実行ごとに、各クロックが 3 分に達する前にオフになっていることを確認するだけで十分です。 ${\displaystyle s}$${\displaystyle c_{i}}$

形式的には、クロックの集合は単なる有限集合である^{[1] : 191}。クロックの集合の各要素はクロックと呼ばれる。直感的には、クロックは一階述語論理の変数に似ており、論理式で使用できる要素であり、さまざまな値を取ることができる。 ${\displaystyle X}$

クロック評価またはクロック解釈^{[1] :193} は、通常、から非負の実数の集合への関数として定義されます。同様に、評価は内の点として考えることができます。 ${\displaystyle \nu}$${\displaystyle X=\{x_{1},\dots ,x_{n}\}}$${\displaystyle X}$${\displaystyle \mathbb {R} _{\geq 0}^{n}}$

初期割り当ては 、各クロックを 0 に送信する定数関数です。直感的には、各クロックが同時に初期化されるプログラムの初期時間を表します。 ${\displaystyle \nu_{0}}$

クロック割り当てと実数が与えられた場合、は各クロックを に送信するクロック割り当てを表します。直感的には、これは時間単位が経過した 後の評価を表します。${\displaystyle \nu}$${\displaystyle t\geq 0}$${\displaystyle \nu +t}$${\displaystyle x\in C}$${\displaystyle \nu (x)+t}$${\displaystyle \nu}$${\displaystyle t}$

クロックのサブセットが与えられた場合、は のクロックがリセットされると同様の割り当てを表します。 正式には、は各クロックを0 に送り、各クロックを に送ります。 ${\displaystyle r\subseteq C}$${\displaystyle \nu [r\rightarrow 0]}$${\displaystyle \nu}$${\displaystyle r}$${\displaystyle \nu [r\rightarrow 0]}$${\displaystyle x\in r}$${\displaystyle x\not \in r}$${\displaystyle \nu (x)}$

プログラムUPPAALは非アクティブクロックの概念を導入します。^[2]クロックは、リセットされることなくクロックの値がチェックされる可能性のある未来が存在しない場合に、ある時点で非アクティブになります。上記の例では、エレベータがフロア に到着するとクロックは非アクティブであるとみなされ、誰かがフロア でエレベータを呼び出すまで非アクティブのままになります。 ${\displaystyle c_{i}}$${\displaystyle i}$${\displaystyle i}$

非アクティブなクロックを許可する場合、評価によってクロックが非アクティブであることを示す特別な値に関連付けられることがあります。の場合、も に等しくなります。 ${\displaystyle x}$${\displaystyle \bot}$${\displaystyle \nu (x)=\bot }$${\displaystyle (\nu +t)(x)}$${\displaystyle \bot}$

原子時計制約は、単に という形式の項です。ここでは時計、は比較演算子 (<、≤、=、≥、> など)、 は積分定数です。前の例では、原子時計制約を使用して、階にいる人の待機時間が 3 分未満であること、およびエレベータがある階に 15 秒以上留まっていたことを記述できます。評価は、 の場合にのみ原子時計評価を満たします。 ${\displaystyle x\simc}$${\displaystyle x}$${\displaystyle \sim}$${\displaystyle c\in \mathbb {N} }$${\displaystyle c_{i}\leq 180}$${\displaystyle i}$${\displaystyle s>15}$${\displaystyle \nu}$${\displaystyle x\simc}$${\displaystyle \nu (x)\sim c}$

クロック制約は、原子時計制約の有限結合か、定数「true」（空の結合と見なすことができます）のいずれかです。評価は、各原子時計制約を満たす場合、クロック制約を満たします。 ${\displaystyle \nu}$${\displaystyle \bigwedge_{i=1}^{n}x_{i}\sim_{i}c_{i}}$${\displaystyle x_{i}\sim _{i}c_{i}}$

コンテキストに応じて、原子時計制約は という形式になることもあります。このような制約は、が の対角線を定義するため、対角制約と呼ばれます。 ${\displaystyle x_{i}\sim x_{j}+c}$${\displaystyle x_{1}=x_{2}+c}$${\displaystyle \mathbb {R} _{\geq 0}^{2}}$

対角制約を許可すると、システムを記述するために使用される式またはオートマトンのサイズを縮小できる場合があります。ただし、対角制約を許可すると、アルゴリズムの複雑さが増す可能性があります。クロックを使用するほとんどのシステムでは、対角制約を許可してもロジックの表現力は向上しません。ここでは、ブール変数と非対角制約を使用してこのような制約をエンコードする方法について説明します。

対角制約は、次のように非対角制約を使用してシミュレートできます。がリセットされると、が成り立つかどうかを確認します。 この情報をブール変数で呼び出し、この変数に置き換えます。 がリセットされると、が < または ≤ の場合、またはが = かつの場合はtrue に設定されます。 ${\displaystyle x_{i}\sim x_{j}+c}$${\displaystyle x_{j}}$${\displaystyle x_{i}\sim c}$${\displaystyle b_{i,j,c}}$${\displaystyle x_{i}\sim x_{j}+c}$${\displaystyle x_{i}}$${\displaystyle b_{i,j,c}}$${\displaystyle \sim}$${\displaystyle \sim}$${\displaystyle c=0}$

ブール変数をエンコードする方法は、クロックを使用するシステムによって異なります。たとえば、UPPAAL はブール変数を直接サポートします。時間指定オートマトンとシグナルオートマトンでは、その場所にブール値をエンコードできます。時間指定ワード上のクロック時相論理では、ブール変数は新しいクロックを使用してエンコードされる場合があります。このクロックの値は、 が偽の場合に限り 0 になります。つまり、が偽であると考えられる限り、 はリセットされます。時間指定命題時相論理では、 を再開してから を評価する式 は、式 に置き換えることができます。ここで、と は式 のコピーであり、 はそれぞれ true と false の定数に置き換えられます。 ${\displaystyle x_{i,j,c}}$${\displaystyle b_{i,j,c}}$${\displaystyle x_{i,j,c}}$${\displaystyle x_{i,j,c}}$${\displaystyle x_{i}.\phi }$${\displaystyle x_{i}}$${\displaystyle \phi}$${\displaystyle x_{i}.((x_{i}\sim x_{j}+c\implies \phi _{\top })\land (\neg x_{i}\sim x_{j}+c\implies \phi \bot ))}$${\displaystyle \phi _{\top}}$${\displaystyle \phi _{\bot}}$${\displaystyle \phi}$${\displaystyle x_{i}\sim x_{j}+c}$

クロック制約は評価のセットを定義します。文献では、このようなセットの 2 種類が検討されています。

ゾーンは、クロック制約を満たす空でない評価の集合です。ゾーンとクロック制約は、差分境界行列を使用して実装されます。

モデル が与えられた場合 、そのクロック制約では有限個の定数が使用されます。が使用される最大の定数であるとします。領域は、より大きい制約が使用されていない空でないゾーンであり、さらに、包含に対して最小です。 ${\displaystyle M}$${\displaystyle K}$${\displaystyle K}$

• 時間制限付きオートマトン
• 信号オートマトン
• クロック時相論理
• 時間制限付き命題時相論理