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用于论证(强)全并发双模拟(或等价地,历史保持双模拟)在有限安全网上的可判定性时所采用的序标记证明技术的一般化推广。