Weakly synchronous systems with three machines are Turing powerful *

Description

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.

Abstract (French)

Les machines à états finis communicantes (CFM) sont un modèle puissant de systèmes distribués à transmission de messages asynchrones. Dans les systèmes faiblement synchrones, les processus communiquent via des phases dans lesquelles les messages sont d'abord envoyés puis reçus, pour chaque processus. De tels systèmes bénéficient d'une forme limitée de synchronisation, et pour certains modèles de communication, cette restriction est suffisante pour rendre le problème d'accessibilité décidable. En particulier, nous explorons le cas intrigant de la communication p2p (FIFO), pour lequel le problème d'accessibilité est connu pour être indécidable pour quatre processus, mais décidable pour deux. Nous montrons que le problème d'accessibilité de la configuration pour les systèmes faiblement synchrones de trois processus est indécidable. Ce résultat est fortement inspiré de notre étude sur la largeur arborescente des diagrammes de séquences de messages (MSC) qui pourraient être générés par de tels systèmes. En ce sens, la principale contribution de ce travail est un système faiblement synchrone à trois processus qui génère des MSC de largeur arborescente arbitrairement grande.

Additional details