Comete-Parsifal Seminar Thu Jul 12, 15:00 LIX, Ecole Polytechnique Salle de Reunion, LIX http://www.lix.polytechnique.fr/comete/seminar/ Lien pour accéder au campus : http://www.polytechnique.edu/accueil/vie-sur-le-campus/acceder-au-campus/ Link to reach the campus: http://www.polytechnique.edu/home/life-on-campus/arriving-on-campus/ Title: Verification of distributed probabilistic systems under partial information. Speaker: 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.