A bisimulation equivalence definition based on partial orders, similar to the definitions proposed by Boudol and Castellani and by Glabbeek and Goltz, is given. Using the notion of lambda-abstraction of a process, the authors improve this definition, including the way the partial orders (and thus the processes) concatenate. The resulting fully concurrent bisimulation (FC-bisimulation) essentially coincides with BS-bisimulation and with history-preserving bisimulation.
The authors show that FC-bisimulation is stronger than the classical bisimulation, so it preserves all the properties preserved by the latter, and it preserves the absence of auto-concurrency (self-concurrency) and the auto-concurrent actions. They give a technically complex construction that transforms a labeled Petri net into an injectively labeled one. Under some restrictions, FC-bisimulation is preserved by the refinement of actions. The references are rich and up to date.