Benedikt Bollig
email: bollig@lsv.fr

Marie Fortin
email: fortin@lsv.fr

Paul Gastin
email: gastin@lsv.fr

Communicating Finite-State Machines, First-Order Logic, and Star-Free Propositional Dynamic Logic $

Keywords: communicating finite-state machines, first-order logic, happened-before relation, propositional dynamic logic

Message sequence charts (MSCs) naturally arise as executions of communicating finite-state machines (CFMs), in which finite-state processes exchange messages through unbounded FIFO channels. We study the first-order logic of MSCs, featuring Lamport's happened-before relation. To this end, we introduce a star-free version of propositional dynamic logic (PDL) with loop and converse. Our main results state that (i) every first-order sentence can be transformed into an equivalent star-free PDL sentence (and conversely), and (ii) every star-free PDL sentence can be translated into an equivalent CFM. This answers an open question and settles the exact relation between CFMs and fragments of monadic second-order logic. As a byproduct, we show that first-order logic over MSCs has the three-variable property.

Introduction

The study of logic-automata connections has ever played a key role in computer science, relating concepts that are a priori very different. Its motivation is at least twofold. First, automata may serve as a tool to decide logical theories. Beginning with the work of Büchi, Elgot, and Trakhtenbrot, who established in the early 60s the expressive equivalence of monadic second-order (MSO) logic and finite automata [START_REF] Büchi | Weak second order logic and finite automata[END_REF][START_REF] Elgot | Decision problems of finite automata design and related arithmetics[END_REF][START_REF] Trakhtenbrot | Finite automata and monadic second order logic[END_REF], the "automata-theoretic" approach to logic has been successfully applied, for example, to MSO logic on trees [START_REF] Thatcher | Generalized finite automata theory with an application to a decision problem of second-order logic[END_REF], temporal logics [START_REF] Vardi | An automata-theoretic approach to automatic program verification[END_REF], and first-order logic with two variables over words with an equivalence relation (aka data words) [BDM + 11]. Second, automata serve as models of various kind of state-based systems. Against this background, Büchi-like theorems lay the foundation of synthesis, i.e., the process of transforming high-level specifications (represented as logic formulas) into faithful system models. In this paper, we provide a Büchi theorem for communicating finite-state machines (CFMs), which are a classical model of concurrent message-passing systems.

Context and Known Results

Let us give a brief account of what was already known on the relation between logic and automata (without claim of completeness).

Finite automata. As mentioned above, Büchi, Elgot, and Trakhtenbrot proved that finite automata over words are expressively equivalent to MSO logic [START_REF] Büchi | Weak second order logic and finite automata[END_REF][START_REF] Elgot | Decision problems of finite automata design and related arithmetics[END_REF][START_REF] Trakhtenbrot | Finite automata and monadic second order logic[END_REF]. Finite automata can be considered as single finite-state processes and, therefore, serve as a model of sequential systems. Their executions are words, which, seen as a logical structure, consist of a set of positions (also referred to as events) that carry letters from a finite alphabet and are linearly ordered by some binary relation ≤. The simple MSO (even first-order) formula ∀x. a(x) =⇒ ∃y.(x ≤ y ∧ b(y)) says that every "request" a is eventually followed by an "acknowledgment" b. In fact, Büchi's theorem allows one to turn any logical MSO specification into a finite automaton. The latter can then be considered correct by construction. Though the situation quickly becomes more intricate when we turn to other automata models, Büchi theorems have been established for expressive generalizations of finite automata that also constitute natural system models. In the following, we will discuss some of them.

Data automata. Data automata accept (in the context of system models, we may also say generate) words that, in addition to the linear order ≤ and its direct-successor relation, are equipped with an equivalence relation ∼ [BDM + 11]. Positions (events) that belong to the same equivalence class may be considered as being executed by one and the same process, while ≤ reflects a sort of global control. It is, therefore, convenient to also include a predicate that connects successive events in an equivalence class. Bojańczyk et al. showed that data automata are expressively equivalent to existential MSO logic with two first-order variables [BDM + 11]. A typical formula is ¬∃x.∃y.(x y ∧ x ∼ y), which says that every equivalence class is a singleton. It should be noted that data automata scan a word twice and, therefore, can hardly be seen as a system model. However, they are expressively equivalent to class-memory automata, which distinguish between a global control (modeling, e.g., a shared variable) and a local control for every process [START_REF] Björklund | On notions of regularity for data languages[END_REF].

Asynchronous automata. Unlike finite automata and data automata, asynchronous automata are models of concurrent shared-memory systems, with a finite number of processes. In his influential paper [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF], Lamport postulated that events in an execution of a distributed system are partially ordered by what is commonly referred to as the happened-before or causal-precedence relation, a fundamental concept in distributed computing [START_REF] Attiya | Distributed Computing: Fundamentals, Simulations and Advanced Topics[END_REF][START_REF]Distributed Algorithms for Message-Passing Systems[END_REF][START_REF] Lynch | Distributed Algorithms[END_REF][START_REF] Tel | Introduction to Distributed Algorithms[END_REF]. In fact, executions of asynchronous automata are Mazurkiewicz traces [START_REF] Diekert | The Book of Traces[END_REF], where the relation ≤ is no longer a total, but a partial order. Thus, there may be parallel events x and y, for which neither x ≤ y nor y ≤ x holds. A typical logical specification is the mutual exclusion property, which can be expressed in MSO logic as ¬∃x.∃y.(CS(x) ∧ CS(y) ∧ x y) where the parallel operator x y is defined as ¬(x ≤ y) ∧ ¬(y ≤ x). The formula says that there are no two events x and y that access a critical section simultaneously. Asynchronous automata are closed under complementation [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF] so that the inductive approach to translating formulas into automata can be applied to obtain a Büchi theorem [START_REF] Thomas | On logical definability of trace languages[END_REF]. Note that complementability is also the key ingredient for MSO characterizations of nested-word automata [START_REF] Alur | Adding nesting structure to words[END_REF] and branching automata running over series-parallel posets (aka N-free posets) [START_REF] Kuske | Infinite series-parallel posets: Logic and languages[END_REF][START_REF] Bedon | Logic and branching automata[END_REF].

Communicating finite-state machines. The situation is quite different in the realm of communicating finite-state machines (CFMs), aka communicating automata or message-passing automata, where a fixed number of finitestate processes communicate by exchanging messages through unbounded FIFO channels [START_REF] Brand | On communicating finite-state machines[END_REF]. A CFM accepts/generates message-sequence charts (MSCs), which are similar to UML's sequence diagrams [START_REF] Araújo | Formalizing sequence diagrams[END_REF] and standardised by the International Telecommunication Union [START_REF]Message Sequence Chart 1999 (MSC99)[END_REF]. MSCs are equipped with 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 [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF]. Additional binary predicates connect (i) the emission of a message with its reception, and (ii) successive events executed by one and the same process. Unfortunately, the class of MSC languages accepted by CFMs is not closed under complementation [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] so that an inductive translation of MSO logic into automata must fail (in fact, CFMs are strictly less expressive than MSO logic).

There have been several attempts to overcome this problem. When channels are bounded, closure under complementation is recovered so that CFMs are expressively equivalent to MSO logic [HMK + 05, Kus03, GKM06, GKM07]. Note that, however, the corresponding proofs are much more intricate than in the case of finite automata. In the unbounded case, since MSO logic is too expressive, first-order (FO) logic is moving into focus. Actually, FO logic can be considered, in many ways, a reference specification language. Apart from being a natural concept in itself, it plays a key role in automated theorem proving and is central in the verification of reactive systems. Over words, FO logic even 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. [START_REF] Diekert | First-order definable languages[END_REF][START_REF] Thomas | Languages, automata and logic[END_REF] 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 [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF].

While FO logic on words is well understood, a lot remains to be said once message-passing concurrency enters into the picture. Actually, algebraic and automata-theoretic approaches that work for words, trees, or Mazurkiewicz traces do not carry over. On the positive side, it was shown that CFMs with unbounded channels capture FO logic (and, therefore, are expressively equivalent to existential MSO logic) when dropping the happened-before relation ≤ [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] or when restricting to two first-order variables [START_REF] Bollig | Communicating finite-state machines and two-variable logic[END_REF]. Both results rely on normal forms of FO logic, due to Hanf [START_REF] Hanf | Model-theoretic methods in the study of elementary logic[END_REF] and Scott [START_REF] Grädel | On logics with two variables[END_REF], respectively. Hanf's normal form is a boolean combination of statements of the form "neighborhood N of radius d occurs at least k times", where the neighborhood of an event e is an isomorphism type of the substructure induced by the elements that have distance at most d from e. Hanf's result requires structures of bounded degree so that the number of possible neighborhoods is actually finite. However, MSCs with the happenedbefore relation are structures of unbounded degree: Due to the happened-before relation ≤, all events on a given process have distance at most 1 from each other. To evaluate Scott's normal form, on the other hand, it is sufficient to determine the type of every event e (the type describing all events for every possible relationship with e), which can be accomplished by a CFM. However, the normal form only applies to two-variable logic, while we consider full FO logic, which, already over one process, is strictly more expressive.

