Product of a Transition System and a Finite Automaton
In Section 4.2.2 of the book "Principles of Model Checking", there is a definition (Definition 4.16; Page 165) of "Product of Transition System and NFA". You are right about the states (i.e., $S \times Q$) of the product but make mistakes about its transition relation. Below I focus on the transition relation.


  Definition 4.16 Product of Transition System $TS = (S, Act, \to, I, AP, L)$ and NFA $\mathcal{A} = (Q, \Sigma, \delta, Q_0, F)$. The transition relation $\to'$ of their product is the smallest relation defined by the rule
  $$\frac{s \to^{\alpha} t \; \land \; q \to^{L(t)} p}{(s,q) \to'^{\alpha} (t,p)}$$


Intuitively, the transition system TS generates atomic propositions and feeds them into the automaton $\mathcal{A}$, driving the automata running. This semantics can be used to verify if the TS satisfies some property expressed by an automaton.

Additionally, the start states of the product is $$I' = \{ (s_0, q) \mid s_0 \in I \land \exists q_0 \in Q_0. q_0 \to^{L(s_0)} q \}.$$ That is, $q_0$ in automaton has moved one step forward, driven by the atomic propositions in $s_0$.



Based on the definition above, I calculate the product as follows (please check it):






For what it concerns the terminal states, please refer to "Remark 4.17" (immediately following the Definition above) in the book.
By the way, the labels for transitions (action denoted by $\alpha$ above) in $TS$ are often ignored (because they are irrelevant).