時間制限付きオートマトン

オートマトン理論では、時間指定オートマトンとは、有限の実数値クロックの集合で拡張された有限オートマトンです。時間指定オートマトンの実行中、クロック値はすべて同じ速度で増加します。オートマトンが遷移する間、クロック値は整数と比較できます。これらの比較により、遷移を有効または無効にするガードが形成され、それによってオートマトンの動作が制限されます。さらに、クロックをリセットすることもできます。時間指定オートマトンとは、ハイブリッド オートマトン型のサブクラスです。

時間オートマトンを使用すると、リアルタイム システムやネットワークなどのコンピュータ システムのタイミング動作をモデル化して分析できます。安全性と活性の両方の特性をチェックする方法が開発され、過去 20 年間にわたって集中的に研究されてきました。

時間付きオートマトンの状態到達可能性問題は決定可能であることが示されている^[1]。このため、これはハイブリッドオートマトンという興味深いサブクラスとなっている。ストップウォッチ、リアルタイムタスク、コスト関数、時間制限付きゲームなど、その拡張は広く研究されてきた。時間付きオートマトンやその拡張を入力および解析するためのツールは多種多様で、モデルチェッカーのUPPAAL、Kronos、スケジュール可能性解析ツールのTIMESなどがある。これらのツールはますます成熟してきていますが、まだすべて学術研究ツールである。

時間付きオートマトンとは何かを正式に定義する前に、いくつかの例を示します。

単項アルファベット上の時間指定単語の言語を考えてみましょう。この言語では、最初の時間単位の間にがあり、2 つの連続する の間には 1 時間単位未満があります。この言語を認識する時間指定オートマトン (近くに示す) は、1 つのクロックを使用しますが、このクロックが 1 になることはありません。このクロックは、 が発行されなかった場合は実行の開始からの時間をカウントし、それ以外の場合は最後に発行された からの時間をカウントします。つまり、 が発行されるたびに、このクロックは 0 にリセットされます。 ${\displaystyle {\mathcal {L}}}$ ${\displaystyle w}$${\displaystyle \{a\}}$${\displaystyle a}$${\displaystyle a}$ ${\displaystyle x}$${\displaystyle a}$${\displaystyle a}$${\displaystyle a}$

バイナリ アルファベット上の時間指定の単語の言語を考えてみましょう。この言語では、各単語の後に次の時間単位で が続きます。この言語を認識する時間指定のオートマトン (近くで図示) は、がまだ続いていない があったかどうかを記憶します。そうでない場合は実行を受け入れ、そうでない場合は拒否します。さらに、そのような がある場合、最初の が発行されてからの経過時間を記録するクロックがあります。この場合、クロックが少なくとも 1 に等しい場合は を発行できないため、実行は失敗します。 ${\displaystyle {\mathcal {L}}}$ ${\displaystyle w}$${\displaystyle \{a,b\}}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle b}$${\displaystyle a}$${\displaystyle x}$${\displaystyle a}$${\displaystyle b}$

正式には、タイムドオートマトンは次のコンポーネントで構成される タプルです。${\displaystyle {\mathcal {A}}=\langle \Sigma ,L,L_{0},C,F,E\rangle }$

• ${\displaystyle \Sigma }$はアルファベットまたはアクションと呼ばれる有限集合です。${\displaystyle {\mathcal {A}}}$
• ${\displaystyle L}$は有限集合です。 の要素はの位置または状態と呼ばれます。${\displaystyle L}$${\displaystyle {\mathcal {A}}}$
• ${\displaystyle L_{0}\subseteq L}$ 開始場所のセットです。
• ${\displaystyle C}$は の時計と呼ばれる有限集合です。${\displaystyle {\mathcal {A}}}$
• ${\displaystyle F\subseteq L}$受け入れ場所の集合です。
• ${\displaystyle E\subseteq L\times \Sigma \times {\mathcal {B}}(C)\times {\mathcal {P}}(C)\times L}$は、遷移と呼ばれるエッジの集合であり、 ${\displaystyle {\mathcal {A}}}$
  • ${\displaystyle {\mathcal {B}}(C)}$は、からのクロックを含むクロック制約の集合であり、${\displaystyle C}$
  • ${\displaystyle {\mathcal {P}}(C)}$は のべき集合です。${\displaystyle C}$

