通信有限状态机的可同步性是不可判定的

若一个通信有限状态机系统的发送轨迹语义（即它能执行的发送序列集合）在其通信为 FIFO 异步与仅为会合同步时相同，则该系统是可同步的。得益于一种小模型性质，该性质曾在多个会议与期刊论文中被声称对于邮箱通信或对等通信是可判定的。本文中，我们表明该小模型性质对于邮箱通信和对等通信均不成立，因此可同步性的可判定性成为一个开放问题。我们关闭了对等通信的这一问题，并表明可同步性实际上是不可判定的。我们表明，若通信拓扑为有向环，则可同步性是可判定的。我们还表明，在此情形下，可同步性意味着不存在未指定接收与孤儿消息，以及可达集的通道可识别性。