|
|||||
|
|
CCS with Hennessy's merge has no finite-equational axiomatization |
|
| Authors: | Luca Aceto Wan Fokkink Anna Inglfsdttir Bas Luttik |
| Affiliation: | aDepartment of Computer Science, BRICS (Basic Research in Computer Science), Centre of the Danish National Research Foundation, Aalborg University, Fr. Bajersvej 7E, 9220 Aalborg Ø, Denmark bDepartment of Software Engineering, CWI, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands cdeCODE Genetics, Sturlugata 8, 101 Reykjavík, Iceland dDepartment of Mathematics and Computer Science, Eindhoven Technical University, P.O. Box 513, 5600 MB Eindhoven, The Netherlands |
| 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 Communicating 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 modulo bisimulation equivalence is desired. |
| Keywords: | Concurrency Process algebra CCS Bisimulation Hennessy's merge Left merge Communication merge Equational logic Complete axiomatizations Non-finitely based algebras |
| 本文献已被 ScienceDirect 等数据库收录！ | |