Bollig Benedikt
email: bollig@lsv.ens-cachan.fr

Lsv

Logic for Communicating Automata with Parameterized Topology

We introduce parameterized communicating automata (PCA) as a model of systems where finite-state processes communicate through FIFO channels. Unlike classical communicating automata, a given PCA can be run on any network topology of bounded degree. The topology is thus a parameter of the system. We provide various B üchi-Elgot-Trakhtenbrot theorems for PCA, which roughly read as follows: Given a logical specification ϕ and a class of topologies T, there is a PCA that is equivalent to ϕ on all topologies from T. We give uniform constructions which allow us to instantiate T with concrete classes such as pipelines, ranked trees, grids, rings, etc. The proofs build on a locality theorem for first-order logic due to Schwentick and Barthelmann, and they exploit concepts from the non-parameterized case, notably a result by Genest, Kuske, and Muscholl.

I. INTRODUCTION

The Büchi-Elgot-Trakhtenbrot theorem states that finite automata and monadic second-order (MSO) logic over words are expressively equivalent [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]. This connection between automata and logic constitutes one of the cornerstones in theoretical computer science, as it bridges the gap between highlevel specifications and operational system models. Various extensions of that result followed, providing logical characterizations of tree automata [START_REF] Thatcher | Generalized finite automata theory with application to a decision problem of second-order logic[END_REF], asynchronous automata [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF], and graph acceptors [START_REF] Thomas | Elements of an automata theory over partial orders[END_REF], to mention just a few.