からのエッジは、アクション、ガード、およびクロックのリセットを伴う、場所からへの遷移です。 ${\displaystyle (\ell ,\sigma ,g,r,\ell ')}$${\displaystyle E}$${\displaystyle \ell }$${\displaystyle \ell '}$${\displaystyle \sigma }$${\displaystyle g}$${\displaystyle r}$

位置とクロック値を持つペアは、拡張状態または状態と呼ばれます。 ${\displaystyle \ell }$ ${\displaystyle \nu }$

状態という言葉は、著者によってはペアを意味する場合もあれば、 の要素を意味する場合もあるため、曖昧であることに注意してください。わかりやすくするために、この記事では、の要素に対しては場所という用語を使用し、ペアに対しては拡張場所という用語を使用します。 ${\displaystyle L}$${\displaystyle L}$

ここに、タイムド オートマトンと有限オートマトンの最大の違いの 1 つがあります。有限オートマトンでは、実行のある時点で、状態は読み取られた文字の数と、実際には「状態」と呼ばれる有限の数の可能な値によって完全に記述されます。つまり、読み取る単語の状態と接尾辞が与えられれば、実行の残りの部分が完全に決定されます。したがって、「有限オートマトン」という名前に「有限」という単語が含まれています。ただし、以下の「実行」のセクションで説明されているように、再開するには、どの遷移を実行できるかを決定するためにクロックが使用されます。したがって、オートマトンの状態を知るには、自分がどの場所にいるかと、クロックの値の両方を知る必要があります。

の時間制限付き単語 、非負数の増加シーケンス、および上記のような時間制限付きオートマトンが与えられた場合、実行は次の制約を満たす 形式のシーケンスになります。${\displaystyle w=(\sigma _{1},t_{1}),(\sigma _{2},t_{2}),\dots ,}$${\displaystyle \sigma _{i}\in \Sigma }$${\displaystyle (t_{i})_{i}}$${\displaystyle {\mathcal {A}}}$${\displaystyle (\ell _{0},\nu _{0}){\xrightarrow[{t_{1}}]{\sigma _{1}}}(\ell _{1},\nu _{1})\dots }$

• （初期化）${\displaystyle \ell _{0}\in L_{0}}$
• (連続)、すべての に対して、の形の辺が存在し、次のようになります。 ${\displaystyle i\geq 1}$${\displaystyle E}$${\displaystyle \langle \ell _{i-1},\sigma _{i},g_{i},r_{i},\ell _{i}\rangle }$
  • 時間単位が経過したと仮定し、この時点でガードは満たされます。つまり、${\displaystyle t_{i}-t_{i-1}}$${\displaystyle \nu _{i-1}+t_{i}-t_{i-1}}$${\displaystyle g_{i}}$
  • 新しいクロックの値は に対応し、 では時間単位が経過し、 では のクロックがリセットされます。正式には、です。${\displaystyle \nu _{i}}$${\displaystyle \nu _{i-1}}$${\displaystyle t_{i}-t_{i-1}}$${\displaystyle r_{i}}$${\displaystyle \nu _{i}=(\nu _{i-1}+t_{i}-t_{i-1})[r_{i}\rightarrow 0]}$

ランを受け入れるという概念は、有限ワードについては有限オートマトンで のように定義され、無限ワードについてはビュッヒオートマトンで のように定義されます。つまり、 が長さ の有限である場合、ランは を受け入れます。ワードが無限である場合、 となる位置が無限数存在する場合、かつその場合に限り、ランは を受け入れます。 ${\displaystyle w}$${\displaystyle n}$${\displaystyle \ell _{n}\in F}$${\displaystyle i}$${\displaystyle \ell _{i}\in F}$

有限オートマトンや Büchi オートマトンの場合と同様に、時間付きオートマトンも決定的または非決定的である可能性があります。直感的には、決定的であることは、いずれの場合も同じ意味を持ちます。つまり、開始位置の集合はシングルトンであり、状態、文字が与えられた場合、 を読み取ることによってから到達できる状態は 1 つだけであるということです。ただし、時間付きオートマトンの場合、正式な定義はやや複雑です。正式には、時間付きオートマトンが決定的であるのは次の場合です。 ${\displaystyle s}$${\displaystyle a}$${\displaystyle s}$${\displaystyle a}$

• ${\displaystyle L_{0}}$シングルトンです
• 遷移との各ペアについて、を満たすクロックの評価値の集合は、を満たすクロックの評価値の集合とは互いに素です。${\displaystyle (\ell ,\sigma ,g,r,\ell ')}$${\displaystyle (\ell ,\sigma ,g',r',\ell '')}$${\displaystyle g}$${\displaystyle g'}$

非決定性時間オートマトンによって認識される言語のクラスは次のとおりです。

• 和集合の下で閉じられており、実際、2 つの時間制御オートマトン同士の互いに素な和集合は、それらのオートマトンによって認識される言語の和集合を認識します。
• 交差点下で閉鎖中。^[2]
• 補語の下で閉じていない。^[3]

時間付きオートマトンに関連するいくつかの問題の計算複雑度を示します。

時間付きオートマトンにおける空問題は、領域オートマトンを構築し、それが空言語を受け入れるかどうかをチェックすることで解決できる。この問題はPSPACE完全である。^{[1] : 207}

非決定性時間オートマトンにおける普遍性問題は決定不可能であり、より正確にはΠ¹
₁しかし、オートマトンにクロックが1つだけ含まれている場合、その性質は決定可能ですが、原始再帰的ではありません。^[3]この問題は、すべての単語が時間制限付きオートマトンによって受け入れられるかどうかを判断することです。

• 交互時間オートマトン: 普遍的な遷移を備えた時間オートマトンの拡張。