2020/10/05 by Luca Aceto, Valentina Castiglioni, Aceto, Luca +7
Computer Science · Mathematics · #Advanced Algebra and Logic #Advanced Topics in Algebra #F.3.1 #F.3.2 #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2010.01943
openalex publication_date 2020/10/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Bergstra and Klop have shown that bisimilarity has a finite equational axiomatisation over ACP/CCS extended with the binary left and communication merge operators. Moller proved that auxiliary operators are necessary to obtain a finite axiomatisation of bisimilarity over CCS, and Aceto et al. showed that this remains true when Hennessy's merge is added to that language. These results raise the question of whether there is one auxiliary binary operator whose addition to CCS leads to a finite axiomatisation of bisimilarity. We contribute to answering this question in the simplified setting of the recursion-, relabelling-, and restriction-free fragment of CCS. We formulate three natural assumptions pertaining to the operational semantics of auxiliary operators and their relationship to parallel composition, and prove that an auxiliary binary operator facilitating a finite axiomatisation of bisimilarity in the simplified setting cannot satisfy all three assumptions.