一句话：提出自动机方法，证明无轮大小限制的邮箱通信系统可同步性判定是 Pspace 完全。
本文重新审视基于轮次通信的有限状态通信系统，但采用邮箱语义，即每个进程拥有一个 FIFO 缓冲区，而非每对进程一个缓冲区。若任一执行都能被重新调度为等价的轮次序列（先发送后接收，且接收与发送同轮），则系统称为可同步。已有工作多假设轮次大小固定。本文的主要贡献是：对于轮次大小不受限制的邮箱通信系统，判定其是否符合轮次通信策略的问题为 Pspace 完全。为此作者提出一种新的基于自动机的方法，并借此确定先前文献中若干相关问题的精确复杂度同为 Pspace。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2407-06968,
title = {An automata-based approach for synchronizable mailbox communication},
author = {Romain Delpy and Anca Muscholl and Grégoire Sutre},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:24)2026}
}