Regularity Results for FIFO Channels

FIFO channel systems, in which messages between processes are cached in queues, are fundamental to the modeling of concurrency. A great deal of effort has gone into identifying scenarios where reasoning about such systems is decidable, often through establishing that the language of all channel contents is regular. Most prior results in this area focus on the effect of repetitions of individual operations sequences or they constrain the channels either to be lossy or to be polynomially bounded (that is, the number of words of a given length describing channel contents is bounded by a polynomial).We focus on piecewise languages for both describing operations and channel contents. Piecewise languages restrict the Kleene star operation to be applied to sets of letters only. For example, a(b+c)* is piecewise (but not polynomially bounded). These languages correspond to the Sigma(2) class of the first-order quantifier hierarchy. It is already known that piecewiseness plays a key role in establishing regularity results about parameterized systems subjected to rewritings according to semi-commutation rules.In this paper, we show that piecewiseness is central to the understanding of FIFO channel systems. Our contribution is to study the effect of iterating sets of operations, while extending and unifying previous work on both lossy and perfect FIFO systems. In particular, we show that well-quasi-orderings are important to Sigma(2), not only to the lossy systems of Pi(1). Moreover, we show that Sigma(2) also describes limits in a class of FIFO systems that include iterations of arbitrary sets of simultaneous read and write operations.