移行システム

理論計算機科学において、遷移システムとは、無限の状態を持つ可能性のある状態機械のことである。これは、離散システムの潜在的な振る舞いを記述するために用いられる。遷移システムは、状態と状態間の遷移から構成され、遷移にはラベルの集合から選択されたラベルが付与される。同じラベルが複数の遷移に付与される場合もある。ラベル集合が単一の要素のみからなる場合、システムは実質的にラベルなしとなり、ラベルを省略したより単純な定義が可能となる。

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

• 状態の集合は必ずしも有限であるとは限らず、可算であるとも限らない。
• 遷移の集合は必ずしも有限であるとは限らず、可算であるとも限らない。
• 「開始」状態も「終了」状態も示されていません。

遷移システムは有向グラフとして表現できる。

形式的には、遷移システムはペアである${\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 ]}

これらの概念の間には多くの関係が存在する。ラベルの集合が1つの要素のみで構成されるラベル付き遷移システムは、ラベルなし遷移システムと等価であるといった単純な関係もある。しかし、これらの関係すべてが同じように自明であるとは限らない。

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

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

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

• 二項関係
• 三項関係
• 遷移モノイド
• 変換モノイド
• 半群作用
• シミュレーションの予約注文
• 双模倣
• 操作的意味論
• クリプキ構造
• 有限状態機械
• モーダルμ計算