Petri nets are a popular formalism for modeling and analyzing distributed systems. Tokens in Petri net models can represent the control flow state or resources produced/consumed by transition firings. We define a resource as a part (submultiset) of the Petri net marking and call two resources equivalent iff replacing one of them with another in any marking does not change the observable Petri net behavior. We investigate the resource similarity and the resource bisimilarity -- congruent restrictions of the bisimulation equivalence on Petri net markings and prove that the resource bisimilarity is decidable in contrast to the resource similarity.
翻译:彼得里网是一种流行的建模和分析分布式系统的形式主义。 彼得里网模型中的托肯可以代表控制流动状态或过渡性点火产生/消耗的资源。 我们定义了一种资源作为彼得里网标记的一部分( 亚倍数), 如果在任何标记中将一种资源替换为另一类资源不会改变可观测到的彼得里网行为, 我们调查资源相似性和资源的两样性 -- -- Petri网标记的平衡等同性受到一致的限制, 并证明与资源相似性相比,资源两样性是可变的。