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.


The following diagramme shows a labelled transition system with Γ={q0, q1, q2, q3}, A={a, b, c, d}, and q0aq1, q1,→bq2, q2cq3, q3dq0.


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