BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:ffe78081-5dff-490b-a4d5-dbe96de2221d
X-WR-CALNAME:[MTV] Romain Delpy (LaBRI) - An automata based approach for sy
 nchronizable mailbox communication
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20260329T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20231029T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20241027T030000
RDATE:20251026T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20240331T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20250330T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:ffe78081-5dff-490b-a4d5-dbe96de2221d
DTSTAMP:20260404T213451Z
CLASS:PUBLIC
DESCRIPTION:We revisit finite-state communicating systems with round-based 
 communication under mailbox semantics. Mailboxes correspond to one FIFO bu
 ffer per process (instead of one buffer per pair of processes in peer-to-p
 eer systems). Round-based communication corresponds to sequences of rounds
  in which processes can first send messages\, then only receive (and recei
 ves must be in the same round as their sends).\n\nA system is called synch
 ronizable if every execution can be re-scheduled into an equivalent execut
 ion that is a sequence of rounds. We know from previous results that reach
 ability is PSPACE-complete for synchronizable systems.\n\nIn this talk we 
 show that we can check if a mailbox system is \nsynchronizable thanks to a
  novel automata-based approach. From this we get that checking synchroniza
 bility is PSPACE-complete. The same question is undecidable under peer-to-
 peer semantics. We also show that model-checking synchronizable systems fo
 r a natural subclass of regular\nproperties is a PSPACE-complete problem.
 \n\nJoint work with Anca Muscholl & Grégoire Sutre.
DTSTART;TZID=Europe/Paris:20240627T130000
DTEND;TZID=Europe/Paris:20240627T140000
LOCATION:salle 178\, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Romain Delpy (LaBRI) - An automata based approach for synchro
 nizable mailbox communication
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
