Luca Aceto, Silvio Capobianco, Anna Ingolfsdottir and Bas Luttik. The Equational Theory of Prebisimilarity over Basic CCS with Divergence. March 2008.
This paper studies the equational theory of prebisimilarity, a bisimulation-based preorder introduced by Hennessy and Milner in the early 1980s, over basic CCS with the divergent process Omega.
It is well known that prebisimilarity affords a finite ground-complete axiomatization over this language. This finite axiomatization is obtained by adding the inequation
Omega <= x
to the complete axiomatization of bisimilarity over basic CCS. In the above paper, we prove that this ground-complete axiomatization is also complete in the presence of an infinite set of actions. Moreover, in sharp contrast to this positive result, we show that prebisimilarity is not finitely based over basic CCS with the divergent process Omega when the set of actions is finite and non-empty.
No comments:
Post a Comment