Communicating finite-state machines (CFMs) are a Turing powerful model of asynchronous message-passing distributed systems. In weakly synchronous systems, processes communicate through phases in which messages are first sent and then received, for each process. Such systems enjoy a limited form of synchronization, and for some communication models, this restriction is enough to make the reachability problem decidable. In particular, we explore the intriguing case of p2p (FIFO) communication, for which the reachability problem is known to be undecidable for four processes, but decidable for two. We show that the configuration reachability problem for weakly synchronous systems of three processes is undecidable. This result is heavily inspired by our study on the treewidth of the Message Sequence Charts (MSCs) that might be generated by such systems. In this sense, the main contribution of this work is a weakly synchronous system with three processes that generates MSCs of arbitrarily large treewidth.
翻译:通信有限状态机(CFMs)是异步消息传递分布式系统中具有图灵完备能力的模型。在弱同步系统中,进程通过阶段进行通信:每个进程先发送消息,再接收消息。此类系统具有有限形式的同步性,对于某些通信模型,这一限制足以使可达性问题可判定。特别地,我们探究了点对点(FIFO)通信这一有趣案例:已知四进程系统的可达性不可判定,而两进程系统可判定。我们证明,三进程弱同步系统的配置可达性问题是不可判定的。该结论深受我们对可能由此类系统生成的消息序列图(MSCs)树宽研究的启发。由此,本文的主要贡献在于构造了一个能生成任意大树宽MSCs的三进程弱同步系统。