In recent years, an analogous question has been studied for communicating automata (CA). A CA consists of several finite-state processes that can exchange messages through FIFO channels by performing send and receive actions. A single execution of a CA is captured by a message sequence chart (MSC), a directed acyclic graph, whose nodes represent the events that are observed during an execution. Its edge relation = proc ∪ msg visualizes causal dependencies between events. Edges from proc connect consecutive events performed by a process, and edges from msg connect send events with their corresponding receives. Logical characterizations have been established for unrestricted CA [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] and channel-bounded CA [START_REF] Henriksen | A theory of regular MSC languages[END_REF], [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF], [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. All these results require the underlying communication topology, which provides a set of processes and channels between them, to be fixed. Now, it is a natural question to ask for an automaton that realizes a given logical specification for a class of topologies (for example, all grid topologies, no matter what the size of the grid is). This is what this paper is about, i.e., we aim for Büchi-Elgot-Trakhtenbrot theorems in a setting with non-fixed, parameterized topology.

In a first step, we introduce parameterized communicating automata (PCA). Unlike classical CA, a given PCA can be run on any network topology of bounded degree (such as pipelines, ranked trees, grids, or rings). PCA are a conservative extension of CA and, as such, also recognize sets of MSCs. Our study is centered around the following question, which depends on a given logical specification ϕ and a given class T of topologies:

Is there a PCA A that is equivalent to ϕ on all topologies T ∈ T (when A is run on T , it accepts precisely the MSCs over T that satisfy ϕ)? If the answer is affirmative, then we say that formula ϕ is realizable for T. This paper investigates realizability wrt. several logics and instances of T in a unifying framework. We consider standard first-order and existential MSO logic, FO[σ] and EMSO[σ], respectively. Here, σ ⊆ { proc , * proc , msg , * , ∼} is the collection of binary relation symbols that are available in the logic. All symbols are self-explanatory apart from ∼, which allows us to say that two events are executed by the same process.

Our first results settle the limits of what we can hope for: (i) There is an FO[ proc , msg ]-formula that is not realizable for the class of "ring forests" (unions of ring topologies). (ii) There is an FO[ * proc , msg , * ]-formula that is not realizable already for the class of binary trees. This shows that we have to restrict both, the topologies and the logic, and that we are left with only a small margin for positive results. However, we are able to provide various Büchi-Elgot-Trakhtenbrot theorems: (iii) Every EMSO[ proc , msg , ∼]-formula is realizable for the classes of pipelines, ranked trees, grids, and rings. (iv) When we suppose that the channels of a PCA are bounded, then every EMSO[ * proc , msg ]-formula is realizable for the classes of pipelines, ranked trees, grids, and rings. In fact, we obtain (iii) and (iv) as corollaries of more general, uniform statements: it is shown that every EMSO formula is realizable for T whenever T is unambiguous. Intuitively, this rules out cycle patterns that a PCA is not able to detect on its own. Indeed, the classes of pipelines, ranked trees, and grids are all unambiguous so that we get realizability as a direct corollary. To capture also rings, some additional arguments are needed.

Note that, for (iii) and (iv) to apply, a class T of topologies has to be fixed in advance. The construction of a PCA A from a formula ϕ is uniform, but it crucially depends on T. That is, though A can still be run on any other topology of bounded degree, it is only guaranteed to be equivalent to ϕ when it is applied to a topology from T. Now, when we fix T, we have in mind that we run A only on topologies T ∈ T. For that reason, A does not have to check membership of T in T. However, it will have to collect some topological information to identify bounded subtopologies among those from T. In fact, the translation from logic to PCA builds on a locality theorem for first-order logic due to Schwentick and Barthelmann, which states that satisfaction of a formula in a structure can be reduced to satisfaction of a normalform formula in bounded portions of the same structure [START_REF] Schwentick | Local normal forms for first-order logic with applications to games and automata[END_REF]. This allows us to apply notions from the setting with fixed topologies, notably a result by Genest, Kuske, and Muscholl [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. Hereby, the assumption that topologies are of bounded degree is crucial.

For EMSO[ proc , msg ] (without process order), we provide a variation of the theme: Every formula ϕ can be translated into a PCA that is equivalent to ϕ on all prime topologies. In that case, the construction is independent of a concrete class of topologies (once the bound on the degree has been fixed). Note that pipelines, trees, and grids are all prime. 1Finally, every PCA A can be transformed into a formula from EMSO[ proc , msg ] that is equivalent to A on all topologies of bounded degree. Thus, overall, we indeed establish a variety of Büchi-Elgot-Trakhtenbrot theorems for PCA. Related Work: It seems that neither PCA nor expressiveness of parameterized systems in general in terms of logic have been considered in the literature.

In [START_REF] Jacobs | Parameterized synthesis[END_REF], Jacobs and Bloem study parameterized synthesis, where a temporal-logic specification is transformed into a system of processes that are arranged in a token ring of arbitrary size. Building on [START_REF] Emerson | On reasoning about rings[END_REF], the idea is to reduce parameterized synthesis to distributed synthesis over a bounded architecture. Though we also use a reduction to a bounded case, our framework differs from [START_REF] Jacobs | Parameterized synthesis[END_REF] in the model (asynchronous rather than token communication), in the topologies, and in the logic.

In parameterized verification, one aims at showing that a given system is correct independently of the number of processes or the communication topology [START_REF] Browne | Reasoning about networks with many identical finite state processes[END_REF], [START_REF] German | Reasoning about systems with many processes[END_REF], [START_REF] Abdulla | Handling global conditions in parameterized system verification[END_REF], [START_REF] Bouajjani | Verification of parametric concurrent systems with prioritised fifo resource management[END_REF], [START_REF] Delzanno | Parameterized verification of ad hoc networks[END_REF]. Our approach is different, since we generate a system model from a high-level specification.

There have been a variety of automata constructions that exploit normal forms of first-order logic [START_REF] Thomas | Elements of an automata theory over partial orders[END_REF], [START_REF] Schwentick | Local normal forms for first-order logic with applications to games and automata[END_REF], [START_REF] Gastin | Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces[END_REF]. We actually borrow a technique from [START_REF] Gastin | Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces[END_REF], but the overall framework is quite different.

Finally, our contribution intersects the area of distributed algorithms. Indeed, the way a PCA evaluates a (sub)topology is similar to constructing a map of an anonymous graph [START_REF] Chalopin | Constructing a map of an anonymous graph: Applications of universal sequences[END_REF]. In particular, our notion of unambiguous classes of topologies is in the spirit of universal sequences. There are also methods to evaluate graphs versus logical specifications [START_REF] Grumbach | Logical locality entails frugal distributed computation over graphs (extended abstract)[END_REF]. Though all those techniques do not seem to be directly applicable, it will be worthwhile to explore possible connections further.

Outline: Sections II-IV settle basic notions such as topologies, MSCs, PCA, and MSO logic. In Section V, we argue that we will have to restrict both topologies and logic. Sections VI and VII present the above-mentioned Büchi-Elgot-Trakhtenbrot theorems, respectively. We conclude in Section VIII. Due to space constraints, proofs are only sketched or omitted. All details can be found in the appendix.

II. PRELIMINARIES A. Communication Topologies

A (communication) topology2 is made up of single entities such as b a . Here, a process (represented by the circle) is equipped with two interfaces, a and b. The interfaces allow the process to communicate with its environment. When they are connected to interfaces of other processes, we obtain a topology. A simple pipeline topology is depicted below. Thus, a topology is essentially a graph, whose nodes are processes that can communicate with adjacent processes via their interfaces. The pipeline, for example, will allow a process to execute actions !a and ?a in order to send a message to (receive a message from, respectively) its right neighbor, if it exists. Accordingly, !b and ?b refer to the left neighbor.

Let us define topologies formally. Throughout the paper, unless stated otherwise, we fix a nonempty finite set N = {a, b, c, . . .} of (interface) names. When we talk about a concrete process, we may also say interface instead of name. Definition 1. A topology over N is a pair T = (P, ) where

• P is the nonempty finite set of processes, and

• ⊆ P × N × N × P is the edge relation.
We write p a b q for (p, a, b, q) ∈ , which signifies that the a-interface of p points to q, and the b-interface of q points to p. We require that, whenever p a b q, the following hold:

(a) p = q, (b) q b a p, and (c) for all a , b ∈ N and q ∈ P such that p a b q , we have a = a iff q = q .

By (a), a topology does not contain self-loops. Condition (b) says that two adjacent processes are mutually connected (in other words, a topology is "undirected"). By (c), a name points to at most one process, and two distinct names point to distinct processes.

We usually consider topologies up to isomorphism. The set of all topologies over N is denoted by T N . Given a topology T = (P, ) ∈ T N , a PCA will run identical subautomata on processes of the same type. We define type T : P → 2 N by type T (p) := {a ∈ N | there are b ∈ N and q ∈ P such that p a b q}. Thus, type T (p) contains those interfaces of p that are connected to some other process. Remark 1. One can also define types independently of N , in terms of an extra finite set Types, and include a mapping type : P → Types in the topology. In our setting, this can be encoded by choosing N × Types as new set of names. In a topology, an edge p a b q is then replaced by an edge with names (a, type(p)) and (b, type(q)). All definitions can be adapted easily and all results hold verbatim in this alternative setting.

Example 1. Let us identify some typical topology classes. We give an informal description. The precise definitions are as expected and can be found in Appendix IX.

Pipelines: A pipeline is a topology over {a, b}, as already indicated above. Recall that interface a points to the right neighbor of a process (if it exists), while b is connected to the left neighbor. Accordingly, the leftmost process has type {a}, the rightmost process has type {b}, and all inner processes have type {a, b}. The pipeline of length n ≥ 2 is denoted by T n lin . Figure 1 depicts T 4 lin . We let T lin = {T n lin | n ≥ 2} ⊆ T {a,b} denote the set of all pipelines.

Trees: We suppose that trees are binary, but we could consider arbitrary ranked alphabets. An example tree is depicted in Figure 2. Hence, a tree is a topology over {a, b, c, d} where interface a points to the left son, and c to the right son of a process, while b and d are their respective "dual" interfaces. We suppose that a tree has at least two processes. The type of a leaf is either {b} or {d}. The type of the root is either {a}, {c}, or, as is the case in Figure 2, {a, c}. The set of all tree topologies is denoted by T tree ⊆ T {a,b,c,d} . Note that pipelines can be seen as a special case of trees.

Grids: A grid is a topology over {a, b, c, d} where processes are arranged in a matrix. It is uniquely given by its number m ≥ 1 of rows and its number n ≥ 1 of columns. Again, there should be at least two processes so that we suppose max{m, n} ≥ 2. A process that is not located on the border has a right and a left neighbor (following a and b, respectively), but also adjacent nodes below and above (following c and d). Let T m,n grid denote the grid with m rows and n columns. An example is illustrated in Figure 3. By T grid = {T m,n grid | m, n ≥ 1 with max{m, n} ≥ 2} ⊆ T {a,b,c,d} , we denote the set of all grids. Again, a pipeline is a special case of a grid.

Rings: A ring can be seen as a pipeline where the endpoints are glued together. Thus, it is a topology over {a, b} in which every process has type {a, b}. The ring with n ≥ 3 processes is denoted by T n ring . Figure 4 illustrates T 5 ring . We denote the set of all rings by T ring = {T n ring | n ≥ 3} ⊆ T {a,b} . Remark 2. For many concrete topology classes of bounded degree such as pipelines, grids, or rings, the names are canonical so that fixing them in advance is not a restriction. Moreover, in most cases considered in the literature, a few (sometimes even one) process types will do. In particular, it is a common assumption that processes in a ring are indistinguishable [START_REF] Browne | Reasoning about networks with many identical finite state processes[END_REF], [START_REF] Emerson | On reasoning about rings[END_REF], [START_REF] Jacobs | Parameterized synthesis[END_REF]. However, one could also assume a distinguished leader process (and add another interface name just for the purpose of identifying the leader; cf. also Remark 1).

B. Message Sequence Charts

The semantics of both an automaton and a logic formula will be defined as a set of messages sequence charts (MSCs). Each MSC depicts a single execution of a system. It is formalized as a labeled directed acyclic graph whose nodes, the events, are associated with processes from a given communication topology. Events are linked by process edges proc and message edges msg . The process edges connect consecutive events of one process, and message edges connect send events with their corresponding receives according to a FIFO policy. Definition 2. An MSC over T = (P, ) ∈ T N is a triple M = (E, , ) where

• E is the nonempty finite set of events,

• ⊆ E × E is the acyclic edge relation, which is partitioned into proc and msg , and

• : E → P determines the location of an event in the topology; for p ∈ P , we let E p := {e ∈ E | (e) = p}. We require that the following hold:

• proc is a union p∈P p where each p ⊆ E p × E p is the direct-successor relation of some total order on E p ,

• there are a partition E = E ! E ? and a bijection µ :

E ! → E ? such that msg = {(e, µ(e)) | e ∈ E ! },
• for all (e, f ) ∈ msg , there are a, b ∈ N such that (e) a b (f ) (communication is restricted to adjacent processes), and

• for all (e, f ), (e , f ) ∈ msg such that (e) = (e ) and

(f ) = (f ), we have e * proc e iff f * proc f (FIFO). We do not distinguish isomorphic MSCs over T . lin ∈ T lin . The behavior of each process is represented by a top-down process line. Arrows between process lines determine the relation msg , connecting send events with their receive events. For illustration, some events are labeled with the actions that they execute. We may consider M n lin as the execution of a P2P protocol: a request from the leftmost process is forwarded by n -2 inner processes of type {a, b}, until it reaches the rightmost process. An acknowledgement is then relayed back to the first process along the same way backwards. Figure 8 depicts an example MSC over T 2,5 grid . Our main result will deal with systems that have (existentially) B-bounded channels, for some B ≥ 1 [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF], [START_REF] Genest | On communicating automata with bounded channels[END_REF]. Intuitively, an MSC is B-bounded if it can be scheduled in such a way that, along the execution, there are never more than B messages in each channel. Formally, we define boundedness via linearizations. A linearization of an MSC M = (E, , ) over T = (P,

) is any total order ⊆ E × E satisfying * ⊆ . Then, is called B-bounded if, for all f ∈ E, p, q ∈ P , and a, b ∈ N such that p a b q, we have |{e ∈ E | e f , (e) = p, and act M (e) = !a}| -|{e ∈ E | e f , (e) = q, and act M (e) = ?b}| ≤ B. In other words, in any prefix of , there are no more than B pending messages, in every "channel" (p, q). Now, we say that MSC M is Bbounded if it has a B-bounded linearization. For example, for all n ≥ 2, the MSC M n lin (cf. Figure 5) is 1-bounded, because its (only) linearization is 1-bounded.

III. PARAMETERIZED COMMUNICATING AUTOMATA

Next, we introduce PCA. Their definition does not depend on a topology, but only on N . The language of a PCA, a set of MSCs, is then parameterized by a topology. Definition 3. A parameterized communicating automaton (PCA) over N is a tuple A = (S, Msg, ∆, I, F ) where • F is the acceptance condition: a finite boolean combination of statements #(s) ≥ k with s ∈ S and k ∈ N (to be read as "s occurs at least k times as the terminal state of a process"), and

• ∆ ⊆ S × Σ A × S is the set of transitions.
Here, Σ A := { ! m a , ? m a | a ∈ N and m ∈ Msg} contains send actions ! m a and receive actions ? m a. A transition (s, η, s ) ∈ ∆ is also written

s η = ⇒ s .
The class of PCA over N is denoted by PCA N . A PCA over N can be run on any topology T = (P, ) ∈ T N . Suppose p a b q for processes p, q ∈ P and names a, b ∈ N . When p executes a transition (s, ! m a, s ) ∈ ∆, it changes its local state from s to s and writes m into the FIFO channel (p, q). The message m can then be received by process q executing a transition with action ? m b. However, messages are abstracted away in the observable MSC behavior (they are in the spirit of stack symbols in pushdown automata).

Formally, we define the semantics of a PCA directly on MSCs. This is equivalent to an operational semantics in terms of an infinite transition system, but closer to the logical approach where formulas are evaluated over MSCs (see Section IV). Let T = (P, ) ∈ T N be a topology and M = (E, , ) be an MSC over T . A run of A on M will be a mapping ρ : E → S. Intuitively, ρ(e) is the state that process (e) reaches after executing e ∈ E. To define when ρ is a run, we will need some more notation.

Set P M := {p ∈ P | E p = ∅}, which is the set of active processes of M . A (global) initial state of A for M is a tuple ι = (ι p ) p∈P M where ι p ∈ I(type T (p)) for all p ∈ P M . Given ι and ρ : E → S (a possible MSC run), we define another mapping ρ - ι : E → S, which returns the source state of a transition. For (f, e) ∈ proc , we let ρ - ι (e) = ρ(f ); for a proc -minimal event e ∈ E, we let ρ - ι (e) = ι (e) . Now, a mapping ρ : E → S is called a run of A on M if there is an initial state ι = (ι p ) p∈P M for M such that, for all (e, f ) ∈ msg , there are a, b ∈ N and m ∈ Msg satisfying (e) a b (f ), ρ - ι (e)

!ma
==⇒ ρ(e), and ρ - ι (f )

?mb = == ⇒ ρ(f ).
To determine if ρ is accepting, we define a multiset h ρ : S → N over S that counts how often each state occurs as the terminal state of an active process. For s ∈ S, we let h ρ (s) = |{e ∈ E | e is proc -maximal and ρ(e) = s}|. We say that ρ is accepting if h ρ satisfies F in the expected manner; in particular, h ρ satisfies #(s) ≥ k if h ρ (s) ≥ k. The MSC M is accepted by A if it admits an accepting run of A. For a topology T , the set of MSCs over T that are accepted by A is denoted by L T (A). Finally, we let L B T (A) be the restriction of L T (A) to B-bounded MSCs.

Example 3. Consider the PCA A over {a, b} from Figure 6. The acceptance condition F is simply the conjunction of formulas ¬ #(s) ≥ 1 with s ranging over the states without double circle. Recall that the messages req and ack do not occur in the accepted MSCs. In this example, we could actually do with just one message (|Msg| = 1). In general, however, message contents increase the expressive power of PCA. Note that MSC M 8 lin is the only MSC that is accepted by A over T 8 lin (cf. Example 2). We actually have

L T n lin (A) = L 1 T n lin (A) = {M n
lin } for all n ≥ 2. Remark 3. The multiset h ρ defined to evaluate the acceptance condition of a PCA does not include any states of non-active (i.e., idle) processes. So, a PCA cannot express "the topology has at least 5 processes", but only "at least 5 processes are active". In principle, one could include idle processes as well. However, this has to be reflected in the logic (cf. Theorem 9). One possibility is to consider processes as single events. But, apart from involving a more technical presentation, this does not seem to be natural. Alternatively, one could consider a two-sorted logic to reason about both events and processes. In that case, one very quickly exceeds the capability of PCA to evaluate a topology, as their runs rely on the messages that occur in an MSC. A two-valued logic also goes against the intuition that PCA accept behaviors rather than topologies.

The section concludes with some closure properties of PCA.

Theorem 1. PCA are closed under union and intersection: For all A 1 , A 2 ∈ PCA N , there are PCA A and B over N such that, for all topologies T ∈ T N , we have

L T (A) = L T (A 1 ) ∪ L T (A 2 ) and L T (B) = L T (A 1 ) ∩ L T (A 2 ).
The construction of A and B is easy. The only (minor) subtle point is the acceptance condition (see Appendix X).

Theorem 2. PCA are not closed under complementation:

There is A ∈ PCA {a,b} such that, for all B ∈ PCA {a,b} , we have

L T 2 lin (B) = {M | M MSC over T 2 lin } \ L T 2 lin (A).
Theorem 2 is an immediate consequence of the fact that fixed-topology CA over two processes are not complementable [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF]. Finally, non-deterministic PCA are strictly more expressive than deterministic ones (we do not give the formal definitions). This already holds over 1-bounded MSCs, which follows from the case of fixed-topology CA and requires a topology with five processes and five interface names [START_REF] Genest | On communicating automata with bounded channels[END_REF].

IV. MSO LOGIC AND LOCALITY OF FO LOGIC

While PCA serve as a model of an implementation of a communicating system, we use monadic second-order (MSO) logic to specify properties of MSCs.

A. Monadic Second-Order Logic

The set MSO N of MSO formulas over N is given by:

ϕ ::= act(x) = !a | act(x) = ?a | a ∈ type(x) | x proc y | x * proc y | x msg y | x * y | x ∼ y | x = y | x ∈ X | ¬ϕ | ϕ ∨ ϕ | ∃xϕ | ∃Xϕ
where a ∈ N , x and y are first-order variables (interpreted as events of an MSC), and X is a second-order variable (interpreted as a set of events), all taken from infinite supplies of variables. We use standard abbreviations such as ϕ ∧ ψ ≡ ¬(¬ϕ ∨ ¬ψ), ϕ → ψ ≡ ¬ϕ ∨ ψ, and ∀xϕ ≡ ¬∃x¬ϕ.

The set FO N of first-order formulas is the fragment of MSO N without second-order quantification ∃X. Moreover, EMSO N (existential MSO) is the set of formulas of the form ∃X 1 . . . ∃X n ϕ with ϕ ∈ FO N .

A formula is evaluated wrt. an MSC M = (E, , ) over some topology T = (P, ) ∈ T N . Free variables x and X are interpreted by a mapping I as an event I(x) ∈ E and a set of events I(X) ⊆ E, respectively. For η of the form !a or ?a, the atomic formula act

(x) = η is true if act M (I(x)) = η. Formula a ∈ type(x) is true if a ∈ type T ( (I(x))), i.e.
, a is contained in the type of the process where I(x) is located. Formula, x * proc y is satisfied if I(x) * proc I(y). Moreover, x ∼ y holds true if (I(x)) = (I(y)), i.e., I(x) and I(y) are located on the same process. Other formulas are interpreted as expected. Though, even in FO N , some binary predicates are mutually expressible in terms of others (e.g., proc and ∼ in terms of * proc , and * proc in terms of * and ∼), we include all of them explicitly in the logic. They will be used in fragments in which they would no longer be expressible.

Let σ ⊆ { proc , * proc , msg , * , ∼} be a nonempty set of relation symbols. The logics FO N [σ] and EMSO N [σ] restrict FO N and EMSO N , respectively: instead of { proc , * proc , msg , * , ∼}, we can only access the relation symbols from σ. Our main (positive) result will concern the logic EMSO N [ * proc , msg ] (recall that proc and ∼ can be expressed in terms of * proc ). Let T ∈ T N be a topology, and let ϕ ∈ MSO N be a sentence, i.e., a formula without free variables. The set of MSCs over T that satisfy ϕ is denoted by L T (ϕ). When ϕ is not a sentence, then L T (ϕ) contains the pairs, of an MSC and an interpretation of the free variables, that satisfy ϕ. Let L B T (ϕ) be the restriction of L T (ϕ) to B-bounded MSCs. Example 4. We will consider two FO {a,b} -sentences. First, ϕ 1 = ∀x(act(x) = ?b → ∃y(x * proc y ∧ act(y) = !b)) says that every process that receives a message from its b-interface, eventually sends a message through b. Note that

M n lin ∈ L T n lin (ϕ 1 ) for all n ≥ 2 (cf. Example 2). Next, let ϕ 2 = ∃x∃y(b ∈ type(x) ∧ a ∈ type(y) ∧ x msg y) .
Interpreted over pipelines, ϕ 2 says that the leftmost process sends a message to the rightmost process. We have

M n lin ∈ L T n lin (ϕ 2 ) iff n = 2.

B. Locality of FO Logic

Next, we state a locality theorem due to Schwentick and Barthelmann [START_REF] Schwentick | Local normal forms for first-order logic with applications to games and automata[END_REF]. 3 It formalizes the intuition that first-order logic can only reason about local neighborhoods, which include elements whose distance from a given center is bounded by a parameter that depends on the formula. ) ∈ T N . The distance dist σ M (e, f ) between events e, f ∈ E is the minimal length of a path between e and f in the graph of M with edges given by σ, in either direction (or ∞ if such a path does not exist). For example, let

σ = { * proc , msg }. Then, dist σ M (e, f ) refers to the distance in the (undirected) graph (E, * proc ∪( * proc ) -1 ∪ msg ∪ -1 msg ) so that dist σ M (e, f ) ≤ 1 for all e, f ∈ E such that (e) = (f ), and dist σ M (e, f ) = dist σ M (f, e) = 1 for all (e, f ) ∈ msg . Example 5.
Let M be the MSC over T 8 lin from Figure 7 and let e be the distinguished event given by the white circle. The set of events f such that dist σ M (e, f ) ≤ 3 depends on σ, and is illustrated for { * }, { * proc , msg } (inducing the same set as { msg , ∼}), and { proc , msg }.

Let r ≥ 1. A formula χ ∈ FO N [σ] is called (r, σ)-
local around a first-order variable y if (i) y is not quantified in χ and (ii) χ is obtained from some FO N [σ]formula by replacing each subformula of the form ∃zψ with ∃z(dist σ (y, z) < r ∧ ψ), and each subformula of the form ∀zψ with ∀z(dist σ (y, z) < r → ψ). Here, dist σ (y, z) < r denotes the obvious FO N [σ]-formula. We use strict inequality for technical reasons (cf. [START_REF] Gastin | Uniform satisfiability problem for local temporal logics over Mazurkiewicz traces[END_REF]). Adapted to our setting, [START_REF] Schwentick | Local normal forms for first-order logic with applications to games and automata[END_REF] yields the following:

Theorem 3 (Schwentick & Barthelmann, [21]). Let ϕ ∈ FO N [σ]. There are r ≥ 1 and ϕ = ∃x 1 . . . ∃x n ∀yχ ∈ FO N [σ] such that χ is (r, σ)-local around y and, for all topologies T ∈ T N , we have L T (ϕ) = L T (ϕ ).

V. NEGATIVE RESULTS

Recall that we are interested in realizability of formulas ϕ for a class T of topologies: Is there a PCA A such that L T (A) = L T (ϕ) for all T ∈ T. In this section, we show that such a PCA does not always exist.

A. Restrictions on Topologies Are Necessary

In fact, there is a sentence from FO {a,b} [ proc , msg ] that is not realizable for the class of all topologies over {a, b}. This even holds for the class T * ring ⊆ T {a,b} of ring forests and when we restrict to 1-bounded MSCs. A ring forest is a disjoint union of an arbitrary number of rings (possibly containing several copies of one and the same ring). Theorem 4. There exists a sentence ϕ ∈ FO {a,b} [ proc , msg ] such that, for all PCA A ∈ PCA {a,b} , there is T ∈ T * ring with L 1 T (A) = L 1 T (ϕ). The proof of Theorem 4 reveals that PCA have limited ability to "detect" cycles in an MSC and in a topology (cf. Appendix XI). In the following sections, we will, therefore, restrict the "cyclic behavior" of a class of topologies (of a single topology, respectively).

In Section VI, the construction of a PCA indeed requires a class T of topologies to be given in advance. We show that certain formulas are realizable for all classes T that are unambiguous: one can tell by looking at a sequence w ∈ (N × N ) * of edge labels whether w produces a cycle or not, in any topology of T. This notion exludes the set of ring forests exploited in Theorem 4, but it captures the classes of pipelines, trees, and grids, as well as singleton rings and the class of "almost all" rings (which will finally allow us to cover the class of all rings with one single PCA).

In Section VII, the construction of a PCA from a given formula does not depend on a class of topologies, but only on N . It makes sure that the synthesized PCA agrees with the formula on all prime topologies. This forbids cycles with a periodic labeling (as it occurs in rings), but includes all pipelines, trees, and grids.

B. Restrictions on Logic Are Necessary

Next, we argue that we have to restrict the logic, too. In fact, when we take FO N (i.e., first-order logic with all binary predicates), then the negative result even holds for the class of trees (actually, for simple bus topologies). This has to be contrasted with the expressive equivalence of MSO and CA over fixed topologies when imposing any existential bound on the channels [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF].

Theorem 5. There exists a sentence ϕ ∈ FO {a,b,c,d} such that, for all PCA A ∈ PCA {a,b,c,d} , there is T ∈ T tree with L 1 T (A) = L 1 T (ϕ). The proof (cf. Appendix XII) uses a technique from [START_REF] Thomas | Elements of an automata theory over partial orders[END_REF], which was employed to show that FO (with reflexive transitive closure relations) and a local variant of EMSO are incomparable over pictures.

We briefly discuss Theorem 5. Let ϕ ∈ FO N [σ], for some σ ⊆ { proc , * proc , msg , * , ∼}, and suppose r is the radius associated with ϕ according to Theorem 3. Satisfaction of ϕ in an MSC M essentially depends on the σ-neighborhoods of the latter (informally, the σ-neighborhood of an event e is the substructure of M , including the actions, induced by all elements f such that dist σ M (e, f ) ≤ r). When σ contains * , there is no a priori bound on the size of the σ-neighborhood of e: it may feature events f that are far from e in terms of the number of messages that separate them. In other words, dist σ M (e, f ) can be small for σ = { * }, but large for σ = { * proc , msg }. This is exemplified in Figure 7. On the other hand, the exchange of information in a PCA relies on messages and is restricted to processes that are adjacent in the topology. This intuitively explains the mismatch between automata and logic that Theorem 5 reveals.

The size of a { * proc , msg }-neighborhood is a priori unbounded as well. However, unlike a { * }-neighborhood, it has "bounded width", since it spans over a bounded area of the underlying topology: Figure 7 illustrates that, provided * ∈ σ, a topology neighborhood of radius r/2 is indeed sufficient to cover all events f with dist σ M (e, f ) ≤ r. As our topologies are structures of bounded degree, there are only a bounded number of such topology neighborhoods. This allows us to take advantage of results on CA over fixed topologies. We pursue this idea in Section VI to show realizability of EMSO N [ * proc , msg ]and EMSO N [ proc , msg , ∼]-formulas for unambiguous classes of topologies (as discussed in the previous subsection).

Any { proc , msg }-neighborhood in an MSC also spans over a bounded topology (cf. Figure 7). But here, we can go one step further: up to isomorphism, there are only a bounded number of { proc , msg }-neighborhoods. Using this, we will build, in Section VII, a PCA that evaluates a formula by "computing" such neighborhoods in an MSC. The construction is independent of a class of topologies. However, the resulting PCA is only guaranteed to be equivalent to the given formula when it is applied to prime topologies.

VI. EMSO VS. PCA OVER UNAMBIGUOUS TOPOLOGY CLASSES A. Main Result and Consequences

Following the discussion in the previous section, we will consider logics that discard * . Particular attention is paid to EMSO N [ * proc , msg ], containing the process-order relation. Recall that the { * proc , msg }-neighborhood of an event is covered by a bounded area in the underlying topology. We exploit this to translate a formula into a PCA by simulating several fixed-topology CA in parallel. In fact, in our construction of a PCA, a process will have to determine its (bounded) topology neighborhood, so that it can launch a corresponding fixed-topology CA. To some extent, it can verify whether it is the source of a w-labeled path, for a given w ∈ (N × N ) * . In general, however, there is no means to discover whether w forms a cycle (cf. Theorem 4). We will, therefore, consider topology classes T in which some words are unambiguous, i.e., they always form a cycle, or never form a cycle in T. For example, (a,b)(c,d)(b,a)(d,c) is unambiguous for the class of grids: it gives rise to a cycle whenever it is applicable. As we deal with bounded topology neighborhoods, we have to consider only words up to a certain length.

Let

w = (a 1 , b 1 ) . . . (a n , b n ) ∈ (N × N ) * .
The length n of w is denoted by |w|. For a topology (P, ) ∈ T N and processes p, q ∈ P , we write p w q if there is a w-labeled path from p to q, i.e., there are p 0 , . . . , p n ∈ P such that

p = p 0 a 1 b 1 p 1 a 2 b 2 . . . a n b n p n = q.
Definition 4. Let k ∈ N and let T ⊆ T N be a class of topologies. We say that T is k-unambiguous if, for all w ∈ (N ×N ) * with |w| ≤ k, all topologies (P, ), (P , ) ∈ T, and all processes p, q ∈ P and p , q ∈ P such that p w q and p w q , we have p = q iff p = q .

In other words, if a topology from T admits a cycle of length ≤k with label w, then following w (if possible) will always form a cycle, in any topology from T. Note that "unambiguous" is a property of a class of topologies. It captures the classes of pipelines, trees, and grids. Moreover, it will allow us to apply our results to ring topologies.

Lemma 1. The classes T lin , T tree , T grid , and {T n ring | n ≥ max{3, k + 1}} are all k-unambiguous, for every k ∈ N. Moreover, {T } is k-unambiguous for all T ∈ T ring and k ∈ N.

For ϕ ∈ EMSO N [ * proc , msg ], let r ϕ ≥ 1 denote the radius associated with the first-order kernel of ϕ according to Theorem 3. Note that an exponential upper bound for r ϕ was given in [START_REF] Keisler | Shrinking games and local formulas[END_REF]. We now present our main result:

Theorem 6. Let ϕ ∈ EMSO N [ * proc
, msg ] be a sentence, B ≥ 1, and T ⊆ T N be an (r ϕ + 2)-unambiguous set of topologies. There is a PCA A ∈ PCA N such that, for all T ∈ T, we have L B T (A) = L B T (ϕ). Before we prove Theorem 6, let us discuss it and state some consequences. First, note that we have to commit to a class T of topologies before constructing the PCA. This is also what usually happens in practice: one has a "concrete" class of topologies in mind when writing a formula. For example, a specifier may want to synthesize a PCA that is equivalent to the given formula on all grids. 4 Though, a priori, different topology classes give rise to different PCA, we give a uniform construction and proof. By Lemma 1, we can then instantiate T in Theorem 6 with various classes so that we obtain the following corollary (for simplicity, we consider pipelines and rings as topologies over {a, b, c, d}):

Corollary 1. Let ϕ ∈ EMSO {a,b,c,d} [ * proc
, msg ] be a sentence, B ≥ 1, and T be any of the following:

• the set of pipeline topologies,

• the set of grid topologies,

• the set of tree topologies,

• the set of ring topologies with at least r ϕ + 3 nodes, or • the singleton set {T } where T is any ring topology. Then, there is a PCA A ∈ PCA {a,b,c,d} such that, for all T ∈ T, we have

L B T (A) = L B T (ϕ)
. The construction where one single ring topology is given is not an immediate consequence of a corresponding result from the setting with fixed topologies [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. The reason is that CA over fixed topologies have an initial state per process, while PCA have initial states per process type, which is a priori weaker. Now, given a formula ϕ, Corollary 1 gives us a way of "covering" all rings in terms of a finite collection of PCA: For those rings with at most r ϕ +2 processes, we can construct tailor-made PCA, i.e., one PCA for each ring. All other rings can be covered by one single PCA. Using this observation, we can even do better than that and show that one single PCA is enough. The idea is to "approximate" the size of the given ring in terms of the number of active processes and to launch a corresponding PCA according to Corollary 1. As we already know that we will run the PCA on a ring, we in fact only have to "determine" its size (see Appendix XV).

Theorem 7. Let ϕ ∈ EMSO {a,b} [ * proc , msg ] be a sentence and B ≥ 1. There is a PCA A ∈ PCA {a,b} such that, for all T ∈ T ring , we have L B T (A) = L B T (ϕ). Let us come back to the generic result of Theorem 6. Its proof uses the logical characterization of fixed-topology CA [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. But it works similarly for EMSO N [ proc , msg , ∼] when we take [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] instead of [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. In the setting of fixed topologies, ∼ reduces to a local comparison of event labels so that [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] is indeed applicable. The logic EMSO N [ proc , msg , ∼] is a priori weaker than EMSO N [ * proc , msg ], but allows us to drop the channel restriction.

Theorem 8. Let ϕ ∈ EMSO N [ proc , msg , ∼] be a sentence and T ⊆ T N be an (r ϕ + 2)-unambiguous set of topologies. There is a PCA A ∈ PCA N such that, for all T ∈ T, we have

L T (A) = L T (ϕ).
From Theorem 8 and Lemma 1, we can derive statements analogous to Corollary 1 and Theorem 7 (which we omit).

We do not know whether Theorem 8 holds for EMSO N [ * proc , msg ] (or, equivalently, whether Theorem 6 holds without channel bound). The answer is affirmative if EMSO N [ * proc , msg ] is equivalent to unbounded CA over fixed topologies. But this is an open problem.

The translation of PCA to EMSO N [ proc , msg ] is not restricted to topologies of a particular form. The proof of the following theorem is by a standard construction. Theorem 9. Let A ∈ PCA N be a PCA. There is a sentence ϕ ∈ EMSO N [ proc , msg ] such that, for all topologies T ∈ T N , we have L T (ϕ) = L T (A).

B. Proof Sketch for Main Result (Theorem 6)

The rest of this section is devoted to the proof of Theorem 6 (which works for Theorem 8 with only minor changes).

Set σ * = { * proc , msg } and let ϕ ∈ EMSO N [σ * ] be a sentence. According to Theorem 3, there are a radius r = r ϕ ≥ 1

and ϕ = ∃X 1 . . . ∃X m ∃x 1 . . . ∃x n ∀yχ ∈ EMSO N [σ * ] such that χ ∈ FO N [σ * ] is (r, σ * )-local
around y and, for all T ∈ T N , we have L T (ϕ) = L T (ϕ ). The free variables of ∀yχ can be considered as unary predicates and are dealt with by projection from an extended alphabet. By means of the acceptance condition of a PCA, one can make sure that variables x i are indeed interpreted as exactly one event. So, it essentially remains to translate the formula ∀yχ into a PCA.

There is, however, another subtlety. Satisfaction of χ in an MSC depends on the neighborhood of y of radius r but also on the truth values of propositions involving only the free variables of ∀yχ. Following [11, page 806], the PCA will guess and verify these truth values. By means of the acceptance condition, we can make sure that the guess is consistent throughout a run.

For simplicity, we henceforth suppose that y is the only free variable of χ (and write χ(y)). Thus, for the rest of the proof, we fix r, B ≥ 1, an (r + 2)-unambiguous set T ⊆ T N of topologies, and a sentence ∀yχ(y) ∈ FO N [σ * ] such that χ(y) is (r, σ * )-local around y. We will build a PCA A ∈ PCA N such that, for all T ∈ T, we have L B T (A) = L B T (∀yχ(y)). We sketch the construction and try to give some intuition. The formal definition of A is technical and requires a lot of additional notation. All details can be found in Appendix XIV.

We exploit locality of χ(y): to know whether M, e |= χ(y), i.e., MSC M satisfies χ(y) when y is interpreted as e, it is sufficient to look at the neighborhood of e with radius r (as y is the only free variable, r -1 actually would be enough).

Example 6. Consider the MSC M over T = T 2,5 grid depicted in Figure 8. Take any event e that is located on process p. All events f such that dist σ * M (e, f ) ≤ r = 3 lie on a process in the gray-shaded topology neighborhood of p with radius R = r/2 = 2, which has p as a distinguished center. We call this neighborhood a sphere and denote it by R-Sph(T , p). One major task of A is to identify spheres in the topology it is run on. But it has to rely on the messages that are predetermined by M . Therefore, A can actually only detect a substructure of R-Sph(T , p). Figure 9 depicts its restriction R-Sph(T , p) M (gray-shaded) to those edges that are "covered" by a message of M and to those nodes that one can reach from p with at most R such edges. However, every process preserves its complete type information. Observe that process (2, 5) is not part of R-Sph(T , p) M anymore. Moreover, the edge between (1, 3) and (1, 4) is removed, since it is not covered by a message. Let R-Sph(M, p) be the restriction of M to R-Sph(T , p) M (cf. again Figure 9). We call R-Sph(M, p) a partial MSC, since it has some unmatched events. In fact, satisfaction M, e |= χ(y) only depends on R-Sph(M, p), for all events e on p.

The example illustrates that, essentially, we have to cope with spheres and partial MSCs, i.e., structures of bounded "width". For a fixed sphere, every MSO N -formula can be translated to a (fixed-topology) CA that accepts exactly the partial MSCs that are a model of the fomula [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. For [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF] to apply, we need to restrict to B-bounded MSCs (unless we prove Theorem 8, which is based on [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF]). Thus, given a sphere θ, we can construct a CA B θ that recognizes the partial MSCs over θ that satisfy χ(y) for all events e located on the sphere center. Up to isomorphism, there are only finitely many spheres θ of radius R and, thus, finitely many CA B θ . To obtain the PCA A running on MSCs over arbitrarily large topologies, we will glue these CA together. Note that, to exploit unambiguousness, it is crucial that we restrict to those spheres that arise from topologies in T.

We proceed as follows. Every process p guesses a sphere θ, supposing that its topology neighborhood looks like θ, and grid , and 2-Sph(T 2,5 grid , p) runs a copy of B θ to make sure that the partial MSC in its neighborhood is accepted by B θ . Whenever p communicates with neighboring processes, the guess is forwarded in terms of messages. Processes receiving the guess also have to simulate B θ . Since neighboring processes have to verify their own guess as well, a process will actually have to run several CA simultaneously. The main difficulty, however, is to verify that a guess is correct so that the right CA is applied. The procedure of guessing and forwarding spheres is not able to check by itself whether a cycle in a sphere is correctly simulated in an MSC, and vice versa. It is only correct by the fact that the underlying set T of topologies is (r + 2)-unambiguous. Indeed, 2R + 1 = 2 r/2 + 1 ≤ r + 2 is the maximal length of a cycle through a sphere center that is needed to cover a given edge in the sphere.

1 ′ 2 ′ 1 ′ 2 ′ 3 ′ 4 ′
Example 7. We resume Example 6 to illustrate the functioning of A. So, assume T = T 2,5 grid ∈ T, r = 3, and R = r/2 = 2. In an accepting run of A on the MSC M from Figure 8, process p = (2, 3) will guess the sphere θ = R-Sph(T , p) M illustrated in Figure 9. Accordingly, it will launch the fixedtopology CA B θ , which accepts the partial MSC R-Sph(M, p) (cf. again Figure 9). Actually, B θ consists of several local automata B θ [q], one per sphere process q (rather than process type). Thus, p simulates the local automaton B θ [(2 , 3 )]. In doing so, it eventually sends θ to process (2, 2), together with its current position (2 , 3 ) in θ. Receiving the message through interface a, (2, 2) can infer its own position (2 , 2 ) in θ, and so it learns that it has to simulate B θ [(2 , 2 )]. Similarly, (2, 2) has to receive a message over interface d that confirms that (1, 2) has launched B θ [(1 , 2 )], and so on. There are subtle arguments and technical issues in A that guarantee that T and θ simulate each other. We sketch only the direction "T simulates θ". Let w = (b, a) (d,c)(a,b)(c,d). Our construction makes sure that, starting from p, T exhibits a w-labeled path. A priori, this does not imply that the path returns to p. But as θ arises from the (r + 2)-unambiguous class T, |w| = 4 ≤ r + 2, and w forms a cycle in θ, w forms a cycle in T as well. Recall that every process has to run several CA simultaneously, which we did not take into account in the example.

Remark 4. The normal form stated in Theorem 3 can be computed effectively (it builds on Gaifman's effective normal form). Thus, Theorem 6 is constructive if the spheres R-Sph(T , p) M with T ∈ T are effectively representable (which holds for all standard classes). It follows from the word case that the PCA cannot be computed in elementary time. Remark 5. We cannot exploit [START_REF] Henriksen | A theory of regular MSC languages[END_REF], [START_REF] Kuske | Regular sets of infinite message sequence charts[END_REF], dealing with universally bounded CA, instead of [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF], even if we restrict to universally B-bounded MSCs M (all linearizations are Bbounded): while R-Sph(M, p) is guaranteed to be (existentially) B-bounded, it is not necessarily universally B-bounded.

VII. EMSO VS. PCA OVER PRIME TOPOLOGIES Next, we present an orthogonal approach to realizability, where the construction of a PCA is independent of a concrete class of topologies. For this, we will restrict the logic further.

Recall that satisfaction of an FO N [ proc , msg ]-formula essentially depends on the { proc , msg }-neighborhoods that occur in an MSC 5 (Theorem 3). Up to isomorphism, there are only finitely many such neighborhoods, for a fixed radius. We slightly modify the construction from [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] (which we had used as a black-box for Theorem 8) and define a PCA that, when running on an MSC, outputs the neighborhood of each event. However, this automaton can, a priori, not detect cycles (cf. Theorem 4) and "needs some help" from the underlying topology. It is only guaranteed to compute neighborhoods correctly when it is run on prime topologies. "Prime" is in the spirit of "unambiguous", but on a lower level, since it is tailored to detecting neighborhoods in MSCs rather than in topologies. While "prime" discards all ring topologies and ring forests, it includes all pipelines, trees, and grids. We give more intuition in the proof sketch for Theorem 10 below.

Definition 5. A topology (P,

) ∈ T N is called prime if, for all p ∈ P , w ∈ (N × N ) * , and n ≥ 1, we have that p w n p implies p w p.

In other words, a prime topology satisfies the following monotonicity property: If p w q with p = q, then starting from p and "applying" w several times will never lead back to p. Note that "prime" is a property of a single topology, while "unambiguous" refers to a class of topologies. Lemma 2. All topologies in T lin , T tree , and T grid are prime, while none of the topologies in T ring is prime.

We build a PCA that is equivalent to a given formula ϕ on all prime topologies. Unlike in Theorem 6, it does not depend on a class of topologies, but only on ϕ and N .

Theorem 10. Let ϕ ∈ EMSO N [ proc , msg ] be a sentence. There is a PCA A ∈ PCA N such that, for all prime topologies T ∈ T N , we have L T (A) = L T (ϕ).

Proof: We sketch the idea, details can be found in Appendix XVI. Thanks to Theorem 3, the problem reduces to constructing a PCA from a formula ∀yχ ∈ FO N [ proc , msg ] where χ is (r, { proc , msg })-local around y, for some r ≥ 1 (cf. proof of Theorem 6). To translate ∀yχ into a PCA, we use the sphere automaton, a PCA that "detects" neighborhoods of radius r in an input MSC (including possible interpretations of free variables). More precisely, it accepts any MSC, over any given prime topology. Moreover, in any accepting run, the state assigned to event e tells us whether χ holds, or not, when y is interpreted as e. A sphere automaton is presented in [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] for a fixed, known topology, but it is actually independent of that topology. In the proof, it is only needed that MSCs are prime, essentially in the same sense as for topologies. But MSCs over prime topologies are indeed prime (cf. Appendix XVI) so that we obtain the desired sphere automaton. As a last step, the latter is restricted to states that signal that χ holds.

To compute neighborhoods, the PCA has to guarantee that certain sequences w of "directions" form a cycle in an MSC. While there is no direct way to enforce that w forms a cycle, a PCA can make sure that, for all n ∈ N, an event admits a w n -labeled path. As MSCs inherit the prime-property from topologies, this implies that w indeed gives rise to a cycle. Remark 6. Using Hanf's normal form (which we did not do to avoid additional notation), the PCA can be built in elementary time [START_REF] Bollig | An optimal construction of Hanf sentences[END_REF]. This is a priori not guaranteed using Theorem 3.

VIII. CONCLUSION

In this paper, we developed a framework for communicating systems with parameterized network topology. In particular, we provided various characterizations of PCA in terms of EMSO logic. Our constructions and proofs are uniform and capture typical cases such as pipelines, trees, grids, and rings.

Theorem 7 reveals that the notion "unambiguous" is not optimal: all EMSO {a,b} [ * proc , msg ]-formulas are realizable for the class of rings, which is not k-unambiguous for all k ≥ 3. It seems difficult to characterize exactly those classes for which all formulas from a given logic are realizable, but it will be worthwhile to examine if classes with comparably simple characterizations exist that generalize our results.

Our constructions crucially rely on the bounded-degree property. An obvious question would be a framework including topologies of unbounded degree such as star topologies or, more generally, unranked trees. However, it is not clear how a parameterized automaton should look like in that case. One possibility is to employ registers so that, at any time, a process can remember "some" of its unboundedly many neighbors.

Our framework may carry over to Zielonka's asynchronous automata [START_REF] Zielonka | Notes on finite asynchronous automata[END_REF] with binary actions. These automata have been considered in [START_REF] Genest | Asynchronous games over tree architectures[END_REF] over tree architectures to get decidability of the controller-synthesis problem. This also raises the question about a parameterized formulation of the control problem.

It is important to study also parameterized verification: Given a PCA A, is there a topology T such that L T (A) = ∅ ? Since those questions are undecidable in general, one has to impose restrictions, on PCA and/or on the topologies.

APPENDIX IX. FORMAL DEFINITION OF TOPOLOGY CLASSES

We give the formal definitions of pipelines, trees, grids, and rings. Recall that we do not distinguish isomorphic topologies. Given n ∈ N, we let in the following [n] := {1, . . . , n}.

For n ≥ 2, the pipeline T n lin is defined as the topology ({1, . . . , n},

) over {a, b} where

= { (i, a, b, i + 1) | i ∈ [n -1] } ∪ { (i + 1, b, a, i) | i ∈ [n -1] } .
A tree topology is a topology (P,

) over {a, b, c, d} where P is a prefix-closed subset of {0, 1} * such that |P | ≥ 2, and

= { (u, a, b, u0) | u, u0 ∈ P } ∪ { (u0, b, a, u) | u, u0 ∈ P } ∪ { (u, c, d, u1) | u, u1 ∈ P } ∪ { (u1, d, c, u) | u, u1 ∈ P } .
For n ≥ 3, the ring T n ring is defined as the topology ({1, . . . , n},

) over {a, b} where

= { (i, a, b, (i + 1) mod n) | i ∈ [n] } ∪ { ((i + 1) mod n, b, a, i) | i ∈ [n] } .
For m, n ≥ 1 such that max{m, n} ≥ 2, we define T m,n grid as the topology

([m] × [n],
) over {a, b, c, d} where

= { ((i, j), a, b, (i, j + 1)) | i ∈ [m] and j ∈ [n -1] } ∪ { ((i, j + 1), b, a, (i, j)) | i ∈ [m] and j ∈ [n -1] } ∪ { ((i, j), c, d, (i + 1, j)) | i ∈ [m -1] and j ∈ [n] } ∪ { ((i + 1, j), d, c, (i, j)) | i ∈ [m -1] and j ∈ [n] } .
X. PROOF OF THEOREM 1 Theorem 1. PCA are closed under union and intersection: For all A 1 , A 2 ∈ PCA N , there are PCA A and B over N such that, for all topologies T ∈ T N , we have

L T (A) = L T (A 1 ) ∪ L T (A 2 ) and L T (B) = L T (A 1 ) ∩ L T (A 2 ).
Proof: The proof is by a standard construction with one subtlety, which is the acceptance condition. Suppose

A 1 = (S 1 , Msg 1 , ∆ 1 , I 1 , F 1 ) and A 2 = (S 2 , Msg 2 , ∆ 2 , I 2 , F 2 ). We assume that S 1 ∩ S 2 = ∅.
For union, A = (S, Msg, ∆, I, F ) chooses and simulates non-deterministically A 1 or A 2 . The acceptance condition makes sure that this choice is consistent throughout a run. So, we let:

• S = S 1 ∪ S 2 , • Msg = Msg 1 ∪ Msg 2 , • ∆ = ∆ 1 ∪ ∆ 2 , • I(t) = I 1 (t) ∪ I 2 (t) for all t ∈ 2 N \ {∅}, and • F = (F 1 ∧ s∈S2 ¬ #(s) ≥ 1 ) ∨ (F 2 ∧ s∈S1 ¬ #(s) ≥ 1 ) .
For intersection, we use a standard product construction and define B = (S, Msg, ∆, I, F ) as follows:

• S = S 1 × S 2 , • Msg = Msg 1 × Msg 2 , • I(t) = I 1 (t) × I 2 (t) for all t ∈ 2 N \ {∅}.
Moreover, ∆ is the classical transition product: there is a transition (s 1 , s 2 )

! (m 1 ,m 2 ) a = ===== ⇒ (s 1 , s 2 ) whenever (s 1 , ! m1 a, s 1 ) ∈ ∆ 1 and (s 2 , ! m2 a, s 2 ) ∈ ∆ 2 .
Receive transitions are defined analogously. Note that the acceptance condition F is a finite boolean combination of statements #((

s 1 , s 2 )) ≥ k with (s 1 , s 2 ) ∈ S 1 × S 2 . It is given as F = [[F 1 ]] 1 ∧ [[F 2 ]] 2 .
Here, [[ . ]] 1 replaces every atomic formula #(s 1 ) ≥ k by

m∈M k (S2) s∈S2 #((s 1 , s 2 )) ≥ m(s 2 )
where M k (S 2 ) is the set of multisets over S 2 of size k, i.e., the set of mappings m :

S 2 → N such that s2∈S2 m(s 2 ) = k.
The transformation [[ . ]] 2 is defined analogously.

XI. PROOF OF THEOREM 4

Theorem 4. There exists a sentence ϕ ∈ FO {a,b} [ proc , msg ] such that, for all PCA A ∈ PCA {a,b} , there is

T ∈ T * ring with L 1 T (A) = L 1 T (ϕ). Proof:
The sentence ϕ will say that every event is part of the cycle pattern that is depicted in Figure 10:

ϕ = ∀x∃x 1 , . . . , x 6 (x ∈ {x 1 , . . . , x 6 } ∧ cycle(x 1 , . . . , x 6 ))
where cycle(x 1 , . . . , x 6 ) is defined as

x 1 msg x 2 proc x 3 msg x 4 proc x 5 msg x 6 ∧ x 1 proc x 6 ∧ i∈{1,3,5} act(x i ) = !a
Towards a contradiction, suppose there is a PCA A such that, for all T ∈ T * ring , L T (A) and L T (ϕ) agree on all 1bounded MSCs. Without loss of generality, we assume that send transitions in A are of the form (s, ! s a, s ), i.e., the message coincides with the target state. Consider the MSC M n that consists of n ≥ 1 disjoint copies of the "atomic" MSC from Figure 10. That is, M n is an MSC over the topology T n = T 3 ring . . . T 3 ring ∈ T * ring with n disjoint copies of T 3 ring . Obviously, M n ∈ L 1 Tn (ϕ) = L 1 Tn (A) for all n ≥ 1. When we choose n large enough, then there is an accepting run ρ of A on M n that behaves the same on at least two disjoint copies of atomic MSCs. More precisely, M n is an MSC over T T 3 ring T 3 ring ∈ T * ring , for some T , such that ρ assigns states s 1 , . . . , s 6 to the events x 1 , . . . , x 6 of the atomic MSCs over the last two copies of T 3 ring , respectively. We will now replace these two atomic MSCs with the larger one from Figure 11, over T 6 ring . The resulting MSC, call it M n , is a 1-bounded MSC over T T 6 ring . There is still a run on M n , using the assignment shown in Figure 11. As the multiset of terminal states does not change, the run is accepting. But this is a contradiction, since M n does not satisfy ϕ.

XII. PROOF OF THEOREM 5

Recall that we consider tree topologies from T tree over {a, b, c, d}.

Theorem 5. There exists a sentence ϕ ∈ FO {a,b,c,d} such that, for all PCA A ∈ PCA {a,b,c,d} , there is T ∈ T tree with L 1 T (A) = L 1 T (ϕ). Proof: A picture over the set Ω = { , , } of colors is a rectangular matrix with m ≥ 1 rows and n ≥ 1 columns, and with entries in Ω. An example picture of dimension

(m = 3, n = 8) is P =    
The coordinates of a picture can be ordered by relations ≤ 1 (for columns) and ≤ 2 (for rows). We let (i, j) ≤ 1 (i , j ) if i ≤ i and j = j , and (i, j) ≤ 2 (i , j ) if i = i and j ≤ j . Accordingly, FO logic over pictures uses the binary predicates x ≤ 1 y and x ≤ 2 y, as well as unary predicates η(x) with η ∈ Ω. Let P = be the set of those pictures that are the concatenation P 1 QP 2 of pictures of the same height, where Q is a single column with entries , and P 1 and P 2 are pictures over { , } whose sets of column labelings coincide. The example picture P above is contained in P = . Note that P = is FO-definable by a sentence that requires that, for all coordinates x in the first row, there has to be a coordinate y on the opposite side of the picture (i.e., beyond column Q) such that their respective column labelings coincide. This can indeed be expressed using ≤ 1 and ≤ 2 . In [START_REF] Thomas | Elements of an automata theory over partial orders[END_REF], Thomas exploits the picture language P = to show that FO over pictures using ≤ 1 and ≤ 2 is incomparable with EMSO using the direct successor relations of ≤ 1 and ≤ 2 , which is equivalent to graph acceptors.

To transfer that result and its proof to our setting, we use MSCs to encode pictures. An MSC encoding of a picture is based on a tree topology of a particular form. Let T pict be the set of topologies T n pict ∈ T tree , with n ≥ 1, as depicted in Figure 12 for n = 8. Note that T n pict has 2n + 1 vertices. As T pict is a subset of T tree , it is k-unambiguous, for all k ∈ N, and contains only prime topologies. The MSC M that encodes picture P (see above) is shown in Figure 12. An event performing !a corresponds to a picture coordinate. If it is immediately followed, on the same process line, by one event performing !c, then its entry is . If it is immediately followed Fig. 12. The communication topology T 8 pict over N = {a, b, c, d}, as well as an MSC that encodes a picture by two events performing !c, then its entry is . Otherwise, it is . Note that M is 1-bounded.

The set of all valid picture encodings is definable by a formula Ψ from FO {a,b,c,d} , i.e., for all n ≥ 1, L T n pict (Ψ) is the set of MSCs that correspond to pictures with n columns. Let L n = be the set of MSCs over T n pict , that encode a picture from P = with n columns. In FO {a,b,c,d} , we can define formulas is-coordinate(x) and η(x) for all η ∈ Ω in the obvious way. Moreover, x ≤ 1 y (which corresponds to walking down in a picture) is given, for MSCs, by x * proc y. Finally, x ≤ 2 y (which corresponds to walking rightwards in a picture) is given by x * y ∧ ∀x (x proc x → ¬(x * y)) . It follows that there is a sentence ϕ ∈ FO {a,b,c,d} such that

L n = = L T n pict (ϕ) = L 1 T n pict (ϕ)
, for all n ≥ 1. Now suppose that there is a PCA A = (S, Msg, ∆, I, F ) such that, for all T ∈ T pict , we have L 1 T (A) = L 1 T (ϕ). In any accepting run of A on an MSC M ∈ L n = encoding picture P 1 QP 2 , say, of height m, all the information needed to compare P 1 and P 2 has to be present in the constant number of equivalence classes induced by F and in the assignments of states and messages to the events located on Q, i.e., on thelabeled column. There are (|S| × |Msg|) m such assignments. On the other hand, there are 2 2 m -1 nonempty sets of words of length m over { , }, which exceeds (|S| × |Msg|) m for sufficiently large m. Thus, there is an accepting run, possibly wrt. a different topology, on the encoding of P 1 QP 2 for some P 1 , P 2 that induce distinct sets of column labelings, a contradiction.

Note that the proof reveals that Theorem 5 already holds for the logic FO {a,b,c,d} [ * , ∼].

XIII. PROOFS OF LEMMA 1 AND LEMMA 2

Lemma 1. The classes T lin , T tree , T grid , and {T n ring | n ≥ max{3, k + 1}} are all k-unambiguous, for every k ∈ N. Moreover, {T } is k-unambiguous for all T ∈ T ring and k ∈ N.

Proof: Note that the claim for pipelines follows from the result for trees or grids. Trees: Set a = b, b = a, c = d, and d = c. We say that a word w ∈ ({a, b, c, d}×{a, b, c, d}) * is well-formed if it is generated by the grammar A → (a, a)A(a, a)A | ε where a ∈ {a, b, c, d}. We show that, for all w ∈ ({a, b, c, d} × {a, b, c, d}) * , all (P, ) ∈ T tree , and all p, q ∈ P such that p w q, we have p = q ⇐⇒ w is well-formed.

This will imply the claim from the lemma. We proceed by induction on the structure of w. The claim is immediate for w = ε. So suppose that w = ε. First, assume p = q. Then, w is of the form (a, a) w 1 (a, a) w 2 such that p a a p w 1 p a a p w 2 p for some p . Using the induction hypothesis, we obtain that w 1 and w 2 are both well-formed. Thus, w is well-formed as well. Conversely, suppose that w is well-formed. Then, it is of the form (a, a) w 1 (a, a) w 2 such that w 1 and w 2 are wellformed. By the induction hypothesis, we get p = q.

Grids: Since the grid T m,n grid ∈ T grid is isomorphic to (P,

) where P = {1, . . . , m} × {1, . . . , n} are coordinates in the plane, "applying" pairs (a, b), (b, a), (c, d), (d, c) to a coordinate (i, j) corresponds to adding, component-wise, (0, 1), (0, -1), (1, 0), (-1, 0), respectively. In the expected manner, every word w ∈ ({a, b, c, d} × {a, b, c, d}) * determines a pair w ∈ Z × Z. For all p, q ∈ P , we have p w q =⇒ p + w = q . Now, p w p implies w = (0, 0), which implies the claim.

Rings:

The set {T n ring | n ≥ max{3, k+1}} is k-unambiguous, since a word of length ≤k is not sufficient to circumnavigate a ring with at least max{3, k + 1} nodes. Thus, the same argument as for pipelines (grids) applies. Finally, {T } is kunambiguous for every ring T ∈ T ring and k ∈ N, since every node in T "looks the same". Lemma 2. All topologies in T lin , T tree , and T grid are prime, while none of the topologies in T ring is prime.

Proof: Again, the claim for pipelines follows from the result for trees or grids.

Trees: The claim follows from the fact that, given a word w ∈ ({a, b, c, d} × {a, b, c, d}) * that is not well-formed (cf. proof of Lemma 1), w n is not well-formed either, for all n ≥ 1 (like for words that are not well-bracketed).

Grids: For grids, we also apply the argument from the proof of Lemma 1. Suppose that p w q with p = q. This implies w = (0, 0). Since addition is monotonous, we have that p w n q implies p = q , for all n ≥ 1.

Rings: Let T n ring = (P, ) ∈ T ring , p ∈ P , and w = (a, b) n . Then, we have p w p. Thus, T n ring is not prime.

XIV. MISSING DETAILS FOR PROOF OF THEOREM 6

Recall that we fixed r, B ≥ 1, a (r + 2)-unambiguous set T ⊆ T N of topologies, and a sentence ∀yχ(y) ∈ FO N [σ * ] such that χ(y) is (r, σ * )-local around y. Moreover, we set R = r/2 . We will build a PCA A such that, for all T ∈ T, we have L B T (A) = L B T (∀yχ(y)).

A. Communicating Automata over Sphere Topologies

Let T = (P, ) ∈ T N . For p, q ∈ P , set dist T (p, q) to be the distance (i.e., the minimal length of a path, or ∞ if such a path does not exist) between p and q in T . By R-Sph(T , p), we denote the R-sphere of T around p, i.e., the substructure of (P, , type T ) induced by the vertices q ∈ P such that dist T (p, q) ≤ R, with p as an additional constant called center. Note that R-Sph(T , p) is always a topology (when we ignore the type mapping and the constant). For example, the shaded area in Figure 8 captures the sphere 2-Sph(T 2,5 grid , p). Let R-Spheres(T N ) := {R-Sph(T , p) | T = (P, ) ∈ T N and p ∈ P }. Any element from R-Spheres(T N ) is called an (R-)sphere. We (mostly) do not distinguish isomorphic spheres so that the number of R-spheres is finite (thanks to the fact that topologies have bounded degree).

Let θ = (U, γ) ∈ R-Spheres(T N ) be an R-sphere, with U = (Q, :: , ξ). Recall that ξ : Q → 2 N and γ ∈ Q is the center. Similarly to topologies, we may also write dist U (p, q) or dist θ (p, q) for dist (Q, :: ) (p, q). We will define (partial) MSCs over θ. These MSCs are connected, are empty or have at least one event on γ, and may have unmatched events, namely those whose communication partners are beyond U. Definition 6. An MSC over θ is a tuple M = (E, , , λ) where E is the finite (possibly empty) set of events, = proc msg ⊆ E ×E is the acyclic edge relation, : E → Q, and λ : E → { !a , ?a | a ∈ N }. For p ∈ Q, let E p := {e ∈ E | (e) = p}. We require that the following hold:

• proc is a union p∈P p where each p ⊆ E p × E p is the direct-successor relation of some total order on E p ,

• there are a partition E = E ! E ? E unm and a bijection µ : E ! → E ? such that msg = {(e, µ(e)) | e ∈ E ! } (events from E unm are called unmatched),

• for all (e, f ) ∈ msg , there are a, b ∈ N such that (e) ::: a b (f ) and (λ(e), λ(f )) = (!a, ?b),

• for all (e, f ), (e , f ) ∈ msg such that (e) = (e ) and (f ) = (f ), we have e * proc e iff f * proc f (FIFO), • for all e ∈ E unm and a ∈ N with λ(e) ∈ {!a, ?a}, we have both dist θ (γ, (e)) = R and there is no pair (b, p) ∈ N × Q such that (e) ::: a b p. Moreover, we require that, if E = ∅, then the graph (E, ) is connected and E γ = ∅.

Note that this definition actually depends on R, which we had fixed. Again, we do not distinguish isomorphic partial MSCs.

The definition of B-bounded MSCs over θ is literally the same as for MSCs over topologies. This means that unmatched events are discarded and considered as internal actions, i.e., they do not count when computing the difference between sends and receives. An example of a 1-bounded MSC over a 2-sphere is depicted in Figure 9.

Definition 7. Suppose θ = (U, γ) to be an R-sphere with U = (Q, :: , ξ). A communicating automaton (CA) over θ is a tuple B = (S, ∆, ι, F ) where

• S is the finite set of states, • ι : Q → S associates with each process an initial state, • F : Q → 2 S determines the local final states, • ∆ ⊆ S × Σ B × S is the set of transitions.

Here, the set of actions is Σ B = { ! m a , ? m a | a ∈ N and m ∈ S}. We require that, for all (s, ! m a, s ) ∈ ∆, we have m = s . This is sufficient and will simplify our constructions.

Runs of CA are defined similarly to PCA, but we have to consider unmatched events. Let M = (E, , , λ) be an MSC over θ, and let ρ : E → S be a mapping. We define ρ -: E → S as follows: For (f, e) ∈ proc , let ρ -(e) = ρ(f ); for a proc -minimal event e ∈ E, we let ρ -(e) = ι( (e)). Then, ρ is a run of B on M if

• for all (e, f ) ∈ msg and names a, b ∈ N with (e) ::: a b (f ), we have both (ρ -(e), ! ρ(e) a, ρ(e)) ∈ ∆ and (ρ -(f ), ? ρ(e) b, ρ(f )) ∈ ∆,

• for all e ∈ E unm and a ∈ N with λ(e) = !a, we have (ρ -(e), ! ρ(e) a, ρ(e)) ∈ ∆,

• for all e ∈ E unm and a ∈ N with λ(e) = ?a, we have (ρ -(e), ? m a, ρ(e)) ∈ ∆ for some m ∈ S (the message is irrelevant). The run is accepting if ρ(e) ∈ F ( (e)) for all proc -maximal events e ∈ E. By L(B), we denote the set of MSCs over θ for which there is an accepting run of B. Note that L(B) always contains the empty MSC over θ.

Let T = (P, ) ∈ T N be a topology, p ∈ P , and M = (E, , ) be an MSC over T . Set H = {(q, a, b, q ) ∈ | q = (e) and q = (f ) for some (e, f ) ∈ msg ∪ -1 msg }. Let Q be the set of processes q ∈ P such that p and q are connected in the graph (P, H) by a path using at most R edges. By R-Sph(M, p) (somewhat abusing notation), we denote the restriction of (E, , , act M ) to events in -1 (Q). We also define R-Sph(T , p) M := ((Q, H |Q , type T |Q ), p) where H |Q = {(q, a, b, q ) ∈ H | q, q ∈ Q} and type T |Q is the restriction of type T to Q. Then, R-Sph(T , p) M is an R-sphere and R-Sph(M, p) is an MSC over R-Sph(T , p) M . For example, consider the MSC M over T 2,5 grid from Figure 8. Figure 9 shows the MSC 2-Sph(M, p) over the sphere 2-Sph(T 2,5 grid , p) M . The next theorem is due to a result by Genest, Kuske, and Muscholl. It allows us to evaluate ∀yχ(y) in terms of CA over bounded topologies.

Theorem 10 (cf. [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF], Theorem 4.1). There is a collection (B θ ) θ∈R-Spheres(T N ) of CA B θ over θ such that the following holds, for all topologies T = (P, ) ∈ T N , all p ∈ P , and all B-bounded MSCs M = (E, , ) over T :

M, e |= χ(y) for all e ∈ E p ⇐⇒ R-Sph(M, p) ∈ L(B R-Sph(T ,p) M ) .
The result from [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF] applies, since R-Sph(M, p) is Bbounded and, given e ∈ E p , all events f ∈ E such that dist σ * M (e, f ) ≤ r are covered by R-Sph(M, p) (cf. Figures 7, 8, and9). Finally, as MSCs over spheres are connected, local final states in CA are enough.

Remark 7. When χ(y) has more free variables than just y, B θ also depends on an assignment of truth values to propositions in χ over these variables.

Remark 8. To prove Theorem 8, we use [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] instead of [START_REF] Genest | A Kleene theorem and model checking algorithms for existentially bounded communicating automata[END_REF]. In fact, Theorem 10 holds verbatim (even without the restriction to B-bounded MSCs) when ∀yχ(y) ∈ FO N [ proc , msg , ∼]. Note that, in the fixed-topology setting, ∼ reduces to the comparison of sphere-process labels that are added to events so that [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] can indeed be applied.

B. The Construction of A

According to Theorem 10, it will be sufficient that each process that is run by the PCA A identifies a subsphere of its actual topology neighborhood. So, we set R-Sub(T) := {R-Sph(T , p) M | T = (P, ) ∈ T, p ∈ P , and M an MSC over T }, which is finite up to isomorphism. Note that, for T ∈ T and a process p of T , R-Sub(T) includes R-Sph(T , p) as well as some spheres that consist only of one single node. We fix the finitely many CA (B θ ) θ∈R-Sub(T) according to Theorem 10, where B θ = (S θ , ∆ θ , ι θ , F θ ) such that the sets S θ are pairwise disjoint.

We say that w ∈ (N × N ) * is circular (wrt. T) if there are T = (P, ) ∈ T and p ∈ P such that p w p.

The PCA A = (S, Msg, ∆, I, F ) ∈ PCA N with S = Msg is defined as follows (U will always refer to (Q, :: , ξ) and U to (Q , :: , ξ )):

States: A state t ∈ S is a nonempty set of tuples κ = (U, γ, α, s, H) where (U, γ) ∈ R-Sub(T) is a guessed sphere, α ∈ Q is the active process, s ∈ S (U ,γ) is the current state of the CA B (U ,γ) that is simulated, and H ⊆ N is the "history" containing the names that have been used by the active process. Intuitively, a process whose current state contains κ simulates process α in B (U ,γ) , supposing that its topology neighborhood resembles (U, γ, α). So, we require that, for all κ = (U, γ, α, s, H) ∈ t and κ = (U , γ , α , s , H ) ∈ t, the following hold: (a) ξ(α) = ξ (α ), (b) if γ = α and γ = α , then κ = κ , (c) if (U, γ, α) = (U , γ , α ), then κ = κ , and (d) for all a, b, b ∈ N , p ∈ Q, and p ∈ Q such that α ::: a b p and α ::: a b p , we have b = b . Let t ∈ S and a, b ∈ N . We let t ab and ba t both denote the set of tuples (U, γ, α, s, H) ∈ t such that there is p ∈ Q satisfying α ::: a b p.

We say that (a, b) is enabled in t if, for all (U, γ, α, s, H) ∈ t, q ∈ Q, and w ∈ (N × N ) ≤2R such that w(a, b) is circular and q ::: w α, we have α ::: a b q.

Initial and Final States: For t ∈ 2 N \ {∅}, a state t ∈ S is contained in I(t) if, for all (U, γ, α, s, H) ∈ t, we have ξ(α) = t, s = ι (U ,γ) (α), and H = ∅. Towards the final states, let G be the set of states t ∈ S such that, for all tuples (U, γ, α, s, H) ∈ t, we have s ∈ F (U ,γ) (α) and {a ∈ N | α ::: a b p for some b ∈ N and p ∈ Q} ⊆ H. The latter means that H contains Next, we show that ρ p0 is accepting. Let e ∈ Ev p0 be process-maximal and suppose κ e = (U, γ, α, s, H). From the fact that ρ is accepting, we can deduce that s ∈ F p0 (α).

To finish the proof, it remains to show (2), i.e., τ p0 ∼ = θ p0 . This is done using the H-component of a state as well as the fact that T is (r + 2)-unambiguous.

For p ∈ P and a triple (U, γ, α), we write (U, γ, α) ∈ ρ(p) if there are s, H, and an event e ∈ E p such that (U, γ, α, s, H) ∈ ρ(e).

Suppose τ p0 = (W = (W, , π), p 0 ) and θ p0 = (U = (Q, :: , ξ), q 0 ). For d ∈ {0, . . . , R}, let ((W d , d , π d ), p 0 ) be the restriction of τ p0 to elements of distance at most d from p 0 in W. Similarly, let ((Q d , :: d , ξ d ), q 0 ) be the restriction of θ p0 to elements of distance at most d from q 0 in U.

The following claim implies (2):

Claim 1. For all d ∈ {0, . . . , R}, there is an isomorphism

h d : ((W d , d , π d ), p 0 ) → ((Q d , :: d , ξ d ), q 0 )
such that, for all p ∈ W d , we have

(U, q 0 , h d (p)) ∈ ρ(p) .
Proof: The claim holds for d = 0, since (U, q 0 , q 0 ) ∈ ρ(p 0 ). Now, suppose the claim holds for some d < R so that we have an isomorphism

h d : ((W d , d , π d ), p 0 ) → ((Q d , :: d , ξ d ), q 0 ) . Towards h d+1 , we extend the domain of h d to elements p ∈ W d+1 \ W d . So let p, p ∈ W such that dist W (p 0 , p) = d, dist(p 0 , p ) = d + 1
, and p and p are connected by an edge in τ p0 . Moreover, set q = h d (p).

Suppose p a b p with a, b ∈ N . Since dist W (p 0 , p) < R, we also have, by induction hypothesis, dist U (q 0 , q) < R. Suppose (e, e ) ∈ msg ∪ -1 msg such that e is located on p and e is located on p . By induction hypothesis, we have (U, γ, q, s, H) ∈ ρ(e) for some s, H. By (ST) and (RT), there is q ∈ Q such that (U, γ, q , s, H) ∈ ρ(e ) and q ::: a b q . Note that, since h d is an isomorphism, q ∈ Q d+1 \ Q d . Set h d+1 (p ) = q . This is well-defined and does not depend on the concrete choice of p or a: if we obtained another, distinct element q , we would have (U, γ, q , s, H) ∈ ρ(e ), which is a contradiction to the definition of the set of states of A. We define h d+1 to agree with h d on W d .

It remains to show that h d+1 is an isomorphism. First, we show that h d+1 is surjective. Let a, b ∈ N , and let q, q ∈ Q with distance d and d + 1, respectively, from q 0 such that q ::: a b q . Let p = h -1 d (q). By induction hypothesis, we have (U, q 0 , q) ∈ ρ(p). As dist U (q 0 , q) < R and ρ is an accepting run, there is p ∈ W satisfying p a b p and (U, q 0 , q ) ∈ ρ(p ). Thus, h d+1 (p ) = q so that h d+1 is surjective.

For w ∈ (N × N ) * , let ←w ∈ (N × N ) * denote its reverse, which is defined inductively by ←ε = ε and ← ---w(a, b) = (b, a) ←w . Now, let us show that h d+1 is indeed an isomorphism. Take

p 1 , p 2 ∈ W d and p 1 , p 2 ∈ W d+1 \ W d as well as w 1 , w 2 ∈ (N × N ) d and a 1 , b 1 , a 2 , b 2 ∈ N such that • p 0 w 1 p 1 a 1 b 1 p 1 and • p 0 w 2 p 2 a 2 b 2 p 2 .
For i = 1, 2, let q i = h d+1 (p i ) and q i = h d+1 (p i ). We will show that

• p 1 = p 2 iff q 1 = q 2 (so that h d+1 is injective), and • p 1 a b p 2 iff q 1 ::: a b q 2 , for all a, b ∈ N .

First, suppose p 1 = p 2 . Let w = (b 1 , a 1 ) ←w 1 w 2 (a 2 , b 2 ). Then, p 1 w p 1 . As T is (r + 2)-unambiguous, τ p0 , θ p0 ∈ R-Sub(T), |w| ≤ 2R = 2 r/2 ≤ r + 2, and q 1 ::: w q 2 , this implies q 1 = q 2 . The same argument applies when we start with q 1 = q 2 . Next, suppose p 1 a b p 2 , for some a, b ∈ N . Since is the relation belonging to τ p0 , a message is exchanged between two events located on p 1 and p 2 , respectively. It follows that there is e

∈ E p 1 such that (a, b) is enabled in ρ(e). Let w = (b 2 , a 2 ) ← - w 2 w 1 (a 1 , b 1 )
. Then, |w| ≤ 2R and w(a, b) is circular. As (a, b) is enabled in ρ(e), (U, q 0 , q 1 ) ∈ ρ(p 1 ), and q 2 ::: w q 1 , we have q 1 ::: a b q 2 . Finally, suppose q 1 ::: a b q 2 , for some a, b ∈ N . Let w = (b 2 , a 2 ) ←w 2 w 1 (a 1 , b 1 ). As ρ is an accepting run, a message has to be exchanged between p 1 and a process p such that p 1 a b p. We have q 2 ::: w q 1 ::: a b q 2 and p 2 w p 1 a b p.

As T is (r + 2)-unambiguous and |w(a, b)| ≤ 2R + 1 = 2 r/2 + 1 ≤ r + 2, we have p = p 2 . Thus, p 1 a b p 2 .
This concludes the proof of Claim 1.

XV. PROOF OF THEOREM 7 Theorem 7. Let ϕ ∈ EMSO {a,b} [ * proc , msg ] be a sentence and B ≥ 1. There is a PCA A ∈ PCA {a,b} such that, for all T ∈ T ring , we have L B T (A) = L B T (ϕ). The rest of the section is devoted to the proof of the theorem. Intuitively, A will "approximate" the size of the ring on which it is run, and launch a corresponding automaton. Set n = r ϕ + 2. According to Corollary 1, let A n+1 be the PCA for the class of rings of size at least n + 1. Moreover, for k ∈ {3, . . . , n}, let A k be the PCA for the single ring topology T k ring . Now, A is the union of several product PCA A k × B k (for the intersection of A k and B k ; cf. Theorem 1), with k ranging over {3, . . . , n + 1}. Here, B k imposes a condition on the number of active processes of an MSC. First, B 3 accepts those MSCs that have ≤3 active processes. For k ∈ {4, . . . , n}, B k checks that an MSC has exactly k active processes. Finally, B n+1 requires that there are at least n + 1 active processes.

The construction of A is straightforward. To prove its correctness, we exploit that, for k < l, PCA A k and A l behave equivalently on MSCs M over T l ring with k active processes. This is why we can apply A k to M even though the underlying ring has size larger than k.

For an MSC M (over some topology) and k ∈ {3, . . . , n + 1}, we write M ≈ k if the following hold:

• M has ≤3 active processes if k = 3, • M has exactly k active processes if k ∈ {4, . . . , n}, and • M has ≥k active processes if k = n + 1. The following observation is crucial: Lemma 4. Let l ≥ 3 and k ∈ {3, . . . , n + 1}. Moreover, let T be the ring topology of size l and M be an MSC over T such that M ≈ k. Then, M ∈ L B T (A k ) iff M ∈ L B T (A min{l,n+1} ). Proof: If k = l, then there is nothing to show (the case k = n + 1 < l is also immediate). Suppose k < l. Since M = (E, , ) is an MSC over T such that M ≈ k, M is acyclic meaning that there is an active process p of M that does not communicate through one of its interfaces:

• for all e ∈ E p , act M (e) ∈ {!a, ?a}, or • for all e ∈ E p , act M (e) ∈ {!b, ?b}. But then, according to the construction from Appendix XIV, every accepting run of A k on M is also an accepting run of A min{l,n+1} on M , and vice versa. An alternative argument is that the truth value of a formula/automaton does not change when we add or remove non-active processes in a topology. Thus, we have M ∈ L B T (A k ) iff M ∈ L B T (A min{l,n+1} ) We will now argue that A is correct. Let l ≥ 3 and let T be the ring of size l. We have to show that L B T (A) = L B T (ϕ). We first consider the inclusion L B

XVI. MISSING DETAILS FOR PROOF OF THEOREM 10

MSCs over Prime Topologies: Recall that the construction of a PCA from a formula is based on the sphere automaton.

For the construction from [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] (which we recall below) to be applicable, we have to show that MSCs are prime just like topologies. Let us define when an MSC is prime. 6 Consider the set D = {proc, proc -1 } ∪ {msg Sphere Automaton: Next, we adapt the construction of the sphere automaton from [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF] to our setting. We build a PCA that is able to tell us whether, at a given event, a local formula holds. Again, we restrict to local formulas with only one free variable. To decide if a local formula holds, it is actually sufficient for the PCA to detect spheres, i.e., local neighborhoods of radius r ∈ N. Let us define spheres formally. Set σ = { proc , msg }. Let T = (P, ) ∈ T N be a topology, M = (E, , ) be an MSC over T , and e ∈ E. The r-sphere of M around e, denoted by r-Sph(M, e), is the restriction of (E, , , act M ) to events of distance at most r from e. More precisely, it is defined as the structure M = (E , , π, λ, e) where E = {f ∈ E | dist σ M (e, f ) ≤ r}, is given by proc = proc ∩ (E × E ) and msg = msg ∩ (E × E ), and π and λ are mappings with domain E : for all e ∈ E , π(e) = type T ( (e)) and λ(e) = act M (e). Note that M does not depend on a topology anymore, as an event is mapped by π to a process type rather than a process.

Let S r := {r-Sph(M, e) | M is an MSC over some topology T ∈ T N and e is an event of M } denote the set of r-spheres that arise from MSCs, ranging over all topologies. Note that S r is finite up to isomorphism. Interestingly, the sphere automaton that we are going to construct has similarities with the PCA built in Section VI. However, the crucial difference is that the sphere automaton is supposed to detect spheres, while the automaton from Section VI evaluates topologies. So, the sphere automaton will guess a sphere, for each event e, and verify that the guessed sphere is indeed isomorphic to the rsphere around e. Lemma 6. Let r ∈ N be some radius. There are a PCA A = (S, Msg, ∆, I, F ) ∈ PCA N and a mapping ν : S → S r such that the following hold, for all prime topologies T ∈ T N

Fig. 4 .

 4 Fig. 1. Pipeline T 4 lin

Fig. 5 . MSC M 8 lin over topology T 8 linExample 2 .

 582 Fig. 5. MSC M 8 lin over topology T 8 lin

Fig. 7 .

 7 Fig. 7. Distance r = 3 in an MSC depending on the signature

Fig. 8 .

 8 Fig. 8. MSC M over T 2,5 grid , and 2-Sph(T 2,5 grid , p)

Fig. 9 .

 9 Fig. 9. MSC 2-Sph(M, p) over 2-Sph(T 2,5 grid , p) M

4 Fig. 11 .

 411 Fig. 10. Cycle

  T (A) ⊆ L B T (ϕ). Let M ∈ L B T (A). There is k ∈ {3, . . . , n + 1} such that M ∈ L B T (A k × B k ). As M ∈ L B T (B k ), we have M ≈ k. Moreover, M ∈ L B T (A k ). By Lemma 4, this implies M ∈ L B T (A min{l,n+1}). The latter equals L B T (ϕ). We deduce that M ∈ L B T (ϕ). Now, we consider the inclusionL B T (A) ⊇ L B T (ϕ). Let M ∈ L B T (ϕ), and let k ∈ {3, . . . , n + 1} such that M ≈ k. Note that k is uniquely determined. Clearly, we have M ∈ L B T (B k ). Moreover, M ∈ L B T (A min{l,n+1} ). By Lemma 4, this implies M ∈ L B T (A k ). We deduce M ∈ L B T (A k × B k ), which finally implies M ∈ L B T (A).

  (a,b) , msg -1 (a,b) | a, b ∈ N } of directions. Let M = (E, , ) be an MSC, over some topology. Every direction δ ∈ D defines a binary relation[[δ]] M ⊆ E × E as follows: • [[proc]] M = proc , • [[proc -1 ]] M = -1 proc , • [[msg (a,b) ]] M = {(e, f ) ∈ msg | (e) a b (f )}, and • [[msg -1 (a,b) ]] M = {(f, e) ∈ -1 msg | (e) b a (f )}. This is extended to strings w = δ 1 . . . δ n ∈ D * : we let (e, f ) ∈ [[w]] M if (e, f ) ∈ id E • [[δ 1 ]] M • . . . • [[δ n ]] M (where • is the relation product). The MSC M is called prime if, for all w ∈ D * , n ≥ 1, and e ∈ E, we have that (e, e) ∈ [[w n ]] M implies6 The property is exploited in [3, Claim 4.1] without being called prime. In [B. Bollig. On the expressive power of 2-stack visibly pushdown automata. Logical Methods in Computer Science, 4(4:16), 2008.], a weaker property (which is implied by prime) is named circular. There, the sphere automaton is constructed for nested words.

proc e 1 or e 1 + 1 + proc e 2 +

 112 (e, e) ∈ [[w]] M . Note that MSCs are in general not prime, i.e., for arbitrary topologies. However, we can show the following: Lemma 5. Let T = (P, ) ∈ T N be a prime topology and M = (E, , ) be an MSC over T . Then, M is prime.Proof: Let w ∈ D * , n ≥ 1, and e ∈ E, and suppose (e, e) ∈ [[w n ]] M . We build the "projection" w ∈ (N × N ) * of w to the alphabet N × N so that it can be applied to the topology T . It is defined by proc = proc -1 = ε and msg (a,b) = msg -1 (a,b) = (a, b). From (e, e) ∈ [[w n ]] M , we deduce (e) w n (e), which implies (e) w (e), since T is prime. Towards a contradiction, assume that (e, e) ∈ [[w]] M (which implies w = ε and n > 1). Consider the unique event e 1 ∈ E such that (e, e 1 ) ∈ [[w]] M . Due to (e) w (e), we have either e + proc e. Suppose e + proc e 1 . The other case is analogous. As (e, e) ∈ [[w n ]] M , there are e 2 , . . . , e n ∈ E such that (e, e 1 ), (e 1 , e 2 ), . . . , (e n-1 , e n ) ∈ [[w]] M . Thus, (e, e n ) ∈ [[w n ]] M . As MSCs obey a FIFO policy, we moreover have e + proc e proc . . . + proc e n and, therefore, e = e n . But this contradicts (e, e) ∈ [[w n ]] M . We conclude that M is prime.

"Prime" is a property of single topologies, while "unambiguous" refers to sets of topologies.

What we call topology is sometimes termed architecture. It seems that, however, in a parameterized setting, the term topology is more custom. Actually, our definition does not quite correspond to architectures from the literature, since processes are not connected by channels but interfaces. The latter are more appropriate in our setting, as they support the view that a process is specified independently of a concrete topology.

Gaifman's normal form appears to be more difficult to deal with in our context.

The synthesized PCA can still be run on any other topology (over the same set of names). However, it is sufficient to know that it is equivalent to the formula when we run it on a grid (respectively, topology from T).

In a neighborhood, we only keep the process types, not the processes.

Acknowledgment: The author thanks Dietrich Kuske for stimulating discussions, and Nicolas Baudru for the pointer to [7].

all verification obligations imposed by the guessed topology U. Then, F is defined as t ∈ S\G ¬ #(t) ≥ 1 .

Send Transitions (ST):

The triple (t -, ! m a, t) ∈ S × Σ A × S is contained in the transition relation ∆ if m = t, there is b ∈ N such that t ab = ∅ and (a, b) is enabled in t, and there is a bijection Φ : t -→ t such that Φ(U -, γ -, α -, s -, H -) = (U, γ, α, s, H) implies 1) (U -, γ -, α -) = (U, γ, α), i.e., the executing process maintains its guesses, 2) (s -, ! s a, s) ∈ ∆ (U ,γ) , which simulates a step of process α in the CA B (U ,γ) , 3) α has an a-successor in U or dist U (γ, α) = R, and 4) H = H -∪ {a}, which marks interface a as "checked".

Receive Transitions (RT):

The triple (t -, ? m b, t) ∈ S × Σ A × S is contained in ∆ if there is a ∈ N such that ab t = ∅, (b, a) is enabled in t, and there are bijections Φ : t -→ t and Φ : m ab → ab t as well as a mapping µ : ab t → θ∈R-Sub(T) S θ (associating with a tuple a message of a CA) satisfying the following:

(a) Φ(U -, γ -, α -, s -, H -) = (U, γ, α, s, H) =: κ implies 1. (U -, γ -, α -) = (U, γ, α), 2. (s -, ? k b, s) ∈ ∆ (U ,γ) for some k such that, if κ ∈ ab t, then k = µ(κ), 3. α has a b-successor in U or dist U (γ, α) = R, and 4.

, the guessed sphere is forwarded, and 3. α -::: a b α (assuming U = (Q, :: , ξ)). (c) For all (U, γ, α, s, H) ∈ (m \ m ab ) ∪ (t \ ab t), we have dist U (γ, α) = R.

Note that the mappings required in (ST) and (RT) are unique, if they exist.

This concludes the construction of the PCA A. It remains to show its correctness in the sense of the following lemma: Lemma 3. For all topologies T ∈ T and all B-bounded MSCs M over T , we have

The rest of the section is devoted to the proof of Lemma 3. So, suppose T = (P, ) ∈ T and let M = (E, , ) be a B-bounded MSC over T . For a process p ∈ P , we let M p = (Ev p , p , p , λ p ) = R-Sph(M, p), and we let τ p = ((Q p , :: p , ξ p ), p) denote R-Sph(T , p) M . Note that, since M is B-bounded, M p is B-bounded, too. Finally, let B p = (S p , ∆ p , ι p , F p ) := B τp , which is a CA over τ p . "⇒": Suppose M |= ∀yχ(y). By Theorem 10, we have M p ∈ L(B p ), for all p ∈ P . Thus, for all p ∈ P , there is an accepting run ρ p : Ev p → S p of B p on M p . From the collection (ρ p ) p∈P , we define a mapping ρ : E → S by ρ(e) = {(τ p , (e), ρ p (e), H e ) | p ∈ P with e ∈ Ev p } [START_REF] Abdulla | Handling global conditions in parameterized system verification[END_REF] where H e = {a ∈ N | there is f ∈ E such that f * proc e and act M (f ) ∈ {!a, ?a}}. Towards an appropriate initial state of A for M , we let ζ = (ζ q ) q∈P M where ζ q = {(τ p , q, ι p (q), ∅) | p ∈ P such that q ∈ Q p } .

We show that ρ is an accepting run of A on M , which implies M ∈ L T (A).

Clearly, ζ p ∈ S, for all p ∈ P M . So, let us prove that ρ(e) ∈ S for all e ∈ E. Suppose κ = (U = (Q, :: , ξ), γ, α, s, H) ∈ ρ(e) and κ = (U = (Q , :: , ξ ), γ , α , s , H ) ∈ ρ(e). Case 2: If e is not proc -minimal, then there is e -such that e - proc e. We have

We set Φ e (τ p , (e -), ρ p (e -), H e -) = (τ p , (e), ρ p (e), H e ).

Note that |ρ

So, Φ e is well-defined and indeed a bijection. It remains to verify that Φ e has the desired properties. We consider only Case 2. So, suppose e - proc e and Φ e (τ p , (e -), ρ p (e -), H e -) = (τ p , (e), ρ p (e), H e ). We show (ST).

1) We have (τ p , (e -)) = (τ p , (e)).

