print · source · login   

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, q0) 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;
  • q0 ∈ 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

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.