Decidability of Branching Bisimulation on Normed Commutative Context-Free Processes

作者：Czerwinski Wojciech^*; Hofman Piotr; Lasota Sawomir

来源：Theory of Computing Systems, 2014, 55(1): 136-169.

DOI：10.1007/s00224-013-9505-9

• Branching bisimulation equivalence
• Commutative context-free graphs
• Equivalence checking
• Basic parallel processes

We investigate normed commutative context-free processes (Basic Parallel Processes). We show that branching bisimilarity admits the bounded response property: in the Bisimulation Game, Duplicator always has a response leading to a process of size linearly bounded with respect to the Spoiler%26apos;s process. The linear bound is effective, which leads to decidability of branching bisimilarity. For weak bisimilarity, we are able merely to show existence of some linear bound, which is not sufficient for decidability. We conjecture however that the same effective bound holds for weak bisimilarity as well. We suppose that further elaboration of novel techniques developed in this paper may be sufficient to demonstrate decidability.

• 出版日期2014-7