信号オートマトン

コンピュータサイエンスの一分野であるオートマトン理論において、シグナルオートマトンとは、有限の実数値クロックの集合で拡張された有限オートマトンである。シグナルオートマトンの実行中、クロック値はすべて同じ速度で増加する。オートマトンが遷移する間、クロック値は整数と比較される。これらの比較は、遷移を有効または無効にするガードを形成し、それによってオートマトンの動作を制限する。さらに、クロックはリセットできる。^[1]

シグナルオートマトンが何であるかを正式に定義する前に、例を示します。バイナリアルファベット上のシグナル言語を考えてみましょう。バイナリアルファベットには次のような シグナルが含まれます。${\displaystyle {\mathcal {L}}}$${\displaystyle \{A,B\}}$${\displaystyle \gamma}$

• ${\displaystyle A}$は特異な間隔で現れる。つまり、時間の集合は離散的であり、${\displaystyle \{t\mid \gamma (t)=A\}}$
• ${\displaystyle A}$長さ 1 の各間隔中に少なくとも 1 回出現します。

この言語は、近くに描かれたオートマトンによって受け入れられます。

有限オートマトンについては、入ってくる矢印は初期位置を表し、二重円は受け入れ位置を表します。ただし、有限オートマトンとは異なり、文字は遷移ではなく位置で発生します。これは、文字が連続的に発行され、遷移が離散的に行われるためです。 記号は時計を表します。この時計により、が最後に発行されてからの時間を測定できます。したがって、が離散的に発行されることが保証されます。また、発生せずに単位時間以上経過できないことが保証されます。 ${\displaystyle x}$${\displaystyle A}$${\displaystyle x=0}$${\displaystyle A}$${\displaystyle 1>x}$${\displaystyle A}$

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

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

からのエッジは、 のクロックをリセットする場所からへの遷移です。 ${\displaystyle (\ell ,r,\ell ')}$${\displaystyle E}$${\displaystyle \ell}$${\displaystyle \ell '}$${\displaystyle r}$

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

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

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

有限オートマトンの場合、実行は基本的に位置のシーケンスであり、2 つの位置の間に遷移が存在します。ただし、2 つの違いを強調する必要があります。文字は遷移ではなく位置によって決定されます。これは、文字が連続的に発行される一方で、遷移が離散的に行われるという事実によるものです。位置にある間には、ある程度の時間が経過します。位置またはその後続のラベルを付けるクロック制約により、単一の位置で費やされる時間が制約される場合があります。

ランは、いくつかの制約を満たす形式のシーケンスです。これらの制約を述べる前に、いくつかの表記法が導入されます。シーケンスは離散的ですが、連続的なイベントを表します。シーケンスの連続バージョン、、が導入されました。積分ととすると、 ${\displaystyle {\xrightarrow[{\nu _{0}}]{C}}(\ell _{0},I_{0}){\xrightarrow[{\nu _{1}}]{r_{1}}}(\ell _{1},I_{1})\dots }$${\displaystyle (\sigma _{i})}$${\displaystyle (\nu _{i})}$${\displaystyle (\ell _{i})}$${\displaystyle i\geq 0}$${\displaystyle t\in I_{i}}$

• を と等しくすると、${\displaystyle \sigma '_{t}}$${\displaystyle \sigma_{i}}$
• を区間の下限とする。${\displaystyle \nu '_{t}}$${\displaystyle \nu _{i}+t-\lceil I_{i}\rceil }$${\displaystyle \lceil I_{i}\rceil }$${\displaystyle I_{i}}$
• させて。${\displaystyle \ell '_{t}=\ell _{i}}$

run が満たす制約は、各積分および実数に対して次のとおりです。 ${\displaystyle i\geq 0}$${\displaystyle t\geq 0}$

• ${\displaystyle \ell _{0}\in L_{0}}$、
• ${\displaystyle (\ell _{i},r_{i},\ell _{i+1})\in E}$、
• ${\displaystyle \nu _{i+1}=(\nu _{i}+\mid I_{i}\mid )[r_{i}\rightarrow 0]}$、
• ${\displaystyle \nu '_{t}\models \beta (\ell '_{t})}$。

この実行によって定義されるシグナルは、上記で定義された関数です。上記で定義された実行は、シグナルに対する実行であると言えます。 ${\displaystyle \sigma '}$${\displaystyle \sigma '}$

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

シグナルオートマトンがシグナルを受け入れるとは、シグナルを受け入れる際にの連続が存在する場合を指します。 が受け入れるシグナルの集合はが受け入れる言語と呼ばれ、 で表されます。 ${\displaystyle \gamma}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}}$${\displaystyle \gamma}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {A}}}$${\displaystyle {\mathcal {S(A)}}}$

有限オートマトンや Büchi オートマトンの場合と同様に、シグナルオートマトンも決定的または非決定的である可能性があります。直感的には、いずれの場合も決定的であることは同じ意味です。つまり、開始位置の集合はシングルトンであり、拡張状態、および文字が与えられた場合、を読み取ることでから到達できる拡張状態は 1 つだけであることを意味します。より正確には、その場所に長く留まることが可能であるか、後続の場所の可能な範囲は最大でも 1 つしかありません。 ${\displaystyle s}$${\displaystyle a}$${\displaystyle s}$${\displaystyle a}$

正式には、次のように定義できます。

