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). 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）。