Algorithmic Analysis of Piecewise FIFO Systems

摘要

Systems consisting of several components that communicate via unbounded perfect FIFO channels (i.e. FIFO systems) arise naturally in modeling distributed systems. Despite well-known difficulties in analyzing such systems, they are of significant interest as they can describe a wide range of communication protocols. Previous work has shown that piecewise languages play an important role in the study of FIFO systems. In this paper, we present two algorithms for computing the set of reachable states of a FIFO system composed of piecewise components. The problem of computing the set of reachable states of such a system is closely related to calculating the set of all possible channel contents, i.e. the limit language. We present new algorithms for calculating the limit language of a system with a single communication channel and a class of multi-channel system in which messages are not passed around in cycles through different channels.We show that the worst case complexity of our algorithms for single-channel and important subclasses of multichannel systems is exponential in the size of the initial content of the channels.