Transition system

Formally, a transition system is a pair ${\displaystyle (S,T)}$ where ${\displaystyle S}$ is a set of states and ${\displaystyle T}$, the transition relation, is a subset of ${\displaystyle S\times S}$. We say that there is a transition from state ${\displaystyle p}$ to state ${\displaystyle q}$ if ${\displaystyle (p,q)\in T}$, and denote it ${\displaystyle p\rightarrow q}$.

A labelled transition system is a tuple ${\displaystyle (S,\Lambda ,T)}$ where ${\displaystyle S}$ is a set of states, ${\displaystyle \Lambda }$ is a set of labels, and ${\displaystyle T}$, the labelled transition relation, is a subset of ${\displaystyle S\times \Lambda \times S}$. We say that there is a transition from state ${\displaystyle p}$ to state ${\displaystyle q}$ with label ${\displaystyle \alpha }$ iff ${\displaystyle (p,\alpha ,q)\in T}$ and denote it

${\displaystyle p\xrightarrow {\alpha } q\,.}$

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. Labelled transitions systems were originally introduced as named transition systems.^[1]

• If, for any given ${\displaystyle p}$ and ${\displaystyle \alpha }$, there exists only a single tuple ${\displaystyle (p,\alpha ,q)}$ in ${\displaystyle T}$, then one says that ${\displaystyle \alpha }$ is deterministic (for ${\displaystyle p}$).
• If, for any given ${\displaystyle p}$ and ${\displaystyle \alpha }$, there exists at least one tuple ${\displaystyle (p,\alpha ,q)}$ in ${\displaystyle T}$, then one says that ${\displaystyle \alpha }$ is executable (for ${\displaystyle p}$).

The formal definition can be rephrased as follows. Labelled state transition systems on ${\displaystyle S}$ with labels from ${\displaystyle \Lambda }$ correspond one-to-one with functions ${\displaystyle S\to {\mathcal {P}}(\Lambda \times S)}$, where ${\displaystyle {\mathcal {P}}}$ is the (covariant) powerset functor. Under this bijection ${\displaystyle (S,\Lambda ,T)}$ is sent to ${\displaystyle \xi _{T}:S\to {\mathcal {P}}(\Lambda \times S)}$, defined by

${\displaystyle p\mapsto \{\,(\alpha ,q)\in \Lambda \times S\mid p\xrightarrow {\alpha } q\,\}}$.

In other words, a labelled state transition system is a coalgebra for the functor ${\displaystyle P(\Lambda \times {-})}$.

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.

As a mathematical object, an unlabeled transition system is identical with an (unindexed) abstract rewriting system. If we consider the rewriting relation as an indexed set of relations, as some authors do, then a labeled transition system is equivalent to an abstract rewriting system with the indices being the labels. The focus of the study and the terminology are different, however. In a transition system one is interested in interpreting the labels as actions, whereas in an abstract rewriting system the focus is on how objects may be transformed (rewritten) into others.^[2]

In model checking, a transition system is sometimes defined to include an additional labeling function for the states as well, resulting in a notion that encompasses that of Kripke structure.^[3]

Action languages are extensions of transition systems, adding a set of fluents F, a set of values V, and a function that maps F × S to V.^[4]

• Binary relation
• Ternary relation
• Transition monoid
• Transformation monoid
• Semigroup action
• Simulation preorder
• Bisimulation
• Operational semantics
• Kripke structure
• Finite-state machine
• Modal μ-calculus