基于自动机的同步邮箱通信方法
An automata-based approach for synchronizable mailbox communication
AI总结：
本文通过自动机方法研究了无大小限制轮次下邮箱通信系统的同步性判定问题，证明该问题为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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
