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.

Task graphics

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?

Solution attempt

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?

  • $\begingroup$ 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? $\endgroup$
    – babou
    Apr 11 '15 at 22:24
  • $\begingroup$ 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 $\endgroup$ Apr 11 '15 at 23:31
  • $\begingroup$ @babou If the action for a transition is irrelevant (for some purpose), it is often ignored. $\endgroup$
    – hengxin
    Apr 13 '15 at 7:48
  • $\begingroup$ Can you intersect two finite automata? This should not be that different. $\endgroup$
    – 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).

  • $\begingroup$ This is essentially the product construction of finite automata, isn't it? $\endgroup$
    – Raphael
    Apr 13 '15 at 10:10
  • $\begingroup$ @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)$. $\endgroup$
    – hengxin
    Apr 13 '15 at 11:32
  • 1
    $\begingroup$ 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$. $\endgroup$
    – Raphael
    Apr 13 '15 at 12:09
  • $\begingroup$ Thank you so much for this answer - it helped a lot. And it's correct. $\endgroup$ Apr 16 '15 at 19:23
  • $\begingroup$ 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. $\endgroup$ Apr 25 '15 at 19:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.