We prove that the well-known (strong) fully-concurrent bisimilarity and the novel i-causal-net bisimilarity, which is a sligtlhy coarser variant of causal-net bisimilarity, are decidable for finite bounded Petri nets. The proofs are based on a generalization of the ordered marking proof technique that Vogler used to demonstrate that (strong) fully-concurrent bisimilarity (or, equivalently, history-preserving bisimilarity) is decidable on finite safe nets.

翻译：我们证明了著名的（强）全并发互模拟以及新型的i-因果网互模拟（一种较因果网互模拟略粗的变体）对于有限有界Petri网是可判定的。这些证明基于对有序标识证明技术的推广，该技术由Vogler用于论证（强）全并发互模拟（或者等价地，历史保持互模拟）在有限安全网上的可判定性。