Basic Theory of Reduction Congruence for Two Timed Asynchronous π-Calculi

**Abstract.**
We study reduction congruence, the most widely used notion of
equality for the asynchronous π-calculus with timers, and derive
several alternative characterisations, one of them being a labelled
asynchronous bisimilarity. These results are adapted to an
asynchronous π-calculus with timers, locations and message failure. In
addition we investigate the problem of how to distribute value-passing
processes in a semantics-preserving way.

**Update (5 May 2005).** An anonymous reviewer found a rather clever
**counterexample** to the labelled characterisation of the
maximal sound theory, in other words: **it is wrong!**
That does not influence the rest of the
development, as it is not really used anywhere. In particular,
the labelled bisimilarities are still sound, but I'm currently
investigating the source of the problem and will publish the
forensics. It seems that the problem can be overcome. Moreover, the
counterexample is such that it is irrelevant to the verification of
realistic programs. The pdf file below has not yet been
modified. I will update the paper when I have some more time. For
now, my *Reply to referees* below explains the problem.

**Downloads:** Short version. Reply to referees. BibTeX