CCS with Hennessy's merge has no finite-equational axiomatization

详细信息	查看全文 | 推荐本文 |

• 作者：Aceto ; Luca ; Fokkink ; Wan ; Ing&oacute ; lfsd&oacute ; ttir ; Anna ; Luttik ; Bas
• 关键词：08A70 ; 03B45 ; 03C05 ; 68Q10 ; 68Q45 ; 68Q55 ; 68Q70 ; Concurrency ; Process algebra ; CCS ; Bisimulation ; Hennessy's merge ; Left merge ; Communication merge ; Equational logic ; Complete axiomatizations ; Non-finitely based algebras
• 刊名：Theoretical Computer Science
• 出版年：2005
• 期刊代码：114_03043975
• 类别：cp
• 出版时间：February 9, 2005
• 卷：330
• 期：3
• 页码：377-405
• 文件大小：337 K

摘要

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.