×

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.

MSC:

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