• ${\displaystyle L_{0}}$シングルトンです
• 各場所、各遷移について、次の 2 つのゾーンは分離しています。 ${\displaystyle \ell \in L}$${\displaystyle (\ell ,r,\ell ')\in E}$
  • クロック制約によって定義されたゾーン、${\displaystyle \beta (\ell )}$
  • クロック制約によって定義される領域で、クロックの制約が削除される。${\displaystyle \beta (\ell ')}$${\displaystyle r}$
• 各位置遷移およびについて、次の 2 つのゾーンは分離しています。 ${\displaystyle (\ell ,r',\ell ')\in E}$${\displaystyle (\ell ,r'',\ell '')\in E}$
  • クロック制約によって定義される領域で、クロックの制約が削除される。${\displaystyle \beta (\ell ')}$${\displaystyle r'}$
  • クロック制約によって定義される領域で、クロックの制約が削除される。${\displaystyle \beta (\ell '')}$${\displaystyle r''}$

著者によっては、シグナルオートマトンの定義が若干異なる場合があります。ここでは、そのような定義を 2 つ示します。

ランの定義を簡略化するために、ランの各区間が右閉じで左開きであることを要求している著者もいます。これにより、オートマトンは、基礎となるパーティションが同じプロパティを満たす信号のみを受け入れるように制限されます。ただし、各時点で、関数、または 上記で紹介した関数のいずれかを表すためにが保証されます。 ${\displaystyle t\geq 0}$${\displaystyle \lim _{t\leftarrow x^{+}}f(x)=f(t)}$${\displaystyle f}$${\displaystyle \sigma '}$${\displaystyle \nu '}$${\displaystyle \ell '}$

二部信号オートマトンとは、開区間と特異区間（つまり、シングルトンである区間）を交互に実行する信号オートマトンです。これにより、オートマトンの基礎となるグラフが二部グラフであることが保証され、したがって、位置の集合は、開位置の集合、特異位置の集合に分割できます。最初の区間には 0 が含まれているため、開位置になることはできず、 となります。各特異位置が実際に特異であることを保証するために、各位置 について、およびに入るときにリセットされ、 のクロック制約に が含まれるクロックが必要です。 ${\displaystyle \{L^{o},L^{s}\}}$${\displaystyle L_{0}\subseteq L^{s}}$${\displaystyle \ell}$${\displaystyle x_{\ell }}$${\displaystyle \ell }$${\displaystyle \ell }$${\displaystyle x=0}$

任意の信号オートマトンを、 同等の二部信号オートマトンに変換できます。各位置を位置のペアに置き換え、各 に対して となる新しいクロック を導入するだけで十分です。${\displaystyle \ell }$${\displaystyle (\ell ^{o},\ell ^{s})}$${\displaystyle x}$${\displaystyle \ell }$${\displaystyle x_{\ell ^{s}}=x}$

近くには、例のセクションの信号オートマトンに相当する二部オートマトンが描かれています。長方形の状態は、特異な場所を表します。

有限オートマトン積の概念は、シグナルオートマトンに拡張されます。ただし、このような積は、考慮される両方のオートマトンで時間が同様に経過するという事実を強調するために、オートマトン同期と呼ばれます。同期と積の主な違いは、2 つの有限オートマトンが同じ単語を読み取ると、同時に遷移することです。シグナルオートマトンの場合は、任意の時間に遷移できるため、これは当てはまりません。したがって、シグナルオートマトンの遷移関係により、1 つまたは 2 つのオートマトンで遷移を行うことができます。

と2 つのシグナルオートマトンがあるとします。それらの同期はシグナルオートマトン であり、次の遷移が含まれます。 ${\displaystyle {\mathcal {A}}^{1}=\langle \Sigma ,L^{1},L_{0}^{1},C^{1},F^{1},\alpha ^{1},\beta ^{1},E^{1}\rangle }$${\displaystyle {\mathcal {A}}^{2}=\langle \Sigma ,L^{2},L_{0}^{2},C^{2},F^{2},\alpha ^{2},\beta ^{2},E^{2}\rangle }$${\displaystyle {\mathcal {A}}1\otimes {\mathcal {A}}^{2}=\langle \Sigma ,\{(\ell ^{1},\ell ^{2})\in L^{1}\otimes L^{2}\mid \alpha ^{1}(\ell ^{1})=\alpha ^{2}(\ell ^{2})\},L_{0}^{1}\otimes L_{0}^{2},C^{1}\cup C^{2},F^{1}\otimes F^{2},(\ell ^{1},\ell ^{2})\mapsto \alpha ^{1}(\ell ^{1}),(\ell ^{1},\ell ^{2})\mapsto \beta ^{1}(\ell ^{1})\land \beta ^{2}(\ell ^{2}),E\rangle }$${\displaystyle E}$

• ${\displaystyle ((\ell ^{1},\ell ^{2}),r^{1},(\ell ^{\prime 1},\ell ^{2})}$については、同様に については、${\displaystyle (\ell ^{1},r,\ell ^{\prime 1})\in E^{1}}$${\displaystyle E^{2}}$
• ${\displaystyle ((\ell ^{1},\ell ^{2}),r^{1}\cup r^{2},(\ell ^{\prime 1},\ell ^{\prime 2})}$およびについて。${\displaystyle (\ell ^{1},r,\ell ^{\prime 1})\in E^{1}}$${\displaystyle (\ell ^{2},r,\ell ^{\prime 2})\in E^{2}}$

時間付きオートマトンも有限オートマトンを拡張したもので、単語に時間の概念を追加します。ここでは、時間付きオートマトンとシグナルオートマトンの主な違いをいくつか説明します。

時間指定オートマトンでは、文字は位置ではなく遷移時に出力されます。上で説明したように、信号オートマトンと有限オートマトンを比較すると、単語や時間指定単語の場合のように単語が離散的に出力されるときは、文字は遷移時に出力されますが、信号の場合のように文字が連続的に出力されるときは、文字は位置で出力されます。

時間指定オートマトンでは、ガードは遷移時にのみチェックされます。これにより、クロックが再起動される前に制約が満たされる必要があるため、決定論的オートマトンの定義が簡素化されます。

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