The nonexistence of finite axiomatisations for CCS congruences

4 December 2002

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 142-153
https://doi.org/10.1109/lics.1990.113741

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.

Keywords

This publication has 10 references indexed in Scilit:

The importance of the left merge operator in process algebras
Published by Springer Nature ,2005
Concurrency and automata on infinite sequences
Published by Springer Nature ,2005
Unique decomposition of processes
Theoretical Computer Science, 1993
Extensional equivalences for transition systems
Acta Informatica, 1987
On the semantics of concurrency: Partial orders and transition systems
Published by Springer Nature ,1987
Modeling concurrency with partial orders
International Journal of Parallel Programming, 1986
Algebra of communicating processes with abstraction
Theoretical Computer Science, 1985
Testing equivalences for processes
Theoretical Computer Science, 1984
Process algebra for synchronous communication
Information and Control, 1984
A Calculus of Communicating Systems
Lecture Notes in Computer Science, 1980