If, for any given and , there exists only a single tuple in , then one says that is deterministic (for ).

If, for any given and , there exists at least one tuple in , then one says that is executable (for ).

Relation between labelled and unlabelled transition system[edit]

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.

Comparison with abstract rewriting systems[edit]

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]

Extensions[edit]

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