ラベル無し状態遷移系は形式的にはタプル (S, →) で表され、S は状態の集合、→ は → ⊆ S × S という S 上の二項関係（つまり遷移）である。p,q ∈ S で (p,q) ∈ → であるとき、これを p → q と記述する。これはすなわち、状態 p から状態 q への遷移が存在することを意味する。
ラベル付き状態遷移系はタプル（S, Λ, →) で表され、S は状態の集合、Λ はラベルの集合、→ ⊆ S × Λ × S は（ラベル付き遷移の）三項関係である。p, q ∈ S で α ∈ Λ であるとき、(p,α,q) ∈ → ならば、これを次のように記述する。
これは、状態 p から状態 q へのラベル α 付きの遷移が存在することを意味する。ラベルは対象言語によって様々な事柄を表現する。一般的には遷移に必要とされる入力を表す場合、遷移のトリガーとなる条件を表す場合、遷移に際して実行される行動を表す場合がある。
