Distributed Liveness and Timers for Mobile Processes (with N. Yoshida)

Abstract. We propose a typing system for the timed distributed pi-calculus and study applications to distributed liveness in the presence of message loss. The typing rules clarify the role of timers as an interface between affine and linear channels for guaranteeing distributed liveness. As applications of our types, we study a class of simple distribution algorithms that take processes, running at one location, and distribute them, so the failure-free behaviour is preserved. Finally, we add message-loss probability to our model and derive quantitative bounds for simple processes which recover message loss by timers.

Downloads: This work is superseded by Timed, Distributed, Probabilistic, Typed Processes. BibTeX