状態遷移系のソースを表示

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

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

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

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

ラベル付き状態遷移系は[[タプル]]（S, &Lambda;, &rarr;) で表され、S は状態の集合、&Lambda; はラベルの集合、&rarr; &sube; S &times; &Lambda; &times; S は（ラベル付き遷移の）[[三項関係]]である。p, q &isin; S で &alpha; &isin; &Lambda; であるとき、(p,&alpha;,q) &isin; &rarr; ならば、これを次のように記述する。
<center>
<math>
\begin{matrix}
  & \alpha & \\ 
p & \rightarrow & q 
\end{matrix}
</math>
</center>

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

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

== 関連項目 ==
* [[双模倣性]]
* [[操作的意味論]]
* [[:en:Simulation preorder]]

{{Normdaten}}
{{DEFAULTSORT:しようたいせんいけい}}
[[Category:計算モデル]]
[[Category:数学に関する記事]]