Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

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

Authors: Moller, F.


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


    author = 	 {Moller, F.},
    title = 	 {The nonexistence of finite axiomatisations for CCS congruences},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {142--153},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}