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.