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?