Technical Report LIT--202, pages 1-33 pp.. Université Libre de Bruxelles (Belgium), Laboratoire d'Informatique Théorique, July 1989.
Abstract: Fully concurrent (FC-) bisimulation of labelled Petri nets is defined using the concurrency semantics of net theory. The relation preserves the level of concurrency of visible operations and, under some conditions, allows to enforce injective labelling on them. Refinements of a visible operation are also defined, and it is shown that, under some conditions, they preserve FC-bisimulation.
Keywords: (fully) concurrent bisimulation; labelled net; concurrency semantics; operation refinement.