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

This paper studies reduction congruence for the asynchronous pi-calculus with timers and derives several alternative characterisations, one of them being a labelled asynchronous bisimilarity. These results are generalised to an asynchronous pi-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" explains the problem.

Extended abstract: ps.gz, pdf. Bibtex.

$Id: index.html,v 1.10 2007/01/18 15:01:12 mberger Exp $