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异步通信与汇合同步通信下具有相同的发送迹语义(即其可执行发送序列的集合),则称该系统是可同步化的。在多个会议和期刊论文中,该性质被断言为可判定(针对邮箱通信或对等通信),其依据是一种小模型性质。本文证明,该小模型性质对邮箱通信和对等通信均不成立,因此可同步化的可判定性成为开放问题。我们解决了对等通信情形下的该问题,证明可同步化实际上是不可判定的。当通信拓扑为有向环时,可同步化是可判定的。我们还证明,在此情形下,可同步化蕴含无未指定接收与孤儿消息,且可达集具有信道可识别性。