シグナル（モデルチェック）

コンピュータサイエンスの分野であるモデル検査において、信号または時間指定の状態シーケンスは、文字が連続的に出力される形式言語における単語の概念の拡張です。単語は伝統的に、非負の整数の集合から文字への関数として定義されますが、信号は実数の集合から文字への関数です。これにより、オートマトン理論に似た形式を使用して連続信号を扱うことができます。

エレベーターについて考えてみましょう。正式には文字と呼ばれているものは、実際には「誰かが 2 階のボタンを押しています」や「現在 3 階のドアは開いています」などの情報である可能性があります。この場合、信号は、各時点でのエレベーターとそのボタンの現在の状態を示します。次に、形式手法を使用して信号を分析し、「エレベーターが呼び出されるたびに、誰も 15 秒以上ドアを押さなかったと仮定すると、エレベーターは 3 分以内に到着する」という特性が成り立つかどうかを確認できます。このようなステートメントは通常、時間制約の表現を可能にする 線形時相論理の拡張である計量時相論理で表現されます。

信号は、信号オートマトンなどのモデルに渡され、すでに発生した文字やアクションに基づいて、次に実行すべきアクション (この例では、エレベーターがどの階に行く必要があるか) を決定します。次に、プログラムがこの信号をテストし、前述のプロパティを確認します。つまり、ドアが 15 秒以上開いたままにならないようにし、ユーザーがエレベーターを呼び出してから 3 分以上待たなければならない信号を生成しようとします。

アルファベット Aが与えられると、信号は有限または無限のシーケンス となり、それぞれが互いに素な区間であり、も区間となります。ある に対して が与えられると、を表します。 ${\displaystyle \gamma}$${\displaystyle (I_{0},a_{0}),(I_{1},a_{1}),\dots ,}$${\displaystyle a_{i}\in A}$${\displaystyle I_{i}\subseteq \mathbb {R} _{+}}$${\displaystyle 0\in I_{0}}$${\displaystyle I_{i}\cup I_{i+1}}$${\displaystyle t\in I_{i}}$${\displaystyle i}$${\displaystyle \gamma (t)}$${\displaystyle a_{i}}$

著者によっては、考慮する信号の種類を制限している場合があります。ここでは、信号が満たす可能性のある、または満たさない可能性のあるいくつかの標準的なプロパティを示します。

直感的に言えば、各制限された間隔中に文字が有限回数だけ変化する信号は有限可変である、または有限可変性特性を持つと言われます。前のエレベーターの例では、この特性は、ユーザーが有限の時間内に有限の回数だけボタンを押せることを意味します。同様に、有限の時間内にエレベーターのドアを開閉できる回数は有限です。

形式的には、信号は、シーケンスが無限で有界でない限り、有限変動性を持つと言われています。直感的には、有限変動性は、有限の時間内に無限の数の変化がないことを示しています。有限変動性を持つことは、時間指定の単語が非ゼノであるという概念に似ています。^[1]${\displaystyle \bigcup _{i}I_{i}}$

有界変動性の概念は有限変動性の概念に対する制限である。同じ文字を持つ2つの間隔の始まりの間に下限値が存在する場合、信号は有界変動性の性質を持つ。^[2]

正式な定義を行う前に、有限変数だが境界可変ではない信号の例を示します。アルファベット を取ります。およびの形式の実数を に送り、他のすべての実数を に送る区間を取ります。各有限時間間隔中に、文字は有限回数変化します。したがって、この信号は有限変数です。ただし、文字が連続して出現する 2 つの間隔は任意の大きさです。したがって、境界可変性の特性はありません。 ${\displaystyle A=\{a,b\}}$${\displaystyle \gamma}$${\displaystyle n+{\frac {c}{n}}}$${\displaystyle n\in \mathbb {N} }$${\displaystyle c<n}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$

数列 とします。各整数 に対して、 となる実数 が存在し、各 に対して となる実数が存在し、となる実数 が存在せず、 の下限と の下限の差が少なくとも である場合、数列は有界変動性を持つと言われます。各数列は、連続する 2 つの文字が異なる数列と同等であることに注意してください。数列 が有界変動性を持つのは、が有界変動性を持つ 場合のみであると言われます。${\displaystyle (I_{0},a_{0}),(I_{1},a_{1}),\dots }$${\displaystyle a_{i}\neq a_{i+1}}$${\displaystyle i}$${\displaystyle r>0}$${\displaystyle i<j}$${\displaystyle a_{i}=a_{j}}$${\displaystyle k}$${\displaystyle i<j<k}$${\displaystyle a_{i}=a_{k}}$${\displaystyle I_{j}}$${\displaystyle I_{i}}$${\displaystyle r}$${\displaystyle \gamma}$${\displaystyle \gamma '}$${\displaystyle \gamma}$${\displaystyle \gamma '}$

信号セットは、セット内の各信号に対して上記の下限が同じになるように選択できる場合、制限された可変性特性を持つと言われます。 ${\displaystyle r}$

制限された可変性を持つ信号を検討する主な理由がわかっています。信号オートマトンなどの、最後の時間単位に発生したすべてのことを思い出す必要があるシステムを作成する必要があると仮定します。信号が制限された可変性を持つことがわかっている場合は、1 つの時間単位中に発生したアクションの数の上限を計算できます。したがって、そのようなシステムを作成し、有限のメモリのみが必要であることを保証できます。

たとえば、任意の述語の場合、「次の時間単位のいつかに当てはまる」というステートメントが当てはまるかどうかを示す信号には、制限された可変性プロパティがあります。実際、このステートメントが真になると、完全な時間単位の間、真のままになります。したがって、このステートメントが真になる 2 つの発生間の差は、時間単位よりも大きくなります。 ${\displaystyle e}$${\displaystyle p}$

信号が二部信号であるとは、区間のシーケンスが特異区間、つまり下限と上限が等しい閉区間、つまりシングルトンである集合で始まる場合です。また、シーケンスが特異区間と開区間を交互に繰り返す場合も同様です。

各信号は二部信号と同等です。実際、左側で閉じている任意の区間は、特異区間と左側で開いている区間の和集合であり、この順序で表されます。右側で閉じている区間についても同様です。

二部信号を読み取る信号オートマトンには特別な形式があります。その位置の集合は、特異区間の位置と開区間の位置に分割できます。各遷移は、特異位置から開位置へ、およびその逆方向に行われます。

• 時間制限付き単語

• Kini, Dileep Raghunath; Krishna, Shankara Narayanan; Pandya, Paritosh K. (2011). 「時間投影を使用した MITL[U,S] の安全信号オートマトンの構築について」フォーマット: 227。