This paper studies types and probabilistic bisimulations for a timed π-calculus as an effective tool for a compositional analysis of probabilistic distributed behaviour. The types clarify the role of timers as 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. © Springer-Verlag Berlin Heidelberg 2007.
CITATION STYLE
Berger, M., & Yoshida, N. (2007). Timed, distributed, probabilistic, typed processes. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4807 LNCS, pp. 158–174). Springer Verlag. https://doi.org/10.1007/978-3-540-76637-7_11
Mendeley helps you to discover research relevant for your work.