2) As ρ p is a run, (ρ p (e -), ! ρp(e) a, ρ p (e)) ∈ ∆ p .

3) We have e ∈ Ev p . By the definition of M p = R-Sph(M, p), we have that (e) has an a-successor in τ p , or dist τp (p, (e)) = R. 4) Clearly, H e = H e -∪ {a}. We define the bijection Φ f : ρ - ζ (f ) → ρ(f ) and verify (RTa) accordingly. It remains to define a bijection Φ(e,f) : ρ(e) ab → ab ρ(f ) as well as a mapping µ : ab ρ(f ) → p∈P S p .

We have ρ(e) ab = {(τ p , (e), ρ p (e), H e ) | p ∈ P such that e ∈ Ev p and (e) ::: a b p q for some q ∈ Q p } , ab ρ(f ) = {(τ p , (f ), ρ p (f ), H f ) | p ∈ P such that f ∈ Ev p and q ::: a b p (f ) for some q ∈ Q p } . Note that ρ(e) ab and ab ρ(f ) are both nonempty. For p ∈ P with e ∈ Ev p and (e) ::: a b p q for some q ∈ Q p , we have f ∈ Ev p . This follows from the definition of M p . We set Φ(e,f) (τ p , (e), ρ p (e), H e ) = (τ p , (f ), ρ p (f ), H f ). Note that Φ(e,f) is bijective. Similarly, for p ∈ P with f ∈ Ev p and q ::: a b p (f ) for some q ∈ Q p , we have e ∈ Ev p . In that case, we set µ(τ p , (f ), ρ p (f ), H f ) = ρ p (e). With this definition, (RTb) is directly verified. In (RTc), we have to show that, for all (U, γ, α, s, H) ∈ (ρ(e) \ ρ(e) ab ) ∪ (ρ(f ) \ ab ρ(f )), we have dist U (γ, α) = R. So, consider (τ p , (e), ρ p (e), H e ) with p ∈ P such that e ∈ Ev p and (e) does not have an asuccessor in τ p . Since, then, e is an unmatched event of M p , we have dist τp (p, (e)) = R by the definition of MSC M p . The reasoning for (U, γ, α, s, H) ∈ ρ(f )\ ab ρ(f ) is analogous.

