State transition system

In theoretical computer science, a state transition system is an abstract machine used in the study of computation. The machine consists of a set of states and transitions between states.

State transition systems differ from finite state automata in several ways:

* In a state transition system the set of states is not necessarily finite, or even countable.
* In a state transition system the set of transitions is not necessarily finite, or even countable.

State transition systems with a finite number of states and transitions can be represented as directed graphs.

There are at least two basic types of state transition systems: labelled (or LTS for "labelled transition system") or unlabelled.

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

: $p\; overset\{alpha\}\{\; ightarrow\}\; q.\; ,$

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.

Relation between labelled and unlabelled transition systems.

There are many relations between these concepts. Some are simple, such as observing that a labelled transition system where the set of labels consists of only one element is equivalent to an unlabelled transition system. However not all these relations are equally trivial.

See also

* Simulation preorder
* Bisimulation
* Operational semantics