Time: Wednesday 29.9.2004, 14:30
Place: Room B2-109, Fr. Bajersvej 7
In this talk I'll present some work that 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 (CCS) 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.
The above negative result is in sharp contrast to the second one that,
time permitting, I'll discuss in this talk. Namely, I'll argue that
split-2 bisimulation equivalence (a notion of bisimulation based on
the idea that actions have observable beginnings and endings) does
afford a finite equational axiomatization over the process algebra
mentioned above. Thus, unlike for standard strong bisimilarity, the
addition of Hennessy's merge to CCS is sufficient for the finite
equational axiomatization of parallel composition modulo this
non-interleaving equivalence.
This is joint work with Wan Fokkink (Free University of Amsterdam and
CWI, NL), Anna Ingolfsdottir (BRICS, Aalborg University, and
University of Iceland) and Bas Luttik (Technical University of
Eindhoven, NL) that is reported in the papers
L. Aceto, W. J. Fokkink, A. Ingolfsdottir and B. Luttik.
CCS with Hennessy's Merge has no Finite Equational Axiomatization.
BRICS Report RS-03-34, November 2003.
To appear in Theoretical Computer Science.
URL: http://www.brics.dk/RS/03/34
L. Aceto, W. J. Fokkink, A. Ingolfsdottir and B. Luttik.
Split-2 Bisimilarity has a Finite Axiomatization over CCS with Hennessy's
Merge. BRICS Report RS-04-1, January 2004.
URL: http://www.brics.dk/RS/04/1
I will also try to discuss some open problems that are closely related
to the topic of this talk, and that have been keeping us busy for a
while.