It remains to show that ρ is accepting. Let G be the set of states t ∈ S such that, for all (U = (Q, :: , ξ), γ, α, s, H) ∈ t, we have s ∈ F (U ,γ) (α) and {a ∈ N | α ::: a b q for some b ∈ N and q ∈ Q} ⊆ H. We have to show that, for all e ∈ E that are proc -maximal, we have ρ(e) ∈ G.

So, let e ∈ E be proc -maximal. Suppose p ∈ P such that e ∈ Ev p . We have to show that ρ p (e) ∈ F p ( (e)) and {a ∈ N | (e) ::: a b p q for some b ∈ N and q ∈ Q p } ⊆ H e , i.e., for all a ∈ N such that (e) has an outgoing a-edge in τ p , there is f * proc e such that act M (f ) ∈ {!a, ?a}. The former holds since ρ p is an accepting run. The latter holds since, by definition, the MSC M p "covers" the a-labeled edge. ===⇒ ρ(f ).

We will show M ∈ L T (∀yχ(y)). By Theorem 10, it is sufficient to prove M p0 ∈ L(B p0 ) for all p 0 ∈ P M , i.e., to determine accepting runs ρ p0 : Ev p0 → S p0 of B p0 on M p0 . Let e, f ∈ E such that (e, f ) ∈ msg . Suppose a, b ∈ N such that (e) a b (f ). According to (ST) and (RT), consider the unique mappings Pick p 0 ∈ P M . For all events e ∈ E of M located on p 0 , the state ρ(e) contains exactly one tuple of the form (U, γ, γ, s, H) (where sphere center and active node coincide). Set κ e = (U, γ, γ, s, H) and ρ p0 (e) = s. Note that, by (ST) and (RT), θ p0 := (U, γ) is invariant along all events on p 0 .

We claim

Recall that, hereby, τ p0 = R-Sph(T , p 0 ) M p0 . In particular, (2) implies that ρ p0 (e) ∈ S p0 for all events e on p 0 . Before we prove (2), we define ρ p0 for all other events of M p0 . In doing so, whenever ρ p0 is defined on e (so that κ e has also been determined), it will be defined for the direct process predecessor e -and process successor e + (if they exist), using the bijections Φ e and Φ e + . The tuples κ e -and κ e + are defined accordingly.

So suppose that we defined ρ p0 for all events of M p0 that are located on processes p with 0 ≤ dist τp 0 (p 0 , p) ≤ k < R. Consider an event f ∈ Ev p0 that is located on some p with dist τp 0 (p 0 , p) = k + 1. There is e ∈ Ev p0 located on a node with distance k to p 0 (i.e., ρ p0 (e) is already defined) such that e and f form a message.

• Suppose that we have (e, f ) ∈ msg where (e) a b (f ), i.e., e sends a message via interface a. Assume that κ e = (U = (Q, :: , ξ), γ, α, s, H) (by induction, this will mean ρ p0 (e) = s). Due to (2), we have κ e ∈ ρ p0 (e) ab . By, (RTb), there is α ∈ Q such that α ::: a b α and Φ(e,f) (κ e ) = (U, γ, α , s , H ) for some s , H . We set ρ p0 (f ) = s . • Suppose that we have (f, e) ∈ msg where (f ) a b (e), i.e., e receives via interface b. Assume that κ e = (U = (Q, :: , ξ), γ, α, s, H), i.e., ρ p0 (e) = s. Due to (2), we have κ e ∈ ab ρ p0 (e). Again, due to (RTb), there is α ∈ Q such that α ::: a b α, and we have Φ-1 (f,e) (κ e ) = (U, γ, α , s , H ) for some s , H . We set ρ p0 (f ) = s .

Note that ρ p0 is well defined. So let us show that ρ p0 is a run of B p0 on M p0 . Pick e ∈ Ev p0 .

• Suppose e is of type !a. We have ρ -

ζ (e)

===⇒ ρ(e). Assume first that e is process-minimal on some process p. Suppose κ e = (U, γ, α, s, H). Recall that ρ p0 (e) = s. Thanks to (ST), ρ - ζ (e) contains (U, γ, α, s -, ∅), with s -= ι p0 (p) and (s -, ! s a, s) ∈ ∆ p0 . Moreover, H = {!a}. If e is not process-minimal, then e has a process-predecessor e -. By (ST), κ e -is of the form (U, γ, α, ρ p0 (e -), H -), for some H -, and we have (ρ p0 (e -), ! s a, s) ∈ ∆ p0 and H = H -∪ {!a}.

• Suppose e executes action ?b and let e -, f ∈ Ev p0 and a ∈ N be such that e - proc e, f msg e, and (f ) a b (e). Suppose κ e = (U = (Q, :: , ξ), γ, α, s, H), κ e -= (U -, γ -, α -, s -, H -), and κ f = (U , γ , α , s , H ). By (RT), (U -, γ -, α -) = (U, γ, α), (U , γ ) = (U, γ), and α ::: a b α. Finally, (s -, ? s b, s) ∈ ∆ p0 . The cases where e does not have a process-predecessor or where e is unmatched are similar. and all MSCs M = (E, , ) over T :

