State Transition System - Formal Definition

Formal Definition

Formally, an unlabelled state transition system is a tuple (S, →) where S is a set (of states) and → ⊆ S × S is a binary relation over S (of transitions). If p, q ∈ S, (p, q) ∈ → is usually written as p → q. This represents the fact that there is a transition from state p to state q.

A labelled transition system is a tuple (S, Λ, →) where S is a set (of states), Λ is a set (of labels) and → ⊆ S × Λ × S is a ternary relation (of labelled transitions). If p, q ∈ S and α ∈ Λ, then (p,α,q) ∈ → is written as

This represents the fact that there is a transition from state p to state q with label α. Labels can represent different things depending on the language of interest. Typical uses of labels include representing input expected, conditions that must be true to trigger the transition, or actions performed during the transition.

If, for any given p and α, there exists only a single tuple (p,α,q) in →, then one says that α is deterministic (for p). If, for any given p and α, there exists at least one tuple (p,α,q) in →, then one says that α is executable (for p).