一句话：证明 peer-to-peer 通信有限状态机的可同步性不可判定，并给出有向环拓扑下可判定
通信有限状态机系统的可同步性指其发送迹语义在 FIFO 异步通信与 rendez-vous 同步通信下相同。此前多篇会议和期刊论文借助小模型性质声称该性质对 mailbox 或 peer-to-peer 通信可判定。本文首先证明该小模型性质在两种通信方式下均不成立，使可判定性成为开放问题；随后针对 peer-to-peer 通信证明可同步性实际上不可判定，从而关闭该问题。作者还证明当通信拓扑是有向环时可同步性可判定，并说明此时可同步性蕴含不存在未指定接收和孤儿消息，且可达集具有 channel-recognizability。
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.
@article{paperbot2161,
title = {Synchronizability of Communicating Finite State Machines is not Decidable},
author = {Alain Finkel and Etienne Lozes},
journal = {Logical Methods in Computer Science},
volume = {Volume 19, Issue 4},
year = {2023},
doi = {10.46298/lmcs-19(4:33)2023}
}