Net bisimulation is a very simple relation, extending ordinary bisimulation on LTSs with two additional conditions: the related markings must have the same size and
the pre-sets of the two matching transitions must be related as well. With these minimal additions, its definition is still very manageable and also very sensible as we proved to coincide with
causal-net bisimilarity [1]} (or, equivalently, structure-preserving bisimilarity [2]}), a truly concurrent behavioral equivalence fully respecting causality and the branching
structure of systems. Van Glabbeek [2]} argued that structure-preserving bisimilarity is the most appropriate behavioral equivalence for Petri nets, as it is the only one
respecting a list of desirable requirements he proposed.
Among these, there is `compositionality', up to structure-preserving bisimilarity, of the operators of the process
algebra CCSP, that Olderog proposed in his monograph [4]}
and equipped with a safe net semantics.
Future research will be devoted to check whether net bisimilarity is a congruence on the process algebra
FNM [5]}, which truly represents all (and only) the finite P/T nets, up to isomorphism.
In this way, we would
be able to have a compositional semantics, fully respecting causality and the branching
structure of systems, for the class of all the finite Petri nets.