• M ∈ L T (A), and • for all accepting runs ρ of A on M and all events e ∈ E, we have ν(ρ(e)) ∼ = r-Sph(M, e).

We define the PCA A = (S, Msg, ∆, I, F ) with S = Msg as follows:

States: A state t ∈ S is either ∅ ω for some ω ∈ 2 N \ {∅} (the empty set with some annotated type; we set type(∅ ω ) = ω and let ν(t) be an arbitrary sphere), or a nonempty set of tuples (M, γ, α, col ) where (M = (E, , π, λ), γ) ∈ S r , α ∈ E is the active event, and col ∈ {1, . . . , 4 • maxE 2 + 1} is a color with maxE the maximal number of events of an r-sphere from S r . The coloring is needed to distinguish isomorphic overlapping spheres. For nonempty t, we require that the following hold:

• there is a unique tuple (M, γ, α, col ) ∈ t such that γ = α (in that case, we set ν(t) = (M, γ)),

• for all tuples ((E, , π, λ), γ, α, col ) ∈ t and ((E , , π , λ ), γ , α , col ) ∈ t, we have π(α) = π (α ) and λ(α) = λ (α ) (we set type(t) = π(α) and label (t) = λ(α)), and

Initial and Final States: For all ω ∈ 2 N \{∅}, we let I(ω) = {∅ ω }. Let G be the set of nonempty states t ∈ S such that there is (M, γ, α, col ) ∈ t with α not proc -maximal in M.

