نتایج منظم برای کانال های FIFO

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)a(b+c)∗ is piecewise (but not polynomially bounded). These languages correspond to the Σ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 Σ2, not only to the lossy systems of Π1. Moreover, we show that Σ2 also describes limits in a class of FIFO systems that include iterations of arbitrary sets of simultaneous read and write operations.

We show that the class of piecewise languages are important to the understanding of finite-state systems that communicate over unbounded channels. Piecewise languages are regular languages that are finite unions of simply piecewise languages of the form M∗ 1 a1 · · ·M∗ nanM∗ n+1, where the Mi’s are subsets of a finite alphabet Σ of symbols and the ai’s are elements of Σ. To express the language consisting of
(the empty word), we allow n = 0. Note that if Mi = {}, then M∗ i is
; also, it can be seen that replacing the ai’s by finite strings of ui’s does not affect the class of languages defined. Piecewise languages can also be characterized as Σ2-languages of the quantifier alternation hierarchy for first-order logic on words over the signature (<, a(·)a∈Σ) or as the level 11 2 of the concatenation hierarchy of Straubing- Th´erien, see [19]. More simply, piecewise languages are those recognized by nondeterministic automata whose only nontrivial strongly connected components are states with self-loops.

Our results for piecewise operations languages can be summarized in the following table: Channel configuration one multiple w/o conditionals multiple w acyclic comm. struct. multiple piecewise eff. piecewise eff. piecewise eff. piecewise piecewise regular eff. regular eff. regular non-regular non-regular The row is the type of language describing initial channel content and the column is the type of the channel configuration. In all cases, we assume that the operation language is itself piecewise. As indicated, our results for extracting the regular or piecewise limit language are generally effective (algorithms are implicit in our proofs).