Saved in:
Bibliographic Details
Main Authors: Cesco, Arnaldo, Gorrieri, Roberto
Format: Preprint
Published: 2021
Subjects:
Online Access:https://arxiv.org/abs/2104.14856
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866910327314055168
author Cesco, Arnaldo
Gorrieri, Roberto
author_facet Cesco, Arnaldo
Gorrieri, Roberto
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2104_14856
institution arXiv
publishDate 2021
record_format arxiv
spellingShingle Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
Cesco, Arnaldo
Gorrieri, Roberto
Logic in Computer Science
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.
title Decidability of Two Truly Concurrent Equivalences for Finite Bounded Petri Nets
topic Logic in Computer Science
url https://arxiv.org/abs/2104.14856