Paper: The nonexistence of finite axiomatisations for CCS congruences (at LICS 1990)

Authors: Faron Moller

Abstract

Equatorial axiomatizations for congruences over a simple sublanguage of R. Milner's (1980) process algebra CCS (calculus of communicating systems) are examined. It is shown that no finite set of equational axioms can completely characterize any reasonably defined congruence which is at least as strong as Milner's strong congruence. In the case of strong congruence, this means that the expansion theorem of CCS cannot be replaced by any finite collection of equational axioms. Moreover, the author isolates a source of difficulty in axiomatizing any reasonable noninterleaving semantic congruence, where the expansion theorem fails to hold

BibTeX

  @InProceedings{Moller-Thenonexistenceoffi,
    author = 	 {Faron Moller},
    title = 	 {The nonexistence of finite axiomatisations for CCS congruences},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {142--153},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }