Timed, Distributed, Probabilistic, Typed Processes (with Nobuko Yoshida )

This paper studies types and probabilistic bisimulations for a timed $\pi$-calculus as an effective tool for a compositional analysis of probabilistic distributed behaviour. The types clarify the role of timers as an interface between non-terminating and terminating communication for guaranteeing distributed liveness. We add message-loss probabilities to the calculus, and introduce a notion of approximate bisimulation that discards transitions below a certain specified probability threshold. We prove this bisimulation to be a congruence, and use it for deriving quantitative bounds for practical protocols in distributed systems, including timer-driven message-loss recovery and the Two-Phase Commit protocol.

extended abstract: pdf. Status: published (bibtex).

$Id: index.html,v 1.5 2007/08/23 16:57:41 mberger Exp$