Luca Aceto

professor at Reykjavik University, Iceland and Gran Sasso Science Institute, Italy.

The equational logic of concurrent processes: Results and proof techniques

Abstract

This course will survey some of the results on the equational axiomatisation of notions of equivalence over algebras of concurrent processes that have been obtained over the last 45 years. It will focus on equational axiomatisations of various notions of process equivalence over fragments of Milner's Calculus of Communicating Systems, presenting both positive and negative results on the existence of (finite) equational characterisations of the resulting algebras of processes. The course will also highlight proof techniques for showing such results, various notions of completeness one might want to consider over algebras and some of the main challenging open problems in this research field.

The course will assume no previous familiarity with equational logic, process algebra and universal algebra.

Course material (updated 7 March 2026)

• Slides [pdf]
  Luca Aceto's comment: During the lectures, for lack of time, we did not cover the material in the slides labelled 26/45 and 33-43/45. I have kept them in the PDF file as further reading for the keenest.

References

References on the equational logic of processes (and other structures) mentioned in the course, roughly in order of appearance on the slides

1. Luca Aceto, Wan J. Fokkink, Anna Ingólfsdóttir, Bas Luttik: Finite Equational Bases in Process Algebra: Results and Open Questions. Processes, Terms and Cycles 2005: 338-367 https://link.springer.com/chapter/10.1007/11601548_18, https://tidsskrift.dk/brics/article/view/21885
2. Matthew Hennessy: Algebraic Theory of Processes, MIT Press, 1988. https://mitpress.mit.edu/9780262580939/algebraic-theory-of-processes/
   Note: This reference is not mentioned in the slides. If you can get hold of this book, I recommend the first part for an extensive and accessible introduction to algebraic semantics and (in)equational logic.
3. Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir: On the Two-Variable Fragment of the Equational Theory of the Max-Sum Algebra of the Natural Numbers. STACS 2000: 267-278 https://doi.org/10.1007/3-540-46541-3_22, https://www.brics.dk/RS/99/22/BRICS-RS-99-22.pdf
4. Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir: The max-plus algebra of the natural numbers has no finite equational basis. Theor. Comput. Sci. 293(1): 169-188 (2003) https://doi.org/10.1016/S0304-3975(02)00236-0
5. Luca Aceto, Zoltán Ésik, Anna Ingólfsdóttir: Equational theories of tropical semirings. Theor. Comput. Sci. 298(3): 417-469 (2003) https://doi.org/10.1016/S0304-3975(02)00864-2
6. Matthew Hennessy, Robin Milner: Algebraic Laws for Nondeterminism and Concurrency. J. ACM 32(1): 137-161 (1985) https://doi.org/10.1145/2455.2460
7. Jan A. Bergstra, Jan Willem Klop: Process Algebra for Synchronous Communication. Inf. Control. 60(1-3): 109-137 (1984) https://doi.org/10.1016/S0019-9958(84)80025-X, https://ir.cwi.nl/pub/1836/1836D.pdf
8. Luca Aceto, Wan J. Fokkink, Anna Ingólfsdóttir, 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) https://doi.org/10.1145/1459010.1459016
9. Luca Aceto, Bard Bloom, Frits W. Vaandrager: Turning SOS Rules into Equations. Inf. Comput. 111(1): 1-52 (1994) https://doi.org/10.1006/inco.1994.1040
10. Faron Moller. Axioms for Concurrency. PhD thesis, University of Edinburgh, 1989 https://era.ed.ac.uk/server/api/core/bitstreams/842b8c21-0ea0-467c-aeb9-8101347ad2cd/content
11. Luca Aceto, Silvio Capobianco, Anna Ingólfsdóttir, Bas Luttik: The equational theory of prebisimilarity over basic CCS with divergence. Inf. Process. Lett. 108(5): 284-289 (2008) https://doi.org/10.1016/j.ipl.2008.05.019
12. Matthew Hennessy: Axiomatising Finite Concurrent Processes. SIAM J. Comput. 17(5): 997-1017 (1988) https://doi.org/10.1137/0217063
13. Luca Aceto, Wan J. Fokkink, Anna Ingólfsdóttir, Bas Luttik: CCS with Hennessy's merge has no finite-equational axiomatization. Theor. Comput. Sci. 330(3): 377-405 (2005) https://doi.org/10.1016/j.tcs.2004.10.003, https://www.brics.dk/RS/03/34/BRICS-RS-03-34.pdf
14. Luca Aceto, Valentina Castiglioni, Wan J. Fokkink, Anna Ingólfsdóttir, Bas Luttik: Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition? ACM Trans. Comput. Log. 23(4): 22:1-22:56 (2022) https://doi.org/10.1145/3529535
15. Robin Milner, Faron Moller: Unique Decomposition of Processes. Theor. Comput. Sci. 107(2): 357-363 (1993) https://doi.org/10.1016/0304-3975(93)90176-T
16. Bas Luttik, Vincent van Oostrom: Decomposition orders another generalisation of the fundamental theorem of arithmetic. Theor. Comput. Sci. 335(2-3): 147-186 (2005) https://doi.org/10.1016/j.tcs.2004.11.019
17. Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, Anna Ingólfsdóttir: Non-finite Axiomatisability Results via Reductions: CSP Parallel Composition and CCS Restriction. A Journey from Process Algebra via Timed Automata to Model Learning 2022: 1-26 https://doi.org/10.1007/978-3-031-15629-8_1, https://l0e42.github.io/resources/axiom_CSP.pdf
18. Luca Aceto, Wan J. Fokkink, Anna Ingólfsdóttir, Mohammad Reza Mousavi: Lifting non-finite axiomatizability results to extensions of process algebras. Acta Informatica 47(3): 147-177 (2010) https://doi.org/10.1007/s00236-010-0114-7, https://staff.ru.is/luca/PAPERS/embedding_tech_rep.pdf
19. Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, Mathias Ruggaard Pedersen: On the Axiomatisability of Parallel Composition. Log. Methods Comput. Sci. 18(1) (2022) https://doi.org/10.46298/lmcs-18(1:15)2022
20. Rowin Versteeg, Valentina Castiglioni, Bas Luttik: From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases. CONCUR 2025: 35:1-35:18 https://doi.org/10.4230/LIPIcs.CONCUR.2025.35
21. Luca Aceto, Wan J. Fokkink, Anna Ingólfsdóttir, Sumit Nain: Bisimilarity is not finitely based over BPA with interrupt. Theor. Comput. Sci. 366(1-2): 60-81 (2006) https://doi.org/10.1016/j.tcs.2006.07.003
22. Luca Aceto, Taolue Chen, Wan J. Fokkink, Anna Ingólfsdóttir: On the axiomatisability of priority. Math. Struct. Comput. Sci. 18(1): 5-28 (2008) https://chentaolue.github.io/pub-papers/Mscs08.pdf
23. Luca Aceto, Taolue Chen, Anna Ingólfsdóttir, Bas Luttik, Jaco van de Pol: On the axiomatizability of priority II. Theor. Comput. Sci. 412(28): 3035-3044 (2011) https://doi.org/10.1016/j.tcs.2011.02.033
24. Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, Mathias Ruggaard Pedersen: On the axiomatisability of priority III: Priority strikes again. Theor. Comput. Sci. 837: 223-246 (2020) https://doi.org/10.1016/j.tcs.2020.07.044
25. Peter Sewell: Nonaxiomatisability of Equivalences over Finite State Processes. Ann. Pure Appl. Log. 90(1-3): 163-191 (1997) https://doi.org/10.1016/S0168-0072(97)00036-5
26. Luca Aceto, Wan J. Fokkink, Anna Ingólfsdóttir: A Menagerie of Nonfinitely Based Process Semantics over BPA* - From Ready Simulation to Completed Traces. Math. Struct. Comput. Sci. 8(3): 193-230 (1998) https://www.brics.dk/RS/96/23/BRICS-RS-96-23.pdf
27. Rob J. van Glabbeek, W. P. Weijland: Branching Time and Abstraction in Bisimulation Semantics. J. ACM 43(3): 555-600 (1996) https://doi.org/10.1145/233551.233556
28. Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik: Axiomatising weak bisimulation congruences over CCS with left merge and communication merge. Theor. Comput. Sci. 1047: 115325 (2025) https://doi.org/10.1016/j.tcs.2025.115325
29. Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik: Non finite axiomatisability of weak bisimulation-based congruences. Theor. Comput. Sci. 1054: 115453 (2025) https://doi.org/10.1016/j.tcs.2025.115453
30. Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik: In search of lost time: Axiomatising parallel composition in process algebras. LICS 2021: 1-14 https://arxiv.org/abs/2105.00735

