Constructing a parallel composition from a given transition system and automaton

Question

I am looking at an exercise, where it asks me to construct a parallel composition from a given transition system and an automaton.

The transition system looks like this:

and the automaton (with its respective LTL formula) like this:

This is the solution - the parallel composition:

Can someone, please, explain how this composition is constructed?

Answer 1

The start state of the transition is $s_o$, the start state of the automaton is $q_o$. So the start state of the parallel composition is $(s_o,q_o)$. From this state:

• The transition from $q_0 \to q_1$ is guarded by $(x \wedge \neg y)$, which is unsatisfied at $(s_o,q_o)$. Therefore, $q_0$ can only make a transition to itself.
• $s_0$ can make transition to $s_1, s_2$ without any $guard$.

Therefore, from $(s_o,q_o)$ we have transition relations to $(s_1,q_o)$ and $(s_2,q_o)$. The transition from $(s_o,q_o) \to (s_1,q_o)$ is the result of the parallel transition of $s_0 \to s_1$ and $q_0 \to q_0$. After this transition, at the state $(s_1,q_o)$, $y$ is satisfied, but the guard $q_0 \to q_1$ is still unsatisfied...

Continue doing this until you enumerate all transition relations, you will have the graph.