zbMATH — the first resource for mathematics

Algebraic theories for name-passing calculi. (English) Zbl 0836.03020
Summary: In a theory of processes the names are atomic data items which can be exchanged and tested for identity. A well-known example of a calculus for name-passing is the \(\pi\)-calculus, where names are additionally used as communication ports. We provide complete axiomatisations of late and early bisimilarity equivalences in such calculi. Since neither of the equivalences is a congruence we also axiomatise the corresponding largest congruences. We consider a few variations of the signature of the language; among these, a calculus of deterministic processes which is reminiscent of sequential functional programs with a conditional construct. Most of our axioms are shown to be independent. The axiom systems differ only by a few simple axioms and reveal the similarities and the symmetries of the calculi and the equivalences.

03B70 Logic in computer science
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI