The aim of this post is to try and start an online collaboration to improve the solution to a problem in the equational logic of processes that I posed in a survey paper in 2003, namely
Can one obtain a finite axiomatisation of the parallel composition operator in bisimulation semantics by adding only one binary operator to the signature of (recursion, restriction, and relabelling free) CCS?
Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, Bas Luttik and I published a partial, negative answer to the above question in a paper at CSL 2021. (See the arXiv version for details and for the historical context for the above question.) Our solution is based on three simplifying assumptions that are described in detail in Section 3 of the above-mentioned paper. We'd be very interested in hearing whether any member of the research community in process algebra, universal algebra and equational logic can relax or remove any of our simplifying assumptions. In particular, one can start with assumptions 3 and 2.
We would also welcome any comments and suggestions on whether some version of that problem can be solved using existing results from equational logic and universal algebra. In particular, are there any general results guaranteeing that, under certain conditions, the reduct of a finitely based algebra is also finitely based? Or, conversely, that if some algebra is not finitely based, then so its expansion with a new operator?
To start with, add any contributions you might have as comments to this post. If ever we make substantial enough progress on the above question, anyone who has played a positive role in extending our results will be a co-author of the resulting paper.
Let PolyConc begin!
