Parameterized Verification of Population Protocols

Séminaire
  • Quand ? 24/10/2018 à partir de 13:30 (America/New_York / UTC-400)
  • Où ? Au local D4-2011 de la Faculté des sciences
  • Nom du contact
  • Participants Stefan Jaax, doctorant de l'Université technique de Munich
  • Ajouter l'événement au calendrier iCal

Résumé : Population protocols (Angluin et al., 2004) are a parameterized model of distributed computation by populations of anonymous, identical, and mobile finite-state agents. Initially introduced to model networks of passively mobile sensors, they also capture the essence of distributed computation in trust propagation or chemical reactions. The talk provides a gentle introduction to population protocols, followed by a demonstration of Peregrine - a parametric verification tool for population protocols developed by the chair for Foundations of Software Reliability and Theoretical Computer Science at Technical University of Munich. Peregrine can automatically verify a large subclass of population protocols, independent of population size. Peregrine also comes with simulation capabilities and support for error diagnostics.

The talk will shine light on the mathematical foundations of Peregrine's verification capabilities and provides an outlook on potential future extensions.

Présentation en anglais

Toutes les personnes intéressées sont cordialement invitées.