Verification of distributed probabilistic systems under partial information

by Dr. Sergio Giro

Abstract
In the verification of systems that involve probabilities, it is crucial to study qualitative properties concerning the probability of certain events as, for instance, 'the probability that a failure occurs is less that 0.01'. In case the system under consideration is distributed, each of the components of the system might have a partial view of the information available to other components. The analysis of these systems is carried out by considering 'distributed adversaries' with restricted observations. In this talk I will summarise six years of research on automatic verification of distributed probabilistic systems. On the negative side, we proved the verification problem to be undecidable in general and NP-complete for some restricted systems. Nevertheless, we also introduced some techniques for overestimation of worst-case probabilities, and showed that the concept of distributed adversaries can be used to improve existing techniques such as partial order reduction.

Bio
Sergio holds an MSc and a PhD in Computer Science, both obtained at National Universities in Argentina, with a strong focus on formal methods, logic and compilers. After serving as a Research Assistant in Oxford University in the area quantitative analysis of distributed systems, he joined Google for 4 years, working on distributed data processing and analysis applied to a variety of problems including demand forecast, fraud detection and development of Java security libraries for Android.