Weakly synchronous systems with three machines are Turing powerful

要約

通信有限状態マシン (CFM) は、非同期メッセージ パッシング分散システムの強力なチューリング モデルです。
弱同期システムでは、プロセスは、プロセスごとにメッセージが最初に送信され、次に受信されるフェーズを通じて通信します。
このようなシステムでは、限られた形式の同期が利用されており、一部の通信モデルでは、この制限は到達可能性の問題を決定可能にするのに十分です。
特に、p2p (FIFO) 通信の興味深いケースを検討します。この場合、到達可能性の問題は 4 つのプロセスでは決定不可能であるが、2 つのプロセスでは決定可能であることが知られています。
3 つのプロセスからなる弱い同期システムの構成到達可能性の問題は決定不可能であることを示します。
この結果は、そのようなシステムによって生成される可能性のあるメッセージ シーケンス チャート (MSC) のツリー幅に関する私たちの研究から大きく影響を受けています。
この意味で、この研究の主な貢献は、任意に大きなツリー幅の MSC を生成する 3 つのプロセスを備えた弱同期システムです。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google