PLS Lab

Labelled Transition Systems

Let S be the set of states of a system, and let A be an alphabet of actions.

A labelled transition system (LTS) on S consists of a relation R \subseteq S \times A \times S. We write

  s \xrightarrow{a} t

to mean that (s, a, t) \in R.

Labelled transition systems are simple models of communicating programs. The states s, t, \dots \in S can be terms of a process calculus, or a description of the state of an abstract machine. The labels of the alphabet A stand for observable actions of the program or process. In particular, we write s \xrightarrow{a} t whenever the program in state s can emit the label a to the environment, and change to state t.

References

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}
}