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 anonyous reviewer found a rather clever
counterexample to my Theorem 25 (the labelled characterisation of the
maximal sound theory). That does not influence the rest of the
development, as Theorem 25 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 ps.gz and pdf files below have not yet been
modified. I will update the thesis when I have some more time. For
now, my *Reply to referees* below explains the problem.

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