The defnitions of Reactive Graph are the follow:
Multi-Action Reactive Graph of order $n$ is a structure $M = (w, \mathcal{F} ,\mathcal{A})$ where:
- $w \in Q $ is the current state;
- $\mathcal{F} = (Q,Act,E,HE)$ is the frame of MAR where:
-$Q$ is the set of states non empty; -$Act$ is the set of actions; -$E \subseteq Q \times Q \times Act$ is the set of level 0 edges; -$HE$ is the set of higher-level edges, where: $$\begin{cases} HE_1 \subseteq E \times E \times \{ ON, OFF \}; \\ HE_2 \subseteq E \times HE_1 \times \{ ON, OFF \}\; \bigcup \;HE_1 \times E \times \{ ON, OFF \}; \\ \qquad \vdots \\ HE_{k+1} \subseteq \bigcup_{i=0}^k \left( HE_{i} \times HE_{k-i} \times \{ ON, OFF \} \right) \text{, with } HE_0 = E \\ \end{cases}$$ So, $HE = \bigcup_{i=1}^n HE_i$, where $n$ is the highest order.
-$\mathcal{A} \subseteq E \cup HE$ is a set that indicates if one edge are enable os disable.
If we consider a LTS (Labelled transition System), basicaly, is the reactive graph (RG) without hyper edges and every edges are enable. And, I want generalise the product with shared actions between RG from the definition for LTS. The definition for LTS, is the following:
$$\begin{array}{c} s_1 \xrightarrow{a}_1 s1' ~\quad~ a \in Act_1 \backslash Act_2 \\\hline (s_1,s_2) ~ \xrightarrow{a} ~ (s'_1,s_2) \end{array}$$
$$\begin{array}{c} s_2 \xrightarrow{a}_2 s2' ~\quad~ a \in Act_2 \backslash Act_1 \\\hline (s_1,s_2) ~ \xrightarrow{a} ~ (s1,s'_2) \end{array}$$
$$\begin{array}{c} s_1 \xrightarrow{a}_1 s1' ~\quad~ s_2 \xrightarrow{a}_2 s2' ~\quad~ a \in Act_1 \cap Act_2 \\\hline (s_1,s_2) ~ \xrightarrow{a} ~ (s'_1,s'_2) \end{array}$$
For the level 0 edges, the problem is solved, these rules work prefectly. However, for hyper edges the problem its not trivial, because a hyper edge can start from an edge that exists and arrive at one that does not exist.
Any hint is welcome to progress. I would be really grateful.