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. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is Pspace-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (Pspace) of several questions considered in previous literature.

翻译：我们重新审视了在邮箱语义下基于轮次通信的有限状态通信系统。邮箱对应于每个进程一个先进先出缓冲区（而非对等系统中每对进程一个缓冲区）。基于轮次的通信对应于一系列轮次，其中进程可先发送消息，随后仅接收消息（且接收必须与发送处于同一轮次）。若系统的每次执行均可重排为等价的轮次序列执行，则称该系统是可同步的。先前研究主要考虑轮次大小固定的情形。我们的主要贡献在于证明：在无轮次大小限制的条件下，判定邮箱通信系统是否符合基于轮次策略的问题是PSPACE完全的。为此，我们提出了一种新颖的基于自动机的方法，该方法同样能够确定先前文献中若干问题的精确复杂度（PSPACE）。