Formally, a
transition system is a pair (S, T) where S is a set of states and T, the
transition relation, is a subset of S \times S. We say that there is a transition from state p to state q if (p, q) \in T, and denote it p \rightarrow q. A
labelled transition system is a tuple (S, \Lambda, T) where S is a set of states, \Lambda is a set of labels, and T, the
labelled transition relation, is a subset of S \times \Lambda \times S. We say that there is a transition from state p to state q with label \alpha iff (p, \alpha, q) \in T and denote it :: 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.
Special cases • If, for any given p and \alpha, there exists only a single tuple (p, \alpha, q) in T, then one says that \alpha is
deterministic (for p). • If, for any given p and \alpha, there exists at least one tuple (p, \alpha, q) in T, then one says that \alpha is
executable (for p).
Coalgebra formulation The formal definition can be rephrased as follows. Labelled state transition systems on S with labels from \Lambda correspond
one-to-one with functions S \to \mathcal{P}(\Lambda \times S) , where \mathcal{P} is the (covariant)
powerset functor. Under this bijection (S, \Lambda, T) is sent to \xi_T : S \to \mathcal{P}(\Lambda \times S) , defined by :: 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 P(\Lambda \times {-}). == Relation between labelled and unlabelled transition system ==