Transition relation ($\to \subseteq S\times S$)

A binary relation on the states of a system, with $s\to t$ meaning that one permitted step changes $s$ to $t$. A Boolean formula can encode a transition relation after choosing bits for the current and next states.