Labelled Transition System

A labelled transition system is a triple (Γ, A, ⇒) where Γ is a set of configurations and A is a set of actions, and ⇒ ⊆ Γ × A × Γ is the transition relation.

A transition is written as γ→^aγ' where γ, γ'∈Γ and a∈A.

The idea behind labelling transitions with actions is that it can give information as to what went on in the configuration.

Example

The following diagramme shows a labelled transition system with Γ={q₀, q₁, q₂, q₃}, A={a, b, c, d}, and q₀→^aq₁, q₁,→^bq₂, q₂→^cq₃, q₃→^dq₀.

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.