Structure-preserving bisimilarity is a truly concurrent behavioral equivalence for finite Petri nets, which relates markings (of the same size only) generating the same causal nets, hence also the same partial orders of events. The process algebra FNM truly represents all (and only) the finite Petri nets, up to isomorphism. We prove that structure-preserving bisimilarity is a congruence w.r.t. the FMN operators, In this way, we have defined a compositional semantics, fully respecting causality and the branching structure of systems, for the class of all the finite Petri nets. Moreover, we study some algebraic properties of structure-preserving bisimilarity, that are at the base of a sound (but incomplete) axiomatization over FNM process terms.
翻译:结构保持双相似性是一种适用于有限彼得里网的真并发行为等价关系,它关联生成相同因果网(且仅具有相同规模)的标识,从而也关联相同的事件偏序。进程代数FNM(在同构意义下)精确表示所有(且仅表示)有限彼得里网。我们证明结构保持双相似性关于FNM算子构成同余关系,由此为所有有限彼得里网类定义了一种完全尊重因果关系及系统分支结构的组合语义。此外,我们研究了结构保持双相似性的若干代数性质,这些性质构成了关于FNM进程项合理(但不完备)公理化的基础。