On Network Topologies and the Decidability of Reachability Problem

摘要

We consider models of distributed systems where processes communicate by means of point-to-point (unbounded) channels. The processes have a finite set of control states whose dynamics is given by a finite state automaton. They may sometimes have auxiliary storage like stacks. They may sometimes have variables storing values from an unbounded data domain. The channels may have access policies, like first-in first-out (queue). The channel may be assumed to be reliable or unreliable (lossy channel). The channels may be allowed to transmit only messages coming from a finite set, or may be allowed to transmit elements from an infinite set. The processes and the channels may be arranged in particular topologies, for example like a tree or a star. We view a topology as a node and edge labelled directed graph, where nodes represent the processes, and the directed edges represents the channels between them. The node labels describe the features of each process, and the edge label represents the assumptions on the channel. We consider local control state reachability on a single process. That is, given a distributed system over a topology, and a specific control state of a specific process, is it possible to ever reach a configuration where the specific process is in the specific control state. This problem is in general undecidable. We present a quick survey of the decidability status of this problem across different topologies.