Let be the set of states of a system, and let be an alphabet of actions.
A labelled transition system (LTS) on consists of a relation . We write
to mean that .
Labelled transition systems are simple models of communicating programs. The states can be terms of a process calculus, or a description of the state of an abstract machine. The labels of the alphabet stand for observable actions of the program or process. In particular, we write whenever the program in state can emit the label to the environment, and change to state .
Keller, Robert M. 1976. ‘Formal Verification of Parallel Programs’. Communications of the ACM 19 (7): 371–84. https://doi.org/10.1145/360248.360251.
@article{keller_formal_1976,
title = {Formal verification of parallel programs},
volume = {19},
doi = {10.1145/360248.360251},
number = {7},
journal = {Communications of the ACM},
author = {Keller, Robert M.},
year = {1976},
pages = {371--384}
}