TY - BOOK
T1 - CCS with Hennessy's merge has no finite equational axiomatization
AU - Aceto, L.
AU - Fokkink, W.J.
AU - Ingólfsdóttir, A.
AU - Luttik, B.
PY - 2004
Y1 - 2004
N2 - Abstract
This paper confirms a conjecture of Bergstra and Klop¿s from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by Hennessy in 1981 to the recursion free fragment of Milner¿s Calculus of Communicationg Systems is not finitely based modulo bisimulation equivalence. Thus Hennessy¿s merge cannot replace the left merge and communication merge operators proposed by Bergstra and Klop, at least if a finite axiomatization of parallel composition is desired.
2000 MATHEMATICS SUBJECT CLASSIFICATION: 08A70, 03B45, 03C05, 68Q10, 68Q45, 68Q55, 68Q70.
CR SUBJECT CLASSIFICATION (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1.
KEYWORDS AND PHRASES: Concurrency, process algebra, CCS, bisimulation, Hennessy¿s merge, left merge, communication merge, parallel composition, equational logic, complete axiomatizations, non-finitely based algebras.
AB - Abstract
This paper confirms a conjecture of Bergstra and Klop¿s from 1984 by establishing that the process algebra obtained by adding an auxiliary operator proposed by Hennessy in 1981 to the recursion free fragment of Milner¿s Calculus of Communicationg Systems is not finitely based modulo bisimulation equivalence. Thus Hennessy¿s merge cannot replace the left merge and communication merge operators proposed by Bergstra and Klop, at least if a finite axiomatization of parallel composition is desired.
2000 MATHEMATICS SUBJECT CLASSIFICATION: 08A70, 03B45, 03C05, 68Q10, 68Q45, 68Q55, 68Q70.
CR SUBJECT CLASSIFICATION (1991): D.3.1, F.1.1, F.1.2, F.3.2, F.3.4, F.4.1.
KEYWORDS AND PHRASES: Concurrency, process algebra, CCS, bisimulation, Hennessy¿s merge, left merge, communication merge, parallel composition, equational logic, complete axiomatizations, non-finitely based algebras.
M3 - Report
T3 - Computer science reports
BT - CCS with Hennessy's merge has no finite equational axiomatization
PB - Technische Universiteit Eindhoven
CY - Eindhoven
ER -