We set

Send Transitions: In the following, we let M refer to (E, , π, λ). The triple (t -, ! m a, t) ∈ S ×Σ A ×S is contained in ∆ if the following hold:

(1) m = t and label (t) = !a, (2) type(t -) = type(t),

for all (M, γ, α, col ) ∈ t and e ∈ E, we have e proc α iff (M, γ, e, col ) ∈ t -, (4) for all (M, γ, α, col ) ∈ t -and e ∈ E, we have α proc e iff (M, γ, e, col ) ∈ t, (5) for all (M, γ, α, col ) ∈ t, if α is proc -minimal in M and t -= ∅, then dist σ M (γ, α) = r, and (6) for all (M, γ, α, col 2)-( 6) as above as well as the following hold: (7) label (t) = ?a, (8) for all (M, γ, α, col ) ∈ t and e ∈ E, we have e msg α iff (M, γ, e, col ) ∈ m, (9) for all (M, γ, α, col ) ∈ m and e ∈ E, we have α msg e iff (M, γ, e, col ) ∈ t.

This concludes the construction of A. The correctness proof in the sense of Lemma 6 follows the same lines as that of [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF].

To show that cycles in spheres are correctly simulated by a given input MSC M , we use the fact that M is prime. Let T = (P, ) ∈ T N be a prime topology, M = (E, , ) be an MSC over T (i.e., according to Lemma 5, M is prime), and ρ be an accepting run of A on M . Let e 0 ∈ E and w ∈ D * , and consider ν(ρ(e 0 )) = (M = (E , , π , λ ), γ). We show that, then, (γ, γ) ∈ [[w]] M (with the obvious meaning) implies (e 0 , e 0 ) ∈ [[w]] M .

So, suppose (γ, γ) ∈ [[w]] M . By the construction of A, we have that, for all n ≥ 1, there is e n ∈ E such that (e 0 , e n ) ∈ [[w n ]] M (cf. proof of [START_REF] Bollig | Message-passing automata are expressively equivalent to EMSO logic[END_REF]Claim 4.11]). In particular, (e n , e n+1 ) ∈ [[w]] M for all n ∈ N. Towards a contradiction, assume e 1 = e 0 . Note that this implies w = ε. As M is prime, we have e 2 = e 0 . But we also have e 2 = e 1 : otherwise, there would be events f 1 , f 2 , f ∈ E and δ ∈ D such that f 1 = f 2 , (f 1 , f ) ∈ [[δ]] M , and (f 2 , f ) ∈ [[δ]] M , which is a contradiction, as f can have at most one δ-predecessor. Continuing this scheme, we get e n ∈ {e 0 , . . . , e n-1 } for all n ≥ 1. But this is a contradiction to the fact that E is finite. We deduce (e 0 , e 0 ) ∈ [[w]] M .