Some references of historical interest on algebraic semantics and abstract data types (not mentioned on the slides)

31. Bruno Courcelle, Maurice Nivat: Algebraic Families of Interpretations. FOCS 1976: 137-146 https://doi.ieeecomputersociety.org/10.1109/SFCS.1976.3
32. V. Giarratana, F. Gimona, Ugo Montanari: Observability Concepts in Abstract Data Type Specifications. MFCS 1976: 576-587 https://doi.org/10.1007/3-540-07854-1_231
33. Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, Jesse B. Wright: Initial Algebra Semantics and Continuous Algebras. J. ACM 24(1): 68-95 (1977) https://doi.org/10.1145/321992.321997

General reading on the role of negative results in Computer Science (and much more), for those amongst you who are interested in some philosophical remarks and the philosophy of science

34. Christos H. Papadimitriou: Database metatheory: asking the big queries. SIGACT News 26(3): 13-30 (1995) https://doi.org/10.1145/211542.211547

General references on equational logic (for the mathematicians and/or those interested in much more than I ever used or learnt)

35. George F. McNulty. Equational logic. Lecture notes. Spring 2017. https://people.math.sc.edu/mcnulty/alglatvar/equationallogic.pdf

Some references on connections with denotational semantics and domain theory

36. Samson Abramsky: A Domain Equation for Bisimulation. Inf. Comput. 92(2): 161-218 (1991)
    https://doi.org/10.1006/inco.1991.9999
37. Luca Aceto, Anna Ingólfsdóttir: CPO Models for Compact GSOS Languages. Inf. Comput. 129(2): 107-141 (1996)
    https://doi.org/10.1006/inco.1996.0077
38. Luca Aceto, Anna Ingólfsdóttir: A Characterization of Finitary Bisimulation. Inf. Process. Lett. 64(3): 127-134 (1997)
    https://doi.org/10.1016/S0020-0190(97)00163-4
39. Matthew Hennessy: A Term Model for Synchronous Processes. Inf. Control. 51(1): 58-75 (1981)
    https://doi.org/10.1016/S0019-9958(81)90082-6
40. Matthew Hennessy, Gordon D. Plotkin: A Term Model for CCS. MFCS 1980: 261-274
    https://doi.org/10.1007/BFb0022510

Equational logic

41. Walter Taylor. Equational logic. Houston Journal of Mathematics, Survey 1979, iii+83 pp.
    https://www.math.uh.edu/~hjm/hjmathsurvey_1979.pdf