Skip to main navigation Skip to search Skip to main content

Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?

  • Luca Aceto
  • , Valentina Castiglioni
  • , Wan Fokkink
  • , Anna Ingólfsdóttir
  • , Bas Luttik

Research output: Contribution to JournalArticleAcademicpeer-review

56 Downloads (Pure)

Abstract

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.

Original languageEnglish
Article number22
Pages (from-to)1-56
Number of pages56
JournalACM Transactions on Computational Logic
Volume23
Issue number4
Early online date20 Oct 2022
DOIs
Publication statusPublished - Oct 2022

Bibliographical note

Funding Information:
This work has been supported by the project "Open Problems in the Equational Logic of Processes" (OPEL) of the Icelandic Research Fund (grant No. 196050-051).

Funding Information:
This work has been supported by the project “ Open Problems in the Equational Logic of Processes’’ (OPEL) of the Icelandic Research Fund IRF (grant No. 196050-051 IRF).

Publisher Copyright:
© 2022 Association for Computing Machinery.

Funding

This work has been supported by the project "Open Problems in the Equational Logic of Processes" (OPEL) of the Icelandic Research Fund (grant No. 196050-051). This work has been supported by the project “ Open Problems in the Equational Logic of Processes’’ (OPEL) of the Icelandic Research Fund IRF (grant No. 196050-051 IRF).

Keywords

  • bisimulation
  • CCS
  • Equational logic
  • non-finitely based algebras
  • parallel composition

Fingerprint

Dive into the research topics of 'Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?'. Together they form a unique fingerprint.

Cite this