Proving Non-finite Axiomatizability Results Via Reductions

I recently completed the writing of two papers before the final rush towards ICALP 2008. The first of these papers, in chronological order, is

Luca Aceto, Wan Fokkink, Anna Ingolfsdottir and MohammadReza Mousavi. Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras. Technical Report CSR-08-05, TU/Eindhoven, February 2008.

The general setting for the work reported in this paper is that of process algebras, which are prototype languages for the description of reactive systems. Since these languages may be used for describing specifications of process behaviour as well as their implementations, an important ingredient in their theory is a notion of equivalence or approximation between process descriptions. The equivalence between two terms in a process algebra indicates that, although possibly syntactically different, these terms describe essentially the same behaviour. Behavioural equivalences are therefore typically used in the theory of process algebras as the formal yardstick by means of which one can establish the correctness of an implementation with respect to a given specification.

In the light of the algebraic nature of process algebras, a natural question is whether the chosen notion of behavioural equivalence or approximation can be axiomatized by means of a finite collection of equations. The first negative results concerning finite axiomatizability of process algebras go back to the Ph.D. thesis of Faron Moller. Since then, several other non-finite axiomatizability results have been obtained for a wide collection of very basic process algebras; see here for a survey of such results dated mid-2005.

In general, results concerning (non-)finite axiomatizability are very vulnerable to small changes in, and extensions of, the formalism under study. Furthermore, proofs of non-finite axiomatizability results in the concurrency-theory literature are extremely delicate, rather long and error-prone. Hence, it would be useful to find some general techniques that can be used to prove non-finite axiomatizability results. Such a general theory would allow one to relate non-finite axiomatizability theorems for different formalisms, and spare researchers (some of) the delicate technical analysis needed to adapt the proofs of such results. The search for such general results is what inspired our research leading to this paper.

In the aforementioned paper, we present a theorem offering a general technique that can be used to prove non-finite axiomatizability results, and present some of its applications within concurrency theory. In this theorem, we give sufficient criteria to obtain new non-finite axiomatizability results from known ones.

The technique we propose is based on a variation on the classic idea of reduction mappings, which underlies the proofs of many classic undecidability results in computability theory and of lower bounds in complexity theory. In this setting, reductions are translations between languages that preserve sound (in)equations and (in)equational proofs over the source language, and reflect families of (in)equations responsible for the non-finite axiomatizability of the target language. In other words, the existence of a reduction shows that

• "nasty" families of (in)equations over the target language are also present in the source language, and
  
• if they were provable by means of a finite collection of valid (in)equations in the source language, they would also be "finitely provable" in the target language.
  

We show the applicability of our reduction-based technique by obtaining seven, to our knowledge novel, non-finite axiomatizability results for timed and stochastic process algebras. We also investigate some limitations of our approach. In particular, we show that prebisimilarity is not finitely based over CCS with the divergent process Omega, but that this result cannot be proved by a reduction to the non-finite axiomatizability of CCS modulo bisimilarity.

There are a few promising areas of further research in this area, and we are currently exploring some of them (ICALP organization and other tasks permitting).

I'll write a few lines on the second paper soon, but those of you who are interested in looking at it may find it here.