However, this paper wants to offer a possible solution to this problem, proposing for Petri nets
a new bisimulation-like, very simple relation on markings that is
a smooth generalization of ordinary bisimulation on Labeled Transition Systems [1]}, [2]}, [3]} (LTSs, for short).
This relation \(R\) , we call net bisimulation, essentially states that if two markings \(m_1\)  and \(m_2\)  are related by \(R\) , then
\((i)\)  they must have the same size, i.e., \(|m_1| = |m_2|\) ; moreover, \((ii)\)  for each transition \(t_1\)  executable from \(m_1\) 
reaching \(m_1^{\prime }\) , there exists a transition \(t_2\)  executable from \(m_2\)  reaching \(m_2^{\prime }\)  such that, not only the labels of \(t_1\)  and \(t_2\) 
are the same and that \((m_1^{\prime }, m_2^{\prime }) \in R\)  (as for ordinary bisimulation), but also that the pre-sets of \(t_1\)  and \(t_2\)  are
related by \(R\)  (i.e., \((\mbox{$^{\bullet }t_1$}, \mbox{$^{\bullet }t_2$}) \in R\) ); finally, \((iii)\) , the symmetric condition if \(m_2\)  moves first.
Note that the two matching transitions \(t_1\)  and \(t_2\)  in the net bisimulation game must have the same shape
because \((i)\)  \((\mbox{$^{\bullet }t_1$}, \mbox{$^{\bullet }t_2$}) \in R\)  implies that
\(|\mbox{$^{\bullet }t_1$}| = |\mbox{$^{\bullet }t_2$}|\) , then \((ii)\)  \(l(t_1) = l(t_2)\)  and, finally, \((iii)\)  from \(|m_1| = |m_2|\) , \(|m_1^{\prime }| = |m_2^{\prime }|\)  and \(|\mbox{$^{\bullet }t_1$}| = |\mbox{$^{\bullet }t_2$}|\) 
we derive that \(|\mbox{$t_1^{\bullet }$}| = |\mbox{$t_2^{\bullet }$}|\) , because
\(m_i^{\prime } = m_i \ominus \mbox{$^{\bullet }t_i$} \oplus \mbox{$t_i^{\bullet }$}\)  for \(i = 1, 2\) .
