A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable in several conference and journal papers for either mailboxes or peer-to-peer communications, thanks to a form of small model property. In this paper, we show that this small model property does not hold neither for mailbox communications, nor for peer-to-peer communications, therefore the decidability of synchronizability becomes an open question. We close this question for peer-to-peer communications, and we show that synchronizability is actually undecidable. We show that synchronizability is decidable if the topology of communications is an oriented ring. We also show that, in this case, synchronizability implies the absence of unspecified receptions and orphan messages, and the channel-recognizability of the reachability set.

翻译：一组通信有限状态机是可同步的，当且仅当在FIFO异步通信与汇合同步通信两种模式下，其发送迹语义（即系统能执行的所有发送序列的集合）保持一致。此前多篇会议与期刊论文声称，借助某种小模型性质，该性质对于邮箱通信或点对点通信是可判定的。本文证明该小模型性质既不能适用于邮箱通信，也不能适用于点对点通信，因此可同步性的可判定性成为开放问题。我们针对点对点通信解决了该问题，证明可同步性实际上是不可判定的。同时证明，当通信拓扑为有向环时，可同步性是可判定的；在此情形下，可同步性还蕴含无未指定接收、无孤儿消息，且可达集具有信道可识别性。