Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
Logic in Computer Science
2024-02-14 v9
Abstract
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.
Keywords
Cite
@article{arxiv.2104.14856,
title = {Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets},
author = {Arnaldo Cesco and Roberto Gorrieri},
journal= {arXiv preprint arXiv:2104.14856},
year = {2024}
}