Options
Non-interleaving bisimulation equivalences on Basic Parallel Processes
Publikationstyp
Journal Article
Date Issued
2009-06-21
Sprache
English
Journal
Volume
208
Issue
1
Start Page
42
End Page
62
Citation
Information and Computation 208 (1): 42-62 (2010)
Publisher DOI
Scopus ID
Publisher
Elsevier
We show polynomial time algorithms for deciding hereditary history preserving bisimilarity (in O (n3 log n)) and history preserving bisimilarity (in O (n6)) on the class Basic Parallel Processes. The latter algorithm also decides a number of other non-interleaving behavioural equivalences (e.g., distributed bisimilarity) which are known to coincide with history preserving bisimilarity on this class. The common general scheme of both algorithms is based on a fixpoint characterization of the equivalences for tree-like labelled event structures. The technique for realizing the greatest fixpoint computation in the case of hereditary history preserving bisimilarity is based on the revealed tight relationship between equivalent tree-like labelled event structures. In the case of history preserving bisimilarity, a technique of deciding classical bisimilarity on acyclic Petri nets is used.
Subjects
Basic Parallel processes
Bisimulation equivalence
Equivalence checking
Hereditary history preserving bisimilarity
History preserving bisimilarity
Labelled event structures
Non-interleaving equivalences
Verification
DDC Class
004: Informatik
More Funding Information
The authors gratefully acknowledge the support by the Czech Ministry of Education, Grant No. 1M0567. This work has been partially supported by Polish Government Grant No. N206 008 32/0810.