It should be noted that distributed automata can also be used as acceptors of the underlying (graph) architecture. In that case, logical characterizations have been obtained in terms of MSO and modal logics [Kuu13, HJK + 15, [START_REF] Reiter | Distributed graph automata[END_REF][START_REF] Reiter | Asynchronous distributed automata: A characterization of the modal mu-fragment[END_REF]. However, in our framework, the architecture is fixed and we rather reason about the set of executions of a CFM.

Contribution

Until now, the following central problem remained open:

Can every first-order sentence, with happened-before relation and arbitrarily many variables, be transformed into an equivalent communicating finite-state machine, without any channel bounds?

In this paper, we answer the question positively. To do so, we make a detour through a variant of propositional dynamic logic (PDL) with loop and converse [START_REF] Fischer | Propositional Dynamic Logic of regular programs[END_REF][START_REF] Streett | Propositional dynamic logic of looping and converse[END_REF], which is another fundamental logic, with applications in artificial intelligence and verification [HM92, DL94, LL05, Lan06, GLL09]. Actually, we introduce star-free PDL, which serves as an interface between FO logic and CFMs. That is, there are two main tasks to accomplish: (i) Translate every FO sentence into a star-free PDL sentence.

(ii) Translate every star-free PDL sentence into a CFM.

Both parts constitute results of own interest. In particular, step (i) implies that, over MSCs, FO logic has the three-variable property, i.e., every FO sentence over MSCs can be rewritten into one that uses only three different variable names. Note that this is already interesting in the special case of words, where it follows from Kamp's theorem [START_REF] Kamp | Tense Logic and the Theory of Linear Order[END_REF]. It is also noteworthy that star-free PDL is a two-dimensional temporal logic in the sense of Gabbay et al. [START_REF] Gabbay | Expressive functional completeness in tense logic[END_REF][START_REF] Gabbay | Temporal Logic: Mathematical Foundations and Computational Aspects[END_REF]. Since every star-free PDL sentence is equivalent to some FO sentence, we actually provide a (higher-dimensional) temporal logic over MSCs that is expressively complete for FO logic.1 While step (i) is based on purely logical considerations, step (ii) builds on new automata constructions that allow us to cope with the loop operator of PDL.

Combining (i) and (ii) yields the translation from FO logic to CFMs. It follows that CFMs are expressively equivalent to existential MSO logic. Moreover, we can derive self-contained proofs of several results on channelbounded CFMs whose original proofs refer to involved constructions for Mazurkiewicz traces (cf. Section 5). In fact, we also extend these results to infinite MSCs.

Outline

In Section 2, we recall basic notions such as MSCs, FO logic, and CFMs. We also give a brief overview of what was already known on the relation between logic and CFMs. Section 3 presents star-free PDL and shows that it captures FO logic over MSCs. In Section 4, we establish the translation of star-free PDL into CFMs. As corollaries, we obtain the translation of FO sentences into CFMs and the equivalence between CFMs and existential MSO logic. Several applications of our results are presented in Section 5. In particular, we obtain known results on CFMs with existentially bounded channels as a corollary. As a reference, an overview of previously known facts is presented in Section 2.4. We conclude in Section 6.

A preliminary version of this paper has been presented at the 29th International Conference on Concurrency Theory (CONCUR'18) and is accessible at http://drops.dagstuhl.de/opus/frontdoor.php?source_opus= 9545. There, we considered finite MSCs. The present paper generalizes our results to infinite MSCs, which require several technical adjustments. Moreover, we provide full proofs as well as an application to channel-bounded CFMs.

Preliminaries

We consider message-passing systems in which processes communicate through unbounded FIFO channels. We fix a nonempty finite set of processes P and a nonempty finite set of labels Σ. For all p, q ∈ P such that p q, there is a channel (p, q) that allows p to send messages to q. The set of channels is denoted Ch.

In the following, we define message sequence charts, which represent executions of a message-passing system, and logics to reason about them. Then, we recall the definition of communicating finite-state machines and state one of our main results.

Message Sequence Charts

A message sequence chart (MSC) (over P and Σ) is a graph M = (E, →, , loc, λ) with nonempty, finite or countably infinite set E of nodes, also called events, edge relations →, ⊆ E × E, and node-labeling functions loc : E → P and λ : E → Σ. An example MSC over P = {p 1 , p 2 , p 3 } and Σ = { , , } is depicted in Figure 1. A node e ∈ E is an event that is executed by process loc(e) ∈ P. In particular, E p := {e ∈ E | loc(e) = p} is the set of events located on p. Note that E p can be finite or infinite. The label λ(e) ∈ Σ may provide more information about e such as the message that is sent/received at e or "enter critical section" or "output some value".

Edges describe causal dependencies between events:

• The relation → contains process edges. They connect successive events executed by the same process, that is, we actually have → ⊆ p∈P (E p × E p ). Every process p is sequential so that → ∩ (E p × E p ) must be the direct-successor relation of some total order on E p . We let ≤ proc := → * and < proc := → + , and we require that every event e ∈ E has a "finite past", i.e., { f ∈ E | f ≤ proc e} is finite.

• The relation contains message edges. If e f , then e is a send event and f is the corresponding receive event.

In particular, (loc(e), loc( f )) ∈ Ch. Each event is part of at most one message edge. An event that is neither a send nor a receive event is called internal. Moreover, for all (p, q) ∈ Ch and (e, f ), (e , f ) ∈ ∩ (E p × E q ), we have e ≤ proc e iff f ≤ proc f (which guarantees a FIFO behavior).

We require that → ∪ be acyclic (intuitively, messages cannot travel backwards in time). The associated partial order is denoted ≤ := (→ ∪ ) * with strict part < = (→ ∪ ) + . Actually, MSCs correspond to the space-time diagrams from Lamport's seminal paper [START_REF] Lamport | Time, clocks, and the ordering of events in a distributed system[END_REF] when we assume a single FIFO channel between each pair of processes, and ≤ is commonly referred to as the happened-before relation.

We do not distinguish isomorphic MSCs. Let MSC(P, Σ) denote the set of MSCs over P and Σ. An MSC is finite if its set of events E is finite. We denote the set of finite MSCs by MSC fin (P, Σ).

It is worth noting that, when P is a singleton, an MSC with events e 1 → e 2 → e 3 → . . . can be identified with the (finite or infinite) word λ(e 1 )λ(e 2 )λ(e 3 ) . . . over Σ.

Example 1. Consider the (infinite) MSC from Figure 1

over P = {p 1 , p 2 , p 3 } and Σ = { , , }. We have E p 1 = {e i | i ∈ N}, E p 2 = { f 0 , . . . , f 5 }, E p 3 = {g i | i ∈ N}.
The process relation is given by e i → e i+1 and g i → g i+1 for all i ∈ N, as well as f i → f i+1 for all i ∈ {0, . . . , 4}. Concerning the message relation, we have e 1 f 0 , e 4 g 5 , etc. Moreover,

e 2 ≤ f 3 , but neither e 2 ≤ f 1 nor f 1 ≤ e 2 .

MSO Logic and Its Fragments

Next, we give an account of monadic second-order (MSO) logic and its fragments. Note that we restrict our attention to MSO logic interpreted over MSCs. We fix an infinite supply V event = {x, y, . . .} of first-order variables, which range over events of an MSC, and an infinite supply V set = {X, Y, . . .} of second-order variables, ranging over sets of events. The syntax of MSO (P and Σ are fixed) is given as follows:

Φ ::= p(x) | a(x) | x = y | x → y | x y | x ≤ y | x ∈ X | Φ ∨ Φ | ¬Φ | ∃x.Φ | ∃X.Φ
where p ∈ P, a ∈ Σ, x, y ∈ V event , and X ∈ V set . We use the standard abbreviations to also include implication =⇒, conjunction ∧, and universal quantification ∀. Moreover, the relation x ≤ proc y can be defined by x ≤ y ∧ p∈P p(x) ∧ p(y). We write Free(Φ) for the set of free variables of Φ.

Let M = (E, →, , loc, λ) be an MSC. An interpretation (for M) is a mapping ν : V event ∪V set → E ∪2 E assigning to each x ∈ V event an event ν(x) ∈ E, and to each X ∈ V set a set of events ν(X) ⊆ E. We write M, ν | = Φ if M satisfies Φ when the free variables of Φ are interpreted according to ν. Hereby, satisfaction is defined in the usual manner. In fact, whether M, ν | = Φ holds or not only depends on the interpretation of variables that occur free in Φ. Thus, we may restrict ν to any set of variables that contains at least all free variables. For example, for Φ(x, y) = (x y), we have M, [x → e, y → f ] | = Φ(x, y) iff e f . For a sentence Φ ∈ MSO (without free variables), we define

L(Φ) := {M ∈ MSC(P, Σ) | M | = Φ}.
We say that two formulas Φ and Φ are equivalent, written Φ ≡ Φ , if, for all MSCs M = (E, →, , loc, λ) and interpretations ν :

V event ∪ V set → E ∪ 2 E , we have M, ν | = Φ iff M, ν | = Φ .
Let us identify two important fragments of MSO logic: First-order (FO) formulas do not make use of second-order quantification (however, they may contain formulas x ∈ X). Moreover, existential MSO (EMSO) formulas are of the form ∃X 1 . . . ∃X n .Φ with Φ ∈ FO.

Let F be MSO or EMSO or FO and let R ⊆ {→, , ≤}. We obtain the logic F [R] by restricting F to formulas that do not make use of {→, , ≤} \ R. Note that

F = F [→, , ≤]. Moreover, we let L(F [R]) := {L(Φ) | Φ ∈ F [R] is a sentence}.
As the reflexive transitive closure of an MSO-definable binary relation is MSO-definable, MSO and MSO[→, ] have the same expressive power:

L(MSO[→, , ≤]) = L(MSO[→, ]
). However, MSO[≤] (without the message relation) is strictly weaker than MSO [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF]. In fact, over totally ordered MSCs, MSO[≤] only has the expressive power of MSO logic over ordinary words, and hence of finite automata, when restricting to valid linear extensions of MSCs. This allows one to apply a classical pumping argument to finite automata to show the result.

Example 2. Let us start with an easy formula saying that an MSC is infinite. This can be expressed in FO[→] by Φ = p∈P ∃x p(x) ∧ ∀x∃y(p(x) =⇒ x → y). Thus, L(Φ) = MSC(P, Σ) \ MSC fin (P, Σ).

Example 3. We now give an FO[≤] formula that allows us to recover, at some event f , the most recent event e that happened in the past on, say, process p. More precisely, we define the predicate latest p (x, y) as x ≤ y ∧ p(x) ∧ ∀z (z ≤ y ∧ p(z)) =⇒ z ≤ x . We are interested in the MSC language where process q always maintains the latest information that it can have about p. Thus, it is defined by

Φ latest p,q = ∀x∀y.        latest p (x, y) ∧ q(y) =⇒ a∈Σ a(x) ∧ a(y)        ∈ FO[≤] .
For example, for P = {p 1 , p 2 , p 3 } and Σ = { , , }, the MSC M from Figure 1 is contained in L(Φ latest p 1 ,p 3 ). In particular, M, [x → e 5 , y → g 5 ] | = latest p 1 (x, y) and λ(e 5 ) = λ(g 5 ) = .

Communicating Finite-State Machines

In a communicating finite-state machine, each process p ∈ P can perform internal actions of the form a , where a ∈ Σ, or send/receive messages from a finite set of messages Msg. A send action a, ! q m of process p writes message m ∈ Msg to channel (p, q), and performs a ∈ Σ. A receive action a, ? q m reads message m from channel (q, p). Accordingly, we let Act p (Msg) := { a | a ∈ Σ} ∪ { a, ! q m | a ∈ Σ, m ∈ Msg, q ∈ P \ {p}} ∪ { a, ? q m | a ∈ Σ, m ∈ Msg, q ∈ P \ {p}} denote the set of possible actions of process p. Definition 1. A communicating finite-state machine (CFM) over P and Σ is a tuple A = ((A p ) p∈P , Msg, Acc) consisting of a finite set of messages Msg and a finite-state transition system A p = (S p , ι p , ∆ p ) for each process p, with finite set of states S p , initial state ι p ∈ S p , and transition relation ∆ p ⊆ S p × Act p (Msg) × S p . Moreover, we have an acceptance condition Acc, which is a positive Boolean combination of atomic conditions p, s or p, s ∞ , where p ∈ P and s ∈ S p .

Intuitively, p, s requires that process p terminates in state s (and, thus, executes only finitely many events), while p, s ∞ requires that process p enters state s infinitely often (which implies that p executes infinitely many events). This kind of "mixed" acceptance condition is quite convenient. Using positive Boolean combinations of acceptance conditions for infinite words was originally proposed in [START_REF] Emerson | Modalities for model checking: branching time logic strikes back[END_REF]. Other, syntactically different acceptance criteria have been adopted in the literature, like Büchi or Muller conditions [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF][START_REF] Bollig | Muller message-passing automata and logics[END_REF]. However, it is easily seen that they are all expressively equivalent.

Given a transition t = (s, α, s ) ∈ ∆ p , we let source(t) = s and target(t) = s denote the source and target states of t. In addition, if α = a , then t is an internal transition and we let label(t) = a. If α = a, ! q m , then t is a send transition and we let label(t) = a, msg(t) = m, and receiver(t) = q. Finally, if α = a, ? q m , then t is a receive transition with label(t) = a, msg(t) = m, and sender(t) = q.

A run ρ of A on an MSC M = (E, →, , loc, λ) ∈ MSC(P, Σ) is a mapping associating with each event e ∈ E p a transition ρ(e) ∈ ∆ p , and satisfying the following conditions:

1. for all events e ∈ E, we have label(ρ(e)) = λ(e), 2. for all →-minimal events e ∈ E, we have source(ρ(e)) = ι p , where p = loc(e), 3. for all process edges (e, f ) ∈ →, we have target(ρ(e)) = source(ρ( f )), 4. for all internal events e ∈ E, ρ(e) is an internal transition, and 5. for all message edges e f , ρ(e) and ρ( f ) are respectively send and receive transitions such that msg(ρ(e)) = msg(ρ( f )), receiver(ρ(e)) = loc( f ), and sender(ρ( f )) = loc(e).

We say that ρ is accepting if it satisfies the acceptance condition Acc, written ρ | = Acc. The relation ρ | = Acc is defined inductively. Disjunction and conjunction are interpreted as usual. Moreover, we let ρ | = p, s if either E p = ∅ and s = ι p , or E p is a nonempty finite set and s = target(ρ(e)), where e is the last event of E p . Finally, ρ | = p, s ∞ if s = target(ρ(e)) for infinitely many events e ∈ E p (which implies that E p is infinite).

The language L(A) of A is the set of MSCs M such that there exists an accepting run of A on M. Moreover, L(CFM) := {L(A) | A is a CFM}. Recall that, for these definitions, we have fixed P and Σ.

Following [HMK + 05, GKM07, Kus03], we call a CFM A = ((A p ) p∈P , Msg, Acc) deterministic if, for all processes p and transitions t 1 = (s 1 , α 1 , s 1 ) and t 2 = (s 2 , α 2 , s 2 ) of A p such that s 1 = s 2 and label(t 1 ) = label(t 2 ), the following hold:

• If t 1 and t 2 are internal transitions, then s 1 = s 2 .

• If t 1 and t 2 are send transitions such that receiver(t 1 ) = receiver(t 2 ), then s 1 = s 2 and msg(t 1 ) = msg(t 2 ).

• If t 1 and t 2 are receive transitions such that sender(t 1 ) = sender(t 2 ) and msg(t 1 ) = msg(t 2 ), then s 1 = s 2 .

Example 4. Consider the simple (deterministic) CFM A depicted in Figure 2. The set of processes is P = {p 1 , p 2 , p 3 }. Moreover, we have Σ = { , , } and Msg = { , }. Process p 1 sends messages to p 2 and p 3 . Each message can be either or , and the message sent is made "visible" in terms of Σ. Process p 2 simply forwards every message it receives to p 3 . In any case, the action is . Finally, p 3 receives and "outputs" messages from p 1 and p 2 in any order. Note that, in this example, there are no local transitions, i.e., every transition is either sending or receiving. As acceptance condition, we take Acc = p 1 , s p 1 ∞ , which says that p 1 executes infinitely many events.

The CFM A can be seen as a first (naïve) attempt to solve the problem described in Example 3 by the formula Φ latest p 1 ,p 3 if we restrict to messages sent from p i to p j with i < j. Unfortunately, the protocol implemented by A is erroneous: For the MSC M in Figure 1, we have M ∈ L(Φ latest p 1 ,p 3 ), but M L(A). In A, at g 2 and g 5 , process p 3 should announce , but it outputs . It turns out that it is very difficult to come up with a CFM A latest p 1 ,p 3 such that L(A latest p 1 ,p 3 ) = L(Φ latest p 1 ,p 3 ) (even to show that such a CFM exists at all). This is already a challenging problem in the more specialized setting of Mazurkiewicz traces. However, we obtain A latest p 1 ,p 3 as a corollary of our logical characterization of CFMs, which we present in the following. As we have demonstrated in the previous example, it is a worthwhile task to translate (simple) logical specifications like Φ latest p,q into (complicated) machine models, preferably automatically. However, coming up with automata models directly can be very difficult. One of our main results (Theorem 3) states that every FO formula can be translated into a CFM. Our proof goes via an intermediate logic, namely star-free propositional dynamic logic (PDL sf ), which is introduced in the next section and shown to be expressively equivalent to FO[→, , ≤]. Then, in Section 4, we show how to translate PDL sf formulas into equivalent CFMs.

s p 1 p 1 p 1 , ! p 2 , ! p 3 , ! p 2 , ! p 3 s 0 p 2 p 2 p

An Overview of Known Results

Let us give a brief account of what was already known on the relation between logic and CFMs. Note that we do not rely on any of these results.

Fact 1 ( [Büc60, [START_REF] Elgot | Decision problems of finite automata design and related arithmetics[END_REF][START_REF] Trakhtenbrot | Finite automata and monadic second order logic[END_REF]). Suppose |P| = 1 (i.e., CFMs are essentially finite automata). We have L(MSO) = L(CFM).

This classical result is known as the Büchi-Elgot-Trakhtenbrot theorem. It was first generalized to CFMs with universally bounded channels (Fact 2). See Section 5.1 for the formal definition of existentially and universally bounded MSCs. Intuitively, a language L of MSCs is universally B-bounded if all linearizations of all MSCs in L can be executed with channel capacity B. We denote by MSC ∀B (P, Σ) the set of MSCs in MSC(P, Σ) which are universally B-bounded. Moreover, MSC fin ∀B (P, Σ) := MSC ∀B (P, Σ) ∩ MSC fin (P, Σ).

Fact 2 ( [HMK + 05]). For all B ∈ N and L ⊆ MSC fin ∀B (P, Σ), the following are equivalent:

1. L = L(A) for some CFM A;

2. L = L(A) for some deterministic CFM A;

3. L = L(Φ) for some MSO formula Φ.

Moreover, there is a deterministic CFM A such that L(A) = MSC fin ∀B (P, Σ).

Kuske generalized the theorem to infinite universally bounded MSCs, while using a different proof technique.

Fact 3 ( [Kus03]

). For all B ∈ N and L ⊆ MSC ∀B (P, Σ), the following are equivalent:

1. L = L(A) for some CFM A;

2. L = L(A) for some deterministic CFM A;

3. L = L(Φ) for some MSO formula Φ.

In the case of finite MSCs, the logical characterization was lifted to existentially bounded MSCs by Genest et al. (cf. Fact 8). We denote by MSC ∃B (P, Σ) the set of MSCs in MSC(P, Σ) which are existentially B-bounded, i.e., for which some linearization can be executed with channel capacity B. We also let MSC fin ∃B (P, Σ) := MSC ∃B (P, Σ) ∩ MSC fin (P, Σ).

Fact 4 ( [GKM06]

). For all B ∈ N and L ⊆ MSC fin ∃B (P, Σ), the following are equivalent: 1. L = L(A) for some CFM A;

2. L = L(Φ) for some MSO formula Φ.

Moreover, there is a CFM A such that L(A) = MSC fin ∃B (P, Σ). On the other hand, it turns out that deterministic CFMs are now strictly weaker: Fact 5 ( [GKM06]). CFMs are inherently non-deterministic: There is a CFM A such that L(A) ⊆ MSC fin ∃B (P, Σ) and, for all deterministic CFMs A , we have L(A) L(A ).

The proofs of Facts 2, 3, and 4 reduce message-passing systems to finite-state shared-memory systems so that involved results from Mazurkiewicz trace theory [START_REF] Diekert | The Book of Traces[END_REF] can be applied. This generic approach is no longer applicable when the restriction on the channel capacity is dropped. In fact, in general, CFMs do not capture MSO logic: Fact 6 ( [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF][START_REF] Bollig | Communicating finite-state machines and two-variable logic[END_REF]). For all L ⊆ MSC fin (P, Σ), the following are equivalent:

1. L = L(A) for some CFM A;

2. L = L(Φ) for some sentence Φ ∈ EMSO[→, ];

3. L = L(Φ) for some sentence Φ ∈ EMSO 2 [→, , ≤].
However, MSO is strictly more expressive than CFMs: There is an MSO sentence Φ such that L(Φ) ⊆ MSC fin (P, Σ) and, for all CFMs A, we have L(Φ) L(A).

The characterizations from Fact 6 were given for finite MSCs. Over infinite MSCs, EMSO[→, ] is strictly weaker than CFMs as it cannot express that there are infinitely many events to satisfy some property. Actually, this is already true for one process, i.e., finite automata and words. However, CFMs can be characterized by the logic EMSO ∞ [→, ], extending EMSO[→, ] by the quantifier ∃ ∞ x.Φ, which requires that there be infinitely many events x such that Φ holds.

Fact 7 ( [BK08]

). For all L ⊆ MSC(P, Σ), the following are equivalent:

1. L = L(A) for some CFM A; 2. L = L(Φ) for some sentence Φ ∈ EMSO ∞ [→, ].
Note that one of our main results (Theorem 4) is the equivalence of CFMs and EMSO[→, , ≤], which properly generalizes Facts 6 and 7. Moreover, we will show in Section 5 how to obtain Fact 4 as a corollary, while generalizing it to infinite MSCs.

Star-Free Propositional Dynamic Logic

In this section, we introduce a star-free version of propositional dynamic logic and show that it is expressively equivalent to FO[→, , ≤]. This is the second main result of the paper. Then, in Section 4, we show how to translate star-free PDL formulas into CFMs.

M | = E ϕ if M, e | = ϕ for some event e ∈ E M | = ¬ξ if M | = ξ M | = ξ 1 ∨ ξ 2 if M | = ξ 1 or M | = ξ 2 M, e | = p if loc(e) = p M, e | = π ϕ if ∃ f ∈ π M (e) : M, f | = ϕ M, e | = a if λ(e) = a M, e | = Loop(π) if (e, e) ∈ π M M, e | = ¬ϕ if M, e | = ϕ M, e | = ϕ 1 ∨ ϕ 2 if M, e | = ϕ 1 or M, e | = ϕ 2 → M := {(e, f ) ∈ E × E | e → f } p,q M := {(e, f ) ∈ E p × E q | e f } ← M := {( f, e) ∈ E × E | e → f } -1 p,q M := {( f, e) ∈ E q × E p | e f } jump p,r M := E p × E r {ϕ}? M := {(e, e) | e ∈ E : M, e | = ϕ} ϕ - → M := {(e, f ) ∈ E × E | e < proc f and ∀g ∈ E: e < proc g < proc f =⇒ M, g | = ϕ} ϕ ← -M := {(e, f ) ∈ E × E | f < proc e and ∀g ∈ E: f < proc g < proc e =⇒ M, g | = ϕ} π 1 • π 2 M := {(e, g) ∈ E × E | ∃ f ∈ E : (e, f ) ∈ π 1 M ∧ ( f, g) ∈ π 2 M } π 1 ∪ π 2 M := π 1 M ∪ π 2 M π c M := (E × E) \ π M π 1 ∩ π 2 M := π 1 M ∩ π 2 M

Syntax and Semantics

Originally, propositional dynamic logic (PDL) has been used to reason about program schemas and transition systems [START_REF] Fischer | Propositional Dynamic Logic of regular programs[END_REF]. Since then, PDL and its extension with intersection and converse have developed a rich theory with applications in artificial intelligence and verification [HM92, DL94, LL05, Lan06, GLL09]. It has also been applied in the context of MSCs [START_REF] Bollig | Propositional dynamic logic for message-passing systems[END_REF][START_REF] Mennicke | Propositional dynamic logic with converse and repeat for message-passing systems[END_REF].

Here, we introduce a star-free version of PDL, denoted PDL sf . It will serve as an "interface" between FO logic and CFMs. The syntax of PDL sf and its fragment PDL sf [Loop] is given by the following grammar:

PDL sf = PDL sf [Loop, ∪, ∩, c] PDL sf [Loop] Sentence ξ ::= E ϕ | ξ ∨ ξ | ¬ξ Event formula ϕ ::= p | a | ϕ ∨ ϕ | ¬ϕ | π ϕ | Loop(π) Path formula π ::= → | ← | p,q | -1 p,q | ϕ - → | ϕ ← -| jump p,r | {ϕ}? | π • π π ∪ π | π ∩ π | π c
where p, r ∈ P, q ∈ P \ {p}, and a ∈ Σ. We refer to ξ as a sentence, to ϕ as an event formula, and to π as a path formula. We name the logic star-free because we use the operators (∪, ∩, c, •) of star-free regular expressions instead of the regular-expression operators (∪, •, * ) of classical PDL. However, the formula ϕ -→, whose semantics is explained below, can be seen as a restricted use of the construct π * .

A sentence ξ is evaluated with respect to an MSC M = (E, →, , loc, λ). An event formula ϕ is evaluated with respect to M and an event e ∈ E. Finally, a path formula π is evaluated over two events. In other words, it defines a binary relation

π M ⊆ E × E. We often write M, e, f | = π to denote (e, f ) ∈ π M . Moreover, for e ∈ E, we let π M (e) := { f ∈ E | (e, f ) ∈ π M }.
When M is clear from the context, we may write π instead of π M . The semantics of sentences, event formulas, and path formulas is given in Table 1. For a sentence ξ, we let

L(ξ) := {M ∈ MSC(P, Σ) | M | = ξ}.
We use the standard abbreviations for sentences and event formulas such as implication and conjunction. Moreover, we let true := p ∨ ¬p (for some arbitrary process p ∈ P) and false := ¬true. Finally, we define the event formula π := π true, and the path formulas

+ -→ := true ---→ and * - → := + -→ ∪ {true}?.
The size of a PDL sf formula is defined by mutual induction. We let

|E ϕ| = |ϕ| + 1, |¬ξ| = |ξ| + 1, and |ξ 1 ∨ ξ 2 | = |ξ 1 | + |ξ 2 | + 1. For p ∈ P and a ∈ Σ, |p| = |a| = 1. Moreover, |¬ϕ| = |ϕ| + 1, | π ϕ| = |π| + |ϕ| + 1, |Loop(π)| = |π| + 1, and |ϕ 1 ∨ ϕ 2 | = |ϕ 1 | + |ϕ 2 | + 1. If π ∈ {→, ←, p,q , -1 p,q | (p, q) ∈ Ch} ∪ {jump p,q | p, q ∈ P}, we let |π| = 1. Moreover, |{ϕ}?| = | ϕ - →| = | ϕ ← -| = |ϕ| + 1 and |π c | = |π| + 1. Finally, |π 1 op π 2 | = |π 1 | + |π 2 | + 1 for all op ∈ {∪, ∩, • }.
The usual temporal logic modalities can be expressed easily. For instance, → ϕ means that the next event on the same process satisfies ϕ, and ϕ -→ ψ corresponds to the strict until X(ϕ U ψ). The corresponding past modalities can be written similarly. See Section 5.2 for more modalities.

Example 5. Consider again the MSC M from Figure 1. For the path formula π

= -1 p 1 ,p 3 → p 1 ,p 2 → p 2 ,p 3 →, we have M, g 5 | = Loop(π). Moreover, (e 2 , e 5 ) ∈ -→ M but (e 2 , e 6 )
-→ M . To give an example of an event formula, note that we have M, e 0 | = + -→ ¬ + -→ ¬ (as we eventually see only ). Finally, since E p 1 is infinite, we also have

M | = ¬ E(p 1 ∧ ¬ → ).
Note that there are some redundancies in the logic. For example (letting

≡ denote logical equivalence), → ≡ false ---→, π 1 ∩ π 2 ≡ (π c 1 ∪ π c 2 ) c
, and Loop(π) ≡ {true}? ∩ π . Some of them are necessary to define certain subclasses of PDL sf . For every R ⊆ {Loop, ∪, ∩, c}, we let PDL sf [R] denote the fragment of PDL sf that does not make use of

{Loop, ∪, ∩, c} \ R. In particular, PDL sf = PDL sf [Loop, ∪, ∩, c]. Syntactically, * - → is not contained in PDL sf [Loop] since union is not permitted.
Given a PDL sf [Loop] path formula π, we denote by Comp(π) the set of pairs (p, q) ∈ P × P such that there may be a π-path from some event on process p to some event on process q. Formally, we let

Comp(→) = Comp(←) = Comp( ϕ - →) = Comp( ϕ ← -) = Comp({ϕ}?) = id, where id = {(p, p) | p ∈ P}; Comp( p,q ) = Comp( -1 q,p ) = {(p, q)}; Comp(jump p,r ) = {(p, r)}; and Comp(π 1 • π 2 ) = Comp(π 2 ) • Comp(π 1 ) = {(p, r) | ∃q : (p, q) ∈ Comp(π 1 ), (q, r) ∈ Comp(π 2 )}.
Notice that, for all path formulas π ∈ PDL sf [Loop], the relation Comp(π) is either empty or a singleton {(p, q)} or the identity id. Moreover, M, e, f | = π implies (loc(e), loc( f )) ∈ Comp(π). Therefore, all events in π (e) are on the same process, and if this set is nonempty (i.e., if M, e | = π ), then min π (e) is well-defined. We also define max π (e) ∈ π (e) ∪ {∞}, with the convention max π (e) = ∞ if π (e) is infinite. We extend ≤ and ≤ proc to E ∪ {∞} by setting e ≤ ∞ and e ≤ proc ∞ for all e ∈ E ∪ {∞}.

Example 6. Consider π = + -→ p 1 ,p 2 → p 2 ,p 3 →. We have Comp(π) = {(p 1 , p 3 )}.

Moreover, given the MSC from

Figure 1, min π (e 2 ) = g 4 and max π (e 2 ) = g 5 . On the other hand, max -→ • p 1 ,p 3 (e 5 ) = ∞.

Remark 1. The logic PDL sf [∪] over MSCs is analogous to Conditional XPath [START_REF] Marx | Conditional XPath[END_REF].2 Formulas from Conditional XPath are interpreted over ordered unranked trees. Therefore, rather than atomic formulas → and p,q as well as their inverse operators, there are tailored formulas allowing one to move to a child or the parent of a given node, or to go to its immediate left/right sibling. However, while Marx showed that Conditional XPath is expressively complete for FO logic over ordered unranked trees, our expressive completeness result over MSCs crucially relies on the Loop modality, which is not contained in PDL sf [∪] and not provided by Conditional XPath.

From PDL sf to FO 3

Let FO 3 [→, , ≤] be the set of formulas from FO[→, , ≤] that use at most three different first-order variables (however, a variable can be quantified and reused several times in a formula). The main result of this section is that, for formulas with zero or one free variable, the logics FO[→, , ≤], FO 3 [→, , ≤], PDL sf , and PDL sf [Loop] are expressively equivalent.

Consider FO[→, , ≤] formulas Φ 0 , Φ 1 (x), and Φ 2 (x, y) with respectively zero, one, and two free variables (hence, Φ 0 is a sentence). Consider also some PDL sf sentence ξ, event formula ϕ, and path formula π. The respective formulas are equivalent, written Φ 0 ≡ ξ, Φ 1 (x) ≡ ϕ, and Φ 2 (x, y) ≡ π, if, for all MSCs M and all events e, f in M, we have

M | = Φ 0 iff M | = ξ M, [x → e] | = Φ 1 (x) iff M, e | = ϕ M, [x → e, y → f ] | = Φ 2 (x, y) iff M, e, f | = π
We start with a simple observation, which can be shown easily by induction:

Proposition 1. Every PDL sf formula is equivalent to some FO 3 [→, , ≤] formula. More precisely, for every PDL sf sentence ξ, event formula ϕ, and path formula π, there exist some FO 3 [→, , ≤] sentence ξ, formula ϕ(x) with one free variable, and formula π(x, y) with two free variables, respectively, such that, ξ ≡ ξ, ϕ ≡ ϕ(x), and π ≡ π(x, y).

The main result of this section is a strong converse of Proposition 1: Every FO[→, , ≤] formula with at most two free variables is equivalent to some PDL sf formula. This is formally stated and proved in Section 3.5. We first investigate in the next section some basic properties of PDL sf . Then, we show in Section 3.4 that the complement of a PDL sf [Loop] formula is equivalent to a finite union of PDL sf [Loop] formulas. This is crucial to deal with negation in the translation from FO to PDL sf . The other main difficulty is existential quantification, which is dealt with in Section 3.5.

Basic Properties of PDL sf

First, the converse of a PDL sf formula is definable in PDL sf (easy induction on π).

Lemma 1. Let R ⊆ {Loop, ∪, ∩, c} and π ∈ PDL sf [R] be a path formula. There exists π -1 ∈ PDL sf [R] such that, for all MSCs M, π -1 M = π -1 M = {( f, e) | (e, f ) ∈ π M }.
A second observation is that unions in PDL sf [Loop, ∪] path formulas can always be pulled to the front of the formula.

Lemma 2. Every PDL sf [Loop, ∪] path formula is equivalent to a finite union of PDL sf [Loop] path formulas, and every PDL sf [Loop, ∪] event formula is equivalent to some PDL sf [Loop] event formula.

Proof. This is easy to prove by induction on PDL sf [Loop, ∪] formulas, using the following identities: if (π i ) 1≤i≤n and (π j ) 1≤ j≤m are PDL sf [Loop] path formulas, then

i π i • j π j ≡ i, j π i • π j , Loop( i π i ) ≡ i Loop(π i ) , i π i ϕ ≡ i π i ϕ .
The next lemma shows that all PDL sf [Loop] path formulas are, in some sense, monotone.

Lemma 3 (monotonicity). Let π ∈ PDL sf [Loop] be a path formula, M be an MSC, and e, f, e be events of M such that M, e, e | = π, and M, f | = π (ie., M, f, g | = π for some event g in M).

(a) If e ≤ proc f , then there exists f such that e ≤ proc f and M, f, f | = π.

(b) If f ≤ proc e, then there exists f such that f ≤ proc e and M, f, f | = π.

Proof. We only show (a). Part (b) is similar. We prove by induction on π that, for all event formulas ψ ∈ PDL sf [Loop], the property holds for π • {ψ}?.

• If π = {ϕ}?, then e = e, and we can take f = f .

• If π = jump p,q , we take f = e .

• If π = p,q , then e e and there exists f such that M, f, f | = p,q • {ψ}?. In particular, f f . Since the channels are FIFO, we have e ≤ proc f .

• The cases π = -1 p,q , π = →, and π = ← are similar.

• Suppose π = ϕ -→. If f < proc e , we take f = e . Otherwise, we let f be any event such that M, f, f | = ϕ -→.

We then have e ≤ proc f < proc f . Similarly, if π = ϕ ← -, then either there exists e ≤ proc f < proc f such that

M, f, f | = ϕ ← -•{ψ}?, or M, f, e | = ϕ ← -. • Suppose π = π 1 • π 2 .
There exists e 1 such that M, e, e 1 | = π 1 and M, e 1 , e | = π 2 • {ψ}?. In particular, M, e, e 1 | = π 1 • { π 2 ψ}?. By induction hypothesis on π 1 , there exists f 1 such that e 1 ≤ proc f 1 and M, f, f

1 | = π 1 • { π 2 ψ}?.
By induction hypothesis on π 2 , there exists

f such that M, f 1 , f | = π 2 • {ψ}? and e ≤ proc f .
A crucial consequence of Lemma 3 is that, for all path formulas π ∈ PDL sf [Loop] and events e in some MSC, π (e) contains precisely the events that lie in the interval between min π (e) and max π (e) and that satisfy π -1 . Lemma 4. Let π be a PDL sf [Loop] path formula. For all MSCs M and events e such that M, e | = π , we have

π (e) = { f ∈ E | min π (e) ≤ proc f ≤ proc max π (e) ∧ M, f | = π -1 } .
Proof. The left-to-right inclusion is trivial. For the right-to-left inclusion, we show by induction on π that, for all events e and f 1

≤ proc f ≤ proc f 2 such that M, e, f 1 | = π, M, e, f 2 | = π, and M, f | = π -1 , we have M, e, f | = π.
All cases apart from concatenation are immediate. So assume π = π 1 • π 2 . There exist g 1 , g 2 , g such that M, e, andM, g | = π -1 1 . We distinguish three cases, illustrated in Figure 3. 1. If g ≤ proc g 1 , then by Lemma 3(a) applied to π 2 , g, f, g 1 , there exists

g i | = π 1 , M, g i , f i | = π 2 , M, g, f | = π 2 ,
e g 1 f 1 f 1 f g ≤ proc π 1 π 2 ≤ proc ≤ proc π 2 π 2 π 2 Case 1. e g 2 f 2 f 2 f g ≤ proc π 1 π 2 ≤ proc ≤ proc π 2 π 2 π 2 Case 2. e g 1 g 2 f 1 f 2 g f ≤ proc ≤ proc π 1 π 1 π 2 π 2 π 2 ≤ proc ≤ proc π 1 Case 3.
f 1 ≥ proc f such that M, g 1 , f 1 | = π 2 . By induction hypothesis on π 2 , we then have M, g 1 , f | = π 2 , hence M, e, f | = π 1 • π 2 .
2. Similarly, if g 2 ≤ proc g, then by applying Lemma 3(b) to π 2 , g 2 , g, f , we find

f 2 ≤ proc f such that M, g 2 , f 2 | = π 2 .
Using the induction hypothesis on π 2 , we obtain

M, g 2 , f | = π 2 , hence M, e, f | = π 1 • π 2 .
3. Otherwise, we have g 1 ≤ proc g ≤ proc g 2 . By induction hypothesis on π 1 , we get M, e, g

| = π 1 , hence M, e, f | = π 1 • π 2 .

Characterizing the Complement of a Path Formula

Using Lemma 4, we can give a characterization of π c (e) (when π ∈ PDL sf [Loop]) that also relies on intervals delimited by min π (e) and max π (e). More precisely, π c (e) is the union of the following sets (see Figure 4): (i) the interval of all events to the left of min π (e), (ii) the interval of all events to the right of max π (e) (assuming max π (e) ∞), (iii) the set of events located between min π (e) and max π (e) and satisfying ¬ π -1 , (iv) all events located on other processes than min π (e). This description of π c (e) can be used to rewrite π c as a union of PDL sf [Loop] formulas. In a first step, we show that, if π is a PDL sf [Loop] formula, then the relation {(e, min π (e)) | e ∈ E} can also be expressed in PDL sf [Loop]. Proof. Let us first observe that, for all PDL sf [Loop] path formulas π 1 and π 2 , for all MSCs M and events e of M such that π 1 • π 2 (e) ∅, we have

(i) (iii) (ii) e π -1 π -1 π -1 π -1 min π max π
min π 1 • π 2 (e) = min π 2 (min π 1 • { π 2 }? (e)) .
(1)

Indeed, if π 1 • π 2 (e) ∅, then f = min π 1 • { π 2 }? (
e) and g = min π 2 ( f ) are well-defined (and reciprocally). Clearly, M, e, g | = π 1 • π 2 . To prove minimality, let f , g such that M, e, f | = π 1 and M, f , g | = π 2 (cf. Figure 5). We have f ≤ proc f , hence, by Lemma 3(b), there exists g ≤ proc g such that M, f, g | = π 2 . Then g ≤ proc g ≤ proc g . We can now give the definition of min π. Since concatenation of paths is associative, we view π as a nonempty sequence of atomic steps and we construct min π by induction on the length of π. Without loss of generality, we assume that the last atomic step of the path formula is {true}?. Hence, the basis of the induction is when π = {true}?, in which case we let min π = {true}?.

e min π 1 • { π 2 }? (e) = f min π 2 ( f ) = g f g g ≤ proc ≤ proc ≤ proc π 1 π 2 π 2
For the inductive case, assume that π = r • π with r an atomic path formula. Inspired by Equation (1), we define inductively min π = r • min π , where r is a path formula such that, for all events e and f with M, e, f | = r • { π }?, we have M, e, f | = r if and only if f = min r • { π }? (e). For an atomic path formula r, we define

r =                      r if r ∈ {{ϕ}?, →, ←, p,q , -1 p,q | (p, q) ∈ Ch} jump p,q • {¬ + ← -• π }? if r = jump p,q ϕ ← -•{¬ϕ ∨ ¬ ϕ ← -• π }? if r = ϕ ← - ϕ∧¬ π ------→ if r = ϕ - → .
Notice that M, e, f | = r does not imply M, f | = π . We could enforce this by appending a test { π }? at the end of r, but this would be redundant due to the right context of r in min π = r • min π . Finally, note that r is of size O(|π|). We deduce immediately that min π is of size O(|π| 2 ).

Moreover, we associate with every path formula π ∈ PDL sf [Loop] a formula max π in PDL sf [Loop]. Note that, for finite MSCs, we could define max π similarly to min π. However, for infinite MSCs, we cannot use the same definition since we may have max

π 1 • π 2 (e) = f but max π 1 • { π 2 }? (e) = ∞.
Lemma 6. Let R = ∅ or R = {Loop}. For every path formula π ∈ PDL sf [R], there exists a PDL sf [R] path formula max π of size O(|π| 2 ) such that, for all MSCs M and events e, f , we have M, e, f | = max π iff f = max π (e).

In particular, if max π (e) = ∞, then no event in M will satisfy max π. So we have max π (e) = ∞ iff M, e | = π ∧¬ max π .

Proof. As in Lemma 5, we view π as a nonempty sequence of atomic steps. If π = r • π with r an atomic path formula, we will define inductively max π = r • max π , where r is a path formula of size O(|π|).

• Without loss of generality, we assume that the last atomic step of the path formula is {true}?. Hence, the basis of the induction is when π = {true}?, in which case we let max π = {true}?.

• If π = r • π 1 , where r ∈ {{ϕ}?, →, ←, p,q , -1 p,q | (p, q) ∈ Ch}, we let

max π = r • max π 1 . • If π = jump p,q • π 1 , we let max π = jump p,q • { π 1 ¬ + -→ • π -1 1 }? • max π 1 .
To prove the correctness, let M be an MSC, and e, f events of M.

First, assume that f = max jump p,q • π 1 (e). Let g such that M, e, g | = jump p,q and M, g, f | = π 1 (see Figure 6a).

We must have

f = max π 1 (g), hence M, g, f | = max π 1 . Suppose that M, g | = π 1 ¬ + -→ • π -1 1 . Then, in particular, M, f | = + -→ • π -1
1 , i.e., there exist f > proc f and g such that M, g , f | = π 1 . Since loc( f ) = loc( f ), we also have loc(g ) = loc(g) = q. Hence M, e, g | = jump p,q and M, e, f | = π, which contradicts the maximality of f . Conversely, assume that M, e, f | = max π. Let g such that M, e, g | = jump p,q , M, g

e g f g f max π (e) = jump p,q π 1 + jump p,q π 1 (a) f = max π (e). e g f f f | = π 1 ¬ + -→ • π -1 1 jump p,q max π 1 + jump p,q • π 1 π 1 * (b) M, e, f | = max π.
| = π 1 ¬ + -→ • π -1
1 , and M, g, f | = max π 1 (see Figure 6b). Clearly, M, e, f | = jump p,q • π 1 . Suppose that f is not maximal, i.e., that there exists f > proc f such that M, e, f | = π. Then, for all f such that M, g, f

| = π 1 , we have f ≤ proc f < proc f (by induction hypothesis), hence M, f | = + -→ • π -1 1 . This contradicts the fact that M, g | = π 1 ¬ + -→ • π -1 1 . • If π = ϕ ← -• π 1 , we let max π = ϕ∧¬ π 1 ← ------• max π 1 .
Let M be an MSC, and e, f events of M. Assume that f = max π (e) and let g be such that M, e, g

| = ϕ ← - and M, g, f | = π 1 . We must have f = max π 1 (g). Let g be maximal with M, e, g | = ϕ ← -• { π 1 }?. We have M, e, g | = ϕ∧¬ π 1
← -----and g ≤ proc g . We deduce from Lemma 3(a) that f = max π 1 (g ).

Conversely, assume that M, e, f | = max π and let g be such that M, e, g | =

ϕ∧¬ π 1 ← ------and M, g, f | = max π 1 . We have M, e, f | = π. Let f , g be such that M, e, f | = π, M, e, g | = ϕ
← -, and M, g , f | = π 1 . We have g ≤ proc g and using Lemma 3(a) we deduce that f ≤ proc f . Therefore, f = max π (e). •

If π = ϕ - → • π 1 , we let max π = ϕ - → • {ψ 1 ∨ ψ 2 }? • max π 1 ,
where

ψ 1 = ¬ϕ ∨ ¬ ϕ - → • π 1 ψ 2 = π 1 ¬ + -→ • π -1 1 .
Let M be an MSC, and e, f events of M.

Assume that f = max π (e), and that

ϕ - → (e) is finite. Then, ϕ - → • { π 1 }? (e)
is also finite and non-empty. Let g = max ϕ -→ • { π 1 }? (e). We have M, g | = ψ 1 . In addition, since π (e) is finite, π 1 (g) must be finite, and by Lemma 3(a), we get max π 1 (g) = f . Hence M, e, f | = max π. Now, assume that ϕ -→ (e) is infinite. Let g be any event such that M, e, g | = ϕ -→ and M, g, f | = π 1 . By maximality of f , we have M, g, f | = max π 1 (see Figure 7a). Suppose towards a contradiction that

M, f | = + -→ • π -1 1 . Then, there exist f > proc f and g such that M, g , f | = π 1 . By Lemma 3(a), g > proc g > proc e.
= max π 1 . If g | = ψ 1 , we have g = max ϕ - → • { π 1 }? (e)
. By Lemma 3(a), we conclude that f = max π (e). Now, suppose that M, g | = ψ 2 , and that there exists f > proc f such that M, e, f | = π (see Figure 7b). For all f such that M, g, f

| = π 1 , we have f ≤ proc f < proc f , hence M, f | = + -→ • π -1 1 . This contradicts the fact that M, g | = π 1 ¬ + -→ • π -1 1 .
We are now ready to prove that any Boolean combination of PDL sf [Loop] formulas is equivalent to a positive one, i.e., one that does not use complement.

Lemma 7. For all path formulas π ∈ PDL sf [Loop], there exist PDL sf [Loop] path formulas (π i ) 1≤i≤|P| 2 +3 such that π c ≡ 1≤i≤|P| 2 +3 π i .
Proof. We show π c ≡ σ, where

σ = (min π • + ← -) ∪ (max π • + -→) ∪ (π • + -→ • {¬ π -1 }?) ∪ (p,q)∈P 2 {¬ π q}? • jump p,q .
Let M = (E, →, , loc, λ) be an MSC and e, f ∈ E. We write p = loc(e), q = loc( f ). Let us show that M, e, f | = π c iff M, e, f | = σ. If M, e | = ¬ π q, then both M, e, f | = π c and M, e, f | = σ hold. In the following, we assume that M, e | = π q, and thus that min π (e) ∈ E q and max π (e) ∈ E q ∪ {∞}. Again, if f < proc min π (e) or max π (e) < proc f , then both M, e, f | = π c and M, e, f | = σ hold. And if min π (e) ≤ proc f ≤ proc max π (e), then, by Lemma 4, we have M, e, f

| = π c iff M, f | = ¬ π -1 , iff M, e, f | = σ.

From FO to PDL sf

We will now show that every FO[→, , ≤] formula with at most two free variables can be translated into an equivalent PDL sf formula, as stated in Theorem 1 below. As we proceed by induction, we actually need a more general statement, which takes into account arbitrarily many free variables. In the following proposition, π(x, y) refers to the FO formula obtained from π due to Proposition 1. To obtain a formula π(x, x) with one free variable, we first construct π(x, y) according to Proposition 1 and then replace y by x.

Proposition 2. Every formula Φ ∈ FO[→, , ≤] with at least one free variable is equivalent to a positive Boolean combination of formulas of the form π(x, y), where π ∈ PDL sf [Loop] and x, y ∈ Free(Φ).

Proof. In the following, we will simply write π(x, y) for π(x, y).

The proof is by induction. For convenience, we assume that Φ is in prenex normal form. If Φ is quantifier free, then it is a Boolean combination of atomic formulas. For x, y ∈ V event , atomic formulas are translated as follows:

p(x) ≡ {p}?(x, x)
x → y ≡ →(x, y) x = y ≡ {true}?(x, y) a(x) ≡ {a}?(x, x) x y ≡ (p,q)∈Ch p,q (x, y)

Moreover, x ≤ y is equivalent to the disjunction of the formulas π

• p 1 ,p 2 • + -→ • p 2 ,p 3 • • • + -→ • p m-1 ,p m • π (x, y)
, where 1 ≤ m ≤ |P|, p 1 , . . . , p m ∈ P are such that p i p j for all 1 ≤ i < j ≤ m, and π, π ∈ { + -→, {true}?}.

Universal quantification. We have ∀x.Ψ ≡ ¬∃x.¬Ψ. Negation can be eliminated thanks to Lemma 7. Hence, this case reduces to existential quantification.

Existential quantification. Suppose that Φ = ∃x.Ψ. If x is not free in Ψ, then Φ ≡ Ψ and we are done by induction. Otherwise, assume that Free(Ψ) = {x 1 , . . . , x n } with n > 1, and that x = x n . By induction, Ψ is equivalent to a positive Boolean combination of formulas of the form π(y, z) with y, z ∈ Free(Ψ). Bringing Ψ into disjunctive normal form, we obtain a finite disjunction of formulas of the form j π j (y j , z j ), where y j = x i 1 and z j = x i 2 for some i 1 ≤ i 2 . This step may cause an exponential blow-up so that the overall construction is nonelementary (which is unavoidable [START_REF] Stockmeyer | The Complexity of Decision Problems in Automata Theory and Logic[END_REF]).

Note that the variable ordering can be guaranteed by replacing π j with π -1 j whenever needed. Now, Φ = ∃x n .Ψ is equivalent to a finite disjunction of formulas of the form

j∈I π j (y j , z j ) ∧ ∃x n . j∈J π j (y j , x n ) ∧ j∈J π j (x n , x n ) =: Υ
for three finite, pairwise disjoint index sets I, J, J such that y j , z j ∈ {x 1 , . . . , x n-1 } for all j ∈ I, and y j ∈ {x 1 , . . . , x n-1 } for all j ∈ J. Notice that Free(Υ) ⊆ {x 1 , . . . ,

x n-1 }. If J = ∅, then 3 Υ ≡ p,q∈P jump p,q • { j∈J Loop(π j )}? • jump q,p (x 1 , x 1 ) .

So assume J

∅. We define below a formula Υ and prove that it is equivalent to Υ. Intuitively, by Lemma 4, we know that Υ holds iff the intersection of the intervals [min π j (y j ), max π j (y j )] contains some event satisfying ψ = j∈J π -1 j ∧ j∈J Loop(π j ). The formula Υ identifies some π k such that min π k (y k ) is maximal (first line), some π such that max π (y ) is minimal (second line), and tests that there exists an event x n satisfying ψ between the two (third line). This is illustrated in Figure 8.

Υ := k, ∈J                   j∈J ((min π j ) • * - → • (min π k ) -1 )(y j , y k ) ∧ j∈J { π j ∧¬ max π j }?(y j , y j ) ∨ ((max π ) • * - → • (max π j ) -1 )(y , y j ) ∧ (π k • {ψ}? • π -1 )(y k , y )                   Claim 1. We have Free(Υ ) = Free(Υ) ⊆ {x 1 , . . . , x n-1 } and Υ ≡ Υ . Proof. Assume M, ν | = Υ.
There exists e ∈ E such that M, ν(y j ), e | = π j for all j ∈ J, and M, e | = Loop(π j ) for all j ∈ J .

In particular, all min π j (ν(y j )) and max π j (ν(y j )) ∈ E ∪ {∞} for j ∈ J are well-defined and on process loc(e) or equal to ∞. Let k ∈ J such that min π k (ν(y k )) is maximal, i.e., min π j (ν(y j )) ≤ proc min π k (ν(y k )) for all j ∈ J. Then, for all j ∈ J, we have M, ν(y j ), ν( (Claim 1)

y k ) | = (min π j ) • * - → • (min π k ) -1 . Similarly, let ∈ J such that max π (ν(y )) ∈ E ∪ {∞} is minimal. Then, for all j ∈ J, either M, ν(y j ), ν(y j ) | = { π j ∧¬ max π j }? (i.e., max π j (ν(y j )) = ∞), or else M, ν(y ), ν(y j ) | = (max π ) • * - → • (max π j ) -1 .
We conclude that Υ is equivalent to some positive Boolean combination of formulas π(x, y), with π ∈ PDL sf [Loop] and x, y ∈ {x 1 , . . . , x n-1 } = Free(Φ). Therefore, so is Φ. Note that, due to * -→, the formulas (min

π j ) • * - → • (min π k ) -1 and (max π ) • * - → • (max π j ) -1 are in PDL sf [Loop, ∪] instead of PDL sf [Loop]
. By Lemma 2, these can be transformed into finite unions of PDL sf [Loop] path formulas.

We are now able to prove the main result relating FO[→, , ≤] and PDL sf [Loop].

Theorem 1. Every FO[→, , ≤] formula with at most two free variables is equivalent to some PDL sf formula. More precisely, for every FO[→, , ≤] sentence Φ 0 , formula Φ 1 (x) with one free variable, and formula Φ 2 (x, y) with two free variables, there exist some PDL sf [Loop] sentence ξ, PDL sf [Loop] event formula ϕ, and PDL sf [Loop] path formulas π i j , respectively, such that, Φ 0 ≡ ξ, Φ 1 (x) ≡ ϕ, and Φ 2 (x, y) ≡ i j π i j .

Proof. Let Φ 2 (x 1 , x 2 ) be an FO[→, , ≤] formula with two free variables. We apply Proposition 2 to Φ 2 (x 1 , x 2 ) and obtain a positive Boolean combination of path formulas π(y, z) with y, z ∈ {x 1 , x 2 }. Next, we replace formula π(x 1 , x 1 ) by p,q ({Loop(π)}? • jump p,q )(x 1 , x 2 ). Similarly, π(x 2 , x 2 ) is replaced by p,q (jump p,q • {Loop(π)}?)(x 1 , x 2 ). Also, π(x 2 , x 1 ) is replaced by π -1 (x 1 , x 2 ). Finally, we transform it into disjunctive normal form: we obtain Φ 1 (x 1 , x 2 ) ≡ i j π i j (x 1 , x 2 ), which concludes the proof in the case of two free variables.

Next, let Φ 1 (x) be an FO[→, , ≤] formula with one free variable. As above, applying Proposition 2 to Φ 1 (x), we obtain PDL sf [Loop] path formulas π i j such that Φ 1 (x) ≡ i j π i j (x, x). Now, M, [x → e] | = π i j (x, x) iff M, e | = Loop(π i j ). Hence, Φ(x) ≡ i j Loop(π i j ).

Finally, an FO[→, , ≤] sentence Φ 0 is a Boolean combination of formulas of the form ∃x.Φ 1 (x). Applying the theorem to Φ 1 (x), we obtain an equivalent PDL sf [Loop] event formula ϕ. Then, we take ξ = E ϕ, which is trivially equivalent to ∃x.Φ 1 (x).

From Theorem 1 and Proposition 1, we deduce that FO has the three variable property:

Corollary 1. L(FO[→, , ≤]) = L(FO 3 [→, , ≤]).

From PDL sf [Loop] to CFMs

In this section, we show that, from a PDL sf [Loop] sentence, we can effectively construct an equivalent CFM of exponential size (Theorem 2). Together with Theorem 1, this implies that every FO sentence can be translated to an equivalent CFM (Theorem 3).

In the inductive translation of PDL sf [Loop] formulas into CFMs, event formulas will be evaluated by MSC transducers. An MSC transducer for an event formula ϕ produces a truth value at every event on the given MSC. More precisely, it outputs 1 when ϕ holds at the current event, and 0 otherwise. We introduce MSC transducers formally in the next section. Then, we present the actual translation of PDL sf [Loop] event formulas into MSC transducers in Section 4.2. We concluce in Section 4.3 with the translation of sentences, PDL sf [Loop] or FO, into CFMs.

Letter-to-letter MSC Transducers

Let Γ be a nonempty finite output alphabet. A (nondeterministic) letter-to-letter MSC transducer (or simply, transducer) A over P and from Σ to Γ is a CFM over P and Σ × Γ. The transducer A accepts the relation

A = { (E, →, , loc, λ), (E, →, , loc, γ) | (E, →, , loc, λ × γ) ∈ L(A)} .
Transducers are closed under product and composition, using standard constructions: Lemma 8. Let A be a transducer from Σ to Γ, and A a transducer from Σ to Γ . There exists a transducer A × A from Σ to Γ × Γ such that

A × A = (E, →, , loc, λ), (E, →, , loc, γ × γ ) | (E, →, , loc, λ), (E, →, , loc, γ) ∈ A , (E, →, , loc, λ), (E, →, , loc, γ ) ∈ A .
Lemma 9. Let A be a transducer from Σ to Γ, and A a transducer from Γ to Γ . There exists a transducer A • A from Σ to Γ such that

A • A = A • A = {(M, M ) | ∃M ∈ MSC(P, Γ) : (M, M ) ∈ A , (M , M ) ∈ A } .

Translation of PDL sf [Loop] Event Formulas into MSC Transducers

For a PDL sf [Loop] event formula ϕ and an MSC M = (E, →, , loc, λ) over P and Σ, we define an MSC M ϕ = (E, →, , loc, γ) over P and {0, 1}, by setting γ(e) = 1 if M, e | = ϕ, and γ(e) = 0 otherwise.

The goal of this section is to show that (Proposition 3), from any PDL sf [Loop] event formula ϕ, we can construct an MSC transducer A ϕ of exponential size which is equivalent to ϕ, that is,

A ϕ = {(M, M ϕ ) | M ∈ MSC(P, Σ)}.
We start with the case of formulas from PDL sf [∅], i.e., without Loop. Lemma 10 actually follows from [BKM10, Theorem 4.16] since PDL sf [∅] is a restricted fragment of the (loop-free) logic studied in [START_REF] Bollig | Propositional dynamic logic for message-passing systems[END_REF]. For completeness, we provide a proof of the following simpler lemma.

Lemma 10. Let ϕ be a PDL sf [∅] event formula. There exists a transducer A ϕ with 2 O(|ϕ|) states per process such that

A ϕ = {(M, M ϕ ) | M ∈ MSC(P, Σ)}.
Proof. Any PDL sf [∅] event formula is equivalent to some linear-size formula ϕ over the syntax

ϕ ::= p | a | ϕ ∨ ϕ | ¬ϕ | p,q ϕ | -1 p,q ϕ | ϕ - → ϕ | ϕ ← -ϕ | jump p,q ϕ
Indeed, we have π 1 • π 2 ϕ ≡ π 1 ( π 2 ϕ), and {ϕ}? ψ ≡ ϕ ∧ ψ. Notice that → ≡ false ---→ and ← ≡ false ← ---. We define A ϕ by induction on ϕ, by composition of the transducers for the atomic formulas ϕ = p with p ∈ P, or ϕ = a with a ∈ Σ, and of transducers B ∨ , B ¬ , B p,q , B -1 p,q , B jump p,q , B XU , and B YS corresponding to each construct of the logic. These transducers are defined in Figure 9. For instance, the transducer B ¬ from {0, 1} to {0, 1} outputs the negation of the bit read and B ∨ from {0, 1} 2 to {0, 1} outputs the disjunction of the two bits read. The transducer B p,q from {0, 1} to {0, 1} outputs 1 at an event e iff e is a send event from p to q and the corresponding receive event f is labeled 1. The transducers B -1 p,q and B jump p,q are defined similarly. The deterministic transducer B YS from {0, 1} 2 to {0, 1} corresponds to the strict since modality. On each process, it outputs 1 at some event e if there is g < proc e, where the second bit is 1 and for all g < proc f < proc e the first bit at f is 1. The transducer B XU corresponds to the reverse strict until modality. We then let

A ϕ 1 ∨ϕ 2 = B ∨ • (A ϕ 1 × A ϕ 2 ) A ¬ϕ = B ¬ • A ϕ A p,q ϕ = B p,q • A ϕ A -1 p,q ϕ = B -1 p,q • A ϕ A ϕ 1 --→ ϕ 2 = B XU • (A ϕ 1 × A ϕ 2 ) A jump p,q ϕ = B jump p,q • A ϕ A ϕ 1 ← --ϕ 2 = B YS • (A ϕ 1 × A ϕ 2 ) .
This concludes the proof of Lemma 10.

Next, we look at a single loop where the path π ∈ PDL sf [∅] is functional. We call a path formula π ∈ PDL sf functional if, for all MSCs M and events e in M, π (e) is either empty or a singleton. Abusing notation, when π (e) ∅, we simply write π (e) = e instead of π (e) = {e }.

We say that a functional path formula π ∈ PDL sf is monotone if, for all MSCs M and events e, f such that π (e) ∅, π ( f ) ∅, and e ≤ proc f , we have π (e) ≤ proc π ( f ).

Notice that, for all path formulas π ∈ PDL sf [Loop], the path formulas min π and max π are functional. Moreover, as a direct consequence of Lemma 3(a), we obtain: Lemma 11. All functional PDL sf [Loop] path formulas are monotone.

Lemma 12. Let π be a PDL sf [∅] functional path formula, and ϕ = Loop(π). There exists a transducer A ϕ with 2 O(|ϕ|) states per process such that A ϕ = {(M, M ϕ ) | M ∈ MSC(P, Σ)}.

Proof. We can assume that Comp(π) ⊆ id. We define A ϕ as the composition of three transducers that will guess and check the evaluation of ϕ. More precisely, A ϕ will be obtained as an inverse projection α -1 , followed by the intersection with some MSC language K, followed by a projection β.

We first enrich the labeling of the MSC with a color from Θ = { , , , }. Intuitively, colors and will correspond to a guess that the formula ϕ is satisfied, and colors and to a guess that the formula is not satisfied. We will construct a CFM that enforces a coloring that, at every event, correctly reflects the truth value of ϕ. We require that labels from { , } alternate on a process (Condition 1. below) and that, moreover, for every event e with a color from { , }, there exist a π-successor and a π -1 -successor that both have the same color (Condition 2.). This will then ensure that an event with color from { , } satisfies ϕ. Moreover, for every { , }-colored event e that has both a π-successor f and a π -1 -successor f , the colors of e, f , and f should not coincide (again, Condition 2.). This, in turn, ensures that e does not satisfy ϕ. Let us formalize these ideas.

Consider the projection α : MSC(P, Σ × Θ) → MSC(P, Σ) which erases the color from the labeling. The inverse projection α -1 can be realized with a transducer A, i.e., A = {(α(M ), M ) | M ∈ MSC(P, Σ × Θ)}.

Define the projection β : MSC(P, Σ × Θ) → MSC(P, {0, 1}) by β((E, →, , loc, λ × θ)) = (E, →, , loc, γ), where γ(e) = 1 if θ(e) ∈ { , }, and γ(e) = 0 otherwise. The projection β can be realized with a transducer A , i.e.,

A = {(M , β(M )) | M ∈ MSC(P, Σ × Θ)}.
Finally, consider the language K ⊆ MSC(P, Σ × Θ) of MSCs M = (E, →, , loc, λ × θ) satisfying the following two conditions:

s p p -/1, - s q q p -/0, - A p Acc = s p p a/1, - b/0, -, b a A a Acc = s p p 1/0, - 0/1, - B ¬ Acc = s p p (-, 1)/1, - (1, -)/1, - (0, 0)/0, - B ∨ Acc = s p p -/1, ! q 1 -/0, ! q 0 -/0, α , α ! q m
s q q 1/0, ? p 1 0/0, ? p 0 -/0, α , α ? ps r r {p, q} -/0, -B p,q Acc = s p p 1/0, ! q 1 0/0, ! q 0 -/0, α , α ! qs q q -/1, ? p 1 -/0, ? p 0 -/0, α , α ? p -

s r r {p, q} -/0, - B -1 p,q Acc = s p p s 0 p s 1 p -/0, - -/1, - -/0, - -/1, - s 0 q q s 1 q 0/0, - 1/0, - -/0, - s r r {p, q} -/0, - Acc = p, s p ∨ i=1,2 ( p, s i p ∨ p, s i p ∞ ) ∧ ( q, s i q ∨ q, s i q ∞ ) B jump p,q s p p s p (-, 0)/0, - (-, 1)/0, - (0, 0)/1, - (1, 0)/1, - (-, 1)/1, - B YS Acc = s 0 p p s 1 p s 2 p s 3 (-, -)/1, - (-, -)/1, - (-, -)/0, - (-, 1)/1, - (1, 0)/1, - (-, 0)/0, - (-, 1)/1, - (1, 0)/1, - (-, 1)/0, - (0, 0)/1, - (0, 0)/1, - B XU Acc = p∈P p, s 0 p ∨ p, s 3 p ∨ p, s 1 p ∞ ∨ p, s 3 p ∞
Figure 9: Transducers used to define A ϕ . In a transition labeled a/b, α , a is the input letter, b is the output letter, and α is either empty or a read or write action. Notice that in B p,q , the automaton for process q has no transitions reading c/0, ? p d , with c d, hence a wrong guess by process p cannot lead to an accepting run. The acceptance condition means true and is always satisfied. 1. Colors and alternate on each process p ∈ P: if e 1 < e 2 < e 3 < • • • are the events in E p ∩ θ -1 ({ , }), then θ(e i ) = if i is odd, and θ(e i ) = if i is even. 2. For all e ∈ E, θ(e) ∈ { , } iff there exist f, f ∈ E such that M, e, f | = π, M, e, f | = π -1 , and θ(e) = θ( f ) = θ( f ). The first property is trivial to check with a CFM. Using Lemma 10, we show that the second property can also be checked with a CFM. First, from π we construct a PDL sf [∅] event formula ψ over P and Σ × Θ such that, for all M = (E, →, , loc, λ × θ) ∈ MSC(P, Σ × Θ) and events e ∈ E, we have M , e | = ψ iff the following holds: θ(e) ∈ { , } iff there are f, f ∈ E such that θ(e) = θ( f ) = θ( f ), α(M ), e, f | = π, and α(M ), e, f | = π -1 . Namely, we define

ψ = ( ∨ ) ⇐⇒ col∈{ , , , } col ∧ π col ∧ π-1 col
where the state formula col from { , , , } is an abbreviation for a∈Σ (a, col) and π is obtained from π by replacing state formulas a by col∈Θ (a, col). Now, the language for the second condition is {M ∈ MSC(P, Σ × Θ) | every event of M ψ is labeled with 1}, for which we can easily give a CFM using the transducer A ψ from Σ × Θ to {0, 1} given by Lemma 10.

We deduce that there is a transducer So there exists f ∈ E such that γ( f ) = 1 and M, f | = ϕ. Notice that θ( f ) ∈ { , }. Let f be the unique event such that M, f, f | = π. Such an event exists by Condition 2., and is unique since π is functional.

A such that A = {(M , M ) | M ∈ K}. We let A ϕ = A • A • A. Notice that A ϕ = {(α(M ), β(M )) | M ∈ K}.
Suppose f < proc f . Let f 0 = f , f 1 = f , and for all i ∈ N, let f i+1 be the unique event such that M, f i , f i+1 | = π. Note that, for all i, θ( f i+1 ) = θ( f i ) ∈ { , }. By Condition 1., there exists g 0 such that f 0 > proc g 0 > proc f 1 and θ( f 0 ) θ(g 0 ) ∈ { , }. For an illustration, see Figure 11. Again, for all i ∈ N, let g i+1 be the unique event such that M, g i , g i+1 | = π. Note that all f 0 , f 1 , . . . have the same color, in { , }, and all g 0 , g 1 , . . . carry the complementary color. Thus, f i g j for all i, j ∈ N. But, by Lemma 11, this implies f 0 > proc g 0 > proc f 1 > proc g 1 > proc • • • , which contradicts the fact that the past of f 0 is finite. Similarly, suppose f < proc f . Let f 0 = f , f 1 = f , and for all i ∈ N, let f i+1 be some event such that M, f i ,

• • • f 0 f 1 f 2 g 0 g 1 g 2 π π π π π
f i+1 | = π -1 and θ( f i+1 ) = θ( f i ) ∈ { , }. Let us show that f 0 > proc f 1 > proc f 2 > proc • • • , by contradiction. Assume that f i ≤ proc f i+1 for some minimal i ≥ 1. Since π is functional, we have π ( f i ) = { f i-1 }, and π ( f i+1 ) = { f i }.
Then, by Lemma 11, f i-1 ≤ proc f i , which contradicts the minimality of i.

(Claim 3)

This concludes the proof of Lemma 12.

The general case is more complicated. We first show how to rewrite an arbitrary loop formula using loops on paths of the form π or π • + -→ where π is functional. Intuitively, this means that loop formulas will only be used to perform the following test. Given an event e such that there exists a (unique) e with M, e, e | = π, and e is on the same process as e, which one of the following is true: e < proc e, e = e, or e < proc e ? Indeed, we have M, e | = Loop(π

• + -→) iff e < proc e.
Lemma 13. For all PDL sf [Loop] path formulas π,

Loop(π) ≡ Loop(min π) ∨ π -1 ∧ Loop((min π) • + -→) ∧ ¬Loop((max π) • + -→) .
Proof. The result essentially follows from Lemma 4, saying that π (e) is exactly the set of events in the interval from min π (e) to max π (e) that satisfy π -1 .

First Finally, we are ready to prove the general case, translating PDL sf [Loop] event formulas to MSC transducers: Proposition 3. For every PDL sf [Loop] event formula ϕ, there exists a transducer A ϕ with 2 O(|ϕ| 2 ) states per process such that

A ϕ = {(M, M ϕ ) | M ∈ MSC(P, Σ)}.
Proof. We proceed by induction on the number of loop subformulas in ϕ. The base case is stated in Lemma 10. Let ψ = Loop(π ) be a subformula of ϕ such that π contains no loop subformulas and Comp(π ) ⊆ id. We will show below that there exists a transducer A ψ with 2 O(|ψ| 2 ) states per process such that

A ψ = {(M, M ψ ) | M ∈ MSC(P, Σ)}.
Suppose that we have constructed A ψ . Consider the formula ϕ over Σ × {0, 1} obtained from ϕ by replacing ψ by a∈Σ (a, 1), and all event formulas a, with a ∈ Σ, by (a, 0) ∨ (a, 1). It contains fewer Loop operators than ϕ, so by induction hypothesis, we have a transducer A ϕ for ϕ . We then let A ϕ = A ϕ •(A Id ×A ψ ), where A Id is the transducer for the identity relation.

Thus, all we need to prove is that we can construct such a transducer A ψ . We first apply Lemma 13. We construct So it suffices to show that for any functional path formula π ∈ PDL sf [Loop], there exists a transducer of size 2 O(|π|) for the formula ψ = Loop(π • + -→). We assume that Comp(π) ⊆ id. We start with some easy remarks. Let p ∈ P be some process and e ∈ E p . A necessary condition for M, e | = ψ is that M, e | = π , and since π is functional, that M, e | = Loop(π).

We let E π p be the set of events e ∈ E p satisfying π . For all e ∈ E π p , we let e ∈ E p be the unique event such that M, e, e | = π. The transducer A ψ will establish, for each e ∈ E π p , whether e < proc e, e = e, or e < proc e , and it will output 1 if e < proc e, and 0 otherwise. The case e = e means M, e | = Loop(π) and can be checked with the help of Lemma 12. So the difficulty is to distinguish between e < proc e and e < proc e when M, e | = π ∧¬Loop(π).

Claim 4. Let ψ = Loop(π • + -→) and let f be the minimal event in E π p (assuming this set is nonempty). Then, M, f

| = ψ iff M, f | = Loop(min ( + ← -• π -1 )).
Proof of Claim 4. The right to left implication holds without any hypothesis. Conversely, let f = π ( f ) and assume that f

+ -→ f . Then, M, f, f | = + ← -• π -1 , and g = min ( + ← -• π -1 ) ( f )
is well-defined and g ≤ proc f . This is illustrated in Figure 12. Moreover, M, g | = π and by minimality of f in E π p , we conclude that g = f . (Claim 4) ---→.

f f g = min ( + ← -• π -1 ) + π
1. If M, e | = ψ, then [M, f | = ψ iff M, f | = Loop(π) ∨ Loop(min ( + -→ • π -1 ))]. 2. If M, e | = ψ, then [M, f | = ψ iff M, f | = Loop(max (π • ¬ π ---→))].
Proof of Claim 5. We show the two statements. ) ( f ) is well-defined and g ≤ proc f . Notice that g ∈ E π p , and f < proc g = π (g). If g < proc f (see Figure 13), we get g ≤ proc e, and using Lemma 11, we obtain g ≤ proc e < proc e < proc f , a contradiction. Therefore, g = f and M, f | = Loop(min ( We have e ≤ proc e and f < proc f (see Figure 14).

+ -→ • π -1 )).
From Lemma 11 we get e ≤ proc f and since e, f are consecutive in

E π p , we obtain M, f , f | = ¬ π ---→. Therefore, M, f | = Loop(π • ¬ π ---→) ≡ Loop(max (π • ¬ π ---→)).
This concludes the proof of the claim. (Claim 5). To conclude the proof of Proposition 3, let us consider the five formulas

ϕ 1 = π , ϕ 2 = Loop(π), ϕ 3 = Loop(min ( + ← -• π -1 )), ϕ 4 = Loop(min ( + -→ • π -1
)), and

ϕ 5 = Loop(max (π • ¬ π ---→)).
We can easily see that ϕ 1 ∧ ¬ϕ 2 ∧ ¬ϕ 4 is a necessary condition for ψ = Loop(π • + -→). Also, both ϕ 3 and ϕ 5 are sufficient conditions for ψ. The only case which is not covered is when M, f | = ϕ 1 ∧ ¬ϕ 2 ∧ ¬ϕ 3 ∧ ¬ϕ 4 ∧ ¬ϕ 5 . In this case, from Claims 4 and 5, we see that

M, f | = ψ iff f is not minimal in E π p and M, e | = ψ
, where e is the predecessor of f in E π p . By Lemmas 10 and 12, we already have transducers A ϕ i for i ∈ {1, 2, 3, 4, 5}. We let

A ψ = A • (A ϕ 1 × A ϕ 2 × A ϕ 3 × A ϕ 4 × A ϕ 5 ), where, at an event f labeled (b 1 , b 2 , b 3 , b 4 , b 5 ), the transducer A outputs 1 if b 3 = 1 or b 5 = 1 or if (b 1 , b 2 , b 3 , b 4 , b 5 ) = (1
, 0, 0, 0, 0) and the output was 1 at the last event e on the same process satisfying ϕ 1 (to do so, each process keeps in its state the output at the last event where b 1 was 1), and 0 otherwise.

Translation of PDL sf [Loop] and FO Sentences into CFMs.

Wrapping-up, we obtain our main results as corollaries. First the translation of PDL sf [Loop] sentences to CFMs:

Theorem 2. For every PDL sf [Loop] sentence ξ, there exists a CFM A ξ with 2 O(|ξ| 2 ) states per process such that

L(A ξ ) = L(ξ).
Proof. Given an event formula ϕ, we can construct A ϕ according to Proposition 3. From A ϕ , it is easy to build CFMs for the sentences E ϕ and ¬ E ϕ. Closure of L(CFM) under union and intersection takes care of disjunction and conjunction.

By Theorem 1, every FO[→, , ≤] sentence Φ is equivalent to some PDL sf [Loop] sentence ξ, for which there is an equivalent CFM A ξ by Theorem 2. Therefore, we obtain:

Theorem 3. L(FO[→, , ≤]) ⊆ L(CFM).
The translation is effective, but inherently non-elementary, already when |P| = 1 [START_REF] Stockmeyer | The Complexity of Decision Problems in Automata Theory and Logic[END_REF]. It is standard to prove L(CFM) ⊆ L(EMSO[→, ]): The formula guesses an assignment of transitions to events in terms of existentially quantified second-order variables (one for each transition) and then checks, in its first-order kernel, that the assignment is indeed an (accepting) run. As, moreover, the class L(CFM) is closed under projection, we obtain the following logical characterization of CFMs as a corollary:

Theorem 4. L(EMSO[→, , ≤]) = L(CFM).

Applications

Existentially bounded MSCs

Though the translation of EMSO/FO formulas into CFMs is interesting on its own, it allows us to obtain some difficult results for bounded CFMs as corollaries. In fact, we even extend known results to infinite MSCs.

Bounded MSCs. The first logical characterizations of communicating finite-state machines were obtained for classes of bounded MSCs. Intuitively, this corresponds to restricting the channel capacity. Bounded MSCs are defined in terms of linearizations. A linearization of a given MSC M = (E, →, , loc, λ) is a total order ⊆ E × E extending ≤ and of order type at most ω, i.e., ≤ ⊆ and {e | e f } is finite for all f ∈ E. For B ∈ N, we call B-bounded if, for all g ∈ E and (p,

q) ∈ Ch, |{(e, f ) ∈ ∩ (E p × E q ) | e g ≺ f }| ≤ B.
In other words, the number of pending messages in (p, q) never exceeds B if we follow the linearization defined by . There are (at least) two natural definitions of bounded MSCs: We call M ∃B-bounded if M has some B-bounded linearization. Accordingly, it is ∀B-bounded if all its linearizations are B-bounded. The set of ∃B-bounded MSCs is denoted by MSC ∃B (P, Σ), the set of ∀B-bounded MSCs by MSC ∀B (P, Σ). Moreover, we let MSC fin ∃B (P, Σ) := MSC ∃B (P, Σ) ∩ MSC fin (P, Σ) and MSC fin ∀B (P, Σ) := MSC ∀B (P, Σ) ∩ MSC fin (P, Σ).

Example 7. The MSC from Figure 1 is ∃1-bounded, but it is not ∀B-bounded, no matter what B is.

In this subsection, we will consider only ∃B-bounded MSCs. We show the following results. First, for a given channel bound B, the set MSC ∃B (P, Σ) is FO[→, , ≤]-definable (essentially due to [START_REF] Lohrey | Bounded MSC Communication[END_REF]). By Theorem 4, we obtain [GKM06, Proposition 5.14] stating that this set is recognized by some CFM. Second, we obtain [GKM06, Proposition 5.3], a Büchi-Elgot-Trakhtenbrot theorem for existentially bounded MSCs, as a corollary of Theorem 4 in combination with a linearization normal form from [START_REF] Thiagarajan | An expressively complete linear time temporal logic for Mazurkiewicz traces[END_REF].

Known results. Let M = (E, →, , loc, λ) be some finite or infinite MSC. Given e ∈ E, we write type(e) = p if e is an internal event on process p, type(e) = p!q if e is a write on channel (p, q), and type(e) = q?p if e is a read from channel (p, q). We associate with the linearization a word M over the alphabet Σ lin = Σ × (P ∪ {p!q, q?p | (p, q) ∈ Ch}). Namely, if the linearization is

e 1 ≺ e 2 ≺ e 3 ≺ • • • , we let M = a 1 a 2 a 3 • • • where a i = (λ × type)(e i ). Note that M can be retrieved from M . We let Lin B (M) = {M | is a B-bounded linearization of M} ⊆ Σ * lin ∪ Σ ω lin .
Fact 8 ( [GKM06, Theorem 4.1]). Let B ∈ N and L ⊆ MSC fin ∃B (P, Σ). The following are equivalent:

1. L = L(A) for some CFM A.

2. L = L(Φ) for some MSO formula Φ.

3. Lin B (L) is a regular language (of finite words).

The proof given in [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF] relies on the theory of Mazurkiewicz traces. Another major part of the proof is the construction of a CFM recognizing the set MSC fin ∃B (P, Σ) of finite ∃B-bounded MSCs [GKM06, Proposition 5.14]. We show below that this CFM, or more generally, a CFM for the set MSC ∃B (P, Σ) of finite or infinite ∃B-bounded MSCs, can in fact be obtained as a simple application of Theorem 4. Moreover, we give an alternative proof of (3) =⇒ (1) (Section 5 in [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]), and again extend the result to infinite MSCs.

As mentioned before, the implication (1) =⇒ (2) follows from a standard translation of CFMs into EMSO. Finally, (2) =⇒ (3) is also easy to prove: the channel bound can be used to translate the MSO sentence Φ into an MSO sentence over Σ lin -labeled words, defining Lin B (L).

A CFM for Existentially Bounded MSCs. The set MSC ∃B (P, Σ) of ∃B-bounded MSCs is in fact FO[ , →, ≤]definable, and thus, we can apply Theorem 4 to construct a CFM A ∃B recognizing MSC ∃B (P, Σ). We describe below a formula defining MSC ∃B (P, Σ).

Let us first recall a characterization of ∃B-bounded MSCs. Let M = (E, →, , loc, λ) be an MSC. We define a relation rev B ⊆ E × E which consists of the set of pairs ( f, g) such that f is a receive event from some channel (p, q) with corresponding send event e f , and g is the B-th send on channel (p, q) after event e. The relation rev B is illustrated in Figure 15 (represented by the dashed edges) for B = 1 and an ∃1-bounded MSC. It can be defined by the PDL sf [∪] path formula

rev B = p q -1 p,q • ¬ p,q ------→ •{ p,q }? B .
For completeness, let us also give a corresponding FO[→, , ≤] formula: In fact, a linearization of M is B-bounded iff it contains rev B . Indeed, assume that rev B ⊆ and that is not B-bounded. Then, we find

rev B (x, y) := ∃z 0 , z 1 , . . . , z B . z 0 x ∧ z B = y ∧ 1≤i≤B ∃x i . z i x i ∧ x ≤ proc x i ∧ 0≤i<B z i < proc z i+1 ∧ ¬(∃z , x . z i < proc z < proc z i+1 ∧ z x ∧ x ≤ proc x ) .
e 0 ≺ e 1 ≺ • • • ≺ e B g ≺ f 0 ≺ f 1 ≺ • • • ≺ f B with (e i , f i ) ∈ p,q ∩ E p × E q .
Without loss of generality, we can assume that there are no other writes on channel (p, q) between e i and e i+1 . This implies ( f 0 , e B ) ∈ rev B , a contradiction. Conversely, if rev B then we find ( f 0 , e B ) ∈ rev B with e B ≺ f 0 . We deduce that

e 0 ≺ e 1 ≺ • • • ≺ e B ≺ f 0 ≺ f 1 ≺ • • • ≺ f B with (e i , f i ) ∈ ∩ E p × E q
and the linearization is not B-bounded.

Note that, if (< ∪ rev B ) contains a cycle, then it contains one of size at most 2|P|. More precisely, M is ∃B-bounded if and only if it satisfies the PDL sf [Loop, ∪] formula ξ ∃B = ¬ E Loop(lt B ), where

lt B = 2≤n≤|P| ( ∪ rev B ) • + -→ n = p q p,q .
Again, let us determine an equivalent FO[→, , ≤] formula:

Φ ∃B = 2≤n≤2|P| ¬ ∃x 0 , . . . , x n . x 0 = x n ∧ 0≤i<n x i < x i+1 ∨ rev B (x i , x i+1 ) .
Applying Theorem 4 we obtain Corollary 2. Given B > 0, we can construct a CFM A ∃B recognizing the set MSC ∃B (P, Σ) of ∃B-bounded finite or infinite MSCs.

FO-definable Linearizations for Existentially Bounded MSCs. We will make use of canonical linearizations of certain MSCs, which we adapt from [TW02, Definition 13] where the definition was given for traces. It is based on the following lemma. Though it is stated for a special case in [START_REF] Thiagarajan | An expressively complete linear time temporal logic for Mazurkiewicz traces[END_REF], the proof can be taken almost verbatim. We only provide the proof for completeness.

Lemma 14 ( [TW02, Lemma 14]). Let (E, ≤) be a partially ordered set, and ⊆ E × E a strict well-founded total order. For e, f ∈ E, we write e f when e ≤ f and f ≤ e, and we let ↑e

= { f ∈ E | e ≤ f }. Then the relation ≺ ⊆ E × E defined by e ≺ f ⇐⇒           e < f ∨ e f ∧ min (↑e \ ↑ f ) min (↑ f \ ↑e)          
is a strict linear order extending <.

Proof. Notice that, for all e f , we have either e ≺ f or f ≺ e, but not both. Indeed, for all e f , we have ↑e \ ↑ f ∩ ↑ f \ ↑e = ∅, and if e f , then the two sets are nonempty as e ∈ ↑e \ ↑ f and f ∈ ↑ f \ ↑e.

It remains to show that ≺ is transitive. Let e 1 , e 2 , e 3 ∈ E such that e 1 ≺ e 2 ≺ e 3 . Note that e 1 , e 2 , e 3 are pairwise distinct. For distinct i, j ∈ {1, 2, 3}, if ↑e i \ ↑e j ∅, we let e i j = min ↑e i \ ↑e j .

To prove e 1 ≺ e 3 , we distinguish several cases.

Case e 1 < e 2 < e 3 : As < is transitive, we get e 1 < e 3 .

Case e 1 < e 2 e 3 : This implies e 3 ≤ e 1 . If e 1 < e 3 , we are done. So suppose e 1 e 3 . Since e 2 ≺ e 3 , we have e 23 e 32 . From ↑e 2 ⊆ ↑e 1 , we deduce ↑e 2 \ ↑e 3 ⊆ ↑e 1 \ ↑e 3 . Thus, e 13 e 23 . Similarly, e 32 e 31 . We obtain e 13 e 23 e 32 e 31 .

Case e 1 e 2 < e 3 : This case is very similar to the previous one.

Case e 1 e 2 e 3 : Since e 1 ≺ e 2 ≺ e 3 , we have e 12 e 21 and e 23 e 32 . Suppose e 1 ≤ e 3 (otherwise, we are done).

We This concludes the proof of Lemma 14.

We now define a canonical linear order on the events of an ∃B-bounded MSC M = (E, →, , loc, λ). We fix some strict total order on P, and extend it to E as follows: e f if e < proc f or loc(e) loc( f ). Clearly, is well-founded and a strict linear order on E. We apply Lemma 14 with and ≤ B = (≤ ∪ rev B ) * which is a partial order when the MSC M is ∃B-bounded. We obtain a linear order B of M extending both < and rev B .

Example 8. Consider the MSC M in Figure 15 andsuppose p 1 p 2 p 3 p 4 . We have min (↑e \ ↑ f ) = g and min (↑ f \ ↑e) = f . Since g f , we obtain e ≺ B f . In general, B need not be of order type at most ω, i.e., it is not necessarily a linearization. For instance, with two processes p q, no communication events, and infinitely many local events on both p and q, the order type of B is ω + ω. When the order type of B is at most ω, it is a B-bounded linearization of M.

Finally, the relation ≺ B is FO[→, , ≤]-definable. Indeed, the strict partial order < B is FO[→, , ≤]-definable since it can be expressed with the path formula lt B given above. From its definition, we deduce that the relation ≺ B is also FO[→, , ≤]-definable.

We are now ready to give our alternative proof of the direction (3) =⇒ (1) in Fact 8.

Proof of Fact 8 (3) =⇒ (1). Let L be a set of ∃B-bounded finite MSCs such that Lin B (L) is regular. There exists an EMSO sentence Φ lin over Σ lin -labeled words such that Lin B (L) = L(Φ lin ). Since B is FO[→, , ≤]-definable, it is easy to translate Φ lin into an EMSO[→, , ≤] formula Φ such that L(Φ) ⊆ MSC fin ∃B (P, Σ) and, for all M ∈ MSC fin ∃B (P, Σ), we have

M | = Φ if and only if M B | = Φ lin . Let A be a CFM such that L(A) = L(Φ ∧ Φ ∃B ). Then, for all M ∈ L, M is ∃B-bounded and M B | = Φ lin , hence M | = Φ ∧ Φ ∃B , i.e., M ∈ L(A). Conversely, if M ∈ L(A), then M ∈ MSC fin ∃B (P, Σ) and B is a linearization of M. Moreover, M B ∈ Lin B (L), hence M ∈ L.
The extension of Fact 8 to infinite MSCs requires some extra work since the order type of B need not be at most ω. We denote by MSC ω ∃B (P, Σ) the set of infinite ∃B-bounded MSCs.

Theorem 5. Let B ∈ N and L ⊆ MSC ω ∃B (P, Σ). The following are equivalent:

1. L = L(A) for some CFM A.

2. L = L(Φ) for some MSO formula Φ.

3. Lin B (L) is an ω-regular language.

The rest of Section 5.1 is devoted to the proof of (3) =⇒ (1), while (1) =⇒ (2) and (2) =⇒ (3) are again standard. Recall that we cannot exactly proceed as in the case of finite MSCs, as the canonical linear order associated with an infinite existentially bounded MSC is not necessarily of order type ω. We therefore adopt decomposition techniques and results from [START_REF] Thiagarajan | An expressively complete linear time temporal logic for Mazurkiewicz traces[END_REF] and [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF], where Mazurkiewicz traces and universally bounded MSCs are considered, respectively. We first define a decomposition of an existentially bounded MSC into a finite part and boundedly many disconnected infinite parts M j such that the canonical linear order of each M j is in fact of order type ω, i.e., a canonical linearization (Lemma 16). Similarly, the given ω-regular word language Lin B (L) can be described as the composition of regular (and therefore EMSO-definable) finite and shuffled infinite parts such that the infinite parts correspond to linearizations of the MSCs M j (Lemmas 18-20). The corresponding EMSO formulas over words can then be transformed into EMSO formulas over MSCs using FO-definability of canonical linearizations (Lemma 21). In this step, it is crucial that the separate infinite parts M j actually have canonical linearizations. This guarantees that word formulas for linearizations are faithfully simulated by the associated formulas over MSCs. Using our main result, Theorem 4, we can now conclude that there is a CFM for the target language L.

Let us be precise. We start by defining a decomposition of infinite MSCs such that in each component of the decomposition, B is of order type at most ω.

Let M = (E, →, , loc, λ) ∈ MSC ω ∃B (P, Σ). We denote by Types fin (M) (resp. Types inf (M)) the set of types that occur finitely many times (resp. infinitely often) in M:

Types fin (M) = {type(e) | e ∈ E ∧ { f ∈ E | type(e) = type( f )} is finite} Types inf (M) = {type(e) | e ∈ E ∧ { f ∈ E | type(e) = type( f )} is infinite} .
We then let

E fin = {e ∈ E | ∃ f ∈ E : e ≤ B f ∧ type( f ) ∈ Types fin (M)} and E inf = E \ E fin .
Recall that ≤ B = (≤ ∪ rev B ) * . The definition of E fin and E inf depends not only on M, but also on the given bound B.

Note that E fin and E inf are not necessarily -closed: there may be some send events in E fin whose matching receive events are in E inf (the converse is not possible, since E fin is downward closed). However, since M is B-bounded, there are at most B unmatched sends in E fin for every channel (p, q). Lemma 15. There exists a B-bounded linearization of M such that for all e ∈ E fin and f ∈ E inf , e f .

Proof. Recall that a linearization of M is B-bounded if and only if it contains ≤ B . Let be any B-bounded linearization of M, and the concatenation of its restrictions to E fin and E inf . That is, e f if and only if e ∈ E fin and f ∈ E inf , or e f and e, f ∈ E fin , or e f and e, f ∈ E inf . Clearly, is a total order on E. Let us show that for all e ≤ B f , we have e f . Since is a B-bounded linearization of M, we have e f , and thus, if e, f ∈ E fin or e, f ∈ E inf , we get e f . If e ∈ E fin and f ∈ E inf , then e f by definition. Finally, we cannot have e ∈ E inf and f ∈ E fin since E fin is downward-closed with respect to ≤ B .

We further decompose E inf into its connected components, as follows. We denote by P 1 , . . . , P m the maximal connected components of the undirected communication graph at infinity (P, {{p, q} | Types inf (M) ∩ {p!q, q!p} ∅}). For all 1 ≤ j ≤ m, we then let

E j = E inf ∩ p∈P j E p .
Note that, by definition, every E j is infinite.

Finally, we associate with E fin , E inf , and each E j the following MSCs over Σ lin :

M fin = (E fin , → ∩ E fin × E fin , ∩ E fin × E fin , loc| E fin , (λ × type)| E fin ) M inf = (E inf , → ∩ E inf × E inf , ∩ E inf × E inf , loc| E inf , (λ × type)| E inf ) M j = (E j , → ∩ E j × E j , ∩ E j × E j , loc| E j , (λ × type)| E j ) .
Note that send events of M which are located in E fin and whose matching receive event is in E inf become internal events in M fin , and similarly for unmatched receive events in the infinite part. Adding the types of all events to the labeling allows us to maintain any information on M in its decomposition.

Lemma 16. For all M j with 1 ≤ j ≤ m, B is of order type ω.

Proof. This is in fact true of any linear extension of ≤ B , and not just the canonical B . We want to prove that for every e ∈ E j , the set { f ∈ E j | f B e} is finite. To do so, it suffices to prove that for all p ∈ P j , there exists f ∈ E j p such that e ≤ B f (and thus e B f ). By definition of P j , there exists a path p 1 , . . . , p such that p 1 = loc(e), p = p, and for all 1 ≤ i < , M j contains infinitely many events of type p i !p i+1 or p i ?p i+1 . If M j contains infinitely many events of type p i !p i+1 , then for all e on process p i , there exist f on process p i and g on process p i+1 such that e ≤ proc f and f g , hence e ≤ B g . If M j contains infinitely many events of type p i ?p i+1 , then for all e on process p i , there exist f on process p i and g on process p i+1 such that e ≤ proc f and f rev B g , hence e ≤ B g . Therefore, we obtain events e 2 , . . . , e on processes p 2 , . . . , p = p such that e ≤ B e 2 ≤ B • • • ≤ B e .

To avoid any ambiguity, in this proof, we write e.g. FO[Σ, P, ≤, ] or FO[Σ lin , P, ≤, ], rather than FO[≤, ], so as to distinguish between formulas over MSCs over Σ and P, and MSCs over Σ lin and P coming from decompositions. We also denote by FO[Σ lin , ], EMSO[Σ lin , ], and MSO[Σ lin , ] formulas over word linearizations, Σ lin being the alphabet, and the underlying total order.

In the rest of the proof, we restrict to MSCs M having a fixed set T = Types inf (M) of types at infinity, with maximal connected components of the induced communication graph at infinity being P 1 , . . . , P m . We decompose Σ lin into disjoint subalphabets Σ fin lin , Σ 1 lin , . . . , Σ m lin as follows. First, we denote by Σ inf lin the set of all (a, t) ∈ Σ lin such that t ∈ T and Σ fin lin = Σ lin \ Σ inf lin . We further decompose Σ inf lin into Σ 1 lin , . . . , Σ m lin , where Σ j lin denotes the set of pairs of the form (a, p), (a, p!q) or (a, p?q) with p ∈ P j (by definition of the decomposition, this is also equivalent to q ∈ P j ). Note that, while every event in M j is labeled with a letter in Σ j lin , events in M fin may have labels in any of the alphabets Σ fin lin , Σ 1 lin , . . . , Σ m lin . However, the labels of all ≤ B -maximal events of M j are in Σ fin lin . For words u, v ∈ Σ * lin ∪ Σ ω lin , we denote by u ¡ v the shuffle of u and v, i.e., the set of words w ∈ Σ * lin ∪ Σ ω lin that are a possible interleaving of u and v. Now, let L ⊆ MSC ω ∃B (P, Σ) be a set of MSCs with types at infinity T . We decompose words in Lin B (L) according to the decomposition of their corresponding MSCs. More precisely, for w ∈ Lin B (L), we denote by w fin , w inf , w 1 , . . . , w m the restrictions of w to positions denoting events located respectively in the parts M fin , M inf , M 1 , . . . , M m of the corresponding MSC M ∈ L. That is, w fin ∈ Σ * lin Σ fin lin ∪{ε} denotes a linearization of M fin , w inf ∈ Σ inf lin ω denotes a linearization of M inf , and w j ∈ Σ j lin ω denotes a linearization of M j . Moreover, w is a shuffle of w fin and w inf , and w inf is itself a shuffle of w 1 , . . . , w m . Lemma 17. For all w ∈ Lin B (L), we have w fin w inf ∈ Lin B (L) and w fin • ¡ m j=1 w j ⊆ Lin B (L). Proof. Let M ∈ L be the MSC corresponding to w. As in Lemma 15, the word w fin w inf is also a B-bounded linearization of M, and thus in Lin B (L). In addition, any v ∈ ¡ m j=1 w j corresponds to a possible B-bounded linearization of M inf . Indeed, since there are no causal dependencies between events in distinct M j , any interleaving of the B-bounded linearizations w 1 , . . . , w m of the different components yields a B-bounded linearization of M inf . This means that we also have w fin v ∈ Lin B (L).

Lemma 18. If Lin B (L) is an ω-regular language then there is a finite sequence of pairs of regular languages (K 1 , L 1 ), . . . , (K k , L k ), with K i ⊆ Σ * lin and L i ⊆ Σ ω lin , such that

(w fin , w inf ) | w ∈ Lin B (L) = 1≤i≤k K i × L i .
Moreover, for all

1 ≤ i ≤ k and (v 1 , . . . , v m ) ∈ Σ 1 lin ω × • • • × Σ m lin ω , if L i ∩ ¡ m j=1 v j ∅ then ¡ m j=1 v j ⊆ L i . Proof.
In order to distinguish, in a linearization, between positions that correspond to the finite or infinite part of the MSC, we define a formula x ≤ B y such that, for all prefixes u of B-bounded linearizations w ∈ Σ ω lin of some MSC M ∈ MSC ω ∃B (P, Σ), and for all positions i and j in u, we have u, [x → i, y → j] | = x ≤ B y if and only if the pair of events in M associated to positions (i, j) is in the relation ≤ B . We first introduce an MSO[Σ lin , ] formula x y with an analogous semantics. The formula simply says that (i) x is a write to channel (p, q) and y a read from channel (p, q), for some (p, q) ∈ Ch, (ii) between x and y, there are less than B messages sent, and read, on channel (p, q), (iii) the count modulo B of messages sent on channel (p, q) up until x, and of messages read from channel (p, q) up until y, are identical. We also let x ≤ proc y := x y ∧ proc(x) = proc(y), where proc(x) = proc(y) is a simple disjunction on the possible labels of x and y. It is then easy to define x ≤ B y from the formulas x y and x ≤ proc y.

We can now define the regular language K ⊆ Σ * lin by the MSO[Σ lin , ] formula ∀x.∃y. x ≤ B y ∧ (a,t)∈Σ fin lin (a, t)(y) . Notice that K contains all finite parts w fin of words w ∈ Lin B (L).

Let ∼ ⊆ K × K be the equivalence relation defined by u ∼ v if u -1 Lin B (L) = v -1 Lin B (L). Since Lin B (L) is regular, ∼ is of finite index. We let K 1 , . . . , K k be the elements of K/∼, and for all 1

≤ i ≤ k, L i = K -1 i Lin B (L) ∩ Σ inf lin ω
. Let w ∈ Lin B (L). By Lemma 17, we have w fin w inf ∈ Lin B (L). Moreover, w fin ∈ K, so there exists i such that

w fin ∈ K i . Then w inf ∈ K -1 i Lin B (L) ∩ Σ inf lin ω , thus (w fin , w inf ) ∈ K i × L i . Conversely, if (u, v) ∈ K i × L i , then u v ∈ Lin B (
L) for some u ∈ K i . Hence, u ∼ u and w = uv ∈ Lin B (L). In addition, since v contains only letters from Σ inf lin , u contains all positions from w fin . Since u is in K, it also contains only positions from w fin , that is, u = w fin . It follows that v = w inf .

Finally, we prove that each L i is closed under commutation of letters in distinct subalphabets

Σ j lin . Let (v 1 , . . . , v m ) ∈ Σ 1 lin ω × • • • × Σ m lin ω
such that there exists some v ∈ L i ∩ ¡ m j=1 v j . Since v ∈ L i , there exist u ∈ K i and w ∈ Lin B (L) such that u = w fin and v = w inf . Since the alphabets Σ j lin are disjoint, this implies v j = w j for all j. By Lemma 17, this

means u • ¡ m j=1 v j ⊆ Lin B (L), hence ¡ m j=1 v j ⊆ u -1 Lin B (L) ∩ Σ inf lin ω = L i .
To further decompose each L i according to the partition of w inf into w 1 , . . . , w m , we apply the lemma below, proven e.g. in [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF]Theorem 4.11].

Lemma 19. Let R be an ω-regular language over a finite alphabet Σ = Σ 1 • • • Σ m . Suppose that every word from R contains every letter from Σ infinitely often and that, for all (u 1 , . . . ,

u m ) ∈ Σ ω 1 × • • • × Σ ω m , u 1 ¡ • • • ¡ u m ∩ R ∅ implies u 1 ¡ • • • ¡ u m ⊆ R. Then R is a finite union of languages of the form R 1 ¡ • • • ¡ R m ,
where R j is an ω-regular language over Σ j .

Lemma 20. If Lin B (L) is an ω-regular language then there is a finite sequence of tuples of regular languages

(K 1 , L 1 i , . . . , L m i ) 1≤i≤ such that (w fin , w 1 , . . . , w m ) | w ∈ Lin B (L) = 1≤i≤ K i × L 1 i × • • • × L m i .
Proof. We apply Lemma 18 and then Lemma 19 to each L i . We obtain a finite family (K i , L 1 i , . . . , L m i ) 1≤i≤ such that all K i ⊆ Σ * lin are regular languages and all L j i ⊆ (Σ j lin ) ω are ω-regular languages, and

(w fin , w inf ) | w ∈ Lin B (L) = 1≤i≤k K i × m ¡ j=1 L j i .
Moreover, for all w ∈ Lin B (L), (w 1 , . . . , w m ) is the unique decomposition of w inf as a shuffle of words in the subalphabets Σ 1 lin , . . . , Σ m lin , which means that w inf ∈ ¡ m j=1 L j i if and only if (w 1 , . . . ,

w m ) ∈ L 1 i × • • • × L m i . We obtain (w fin , w 1 , . . . , w m ) | w ∈ Lin B (L) = 1≤i≤ K i × L 1 i × • • • × L m i .
Since all languages K i and L j i from Lemma 20 are regular or ω-regular, they can be defined in EMSO[Σ lin , ]. This translates into a set of tuples of EMSO[Σ lin , , ≤] formulas over MSC decompositions (using the canonical decomposition similarly to the proof for finite MSCs):

Lemma 21. If Lin B (L) is an ω-regular language then there exists a finite set of tuples of EMSO[Σ lin , P, , ≤] sentences (Φ i , Ψ 1 i , . . . , Ψ m i ) 1≤i≤ such that for all M ∈ MSC ω ∃B (P, Σ) with Types inf (M) = T , we have M ∈ L if and only if there exists i such that M fin | = Φ i and M j | = Ψ j i for all 1 ≤ j ≤ m.

Proof. Let (K 1 , L 1 i , . . . , L m i ) 1≤i≤ be as in Lemma 20. There are EMSO[Σ lin , ] formulas Φ i , Ψ 1 i , . . . , Ψ m i such that K i = L(Φ i ) and L j i = L(Ψ j i ) for all i, j. Let Φ i , Ψ We have M ∈ L if and only if w ∈ Lin B (L), which means, by Lemma 20, if and only if there exists i such that u | = Φ i and v j | = Ψ j i for all j, that is, if and only if there exists i such that M inf | = Φ i and M j | = Ψ j i for all j. Finally, we conclude the proof of Theorem 5 (3) =⇒ (1). First, we can assume that all MSCs M ∈ L have the same set T = Types inf (M) of types at infinity. Indeed, properties (1), (2), and (3) hold for L if and only if they hold for every restriction of L to a particular set T of types at infinity. Now, by Theorem 4, definability of MSC ω ∃B (P, Σ) and Lemma 21, it is now enough to construct an EMSO[Σ, P, , ≤] formula Ξ such that, for all M ∈ MSC ω ∃B (P, Σ), we have M | = Ξ if and only if there exists i such that M fin | = Φ i and M j | = Ψ j i for all 1 ≤ j ≤ m. First, we can define FO[Σ, P, , ≤] formulas fin(x), inf 1 (x), . . . , inf m (x) that hold precisely at events in M fin , M 1 , . . . , M m , respectively. Let Φ i be the FO[Σ, P, , ≤] formula obtained from Φ i by (i) restricting every quantification to events in M fin , for instance, replacing ∃x.ξ with ∃x.fin(x) ∧ ξ, and (ii) replacing Σ lin predicates in a straightforward way, for instance, the formula (a, p?q)(x) is replaced with a(x) ∧ p(x) ∧ ∃y.q(y) ∧ y x. We define similarly formulas Ψ j i relativized to M j . We then let

Ξ = 1≤i≤         Φ i ∧ 1≤ j≤m Ψ j i         .

Temporal Logic

The transformation of temporal-logic formulas into automata has many applications, ranging from synthesis to verification. Temporal logics are well understood in the realm of sequential systems where formulas can reason about linearly ordered sequences of events. As we have seen, executions of concurrent systems are actually partially ordered. Over partial orders, however, there is no longer a canonical temporal logic like LTL over words. Several natural temporal logics have been studied over Mazurkiewicz traces (see [START_REF] Gastin | Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces[END_REF] for an overview). Starting from a formula in all these logics, we can always construct an equivalent asynchronous automaton [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF], a standard model of shared-memory systems. We will show below that this is still true when formulas are interpreted over MSCs and the system model is given in terms of CFMs.

Many temporal logics over partial orders are captured by the following generic language, which we will call TL(Co, , -1 , Ũ, S). Its formulas are defined as follows: We define derived modalities X p , Y p and U p , with the following meaning: X p moves to the first event on process p that is in the strict future of the current event, while Y p moves to the last event on process p that is in the strict past of the current event; finally, U p is the usual LTL (non-strict) until for a single process p, evaluated at the current event if it is on process p, or the first event of its future that is on process p otherwise:

ϕ ::= a | p | ϕ ∨ ϕ | ¬ϕ | Co ϕ | ϕ | -1 ϕ | ϕ Ũ ϕ | ϕ S ϕ where a ∈ Σ, p ∈ P . A formula ϕ ∈ TL(Co, , -1 , Ũ, S)
X p ϕ := ¬p Ũ (p ∧ ϕ) Y p ϕ := ¬p S (p ∧ ϕ) ϕ 1 U p ϕ 2 := p ∧ ϕ 2 ∨ ϕ 1 ∧ (¬p ∨ ϕ 1 ) Ũ (p ∧ ϕ 2 ) .
This temporal logic and others have been studied in the context of Mazurkiewicz traces [GK07, GK10, Thi94, DG06]. The logic introduced by Thiagarajan in [START_REF] Thiagarajan | A trace based extension of linear time temporal logic[END_REF] uses an until modality similar to U p , except that if the current event is not on process p, the evaluation starts at the latest event on process p in the past of the current event (or the first event of process p if none exists). The second temporal modality of this logic is a unary modality O p interpreted as follows: O p ϕ holds at e if the first event on process p that is not in the past of e satisfies ϕ. Both can similarly be expressed in TL(Co, , -1 , Ũ, S).

All these modalities can be easily translated into FO[→, , ≤], and thus we can apply Theorem 1 and Proposition 3 to translate any TL(Co, , -1 , Ũ, S) formula into a transducer which determines the set of events where the formula holds. However, this approach does not give any guarantee on the size of the resulting transducer. Instead, we present a direct translation from TL(Co, , -1 , Ũ, S) to PDL sf [Loop], leading to a transducer of size exponential in the size of the formula and doubly exponential in the number of processes. Theorem 6. For all ϕ ∈ TL(Co, , -1 , Ũ, S, X p , Y p , U p ), there exists a transducer A ϕ with

2 |ϕ|•2 O(|P| log |P|) states per process such that A ϕ = {(M, M ϕ ) | M ∈ MSC(P, Σ)}.
Proof. Similarly to the proof of Lemma 10, we will first translate every modality Mod into a transduceer B Mod . In particular, if Mod is a unary modality, then B Mod is a transducer from {0, 1} to {0, 1}, and if it is binary, then B Mod is a transducer from {0, 1} 2 to {0, 1}. where out = a,b∈{0,1} ((a, b), 1), in 1 = a,b∈{0,1} ((1, a), b), and in 2 = a,b∈{0,1} ((a, 1), b). In the following, we will exploit that, in the unary and the binary case, the formulas out, in, in 1 , and in 2 can also be considered as event formulas from PDL sf [Loop].

The number of states per process of B Mod will be bounded by 2 2 O(|P| log |P|) . We then compose these transducers for a given formula ϕ ∈ TL(Co, , -1 , Ũ, S, X p , Y p , U p ), just like in the proof of Lemma 10, so that we finally obtain the desired transducer A ϕ with 2 |ϕ|•2 O(|P| log |P|) states per process. Note that this procedure is in the spirit of [START_REF] Gastin | Uniform satisfiability in PSPACE for local temporal logics over Mazurkiewicz traces[END_REF][START_REF] Gastin | Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces[END_REF], where formulas from temporal logics with MSO-definable modalities over Mazurkiewicz traces are translated into small Büchi automata.

We obtain B Mod as the transducer A ξ Mod according to Theorem 2, where |P|) . It remains to specify the event formulas ψ Mod , which we address in the following.

