Bisimulation equivalence is decidable in polynomial time for both sequential and commutative normed context-free processes, known as BPA and BPP, respectively. Despite apparent similarity between the two classes, different techniques were used in each case. We provide one polynomial-time algorithm that works in a superclass of both normed BPA and BPP. It is derived in the setting of partially-commutative contextfree processes, a new process class introduced in the paper. It subsumes both BPA and BPP and seems to be of independent interest. We investigate the bisimulation equivalence of the context-free processes, i.e., the process graphs defined by a context-free grammar in Greibach normal form. In process algebra, there are two essentially different ways of interpreting such grammars, depending on whether the concatenation is understood as the sequential or parallel composition of processes. These two process classes are known as BPA (Basic Process Algebra) and BPP (Basic Parallel ...
Wojciech Czerwinski, Sibylle B. Fröschle, Sla