Transition relation
= Transition relation
{title2=$\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>.