A Finite Equational Base for CCS with Left Merge and Communication Merge
Using the left merge and the communication merge from ACP, we present an equational base (i.e., a ground-complete and omega-complete set of valid equations) for the fragment of CCS without recursion, restriction and relabeling modulo (strong) bisimilarity. Our equational base is finite if the set of actions is finite.
finite equational base ccs left merge communication merge bisimilarity languages theory verification concurrency handshaking parallel composition process algebra