order that reflects a chronological succession of events, it represents an execution of a sequential system. Apart from being a natural concept in itself, FO logic over words enjoys manifold characterizations. It defines exactly the star-free languages and coincides with recognizability by aperiodic monoids or natural subclasses of finite (B[ü]{}chi, respectively) automata (cf.[@DiGa08Thomas; @Tho97handbook] for overviews). Moreover, linear-time temporal logics are usually measured against their expressive power with respect to FO logic. For example, LTL is considered the yardstick temporal logic not least due to Kamp’s famous theorem, stating that LTL and FO logic are expressively equivalent [@Kamp68].

While FO logic on words is well understood, a lot remains to be said once concurrency enters into the picture. When several processes communicate through, say, unbounded first-in first-out (FIFO) channels, events are only partially ordered and a behavior, which is referred to as a *message sequence chart (MSC)*, reflects Lamport’s happened-before relation: an event $e$ happens before an event $f$ if, and only if, there is a “message flow” path from $e$ to $f$ [@Lamport78]. *Communicating finite-state machines* (CFMs) [@Brand1983] are to MSCs what finite automata are to words: a canonical model of finite-state processes that communicate through unbounded FIFO channels. 