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?
Asked By : eyes enberg
Answered By : hengxin
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).
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/41268
