Product of a Transition System and a Finite Automaton

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?

• According to wikipedia, a Transition System has labels on the transitions, You have thm on the states. What definition are you using? What is the product suppose to do or to be used for? – babou Apr 11 '15 at 22:24
• The standard definiton found in Principles of model checking by Joost-Pieter Katoen and Christel Baier. Didn't really think about that, but for this module I have seen transition systems with labels on the transition systems as well as transition systems with just the atomic propositions on the states (like above). I think the transition labels are implied by the atomic propositions (e.g. if you go from a state with {a, b} to the state {a} then the transition is ¬b) but I'm not entirely sure. There is no context to this question unfortunately – eyes enberg Apr 11 '15 at 23:31
• @babou If the action for a transition is irrelevant (for some purpose), it is often ignored. – hengxin Apr 13 '15 at 7:48
• Can you intersect two finite automata? This should not be that different. – Raphael Apr 13 '15 at 10:09

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).

• This is essentially the product construction of finite automata, isn't it? – Raphael Apr 13 '15 at 10:10
• @Raphael I don't get it. For me, the purpose of $TS \times \mathcal{A}$ differs from that of $\mathcal{A}_1 \times \mathcal{A}_2$: The former is feeding the $TS$ paths into the automaton and to check whether the $TS$ satisfies some property expressed by that automaton; and the latter is to calculate $L(\mathcal{A}_1) \cap L(\mathcal{A}_2)$. – hengxin Apr 13 '15 at 11:32
• Isn't that the same? If $L(A_1) \cap L(A_2) = L(A_1)$ then $A_1$ conforms to the property expressed by $A_2$. – Raphael Apr 13 '15 at 12:09
• Thank you so much for this answer - it helped a lot. And it's correct. – eyes enberg Apr 16 '15 at 19:23
• Would you happen to know how I could use DFS to find out if there exists an execution accepted by the product? I know what DFS is but I don't know what exactly I'm checking for at each state. – eyes enberg Apr 25 '15 at 19:22