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.

翻译：本文重新研究了邮箱语义下基于轮次的有限状态通信系统。邮箱对应每个进程拥有一个FIFO缓冲区（而非点对点系统中每对进程共享一个缓冲区）。基于轮次的通信要求进程先发送消息，随后仅接收消息（且接收操作必须与发送操作处于同一轮次）。若系统的所有执行过程均可重新调度为等效的轮次序列，则称该系统具有同步性。既往研究主要关注固定轮次规模的场景。本文的核心贡献在于证明以下问题的Pspace完备性：在无轮次规模限制条件下，判断邮箱通信系统是否遵循基于轮次的通信策略。为此我们提出了一种创新的自动机方法，该方法同时能精确判定既往文献中多个问题的计算复杂度（Pspace）。