I was perusing the internet for a precise def. of a simulation relation and one of the top search results was a paper Bisimulation, The Supervisory Control Problem and Strong Model Matching for Finite State Machines, https://www.researchgate.net/figure/Example-of-simulation-relation_fig2_262243963. The authors say that F2 simulates F1, but F1 does not simulate F2. I understand intuitively why this is the case (F1 can't make a transition on 'b' if it were to end up in state C). However I don't see how it follows from their defn, for example the following seems like a simulation relation : {(1,A), (2,B), (2,C), (3,D), (4,E)}. If this is indeed a simulation relation, and as its total on F2 and 1 and A are the respective start states of the two automata, then should it not be the case that F1 simulates F2?
Their def. of simulation (Def 2.9) is Let H and G be [labeled transition systems]. A simulation relation of H and G wrt $\Sigma_S \subseteq \Sigma_H$ is a binary relation $S \subseteq X_H \times X_G$ satisfying
- If $x_HSx_G$ and $\sigma \in \Sigma_S$ and $x_H \longrightarrow_\sigma x'_H$ then there exists $x'_G$ s.t. $x_G \longrightarrow_\sigma x'_G$ and $x'_HSx'_G$
- (Simulation with marking) $x_HSx_G$ implies $x_H \in X_{Hm}$ iff $x_G \in X_{Gm}$
$X_H,X_G$ are the node alphabets resp. and $X_{Hm},X_{Gm}$ are subsets of $X_H,X_G$ that represent marked states