Labelled Transition System

An labelled transition system describes an system with either observable or internal action labels on its transitions.

Formal definition

Source: [Tre08]

Definition 1. A labelled transition system is a 4-tuple (Q, L, T, q₀) where

• Q is a countable, non-empty set of states;
• L is a countable set of labels;
• T ⊆Q×(L∪{τ})×Q, with τ ∉ L, is the transition relation;
• q₀ ∈ Q is the initial state.

The labels in L represent the observable actions of a system; they model the system’s interactions with its environment. Internal actions are denoted by the special label τ (τ ∉ L), which is assumed to be unobservable for the system’s environment. Also states are assumed to be unobservable for the environment.

We write q −μ→ q if there is a transition labelled μ from state q to state q , i.e., (q,μ,q′) ∈ T. The informal idea of such a transition is that when the system is in state q it may perform action μ, and go to state q′ .

Model definitions

LTS

A Labelled Transition System (LTS) is a structure consisting of states with transitions, labelled with actions, between them. The states model the system states; the labelled transitions model the actions that a system can perform. An action can be a label from the set of labels L or can be an internal action.