2 April 2004A FOSSACS 2004 Paper by Wan Fokkink and Sumit Naim
Yesterday Wan Fokkink (who is, after Anna Ingólfsdóttir, the co-author with whom I have written more papers) delivered a talk at FOSSACS 2004 entitled On finite alphabets and infinite bases: from ready pairs to possible worlds. This FOSSACS paper answers an open problem raised by Jan Friso Groote in his paper
A New Strategy for Proving omega-Completeness applied to Process Algebra. CONCUR 1990: 314-331,
namely whether readiness and ready trace semantics afford finite omega-complete axiomatizations over the language BCCSP with a finite action set of cardinality at least two. (The answer is positive for singleton or infinite action sets.) In fact, Wan and Sumit Nain show more, viz. that no congruence over the language BCCSP that is included in possible worlds equivalence, and includes ready trace equivalence, affords a finite omega-complete equational axiomatization. This is a strong result that offers a negative answer to the problem raised by Groote.
The paper is written concisely and clearly. The proof techniques used by the authors in establishing their main result are ingenious and highly non-trivial. I can vouch that the type of negative results presented by the authors in this contribution are not easy to prove, even for tiny process languages like BCCSP. I warmly recommend that paper to readers interested in the equational logic of processes.
I am fascinated by non-finite axiomatizability results as those presented in the paper by Wan and Sumit Nain. I hope one day to write a survey of this type of results in process algebra, and that I will be able to contribute to this line of research in joint work with Anna, Wan and whoever else may be interested.
Last modified: Friday, 02-Apr-2004 14:46:46 CEST.