状態遷移系

状態遷移系（じょうたいせんいけい、State Transition System）とは、理論計算機科学での計算の研究に使用される抽象機械の一種。状態遷移系は状態群と状態間の遷移から構成される。

状態と遷移が有限個の状態遷移系は有向グラフで表すことができる。

また、状態遷移系は「ラベル付き」と「ラベル無し」の2種類に分類することができる。

形式的定義

ラベル無し状態遷移系は形式的にはタプル (S, →) で表され、S は状態の集合、→ は → ⊆ S × S という S 上の二項関係（つまり遷移）である。p,q ∈ S で (p,q) ∈ → であるとき、これを p → q と記述する。これはすなわち、状態 p から状態 q への遷移が存在することを意味する。

ラベル付き状態遷移系はタプル（S, Λ, →) で表され、S は状態の集合、Λ はラベルの集合、→ ⊆ S × Λ × S は（ラベル付き遷移の）三項関係である。p, q ∈ S で α ∈ Λ であるとき、(p,α,q) ∈ → ならば、これを次のように記述する。

${\displaystyle {\begin{matrix}&\alpha &\\p&\rightarrow &q\end{matrix}}}$

これは、状態 p から状態 q へのラベル α 付きの遷移が存在することを意味する。ラベルは対象言語によって様々な事柄を表現する。一般的には遷移に必要とされる入力を表す場合、遷移のトリガーとなる条件を表す場合、遷移に際して実行される行動を表す場合がある。

ラベル付き状態遷移系とラベル無し状態遷移系の関係

これらの概念には様々な関係がある。単純な関係としては、ラベルの集合に1つしか要素が無いラベル付き状態遷移系は、ラベル無し状態遷移系と等価である。しかし、これらの関係は必ずしもそのような瑣末なものばかりではない。

関連項目

• 双模倣性
• 操作的意味論
• en:Simulation preorder