Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras

L. Aceto, W. Fokkink, A. Ingolfsdottir, M. R. Mousavi. Proceedings of the 5th IFIP International Conference on Theoretical Computer Science (TCS'08), Milano, Italy, Springer, September 2008.

Abstract

This paper presents a general technique for obtaining new results pertaining to the non-finite axiomatizability of behavioural (pre)congruences over process algebras from old ones. The proposed technique is based on a variation on the classic idea of reduction mappings. In this setting, such 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.

The proposed technique is applied to obtain a number of new non-finite axiomatizability theorems in process algebra via reduction to Moller's celebrated non-finite axiomatizability result for CCS. The limitations of the reduction technique are also studied. In particular, it is shown 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.

An extended version of this paper appeared as: Technical Report CSR-08-05, Department of Computer Science, Eindhoven University of Technology, February 2008.

@TechRep{MousaviTechRep08-05,
    author      = "Aceto, Luca and Fokkink, Wan and Ingolfsdottir, Anna and Mousavi, MohammadReza",
    title       = "Lifting Non-Finite Axiomatizability Results to Extensions of Process Algebras",
    number      = "CSR-08-05",
    school      = "Department of Computer Science, Eindhoven University of Technology",
    year        = "2008"
}