Net bisimulation is a smooth generalization of ordinary bisimulation on LTSs
(see, e.g., [1]}, [2]}). In fact, on sequential finite-state machines (which
are essentially labeled transition systems, as each reachable marking is a singleton; cf.
Definition ), its definition reduces to standard bisimulation, as the
side conditions \(|m_1| = |m_2|\)  and \((\mbox{$^{\bullet }t_1$}, \mbox{$^{\bullet }t_2$}) \in R\)  are redundant.
