時間制限付き単語

コンピュータサイエンスの分野であるモデル検査において、タイムドワードは、形式言語におけるワードの概念の拡張であり、各文字は正の時間タグに関連付けられています。時間タグのシーケンスは非減少でなければなりません。これは、直感的には文字が受信されることを意味します。たとえば、ネットワーク経由でワードを受信するシステムは、各文字に、文字が受信された時間を関連付けることができます。ここでの非減少条件は、文字が正しい順序で受信されることを意味します。

時間制限のある言語時間制限のある単語のセットです。

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

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

アルファベット Aが与えられると、タイムドワードは、各整数 に対してとなる有限または無限のシーケンスになります。 ${\displaystyle w=(a_{0},t_{0})(a_{1},t_{1})\dots }$${\displaystyle a_{i}\in A}$${\displaystyle t_{i}\in \mathbb {R} _{+}}$${\displaystyle t_{i}\leq t_{i+1}}$${\displaystyle i}$

シーケンスが無限であるがシーケンスが有界である場合、この単語はゼノタイムド単語と呼ばれる。${\displaystyle (t_{0})(t_{1})\dots }$^[1]ゼノンのパラドックスに関連して、有限の時間内に無限の数の行動が発生する。

言葉${\displaystyle \operatorname {時間指定なし} (w)}$はタイムスタンプのない単語、つまり です。時間制限のある言語 が与えられた場合、のの集合は です。 ${\displaystyle w}$${\displaystyle a_{0}a_{1}\dots }$${\displaystyle L}$${\displaystyle \operatorname {untimed} (L)}$${\displaystyle \operatorname {時間指定なし} (w)}$${\displaystyle w\in L}$

• Alur, Rajeev ; Dill, David (1994). 「タイムドオートマトン理論」理論計算機科学. 126 (2): 190. doi : 10.1016/0304-3975(94)90010-8 .