Right! For the transition relation, you double all variables. You then have un-primed and primed variables. Each assignment corresponds to a pair of a state (un-primed variables) and a next state (primed variables). There exists a transition from the state to the next state iff the assignment is a satisfying assignment of the transition relation formula.