13:00
14:00

We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends).

A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. We know from previous results that reachability is PSPACE-complete for synchronizable systems.

In this talk we show that we can check if a mailbox system is
synchronizable thanks to a novel automata-based approach. From this we get that checking synchronizability is PSPACE-complete. The same question is undecidable under peer-to-peer semantics. We also show that model-checking synchronizable systems for a natural subclass of regular
properties is a PSPACE-complete problem.

Joint work with Anca Muscholl & Grégoire Sutre.

salle 178, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159