Dealing with a question that asks me to compute the product of the following transition system and finite automaton.Compute the product between the transition system TS and the finite-word automaton A depicted below.Can't seem to find a good example on how to do this so I sort of just freestyled my answer. The best I found was in Principles of Model Checking but the book didn't really explain how the product was derived (it just provided a TS, FA and product), so I had to guess the logic.Can anybody have a quick look at my solution and see if there are there any obvious mistakes I have made?Also I can't figure out whether or not I should indicate any terminal states. I know that a TS doesn't have any terminal states, but an FA can - so what about the product? 
Product of a Transition System and a Finite Automaton
automata;finite automata;model checking
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).