ξ Mod = A out ⇐⇒ ψ Mod is a PDL sf [Loop] sentence of size 2 O(|P| log
Let Π denote the set of PDL sf [∅] path formulas

π = π 1 • p 1 ,p 2 • + -→ • p 2 ,p 3 • • • + -→ • p m-1 ,p m • π 2
with 1 ≤ m ≤ |P|, p 1 , . . . , p m ∈ P and p i p j for 1 ≤ i < j ≤ m, π 1 , π 2 ∈ { + -→, {true}?} and π {true}?. Note that for all events g, h, we have g < h if and only if M, g, h | = π for some π ∈ Π. Given π ∈ Π, we then define a state formula is-next(π) in PDL sf [Loop] such that for all events e, we have M, e | = is-next(π) if and only if min π (e) is well-defined, and is the minimal event on its process which is in the future of e:

is-next(π) = π ∧ π ∈Π ¬Loop(min π • + ← -• (π ) -1 ) . Symmetrically, we let is-latest(π) = π -1 ∧ π ∈Π ¬Loop(max (π -1 ) • + -→ • π ) so that M, e | = is-latest(π)
if and only if there exists p ∈ P such that max π -1 (e) = max{g ∈ E p | g < e}. Note that ∅ π -1 (e) ⊆ {g ∈ E p | g < e} which is finite, hence its maximum is well-defined. Given the special shape of π, we can simplify the definitions of min π and max π -1 to obtain formulas of size O(|P|), so that both is-next(π) and ← ------------• -1 p m-2 ,p m-1 • • • -1 p 1 ,p 2 .

We now determine the formulas ψ Mod for each modality in the temporal logic. The base cases and message modalities are trivial.

• Suppose that Mod = X p (the case Mod = Y p is similar). We let

ψ X p = π∈Π π p ∧ is-next(π) ∧ min π in ,
where, as above, in = b∈{0,1} (1, b). The formula ψ X p is of size 2 O(|P| log |P|) . Notice that if we are already on process p then we get a simpler, constant size, formula ψ p∧X p = → in.

• Suppose that Mod = U p . We use the constant size formula

ψ U p = p ∧ in 2 ∨ in 1 ∧ in 1 --→ in 2 .
• Suppose that Mod = Ũ (the case Mod = S is similar). Notice that in order to determine if ψ Ũ is true at a given event e, it suffices to consider all potential "minimal" events f > e such that M, f | = in 2 and check whether M, g | = in 1 for all e < g < f . More precisely, we have M, e | = in 1 Ũ in 2 if and only if there exists π ∈ Π such that f = min (π • {in 2 }?) (e) is well-defined and for all e < g < f , M, g | = in 2 , that is, if and only if M, e | = ψ Ũ, where

ψ Ũ = π∈Π π in 2 ∧ σ,τ∈Π
¬Loop(σ • {¬in 1 }? • τ • (min (π • {in 2 }?)) -1 ) .

The formula ψ Ũ is of size 2 O(|P| log |P|) .

• Suppose that Mod = Co. Given e, f ∈ E with loc( f ) = q loc(e), we have f e if and only if one of the following holds: (a) all events on process q are parallel with e, (b) no event on q is in the past of e, and f < proc min{g ∈ E q | e < g}, (c) no event on q is in the future of e, and max{g ∈ E q | g < e} < proc f , (d) max{g ∈ E q | g < e} < proc f < proc min{g ∈ E q | e < g}. This leads to the following definition:

ψ Co = p q σ,τ∈Π\{ + -→}        jump p,q in ∧ π∈Π ¬ π q ∧ ¬ π -1 q        ∨        is-next(τ) ∧ min τ • + ← -(q ∧ in) ∧ π∈Π ¬ π -1 q        ∨        is-latest(σ) ∧ max (σ -1 ) • + -→ (q ∧ in) ∧ π∈Π ¬ π q        ∨ is-latest(σ) ∧ is-next(τ) ∧ Loop(max (σ -1 ) • + -→ • {in}? • + -→ • (min τ) -1 ) .
The formula ψ Co is of size 2 O(|P| log |P|) . This concludes the proof of Theorem 6.

Note that the transducer constructed in Theorem 6 is non-deterministic. Informally, a transducer from Σ to Γ is deterministic if it can be obtained from a deterministic CFM over P and Σ by adding one output to each transition. So here a first source of non-determinism is that all the transducers we constructed essentially "guess" their output. However, even if we fix the output as part of the MSC and only want to construct a CFM which checks that the output is correct, it is not possible to avoid non-determinism. We cannot even avoid it for simple past formulas, which is in contrast to what happens for words or Mazurkiewicz traces. Proof. Let P = {p, q, r} and Σ = {0, 1}. We show that there exists no deterministic CFM recognizing the set L of MSCs M = (E, →, , loc, λ × γ) such that for all e ∈ E q , γ(e) = 1 if and only if (E, →, , loc, λ), e | = Y p 1. Assume that there exists a deterministic CFM A = (A p , A q , A r , Msg, Acc) such that L(A) = L. Fix n > |S q | 2 , where S q is the set of states of A q . For all k ∈ {0, . . . , n -1}, we define an MSC M k = (E, →, k , loc, λ × γ k ), as depicted in Figure 16 (for n = 5 and k = 2): • For all 0 ≤ i < k, e 2i k f i , and for all k ≤ i < n, e 2i k f n+i .

• E p = {e i | 0 ≤ i < 2n}, E q = { f i | 0 ≤ i <
For all 0 ≤ i < n, e 2i+1 k g 2i , and g 2i+1 k f k+i .

• For all 0 ≤ i < n, λ(e 2i ) = 0 and λ(e 2i+1 ) = 1.

For all h ∈ E r ∪ E q , λ(h) = 0.

• For all 0 ≤ i < 2k -1, γ k ( f i ) = 0, and for all 2k -1 ≤ i < 2n, γ k ( f i ) = 1.

For all h ∈ E p ∪ E r , γ k (h) = 0.

Clearly, M k ∈ L(A). Let s k and t k be the states before reading respectively f k and f k+n in the unique run ρ k of A on M k : s k = source(ρ k ( f k )) and t k = source(ρ k ( f k+n )).

Note that for all k, the sequence of send and receive actions performed by process p or process r in M k are the same, so the runs of A on MSCs M k only differ on process q. In particular, the sequence of n messages sent by process r to process q is the same for all k. Moreover, since n > |S q | 2 , there exist 0 ≤ k < k < n such that s k = s k and t k = t k . We can then combine the runs of A on M k and M k to define a run where process q receives the messages from process p and r in the same order as in M k , but behaves as in M k in the middle part where it receives the n messages from process r. More precisely, let M = (E, →, k , loc, λ × γ), where (E, →, k , loc, λ) is as in M k , and γ is defined as follows: γ(h) = 0 for all h ∈ E p ∪ E r , γ( f i ) = 0 for all 0 ≤ i < k + k -1, and γ( f i ) = 1 for all k + k -1 ≤ i < n. Then, M ∈ L(A), but M L.

The Gossip Problem

Gossiping is a technique used to maintain a consistent view of the global system state in a distributed system. The problem can be stated as follows: whenever process q receives a message from process r, q has to decide, for all processes p, whether it has more recent information on p than r. This problem is at the heart of many distributed algorithms. Interestingly, gossip protocols and related techniques, such as asynchronous mappings, have also been exploited in formal methods, in particular when it comes to establishing the expressive power of automata models [MS97, CMZ93, MKS03, DS97]. In particular, gossip protocols are the key to simulating high-level specifications, which include message sequence graphs and monadic second-order logic [HMK + 05, GKM06, Kus03, Zie87, Tho90]. All known techniques and algorithms, however, require that communication be synchronous or accomplished through FIFO channels with limited capacity.

We show that we can apply our results to construct a CFM that solves the gossip problem. This is defined more precisely below. Let M = (E, →, , loc, λ) be an MSC and e ∈ E. For all processes p such that { f ∈ E p | f < e} ∅, we let latest p (e) = max{ f ∈ E p | f < e}. The gossip transducer should determine, for all processes p and all receive events e with f e, whether latest p (e) < latest p ( f ). We show that this property can be expressed in PDL sf [Loop] so that we can obtain the gossip transducer as a corollary of Proposition 3.

Let Π and is-latest(π) be defined as in the proof of Theorem 6. The property described above is expressed by the PDL sf [Loop] formula below. It states that the event latest p (e) is obtained from e with max (σ -1 ) and the event latest p ( f ) is obtained from f with max (τ -1 ). Then, it compares the two events using the loop modality. σ,τ∈Π q,r∈P σ -1 p ∧ is-latest(σ) ∧ -1 q,r ( τ -1 p ∧ is-latest(τ)) ∧ Loop(max (σ -1 ) • + -→ • (max (τ -1 )) -1 • q,r ) .

Note that the gossip CFM is unavoidably nondeterministic (this follows from Proposition 4). This is in contrast to the deterministic protocols for synchronous communication or message-passing environments with bounded channels [MS97, CMZ93, MKS03, DS97].

Conclusion

In this paper, we showed that every FO[→, , ≤] formula over MSCs is effectively equivalent to a CFM. As an intermediate step, we used a purely logical transformation of own interest, relating FO logic with a star-free fragment of PDL. While star-free PDL constitutes a two-dimensional temporal logic over MSCs, we leave open whether there is a one-dimensional one, with a finite set of FO-definable modalities, that is expressively complete for FO[→, , ≤].

Though our result closes an important gap concerning the expressive power of CFMs, there remain interesting open questions addressing both CFMs and automata on graphs in general:

First, it is still open whether every formula from the full PDL logic over MSCs can be translated into CFMs. In [START_REF] Bollig | Propositional dynamic logic for message-passing systems[END_REF], only a unidirectional fragment was considered. The difficulty comes with unrestricted usage of the star operator, which allows one to go forth and back in an MSC unboundedly many times. While such two-way mechanisms do not add expressive power in the setting of words, the situation is unclear in the realm of MSCs. It would already be interesting to solve this question for more specialized structures such as pictures, which also come with natural notions of recognizability in terms of graph acceptors and two-way automata [START_REF] Kari | New results on alternating and non-deterministic two-dimensional finite-state automata[END_REF].

Second, it is worthwhile to also study architectures with one unbounded FIFO channel per process (as considered, e.g., in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF]), or including pushdown processes. The latter give rise to multiply nested words, and it is an open question whether every first-order formula over multiply nested words (including the total order and the push-pop relation) can be translated into an equivalent multi-pushdown automaton (aka nested-word automaton). Unlike in MSCs, the matching relation of a nested word is not monotone so that the techniques presented in this paper do not apply. Note that, when dropping the total order and restricting to two nesting relations, one can still take advantage of Hanf's theorem [START_REF] Bollig | On the expressive power of 2-stack visibly pushdown automata[END_REF].

Finally, it will be interesting to see whether the technique from Section 5 can be applied to other meaningful classes of MSCs so as to obtain logical characterizations of restricted CMFs in terms of full MSO logic.

Figure 1 :

 1 Figure 1: An (infinite) message sequence chart (MSC).

Figure 3 :

 3 Figure 3: Proof of Lemma 4.

Figure 4 :

 4 Figure 4: Characterization of π c (e) for π ∈ PDL sf [Loop].

Figure 5 :

 5 Figure 5: Proof of Lemma 5.

Figure 6 :

 6 Figure 6: Proof of Lemma 6 where π = jump p,q • π 1 .

  f = max π (e) and ϕ -→ (e) infinite.

  M, e, f | = max π.

Figure 7 :

 7 Figure 7: Proof of Lemma 6 where π = ϕ -→ • π 1 .

  Since

  ϕ -→ (e) is infinite, we have M, e, g | = ϕ -→, and thus M, e, f | = π, which contradicts the maximality of f . Hence, M, f | = ¬ + -→ • π -1 1 , M, g | = ψ 2 , and M, e, f | = max π. Conversely, assume that M, e, f | = max π. Let g such that M, e, g | = ϕ -→, M, g | = ψ 1 ∨ ψ 2 , and M, g, f |

Figure 8 :

 8 Figure 8: Proof of Claim 1.

  In addition, we have M, e | = ψ, M, ν(y k ), e | = π k , and M, ν(y ), e | = π . Hence, M, ν(y k ), ν(y ) | = π k • {ψ}? • π -1 . So we have M, ν | = Υ . Conversely, assume M, ν | = Υ . Let k, ∈ J such that the corresponding sub-formula is satisfied. There exists e ∈ E such that M, ν(y k ), e | = π k , M, e | = ψ, and M, e, ν(y ) | = π -1 . Note that we have min π k (ν(y k )) ≤ proc e ≤ proc max π (ν(y )). For all j ∈ J , we have M, e | = Loop(π j ), i.e., M, ν[x n → e] | = π j (x n , x n ). Now, let j ∈ J. We have M, ν(y j ), ν(y k ) | = (min π j ) • * -→ • (min π k ) -1 , hence min π j (ν(y j )) ≤ proc min π k (ν(y k )) ≤ proc e. Similarly, e ≤ proc max π (ν(y )) ≤ proc max π j (ν(y j )) ∈ E ∪ {∞}. In addition, since M, e | = ψ, we have M, e | = π -1 j . Applying Lemma 4, we get M, ν(y j ), e | = π j , i.e., M, ν[x n → e] | = π j (y j , x n ). Hence, M, ν | = Υ.

Figure 10 :

 10 Figure 10: Proof of Claim 2: 2-coloring of E 0 in Graph G.

  From the following two claims, we deduce immediately that A ϕ = {(M, M ϕ ) | M ∈ MSC(P, Σ)}. Claim 2. For all M ∈ MSC(P, Σ), there exists M ∈ K with α(M ) = M. Proof of Claim 2. Let M = (E, →, , loc, λ) ∈ MSC(P, Σ). Let E 1 = {e ∈ E | M, e | = ϕ} and E 0 = E \ E 1 . Consider the graph G = (E, {(e, f ) | M, e, f | = π}). Since π is functional, every vertex has outdegree at most 1, and, by Lemma 11, there are no cycles except for self-loops. So the restriction of G to E 0 is a forest, and there exists a 2-coloring χ : E 0 → { , } such that, for all e, f ∈ E 0 with M, e, f | = π, we have χ(e) χ( f ). This is illustrated in Figure 10. Moreover, there exists θ : E → Θ such that θ(e) = χ(e) for e ∈ E 0 , and θ(e) ∈ { , } for e ∈ E 1 is such that Condition 1 of the definition of K is satisfied. It is easy to see that Condition 2 is also satisfied. Indeed, if θ(e) ∈ { , }, then e ∈ E 1 , M, e, e | = π, and M, e, e | = π -1 . Now, if θ(e) { , }, then e ∈ E 0 and either M, e | = π or, by definition of θ, we have θ(e) θ( f ) for the unique f such that M, e, f | = π. (Claim 2) Claim 3. For all M ∈ K, we have β(M ) = M ϕ , where M = α(M ). Proof of Claim 3. Let M = (E, →, , loc, λ × θ) ∈ K and M = α(M ). Suppose towards a contradiction that M ϕ β(M ) = (E, →, , loc, γ). First, we show that, for all e ∈ E, γ(e) = 0 implies M, e | = ϕ. So assume γ(e) = 0. Then, we have θ(e) ∈ { , }. Take any f, f ∈ E such that M, e, f | = π and M, e, f | = π -1 (if there are no such events, we have M, e | = ϕ). Due to Condition 2., θ(e) = θ( f ) = θ( f ) does not hold, which implies M, e | = ϕ.

Figure 11 :

 11 Figure 11: Proof of Claim 3.

  , if we have M, e | = Loop(π) and M, e | = Loop(min π), then min π (e) < proc e ≤ proc max π (e) and M, e | = π -1 , hence M, e | = π -1 ∧ Loop((min π) • + -→) ∧ ¬Loop((max π) • + -→). Conversely, if we have M, e | = Loop(min π), then M, e | = Loop(π), and if M, e | = π -1 ∧ Loop((min π) • + -→) ∧ ¬Loop((max π) • + -→), then M, e | = π -1 and min π (e) < proc e ≤ proc max π (e). By Lemma 4, this implies M, e, e | = π. Hence, M, e | = Loop(π).

  transducers of size 2 O(|π | 2 ) for the formulas Loop(min π ), π -1 , Loop((min π ) • + -→) and Loop((max π ) • + -→), and define A ψ as the expected composition of these transducers. Recall that both min π and max π are functional, and of size O(|π | 2 ). Using Lemmas 12 and 10, we already have transducers for Loop(min π ) and π -1 .

Figure 12 :

 12 Figure 12: Proof of Claim 4.

1.

  Assume that M, e | = ψ. The left-to-right implication holds without any hypothesis. Conversely, assume that M, f | = ψ. If M, f | = Loop(π), we are done. Otherwise, let e = π (e) and f = π ( f ). We have e < proc e and f < proc f . Moreover, M, f | = + -→ • π -1 , hence g = min ( + -→ • π -1

Figure 13 :

 13 Figure 13: Proof of Claim 5(1.).

2.

  Assume that M, e | = ψ. The right-to-left implication holds easily since max (π • ¬ π ---→) ⊆ π • + -→ . Conversely, assume that M, f | = ψ. Let e = π (e) and f = π ( f ).

Figure 14 :

 14 Figure 14: Proof of Claim 5(2.).

Fact 9 Figure 15 :

 915 Figure 15: The relation rev B for B = 1, and the sets ↑ B e and ↑ B f .

  is interpreted over events of MSCs. We say that M, e | = a if λ(e) = a; similarly, M, e | = p if loc(e) = p. The Co modality jumps to a parallel event: M, e | = Co ϕ if there exists f ∈ E such that e ≤ f , f ≤ e, and M, f | = ϕ. The message modality goes to the matching receive: M, e | = ϕ if e f for some f ∈ E such that M, f | = ϕ. The definition is symmetric for -1 ϕ. We use strict versions of until and since: M, e | = ϕ 1 Ũ ϕ 2 if there exists f ∈ E such that e < f and M, f | = ϕ 2 and, for all e < g < f, M, g | = ϕ 1 M, e | = ϕ 1 S ϕ 2 if there exists f ∈ E such that f < e and M, f | = ϕ 2 and, for all f < g < e, M, g | = ϕ 1 .

  Consider, for example, Mod = Co. For M = (E, →, , loc, λ × γ) with λ, γ : E → {0, 1}, we will have M ∈ L(B Co ) iff, for all events e ∈ E, M, e | = out ⇐⇒ M, e | = Co in with temporal-logic formulas out = a∈{0,1} (a, 1) and in = b∈{0,1} (1, b). Now suppose Mod = Ũ. Then, for M = (E, →, , loc, λ × γ) with λ : E → {0, 1} 2 and γ : E → {0, 1}, we will get M ∈ L(B Ũ) iff, for all events e ∈ E, M, e | = out ⇐⇒ M, e | = in 1 Ũ in 2 .

  is-latest(π) are of size 2 O(|P| log |P|) . For instance, if π = p 1 ,p 2 • + -→ • p 2 ,p 3 • • • + -→ • p m-1 ,p m • + -→, we have max π -1 ≡ {¬ -1 p m-1 ,pm }? ← -----------• -1 p m-1 ,p m • {¬ -1 p m-2 ,p m-1 }?

Proposition 4 .

 4 Assume that |Σ| ≥ 2 and |P| ≥ 3. For p ∈ P and a ∈ Σ, there is no deterministic CFMA over Σ × {0, 1} such that L(A) = {(E, →, , loc, λ × γ) | γ(e) = 1 iff (E, →, , loc, λ), e | = Y p a}.

  2n}, andE r = {g i | 0 ≤ i < 2n}, with e 0 → e 1 → • • • → e 2n-1 , f 0 → f 1 → • • • → f 2n-1 , and g 0 → g 1 → • • • → g 2n-1 .

Figure 16 :

 16 Figure 16: Definition of M k . We only indicate the value of λ on process p, and of γ k on process q.

Table 1 :

 1 The semantics of PDL sf .

  have e 3 ≤ e 1 , since e 3 < e 1 implies e 32 e 12 e 21 e 23 , a contradiction. So we can assume e 1 e 3 . It remains to show e 13 e 31 . First, one shows that e 13 e 12 . (2) If e 12 ↑e 3 , then (2) is immediate. So suppose e 12 ∈ ↑e 3 , i.e., e 12 ∈ ↑e 3 \ ↑e 2 . Then, e 23 e 32 e 12 . (3) Let us consider two cases. If e 23 ↑e 1 then e 21 e 23 . By (3), we obtain e 21 e 12 , which contradicts e 1 ≺ e 2 . Hence e 23 ∈ ↑e 1 and we get e 13 e 23 . We deduce that (2) holds. To conclude the proof, we distinguish once more two cases: Case e 31 ∈ ↑e 2 : Then, e 12 e 21 e 31 . Applying (2), we obtain e 13 e 31 . Case e 31 ↑e 2 : Then, e 23 e 32 e 31 . If e 23 ∈ ↑e 1 , then e 13 e 23 e 31 and we are done. If e 23 ↑e 1 , then e 21 e 23 , which implies e 12 e 31 . By (2), we obtain e 13 e 31 .

  1 i , . . . , Ψ m i be the EMSO[Σ lin , P, ≤, ] formulas obtained by replacing, in these EMSO[Σ lin , ] formulas, every predicate x y with the FO[Σ lin , P, ≤, ] formula defining the canonical linearization B . Let M ∈ MSC ω ∃B (P, Σ) with types at infinity T , and let u ∈ Σ * lin , v 1 ∈ (Σ 1 lin ) ω , . . . , v m ∈ (Σ m lin ) ω be the canonical linearizations of the MSCs M inf , M 1 , . . . , M m (by Lemma 16, this is well-defined). Let w ∈ u • ¡ m j=1 v j . Then w is a B-bounded linearization of M.

It is open whether there is an equivalent one-dimensional one.

Thanks to Sylvain Schmitz for pointing this out.

In this case, Υ is a sentence whereas x 1 is free in the right hand side. Notice that ≡ does not require the two formulas to have the same free variables.

$ Partly supported by ANR FREDDA (ANR-17-CE40-0013) and ReLaX, UMI2000 (