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