BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:499a0feb-a61d-4dcf-8bbd-bcb54ce48526
X-WR-CALNAME:GT AlgoDist\, «Verification of Population Protocols with Unord
 ered Data»\, Corto Mascle
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20261025T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20241027T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20251026T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
RDATE:20260329T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:499a0feb-a61d-4dcf-8bbd-bcb54ce48526
DTSTAMP:20260921T221303Z
CLASS:PUBLIC
DESCRIPTION:Corto Mascle (LaBRI)\n\nTitle: Verification of Population Proto
 cols with Unordered Data\n\nAbstract:\n\nPopulation protocols are a well-s
 tudied model of distributed computation in which a crowd of anonymous fini
 te-state agents communicate via pairwise interactions. Together they decid
 e whether their initial configuration\, i.e.\, the initial distribution of
  agents in each state\, satisfies a property. We will start with a reminde
 r on Population protocols.\n\nPopulation protocols with unordered data (PP
 UD) is an extension introduced by Blondin and Ladouceur (ICALP'23) where p
 rocesses carry a piece of data from an infinite data domain. We consider t
 he decidability and complexity of formally verifying these protocols. We s
 how that checking if a PPUD is well-specified\, i.e.\, whether it correctl
 y computes some function\, is undecidable in general. By contrast\, we con
 sider a  subclass of PPUD\, called Immediate-Observation\, on which the pr
 oblem is decidable. Moreover\, we exhibit a large yet natural class of pro
 blems on IOPPUD\, which are all decidable in EXPSPACE. We will also see so
 me intriguing open problems on this model.\n\n\nhttps://algodist.labri.fr/
 index.php/Main/GT\n\nImport automatique depuis https://webmel.u-bordeaux.f
 r/home/bf-labri.ca@u-bordeaux.fr/gt.algo-dist.ics par sync_icals_to_drupal
 .py pour gt-algodist
DTSTART;TZID=Europe/Paris:20241106T110000
DTEND;TZID=Europe/Paris:20241106T120000
LOCATION:LaBRI salle 178 - lien visio https://webconf.u-bordeaux.fr/b/arn-4
 tr-7gp
SEQUENCE:0
SUMMARY:GT AlgoDist\, «Verification of Population Protocols with Unordered 
 Data»\, Corto Mascle
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR