Date and Time: Thursday, 29 September 2011, 15:50 - 16:45

Location: HG 6.96

Speaker: Pedro D'Argenio (National University of Cordoba)

Title: Model Checking of Distributed Probabilistic Systems

Abstract:

Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other (and hence arbitrary schedulers may result too powerful). In this talk I will revisit probabilistic model checking under a restricted set of schedulers which properly encode the behavior of nondeterminisim of distributed probabilistic systems induced by the interleaving of components. I will discuss decidability issues, algorithms and tools for model checking as well as the impact of this new approach on security protocols.