移行システム

理論計算機科学において、遷移システムとは計算の研究で使用される概念である。離散システムの潜在的な動作を説明するために使用される。遷移システムは状態と状態間の遷移で構成され、セットから選択されたラベルでラベル付けされる。同じラベルが複数の遷移に現れることもある。ラベルセットがシングルトンである場合、システムは本質的にラベル付けされず、ラベルを省略したより単純な定義が可能となる。

遷移システムは、抽象的な書き換えシステム（この記事でさらに説明）や有向グラフと数学的に一致します。有限状態オートマトンとはいくつかの点で異なります。

• 状態の集合は必ずしも有限ではなく、また数えられるわけでもありません。
• 遷移の集合は必ずしも有限ではなく、また数えられるわけでもありません。
• 「開始」状態または「最終」状態は指定されません。

遷移システムは有向グラフとして表すことができます。

正式には、遷移システムとは、 が状態の集合であり、 の遷移関係がのサブセットであるペアです。の場合、状態から状態への遷移があると言い、それを と表記します。 ${\displaystyle (S,T)}$${\displaystyle S}$${\displaystyle T}$${\displaystyle S\times S}$${\displaystyle p}$${\displaystyle q}$${\displaystyle (p,q)\in T}$${\displaystyle p\rightarrow q}$

ラベル付き遷移システムは、が状態の集合、がラベルの集合、（ラベル付き遷移関係）が のサブセットである組です。状態から状態への遷移がラベルとともに存在するとは、次の場合に限り、言い、それを次のように表記します 。${\displaystyle (S,\Lambda,T)}$${\displaystyle S}$${\displaystyle \Lambda}$${\displaystyle T}$${\displaystyle S\times \Lambda \times S}$${\displaystyle p}$${\displaystyle q}$${\displaystyle \alpha}$${\displaystyle (p,\alpha ,q)\in T}$

${\displaystyle p\xrightarrow {\alpha } q\,.}$

ラベルは、対象となる言語に応じてさまざまなものを表すことができます。ラベルの一般的な用途には、予想される入力、遷移をトリガーするために真でなければならない条件、または遷移中に実行されるアクションを表すことが含まれます。ラベル付き遷移システムは、もともと名前付き遷移システムとして導入されました。^[1]

• 任意の および に対して、に単一のタプルのみが存在する場合、 は決定論的である( に対して) といいます。${\displaystyle p}$${\displaystyle \alpha}$${\displaystyle (p,\alpha,q)}$${\displaystyle T}$${\displaystyle \alpha}$${\displaystyle p}$
• 任意の および に対して、に少なくとも 1 つのタプルが存在する場合、 は実行可能である( に対して) と言います。${\displaystyle p}$${\displaystyle \alpha}$${\displaystyle (p,\alpha,q)}$${\displaystyle T}$${\displaystyle \alpha}$${\displaystyle p}$

正式な定義は次のように言い換えることができる。からのラベルを持つ 上のラベル付き状態遷移システムは、関数 と1対1で対応しており、ここで は（共変）べき集合関数である。この下では、単射はに送信され、次のように定義される 。${\displaystyle S}$${\displaystyle \Lambda}$${\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}$${\displaystyle {\mathcal {P}}}$${\displaystyle (S,\Lambda,T)}$${\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}$

${\displaystyle p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}}$。

言い換えれば、ラベル付き状態遷移システムは、関数の余代数です。 ${\displaystyle P(\Lambda \times {-})}$

これらの概念の間には多くの関係があります。ラベルのセットが 1 つの要素のみで構成されるラベル付き遷移システムは、ラベルなし遷移システムと同等であるなど、単純な関係もあります。ただし、これらの関係のすべてが同じように自明というわけではありません。

数学的対象として、ラベルなし遷移システムは（インデックスなしの）抽象書き換えシステムと同一である。一部の著者が行っているように、書き換え関係をインデックス付きの関係集合と見なすと、ラベル付き遷移システムは、インデックスがラベルである抽象書き換えシステムと同等になる。ただし、研究の焦点と用語は異なる。遷移システムでは、ラベルをアクションとして解釈することに関心があるのに対し、抽象書き換えシステムでは、オブジェクトが他のオブジェクトに変換（書き換え）される方法に焦点が当てられる。^[2]

モデル検査では、遷移システムは状態に対する追加のラベル付け関数も含むように定義されることがあり、その結果、クリプキ構造の概念が生まれます。^[3]

アクション言語は遷移システムの拡張であり、流暢性 のセットF、値のセットV 、およびF × SをVにマッピングする関数を追加します。^[4]

• 二項関係
• 三項関係
• 遷移モノイド
• 変換モノイド
• セミグループアクション
• シミュレーション予約
• バイシミュレーション
• 操作的意味論
• クリプキ構造
• 有限状態機械
• 様相μ計算