Non-interleaving bisimulation equivalences on Basic Parallel Processes
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.
Basic Parallel processes
Hereditary history preserving bisimilarity
History preserving bisimilarity
Labelled event structures
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.