Document Open Access Logo

Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?

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

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2021.8.pdf
  • Filesize: 486 kB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
  • Theory of computation → Process calculi
  • Theory of computation → Operational semantics
Keywords
  • Equational logic
  • CCS
  • bisimulation
  • parallel composition
  • non-finitely based algebras

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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. This study provides a negative answer to that question based on three reasonable assumptions.

Cite As Get BibTex

Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are Two Binary Operators Necessary to Finitely Axiomatise Parallel Composition?. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.CSL.2021.8

Author Details

Luca Aceto
  • Reykjavik University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy
Valentina Castiglioni
  • Reykjavik University, Iceland
Wan Fokkink
  • Vrije Universiteit Amsterdam, The Netherlands
Anna Ingólfsdóttir
  • Reykjavik University, Iceland
Bas Luttik
  • Eindhoven University of Technology, The Netherlands

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).

Acknowledgements

We thank the anonymous reviewers for their valuable comments.

References

  1. Luca Aceto. Some of my favourite results in classic process algebra. Bulletin of the EATCS, 81:90-108, 2003. Google Scholar
  2. Luca Aceto, Bard Bloom, and Frits W. Vaandrager. Turning SOS rules into equations. Inf. Comput., 111(1):1-52, 1994. URL: https://doi.org/10.1006/inco.1994.1040.
  3. Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are two binary operators necessary to finitely axiomatise parallel composition? CoRR, abs/2010.01943, 2020. URL: http://arxiv.org/abs/2010.01943.
  4. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. CCS with Hennessy’s merge has no finite-equational axiomatization. Theor. Comput. Sci., 330(3):377-405, 2005. URL: https://doi.org/10.1016/j.tcs.2004.10.003.
  5. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Finite equational bases in process algebra: Results and open questions. In Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, and Roel C. de Vrijer, editors, Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday, volume 3838 of Lecture Notes in Computer Science, pages 338-367. Springer, 2005. URL: https://doi.org/10.1007/11601548_18.
  6. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. A finite equational base for CCS with left merge and communication merge. ACM Trans. Comput. Log., 10(1):6:1-6:26, 2009. URL: https://doi.org/10.1145/1459010.1459016.
  7. Luca Aceto, Wan Fokkink, and Chris Verhoef. Structural operational semantics. In Handbook of Process Algebra, pages 197-292. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50021-7.
  8. Luca Aceto, Anna Ingólfsdóttir, Bas Luttik, and Paul van Tilburg. Finite equational bases for fragments of CCS with restriction and relabelling. In Proceedings of IFIP TCS 2008, volume 273 of IFIP, pages 317-332, 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_22.
  9. Jan A. Bergstra and Jan Willem Klop. The algebra of recursively defined processes and the algebra of regular processes. In Proceedings of ICALP 2011, volume 172 of Lecture Notes in Computer Science, pages 82-94, 1984. URL: https://doi.org/10.1007/3-540-13345-3_7.
  10. Jan A. Bergstra and Jan Willem Klop. Process algebra for synchronous communication. Information and Control, 60(1-3):109-137, 1984. URL: https://doi.org/10.1016/S0019-9958(84)80025-X.
  11. Jan A. Bergstra and Jan Willem Klop. Algebra of communicating processes with abstraction. Theor. Comput. Sci., 37:77-121, 1985. URL: https://doi.org/10.1016/0304-3975(85)90088-X.
  12. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, 1995. URL: https://doi.org/10.1145/200836.200876.
  13. Robert de Simone. Higher-level synchronising devices in meije-SCCS. Theor. Comput. Sci., 37:245-267, 1985. URL: https://doi.org/10.1016/0304-3975(85)90093-3.
  14. Matthew Hennessy. Axiomatising finite concurrent processes. SIAM J. Comput., 17(5):997-1017, 1988. URL: https://doi.org/10.1137/0217063.
  15. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  16. Robert M. Keller. Formal verification of parallel programs. Commun. ACM, 19(7):371-384, 1976. URL: https://doi.org/10.1145/360248.360251.
  17. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  18. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  19. Faron Moller. Axioms for Concurrency. PhD thesis, Department of Computer Science, University of Edinburgh, July 1989. Report CST-59-89. Also published as ECS-LFCS-89-84. Google Scholar
  20. Faron Moller. The importance of the left merge operator in process algebras. In Proceedings of ICALP `90, volume 443 of Lecture Notes in Computer Science, pages 752-764, 1990. URL: https://doi.org/10.1007/BFb0032072.
  21. Faron Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings of LICS '90, pages 142-153, 1990. URL: https://doi.org/10.1109/LICS.1990.113741.
  22. David M. R. Park. Concurrency and automata on infinite sequences. In Proceedings of GI-Conference, volume 104 of Lecture Notes in Computer Science, pages 167-183, 1981. URL: https://doi.org/10.1007/BFb0017309.
  23. Gordon D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981. Google Scholar
  24. Walter Taylor. Equational logic. In Contributions to Universal Algebra, pages 465-501. North-Holland, 1977. URL: https://doi.org/10.1016/B978-0-7204-0725-9.50040-X.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact