Marie Fortin
email: mfortin@ens-cachan.fr

LSV Paul Gastin
email: gastin@lsv.ens-cachan.fr

Verification of parameterized communicating automata via split-width

Keywords: Parameterized distributed systems, Model checking, Split-width, Message sequence charts

published or not. The documents may come

Verification of parameterized communicating automata via split-width

Introduction

We study verification problems for parameterized communicating automata (PCAs), which model distributed systems consisting of arbitrarily many identical processes, distributed on some communication topology. Each process runs a copy of the same finite automaton, that can send and receive messages from other processes through FIFO channels. Though the system may contain unboundedly many processes, we assume that each process may only communicate with a bounded number of other processes.

PCAs were introduced in [START_REF] Bollig | Logic for communicating automata with parameterized topology[END_REF] to study logical characterizations of parameterized systems. They extend communicating finite-state machines [START_REF] Brand | On communicating finite-state machines[END_REF]. While the latter assume a fixed and known communication topology, a PCA can be run on any communication topology of bounded degree. Communicating finite-state machines are already Turing equivalent, and thus their verification is undecidable. The fact that PCAs can be run on arbitrarily large topologies induces other sources of undecidability. For instance, a Turing machine can be simulated on grid topologies by a PCA performing a bounded number of actions on each process. Thus, some restrictions on the topologies are necessary. Yet, even when fixing a simple class of topologies such as pipelines, and imposing rendez-vous synchronization, reachability of PCAs is undecidable [START_REF] Bollig | Parameterized communicating automata: Complementation and model checking[END_REF].

In order to regain decidability, we focus on under-approximate verification. The idea is to restrict the verification problems to meaningful classes C of behaviors. Typically, we are interested in the following problem: given a PCA S, is there a topology T and a behavior in C over T on which S reaches some local/global state? Our aim is to study under-approximation classes C for which verification problems of PCAs becomes decidable. Even when we cannot cover all behaviors of a system with a decidable class, under-approximate verification is still very useful to detect bugs. Usually, the classes C i are parameterized and cover more and more behaviors when the parameter i increases.

The behaviors of PCAs are described by message sequence charts (MSC) [START_REF]Formal Semantics of Message Sequence Charts[END_REF], that is, graphs describing the communications between the different processes. Each node of the graph corresponds to an action performed by some process (sending or receiving a message), and the dependencies between the different actions are indicated by the edges of the graph. For model-checking, the specifications of our systems are typically given as monadic second order logic (MSO) or propositional dynamic logic (PDL) formulas over MSCs.

It is known that for any MSO definable class of bounded degree graphs, having a decidable MSO theory is equivalent to having bounded tree-width [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF]. This applies to classes of MSCs, and characterizes decidability of MSO modelchecking. However, showing a bound on tree-width is in general difficult. In the case of MSCs over a fixed architecture, an alternative notion called split-width has been introduced [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF][START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF]. Split-width is equivalent to tree-width on MSCs, but easier to use. It provides means to define uniform decision procedures, applying to many well-studied restrictions of communicating finite-state machines [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF].

Following this approach, we generalize the definition of split-width, and we extend existing results over fixed architectures to the parameterized case. The idea of split-width is to decompose an MSC into atomic pieces, that is, pairs of matching send and receive events. This is done using two operations: splitting some edges between consecutive events of a same process, and dividing the resulting graph into disjoint components. Intuitively, an MSC has bounded splitwidth when this can be done while splitting a bounded number of edges at each step, on a bounded number of processes.

We show that emptiness and reachability of PCAs restricted to MSCs of bounded split-width are decidable. These problems are Exptime-complete but only polynomial in the size of the PCA. Our decision procedures are based on an interpretation of MSCs of bounded split-width into binary trees, and reductions to tree automata verification problems.

In the extended version [?] we also prove that model-checking restricted to bounded split-width is decidable. For MSO specifications, it has non-elementary complexity. However, the under-approximate model-checking is respectively Exptime-complete and 2-Exptime complete for CPDL (PDL with converse) and ICPDL (PDL with converse and intersection). In all cases, the problem is still polynomial in the size of the PCA.

Topologies. We model distributed systems consisting of an unbounded number of processes. Each process is equipped with a bounded number of interfaces, through which it can communicate with other processes. A topology is a graph, describing the connections between the different processes (each of which is represented by a node in the graph, see example on the right). Throughout the paper, we assume a fixed nonempty finite set N = {a, b, . . .} of interface names (or, simply, interfaces). 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 means that the a-interface of p is connected the b-interface of q. We require that, whenever p a b q, the following hold:

(a) p = q (there are no self loops), (b) q b a p (adjacent processes are mutually connected), and (c) for all a , b ∈ N and q ∈ P such that p a b q , we have a = a iff q = q (an interface is connected to at most one process, and two distinct interfaces are connected to distinct processes).

Message sequence charts. The possible behaviors of our systems are depicted as message sequence charts. A message sequence chart consists of a set of processes, and, for each process, of a sequence of events. Each event corresponds to an action of the process (sending or receiving a message through a given interface), and matching send and receive events are connected by a message edge. Events are labeled with elements of Σ def = {a? | a ∈ N } ∪ {a! | a ∈ N }, according to the type of action they execute. Definition 2. A pre-message sequence chart (pre-MSC) over the set of interfaces N is a tuple M = (P, E, →, , π, λ), where -P and E are nonempty finite sets of processes and events, respectively. π : E → P is a surjective map determining the location of an event. For p ∈ P , we let

E p def = {e ∈ E | π(e) = p}.
λ : E → Σ associates with each event the type of action that it executes. We let

E ? def = {e ∈ E | ∃a ∈ N .λ(e) = a?}, and E ! def = {e ∈ E | ∃a ∈ N .λ(e) = a!}. -→ 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 . - ⊆ E ! ×E ? defines a bijection from E ! to E ? . Moreover, for each (e, f ) ∈ , π(e) = π(f ).
Given such a pre-MSC, we define

T M def = (P, {(p, a, b, q) ∈ P × N 2 × P | ∃(e, f ) ∈ E p ×E q . (e f ∧λ(e) = a!∧λ(f ) = b?) or (f e∧λ(e) = a?∧λ(f ) = b!)}).
Not all pre-MSCs correspond to actual behaviors of systems. To define MSCs, we additionally require that the events are coherently ordered, and that communications are compatible with some topology and follow a FIFO policy. -T M as defined above is a topology, called the observable topology of M .

-For all e 1 e 2 ,

f 1 f 2 s.t. π(e i ) = π(f i ), we have e 1 ≤ f 1 iff e 2 ≤ f 2 (FIFO).
An MSC M is called compatible with a topology T when T M is a subgraph of T . Intuitively, an MSC is compatible with a topology T when it can be interpreted as a behavior over T , in which some processes may be inactive or may not use all their interfaces. We denote by MSC the set of all MSCs over N , and by MSC T the set of all MSCs compatible with a topology T . Example 4. An example MSC is depicted in Figure 1. The vertical lines represent the succession of events on a given process, and -edges are depicted by arrows.

Parameterized communicating automata. The idea is that each process of a topology runs one and the same automaton, whose transitions are labeled with actions of the form a!m, which emits a message m through interface a, or a?m, which receives m from interface a. The acceptance condition of a parameterized communicating automaton is given as a boolean combination of conditions of the form "at least n processes end in state s", written #(s) ≥ n . Definition 5. A parameterized communicating automaton (PCA) over N is a tuple S = (S, ι, Msg, ∆, F ) where S is the finite set of states, ι ∈ S is the initial state, Msg is a nonempty finite set of messages, ∆ ⊆ S × (Σ × Msg) × S is the transition relation, and F is the acceptance condition, a finite boolean combination of statements of the form #(s) ≥ n , with s ∈ S and n ∈ N.

The size |F | of the acceptance condition of S is defined as the length of its encoding, where all integer values are written in binary.

Let M = (P, E, →, , π, λ) be an MSC. A run of S on M will be a mapping ρ : E → S satisfying some requirements. Intuitively, ρ(e) is the local state of π(e) after executing e. To determine when ρ is a run, we define another mapping, ρ -: E → S, denoting the source state of a transition: whenever f → e, we let ρ -(e) = ρ(f ); moreover, if e is →-minimal, we let ρ -(e) = ι. With this, we say that ρ is a run of S on M if, for all (e, f ) ∈ , there is a message m ∈ Msg such that (ρ -(e), (λ(e), m), ρ(e)) ∈ ∆, and (ρ -(f ), (λ(f ), m), ρ(f )) ∈ ∆. A run Fig. 3. Undecidability with pipelines and rendez-vous synchronization Fig. 4. Undecidability with a bounded number of actions on each process, using grid topologies ρ is accepting if it satisfies the acceptance condition. In particular, ρ satisfies #(s) ≥ n when |{e ∈ E | e is →-maximal and ρ(e) = s}| ≥ n.

The set of MSCs that allow for an accepting run is denoted by L(S). Given a topology T , we let L T (S) = L(S) ∩ MSC T . Remark 6. We could add labels from a finite alphabet to the events of MSCs and to the transitions of PCAs. Such labels can be handled similarly to the λ-labeling, and all our results can easily be adapted to this setting. Similarly, allowing internal transitions for PCAs would not add any technical difficulties.

Verification problems. The non-emptiness problem asks, given a PCA S, whether its language L(S) is non empty; or in other words, whether L T (S) = ∅ for some topology T . The (local) reachability problem asks, given a PCA S and a state s of S, whether there exists a run of S in which some process reaches the state s. It can be seen as a special instance of the non-emptiness problem, by modifying the acceptance condition of S to #(s) ≥ 1 .

Notice that the non-emptiness problem L T (S) = ∅ for a fixed topology T is already undecidable, since two finite automata connected by two queues can easily simulate a Turing machine. Furthermore, many decidable restrictions over fixed topologies remain undecidable in the parameterized case: for instance, bounding the number of contexts, or even of actions, performed by each process, or imposing rendez-vous synchronization (even when restricted to pipeline topologies [START_REF] Bollig | Parameterized communicating automata: Complementation and model checking[END_REF]). The idea is that the unbounded number of processes can be used to construct a PCA whose behaviors are grid-like MSCs of arbitrary height and width (see Figures 3 and4). It is then easy to encode runs of a Turing machine: the unbounded horizontal direction encodes the tape of the machine, and the vertical direction its evolution with time.

In the remaining of the paper, we will study several decidable underapproximations of the problem. For a family (C i ) i of classes of MSCs (for the concrete families studied in Section 4, the index i is a tuple of integers), we define the problem C-NonEmptiness as follows (and similarly, C-Reachability):

Input: i in unary, a set of interfaces N , a PCA S over N . Question: L(S) ∩ C i = ∅ ? M a! b? b! a? a! b? b! a? a! b? a! b? M a! b? b! a? a! b? b! a? a! b? a! b? M 1 a! b? b! a? a! b? b! a? M 1 a! b? b! a? a! b? b! a? M 3 a! b? b! a? M 3 a! b? b! a? M 4 a! b? b! a? M 5 . . . a! b? a! b? M 2 a! b? a! b? M 2 a! b? a! b? M 7
Fig. 5. A split decomposition of width 4

(n) -split (ε) (n ) -div (B BrB ) (n1) -split (ε, B1B1) (n 1 )
-div (B Br, B Br)

(n3) -split (B2, B2) (n 3 ) -div (B Br, BrB ) (n4) (B!, B?) a! b? (e) (n5) (B?, B!) a! b? . . . -split (n2) (B1, ε) -div (n 2 ) (B , B Br) (n6) (B!, B?) (f ) a! b? (n7) (B!)
a! b? Fig. 6. 4-DST associated with the decomposition of Figure 5 3 Split-width

In this section, we introduce the notion of split-width, and state our decidability result for MSCs of bounded split-width. The main motivation behind split-width is that it allows to design generic decision procedures that apply to many underapproximation classes, instead of having to develop for each class a specific decision procedure with its complexity. Several examples of classes of MSCs that are captured with split-width will be given in Section 4.

The idea of split-width is to decompose an MSC into atomic pieces consisting of a pair of matching send and receive events, using two operations: split (removing some process edges of the MSC), and divide (separating the resulting graph into two independent parts). This is described below as a two-player game. First, we introduce the notion of split MSC (an MSC missing some of its process edges). The edges are called elastic, and the → edges rigid. Processes of P \O are called closed. The intuition is that an open process of M is a process that may be missing some of its events or process edges, and an elastic edge represents a missing part of a process between two events. Any MSC can be seen as a split MSC, by taking O and empty. A block of a split (pre-)MSC M is a maximal connected component of (E, →) on some open process. In particular, M has exactly |O| + | | blocks.

Several split MSCs are depicted in Figure 5. Elastic edges are represented by red dotted lines. Open processes are indicated by dotted lines at their extremities. For instance, M has one open process with 3 blocks, and M 2 has 2 open processes, with resp. 1 and 2 blocks.

We call splitting an edge of M the action of making elastic some rigid edge e → f of M . The resulting split MSC is M = (P, O∪{π(e)}, E, →\{(e, f )}, ∪ {(e, f )}, , π, λ). For instance in Figure 5, M is obtained by splitting two process edges of M .

We say that M can be divided into

M 1 = (P 1 , O 1 , E 1 , → 1 , 1 , π 1 , λ 1 ) and M 2 = (P 2 , O 2 , E 2 , → 2 ,
2 , π 2 , λ 2 ) when M 1 and M 2 are split (pre)-MSCs, and

E = E 1 E 2 , → = → 1 → 2 , = 1 2 , π = π 1 π 2 , λ = λ 1 λ 2 , and for i ∈ {1, 2}, O i = O ∩ P i and i ⊆ (→ ∪ ) + . For instance, in Figure 5, M can be divided into M 1 and M 2 . A connected component of M is a split MSC M 1 = (P 1 , O 1 , E 1 , → 1 , 1 , π 1 , λ 1 )
such that E 1 is a connected component of (E, → ∪ ). Then, either M = M 1 or M can be divided into M 1 and some M 2 .

Split-game. Let M be a split MSC with at most k blocks. A split-game with budget k on M is a two player game in which the existential player (Eve) tries to prove that M has split-width at most k, while the universal player (Adam) tries to disprove it. Eve begins by trying to disconnect M by splitting some of its process edges, with the condition that the resulting split MSC M has at most k blocks. Adam then chooses a connected component M of M , and the game resumes on M . Eve wins a play if it ends in an atomic MSC, i.e. a pair of matching send and receive events. She loses if she cannot disconnect a non-atomic MSC without introducing more than k blocks.

The split-width of an MSC M is the minimal k such that Eve wins the splitgame with budget k on M . It is defined identically for pre-MSCs. We denote by SW k the set of MSCs of split-width at most k.

Example 8. Eve wins the split-game with budget 4 on M (see Figure 5). She starts by splitting two process edges of M , which results in the split MSC M with three blocks. M has two connected components, M 1 and M 2 , providing two choices for Adam. If he chooses M 2 , Eve wins by cutting the only remaining process edge: both connected components of the resulting M 2 are atomic. If he chooses M 1 , Eve split the middle process edge on the first process, which creates two more blocks, and results in a total of four blocks. M 1 has two isomorphic connected components, so Adam's choices are all equivalent. Eve can then cut the two remaining process edges while still respecting her budget of four blocks.

Shuffle and merge. One can also give a bottom-up description of split-width. The duals of the split and divide operations are called respectively merge ( ) and shuffle ( ). (M ) is the set of split MSCs that can be obtained by making some elastic edges of M rigid, and/or closing some of its open processes. M 1 M 2 is the set of split MSCs M such that M can be divided into M 1 and M 2 .

An MSC has split-width at most k when it can be obtain by combining atomic MSCs with shuffle and merge operations, while keeping the number of blocks at most k at each step.

Remark 9.

The notion of open and closed processes is new. Our bound on the number of blocks (i.e. the number of open processes plus the number of elastic edges) replaces the bound on the number of elastic edges only that was used in [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF][START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF] for the split-width of MSCs over fixed architectures. When the topology T is fixed, the two definitions are equivalent since the number of open processes is already bounded by the number of processes in T . This is no longer true in the parameterized case. For instance, the families of MSCs defined in Figures 3 and4 can be decomposed into atomic pieces while using only two elastic edges, but this introduces an unbounded number of open processes. In fact, they embed a grid, hence they should have unbounded width.

Remark 10. For MSCs, split-width is equivalent to tree-width and clique-width: there are linear bounds between the three measures (the proof is an easy adaptation from the non-parameterized case [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF]). The motivation for introducing split-width rather than using existing measures on graphs is that it allows to take into account the specificities of MSCs, and is thus both simpler to understand and to use. In particular, using tree-width or clique-width would result in more involved automata constructions in Section 5.

Notice also that a bound on the split-width of an MSC M induces a bound on the tree-width of the observable topology T M (See Theorem 20).

Decidability. The non-emptiness problem becomes decidable when restricted to MSCs of bounded split-width. Roughly, the proof goes as follows. First, we show that trees representing Eve's winning strategies can be abstracted by trees over a finite alphabet (that depends only on the bound k on split-width). Then, we reduce the verification problems for PCAs to emptiness problems on tree automata. The details for these constructions will be given in Section 5, and the complexity lower bounds are proven in Appendix G. The proof is inspired from the non-parameterized case [START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF], and we show that the complexity remains the same in our setting.

Theorem 11. SW-NonEmptiness is Exptime-complete, and only polynomial in the number of states and transitions of the input PCA.

Classes of bounded split-width

The decision procedures based on split-width are generic and apply to various classes of MSCs (the main condition being that MSCs in the class have bounded split-width). When the topology is fixed, this covers many well-studied restrictions [START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF]. In this section, we give two examples of such classes that can be generalized to the parameterized setting: existentially bounded MSCs, and contextbounded MSCs. We also define a further extension of context-bounded MSCs, called tile-bounded MSCs, and show that it is equivalent to bounded split-width. Existentially bounded MSCs. M is called existentially k-bounded when there exists a linearization ≤ lin of its events (i.e. a total order extending ≤) such that there are at most k process or message edges going out of any prefix of the linearization: for all g ∈ E,

(e, f ) ∈ E 2 | (e f ∨ e → f ) ∧ e ≤ lin g < lin f ≤ k .
In the case of MSCs over a fixed topology, this is equivalent to bounding the number of pending messages at each prefix of the linearization, which is the usual definition of existentially bounded. This is no longer the case when considering topologies with an unbounded number of processes. For instance, the MSC of Figure 3 is not existentially k-bounded. It is possible to find a linearization for which every prefix has at most one pending message, but it is not possible to simultaneously bound the number of non-terminated processes.

We denote by EB k the set of all existentially k-bounded MSCs over N .

Lemma 12. An existentially k-bounded MSC has split-width at most k + 2.

Proof. Eve's strategy is as follows. She successively isolates the first events of the linearization by splitting the process edges originating from them, until a pair of matching send/receive events is disconnected. Adam chooses the remaining component, and Eve continues as before. In the split MSC obtained by isolating the first events e 1 < lin . . . < lin e i of the linearization and removing the disconnected messages, each block either consists of a single e j (1 ≤ j ≤ i), or only contains events that occur after e i in the linearization, and is the last block on some open process. Blocks of the first kind are necessarily send events whose matching receive event occurs after e i , hence they correspond to pending messages at e i . Now consider a block of the second kind, and let f be its first event. Then f must occur after e i in the linearization (otherwise, its block would be of the first kind). Moreover, since its process is open, there must be some e ∈ {e 1 , . . . , e i } such that e → f in the initial MSC. Hence, each block of the second kind correspond to a pending process edge at e i (the edge e → f ). Thus, there are in total at most k blocks. Eve introduces at most two extra blocks when splitting a process edge. Hence she wins with budget k + 2.

Eve's winning strategy results in a tree that is word-like [START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF][START_REF] Cyriac | Verification of Communicating Recursive Programs via Split-width[END_REF], i.e., at every binary node, one of the subtree is small (bounded size). Hence, we can use word automata instead of tree automata, resulting in a better complexity for the verification problems.

Theorem 13. EB-NonEmptiness is Pspace-complete.

Context-bounded MSCs. A context is an interval of events on a process, in which only one interface is accessed, and in a single direction (send or receive). More formally, let M = (P, E, →, , π, λ) be an MSC. A context of M is a subset c = {e 1 , . . . , e n } of E such that e 1 → • • • → e n and λ(e i ) = λ(e j ) for all i, j.

An MSC M is k-context bounded when for all p ∈ P , there are contexts c 1 , . . . , c i with i ≤ k such that E p = c 1 . . . c i . The class of k-context bounded MSCs has unbounded split-width. Actually, this is even the case for MSCs having a bounded number of events on every process (see Figure 4). However, we obtain a bound on split-width when we additionally require that the topology has bounded tree-width (cf. Appendix B). The proof is in Appendix D. Lemma 14. If M is a k-context-bounded MSC and T M has tree-width at most h, then M has split-width at most k(h + 1) + 2.

We denote by CB k,h the set of all k-context bounded MSCs over topologies of tree-width at most h. Theorem 15. CB-NonEmptiness is Exptime-complete, and polynomial in the number of states and transitions of the input PCA.

Tile-bounded MSCs. We can generalize the notion of contexts introduced above to tiles, which are independant parts of an MSC involving a bounded number of processes. In some sense, this section gives the link between fixed and parameterized topologies, when it comes to conditions ensuring decidability. Intuitively, an MSC with split-width at most k over an arbitrary topology (involving arbitrarily many processes) can be decomposed in tiles involving at most some fixed number (k) of processes. Moreover, each tile has bounded splitwidth and each process intersects at most some fixed number of tiles.

A k-tile is a split MSC T of split-width at most k and having only open processes. In particular, T has at most k blocks, hence at most k processes.

Let M = (P, E, →, , π, λ) be an MSC. A (k, )-tile-decomposition of M is a sequence T 1 , . . . , T n of k-tiles such that M ∈ (T 1 . . . T n ) and every process p ∈ P is part of at most tiles. An MSC is called (k, )-tile-bounded when it admits some (k, )-tile-decomposition.

Example 16. A (5, 3)-decomposition with three tiles is depicted on the right. The first and the last process intersect with one tile, the middle one with 3 tiles and the other two processes intersect with two tiles. Tiles T 1 and T 3 have split-width exactly 5 (note that the first process is counted as open in T 1 ). Tile T 2 tile has split-width 4.

T 1 T 2 T 3
Example 17. A k-context bounded MSC M (see page 11) admits a (2k+2, 2|N |)tile-decomposition. The tile decomposition is given by defining, for each pair of processes (p, q) connected in T M , a tile T p,q induced by the contexts of p in which it sends to q, and the contexts of q in which it receives from p. Notice that a tile needs not be a connected graph. In particular, each tile has at most 2k blocks, and can be decomposed by disconnecting one by one its messages, which introduces at most 2 extra blocks. Each process of M takes part in at most 2|N | tiles, one for each type (a!, a?, . . .) of contexts it has.

We obtain the same results as for context-bounded MSCs (cf. Appendix E.1). We denote by TB k, ,h the set of (k, )-tile-bounded MSCs M such that T M has tree-width at most h. Lemma 18. Let M ∈ TB k, ,h . Then M has split-width at most 2k 2 2 (h + 1).

Theorem 19. TB-NonEmptiness is Exptime-complete, and polynomial in the number of states and transitions of the input PCA.

In fact, such bounds are equivalent to bounding split-width, as shown by the theorem below (proof is in Appendix E.2).

Theorem 20. Let M ∈ SW k . Then T M has tree-width at most k -1, and M is (k 2 + 2k, 3|N | k )-tile-bounded.

Tree interpretation

We present the decision procedures leading to our complexity results. The general idea is to encode MSCs of bounded split-width into binary trees over a finite alphabet, and reduce our verification problems to problems on tree automata.

Split-terms. The encoding of MSCs of bounded split-width into trees is based on the bottom-up description of split-width. Recall that an MSC has split-width at most k if it can be constructed by combining through shuffles and merges split MSCs with at most k blocks, the starting points being atomic MSCs. This construction can be described by a split-term, that is, a term over the following grammar: s ::= a! b? | (s) | s s (with a, b ∈ N ). However, since the merge and shuffle operations are ambiguous, a split-term may correspond to several MSCs. The next step is to disambiguate these operations by adding labels to the nodes of split-terms, describing respectively how the blocks of the children are shuffled, or which blocks are merged and which processes are closed.

Compared to the non-parameterized case [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF][START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF], the difficulty is that the number of processes may grow arbitrarily along the DST, instead of being fixed from the beginning -and we still need to use labels from a bounded domain. Thus, the disambiguated labels will focus on open processes. The idea is to describe how many blocks each process has after the operation, and the origin of each block. A k-disambiguated split-term (k-DST) is a split-term in which each internal node is labeled by a tuple of words (w p ) 1≤p≤m such that m p=1 |w p | ≤ k, and -For a -node, the word w p ∈ {B , B r } + describes the composition of some open process, where B stands for a block coming from the left child, and B r stands for a block coming from the right child (see for instance the label of n in Figure 6 which describes the origin of the 3 blocks of the open process of M in Figure 5). -For a -node, the word Further examples and explanations are given in Appendix A. We denote by DST k the set of all k-DSTs. A k-DST is called valid when the label of each node is coherent with the number of processes and blocks appearing in the label of its child/children (see Appendix A for a formal definition). For instance, we cannot have w p = B 2 B 1 at a -node if its child does not have 3 blocks on process p.

w p ∈ {B i | 1 ≤ i ≤ k} * describes
A valid k-DST t can be associated with a unique split pre-MSC (which is not necessarily a split MSC) M t = (P, O, E, →, , , π, λ), defined as follows. E is the set of leaves of t, and λ associates with a leaf e its label. We let e f whenever e and f are respectively the left and right children of a same -node.

To determine whether two leaves e and f are connected by a →-edge, we proceed as follows. We track the block associated with leaf e, until reaching a -node n in which it is merged with the block on its right (see example in green in Figure 6). Similarly, we track the block associated with leaf f , until reaching a -node n in which it is merged with the block on its left (in blue in Figure 6). We set e → f if n = n and the blocks coincide. Similarly, we let e f when no merge ever occurs on the right of the block of e or on the left of the block of f , and at the root, the block of f is located just after the block of e.

We identify processes with connected components of (E, → ∪ ). To determine whether the process of an event e is open or closed, we walk up the tree remembering the process of e, until reaching a -node in which it is closed, or the root (in which case it is open).

For example, in Figures 5 and6 the split pre-MSC associated with the k-DST starting in node n i (resp.

n i ) is M i (resp. M i ).
The next lemma states that the conditions for M t to be an MSC can be checked by a tree automaton (proof given in Appendix A). We denote by DST k msc the set of all valid k-DSTs t such that M t is an MSC. From PCAs to tree automata. Given a PCA, we can construct a tree automaton that accepts a tree t ∈ DST k msc iff M t is accepted by the PCA.

Lemma 22. Let S = (S, ι, Msg, ∆, F ) be a PCA, and k ∈ N. There is a bottomup tree automaton

A k S of size |S| O(k|F | 2 ) such that L(A k S ) ∩ DST k msc = {t ∈ DST k msc | M t ∈ L(S)}.
It can be constructed in space polynomial in k and |F |, and logarithmic in |S| and |∆|.

Proof. A k

S guesses a run of S on M t , and inductively checks that it is a valid accepting run. To do so, it remembers the states of S before and after each block in the split MSC associated with the current subtree, that is, a pair (ρ -, ρ + ) of partial functions from [k] to S. (The blocks are numbered according to their position in the concatenation w 1 w 2 . . . w m of the words in the label of the current node.) In addition, for each s ∈ S appearing in F , A k S remembers the number n s of closed processes that ends in state s, up to the maximal n such that #(s) ≥ n appears in F . A state is accepting if it satisfies F . At leaves, A k S remembers the type of action executed (in Σ), and at anode of the form a! b?, it guesses a message m and transitions p a!m --→ p and q b?m --→ q of S. The functions ρ -and ρ + of the -node are initialized accordingly. For instance, after reading a! (B ! ,B ? ) b? and guessing the transitions, A k S goes to the state where ρ -(1) = p, ρ + (1) = p , ρ -(2) = q, ρ + (2) = q and ρ -, ρ + are undefined elsewhere. After reading a! (B ? ) b?, A k S checks that p = ι and increments n p , and moves to state ρ -(1) = q, ρ + (1) = q .

The functions ρ -and ρ + are updated at each -and -node according to the renaming of the blocks. At a -node, A k S checks than whenever two blocks b and b + 1 are merged, ρ + (b) = ρ -(b + 1). It also checks that each process being closed starts in ι, and increments the counter n s of its end state s (unless it has already reached its maximal value).

We then have L(S) Classes of bounded split-with. The above decision procedure can be adapted for any class C of MSCs of split-width at most k, provided we can construct an automaton A C that accepts only encodings of MSCs in C, and at least one encoding for each M ∈ C. Under those assumptions, and given a PCA S, deciding whether L(S) ∩ C = ∅ e.g. reduces to deciding whether

∩ SW k = ∅ iff L(A k S ∩ A k msc ) = ∅,
L(A k S ∩ A k msc ∩ A C ) = ∅. C k = EB k C (k,h) = CB k,h C k = SW k C (k, ,h) = TB k, ,h C-Reachability Pspace-c Exptime-c C-NonEmptiness C-CPDL-Sat/MC C-ICPDL-Sat/MC Expspace-c 2-Exptime-c C-MSO-Sat/MC
Non-elementary This applies in particular to existentially bounded MSCs, and context-or tile-bounded MSCs over topologies of bounded tree-width. The construction of A C is in all three cases based on the proof that C has split-width at most k (cf. Appendix C, D and E, resp.).

Note that this would also apply for instance to any class of bounded splitwidth that is recognized by a PCA.

Further results

Model-checking. The results presented in Sections 3 and 5 can be generalized to model-checking problems (the details are in Appendix F). Our most general decidability result states that the model-checking of PCAs against Monadic Second-Order (MSO) formulas is decidable. The idea is to construct, for a given specification ϕ, a tree automaton A k ϕ that accepts a valid k-DST t iff M t satisfies ϕ. The bounded split-width model-checking problem then reduces to testing whether L(A k S ∩ A k ¬ϕ ∩ A k msc ) = ∅, and similarly for the other classes. However, when the specification ϕ is given by an MSO formula, the construction of A k ϕ is non-elementary. Towards a better complexity, we study model checking against PDL specifications. PDL is both expressive (it subsumes most if not all temporal logics), easy to use and understand, and enjoys a very good complexity. We show that model-checking against PDL formulas is Exptimecomplete, i.e., not harder than non-emptiness and reachability. It remains in Exptime when we extend PDL with converse (CPDL), and is 2-Exptime-complete for ICPDL (PDL with converse and intersection). A summary of our results is given in Figure 7. Multi-pushdown processes. Our model could be extended by adding one or several stacks to processes, similarly to what is done in the case of fixed architectures [START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF]. We could also allow several FIFO channels between any pair of processes. This means relaxing the definition of topologies to allow loops or multiple edges, and similarly adapt the definition of MSCs. The definition of split-width and k-DSTs is the same, except that at -nodes, the send and receive events may be placed on the same process. Our decision procedures remain correct, with an additional check by A k msc of the LIFO conditions on the stacks. The results on existentially-bounded MSCs, context-bounded MSCs, or tile decompositions are also still valid.

A Details on k-DSTs

Disambiguated split-terms. We give more detailed explanations on the labels of DSTs, that should be helpful in understanding the examples and the formalization of our constructions.

As explained in the main body of the paper, the idea is to describe how many blocks each process has after the operation, and the origin of each block. In this way, a -node is labeled by a tuple (w p ) 1≤p≤m , where m is the number of open processes after the shuffle, and each w p describes the composition of some open process. More precisely, w p is a word over {B , B r } * , where B stands for a block coming from the left child, and B r stands for a block coming from the right child. For instance, M in Figure 5 has only one open process, with 3 blocks, so the label of the associated node n in Figure 6 consists of a single word w of length 3. The first and last blocks come from M 1 (the left child), and the second block comes from M 2 (the right child), so w = B B r B . There is no ambiguity regarding which blocks of M 1 are respectively represented by the two occurrences of B , since the shuffle preserves by definition the order of the blocks on each process. To handle the case of nodes with several open processes, we add the convention that the order on the open processes (implied by the labels of the DST) is preserved by the shuffle. For instance, the label of n A -node is labeled by a tuple (w p ) 1≤p≤m , where m is the number of open processes before the merge. When an open process p is closed (and all its elastic edges made rigid if it still had some), we set w p = ε. For instance, the label of n indicates that all the elastic edges of M are made rigid in M , and that the corresponding open process of M is closed in M . Else, w p is a word over {B 1 , . . . , B k } * , where B i stands for a block resulting from the merge of i successive blocks (meaning that the i -1 elastic edges separating these blocks have been made rigid). For instance, the label (B 2 , B 2 ) of node n 3 indicates that on both processes of M 3 , the two blocks are merged in M 3 .

Finally, a -node is labeled by an element of {(), (B ! ), (B ? ), (B ! , B ? ), (B ? , B ! )}, where B ! (resp. B ? ) stands for a block consisting of the send (resp. receive) event (meaning in particular that its process is open). The label of the node indicates which processes of the associated split MSC are open, and how they are ordered. For instance, n 7 is labeled (B ! ), which means that in M 7 the process of the send event is open whereas the process of the receive event is closed. Both n 4 and n 5 are labeled by a pair of words, so their associated split MSC M 4 and M 5 are isomorphic. The only difference is that in the rest of t, the sending process of M 4 will always come before its receiving process, while it is the opposite for M 5 .

Valid k-DST. The type of a node n in a k-DST t consists of its number of open processes, together with the number of blocks on each open process. More precisely, if n has label (w p ) 1≤p≤m , type(n) is the list obtained by removing all occurrences of 0 in (|w p |) 1≤p≤m . For instance, node n 1 in Figure 5 has type (2), and node n 1 has type (2, 2). A k-DST is called valid when for all nodes n with label (w p ) 1≤p≤m , the following conditions hold:

-Assume n is a -node with child n . Then type(n ) is of the form (x p ) 1≤p≤m , and for all p such that w p = ε, writing w p = B i1 . . . B is , we have x p = s j=1 i j . -Assume n is a -node with left and right children n and n r . Let p 1 < . . . < p s be the indices p such that

|w p | B ≥ 1. Then type(n ) = (|w pi | B ) 1≤i≤s .
Similarly, for the right child.

The set of all valid k-DSTs is denoted by DST k valid . It can be recognized by a deterministic bottom-up tree automaton A k valid with k O(k) states: A k valid remembers the type of the last seen node, and checks the validity conditions and membership in DST k , i.e., that each node has at most k blocks.

The conditions for M t to be an MSC (instead of any pre-MSC) can also be checked by a tree automaton.

Lemma 21. One can construct in space polynomial in k and |N | a deterministic bottom-up tree automaton A k msc with 2 O(|N |k 4 ) states such that L(A k msc ) = DST k msc . Proof. A k msc is the intersection of A k valid with a tree automaton A msc that keeps in its state the known neighbors of each open process, that is, partial functions

neighbor a : [k] → [k] ∪ { * }.
The meaning of neighbor a (p) = q is that the ainterface of the p-th open process points to the q-th open process (the order on open processes refers to the label (w p ) 1≤p≤m ). We let neighbor a (p) = * when the a-interface of the p-th open process points to some closed process. neighbor a is undefined for all open processes p on which there is no event of type a! or a? yet. Also, A msc remembers the set of pairs of blocks that are connected by -edges, that is, a set ⊆ [k] 4 (the i-th block on the p-th open process being represented by the pair (p, i)). Then, A msc checks at each -node that:

-If two open processes p and p r of the left and right children are shuffled into some process p and both had a-neighbors, then their a-neighbors are open processes q and q r which are also shuffled in a same process q. -For all a = b, if a process p had an open a-neighbor q , and is shuffled with a process p r that had an open b-neighbor q r , then q and q r are mapped to different processes by the shuffle.

Moreover, states that violate the FIFO policy, that is, such that contains two pairs ((p, i), (q, j)) and ((p, i ), (q, j )) such that i < i and j < j, are disabled. Similarly, in order to check that in the resulting graph ≤ = ( ∪ →) * is a partial order, states such that the graph ([k] 2 , ∪ {(p, i), (p, i + 1)}) contains a cycle are disabled.

Remark 23. We could also want to reason about a specific class T of topologies among the classes of pipelines, rings, or trees, as in [START_REF] Bollig | Parameterized communicating automata: Complementation and model checking[END_REF][START_REF] Bollig | Parameterized Verification of Communicating Automata under Context Bounds[END_REF]. This can be done with slight modifications of A k msc , resulting in an automaton that recognizes exactly the set of valid k-DSTs t such that T Mt ∈ T.

C Details for existentially-bounded MSCs

Lemma 25. One can construct in space polynomial in k a deterministic automaton

A EB k with 2 O(k) states over (k + 2)-DSTs such that EB k = {M t | t ∈ L(A EB k ∩ A k+2 msc )}.
Proof. The construction of A EB k is based on the proof of Lemma 12. We describe A EB k as a top-down automaton. Thus, we interpret -node as splitting edges rather than merging blocks (or opening rather that closing processes), and -nodes as the removal of a single message edge (which is the case for Eve's strategy as described in the proof of Lemma 12).

Recall that in the proof of Lemma 12, events are detached one by one, according to the order given by the linearization. More precisely, we associate with any k-bounded linearization e 1 < lin • • • < lin e m of a split MSC M a (k + 2)-DST t such that M = M t , with m -nodes denoted x 1 , . . . , x m (x 1 being the root, and x m the -node of greatest depth). It is defined uniquely by the following conditions:

-If e i is the only event on its process, then x i opens its process.

-If e i is not →-maximal, then x i splits its outgoing process edge.

-If e i is →-maximal and is not the only event on its process, then x i does not do anything (i.e. w p ∈ (B 1 ) * for any word of its label).

-If e i is a receive event, then x i is immediately followed by a -node removing its associated message pair.

The idea is for A EB k to accepts all, and only, such DSTs. We associate with each node x i the prefix {e 1 , . . . , e i } of the linearization (and with any -node, the prefix of its parent -node).

In the top-down view, A EB k has a priori no information on the composition of the different blocks at each node. To handle this, it guesses at each -node whether the two blocks resulting from the split (or the block resulting from opening a process) consist of a single send event, a single receive event, or several events. Later, it checks that its guesses are correct: it verifies that a block guessed as a singleton is never split at a -node, and that the labels of -nodes are coherent with the guessed type (send or receive) of the singleton blocks.

In addition, A EB k also guesses a linearization as follows. At each -node, it checks that at most one block is split and at most one process is open. If some block is split, the left part is guessed to be a singleton and its event is added to the linearization. This singleton block is marked. If no edge is split but a process is opened, A EB k guesses that its block is a singleton, adds its event to the linearization and marks it. If no edge is split and no process is opened, A EB k chooses non-deterministically a singleton block which is not yet marked and which is the first block on its process. As before, it marks this block and adds its event to the linearization.

A run of A EB k on a DST t thus defines an enumeration of the events of M t . To ensure that it is a linearization, A EB k checks that at each -node, both events being removed are marked, and that at each -node, if the event added to the linearization is a receive, then the next node is a -node removing its associated message pair.

To ensure that the linearization e 1 < lin • • • < lin e m associated with a run of A EB k is k-bounded, it is sufficient to prove that for all send events e i we have |{(j, j ) | (e j e j ∨e j → e j )∧j ≤ i < j }| ≤ k. Indeed, when e i is a receive event, adding e i to the prefix adds at most one pending process edge, and removes one pending message. Hence the number of pending edges never increases at receive events.

Let {e 1 , . . . , e i } be some prefix of the linearization, such that e i is a send event. Let x i be the -node at which e i is added to the linearization, and M i its associated MSC. For all 1 ≤ j ≤ i, event e j is either a singleton block of M i , or is part of a message pair which has been already removed. Moreover, all events occurring after e i are events of M i (and thus so are their matching events). So any edge e j e j with j ≤ i < j can be associated with the block formed by e j in M i . Similarly, any edge e j → e j with j ≤ i < j can be associated with the block of e j in M i (note that e j is necessarily on an open process, since its incoming process edge is missing). In that case e j is necessarily the first event of its block, so this mapping is injective.

Thus, to ensures that the linearization is k-bounded, A EB k can simply check that at each -node, if the event being added to the linearization is a send, then there are at most k blocks.

Conversely, it is clear that all (k + 2)-DSTs obtained from the proof of Lemma 12 and described above are accepted by A EB k .

D Details for context-bounded MSCs

Lemma 14. If M is a k-context-bounded MSC and T M has tree-width at most h, then M has split-width at most k(h + 1) + 2.

Proof. We first describe Eve's strategy in the case of tree topologies, which have tree-width 1. Eve starts by splitting all the edges separating the contexts of the root p 0 of T M . This creates at most k blocks, and divides M into one component per child of p 0 . Adam chooses one of these components, associated with some child p 1 of p 0 . Eve splits all the edges separating the contexts of p 1 . The resulting split MSC can be divided in two parts, M 1 and M 2 , where M 1 consists of all the contexts in which p 0 and p 1 communicate with one another. In M 1 , each connected component has the form described in Figure 9: it is composed of some contexts in which p 0 sends to p 1 , and matching receive contexts of p 1 , or the opposite. Since the messages are received in the same order as they are sent, they can be detached one by one with two splits, which creates two extra blocks. So Eve wins on this part with budget 2k + 2. Therefore, Adam must choose a component of the remaining part M 2 . But M 2 is again a k-context-bounded split MSC over a tree topology (with root p 1 ), whose blocks are the contexts of the root p 1 . So whatever component of M 2 Adam chooses, Eve can apply the same strategy as for the previous move.

In the general case where T M has tree-width bounded by h, the strategy of Eve is similar: she separates at each step all the contexts of some processes. Her strategy for choosing these processes is determined by some (h + 1)-term τ for T M .

Alternatively, we can construct in a bottom-up fashion a DST τ for M by induction on τ . The colored vertices of τ correspond to the open processes of τ and the blocks of each open process correspond to some of its contexts. We can assume that τ contains no occurrence of ∅, x, and rename x,y , and that for each subterm τ 1 τ 2 and pairs of colors (x, y) occurring both in τ 1 and τ 2 , if there is an edge in G τ1 (resp. G τ2 ) between the vertices colored x and y, then there is none in G τ2 (resp. G τ1 ).

-xy is some (2k + 2)-DST t p,q denoting the split MSC induced by all the contexts in which the processes p and q colored x and y in G xy communicate with one another. We have explained above for tree topologies how to obtain such a (2k + 2)-DST. τ 1 τ 1 is the shuffle of τ 1 and τ 2 , according to the partial order of M .

forget x (τ 1 ) is the merge of τ 1 closing the process colored x in G τ1 , and keeping unchanged all the other processes. Notice that the blocks/contexts of a process are merged when it is closed.

At any node of τ (except subterms of t p,q ), there are at most (h + 1) open processes and at most k blocks on each open process. Hence τ is a (k(h + 1) + 2)-DST.

Lemma 26. One can construct in space polynomial in k and h a tree-automaton

A CB k,h with |N | O(kh) states such that CB k,h = {M t | t ∈ L(A CB k,h ∩ A k msc )}, where k = k(h + 1) + 2.
Proof. A CB k,h recognizes DSTs such that: (1) at any moment, there are at most h+1 open processes (this is given by the node labels); (2) until a process is closed, each of its blocks are contexts (A CB k,h remembers the type of each block/context in its state, and checks that there is no merge between two blocks of different types); (3) when a process is closed, it has at most k blocks, hence at most k contexts; (4) there are always at most k + 1 blocks on each process, and at most k blocks on a process which communicates with at least two different processes.

For any k-context bounded MSC M such that T M has tree-width at most h, we can construct (based on the proof of Lemma 14) a (k(h + 1) + 2)-DST accepted by A CB k,h . Conversely, it is clear that any MSC accepted by A CB k,h is k-context-bounded. The fact that its topology has tree-width at most h is a consequence from the fact that it uses at most h + 1 open processes (see proof of Theorem 24).

E Details for tile-bounded MSCs

E.1 Decidability Lemma 18. Let M ∈ TB k, ,h . Then M has split-width at most 2k 2 2 (h + 1).

Proof. Let {T 1 , . . . , T n } be a (k, )-tile-decomposition of M . Note that, if the observable topology T Ti of a k-tile T i is not connected, we can replace T i by several k-tiles having connected observable topologies. This does not change the number of tiles intersecting each process. Hence, w.l.o.g., we can assume that the observable topology T Ti is connected for all i. We denote by P i ⊆ the set of processes of T i , and by t i some k-DST denoting T i .

We are going to construct a DST for M from successive shuffles of the t i , in an order defined according to some (h + 1)-term τ for T M . The idea is to follow the order in which the processes are added to the topology in the tree-term, and to add a tile T i as soon as all its processes have been added to the topology and uncolored. The elastic edges separating the different tiles are made rigid as soon as possible, and open processes are closed as soon as all their tiles have been added to the split MSC.

For P ⊆ P , we let M P be the sub-MSC of M resulting from the shuffle of all the T i 's such that P i ⊆ P , followed by a merge (merging all blocks that are consecutive in M , and closing all processes that already have all their events). In particular, M = M P .

For each subterm τ of τ , we define a DST τ such that, with P τ the set of all uncolored processes of G τ , we have M τ = M P τ . To keep the definition simple, we do not provide the disambiguating labels. At shuffle nodes, we follow on each open process the ordering of the blocks defined by M . At merge nodes, we merge consecutive blocks and we close processes as soon as possible, as explained above.

-If τ = x or τ = xy, then τ is empty since

P τ = ∅. -if τ = τ 1 τ 2 then τ = (τ 1 τ 2 t i1 . . . t ij )
where i 1 , . . . , i j are the indices i such that P i ⊆ (P τ1 ∪ P τ2 ) but P i P τ1 and P i P τ2 . Since P τ = P τ1 P τ2 , using the induction hypothesis, we can check that M τ = M P τ .

-If τ = forget x (τ ): let p be the process being uncolored. We let τ = (τ t i1 . . . t ij ), where i 1 , . . . , i j are the indices i such that P i ⊆ P τ = P τ {p}, but P i P τ . Since P τ = P τ {p}, using the induction hypothesis, we can check that M τ = M P τ .

To prove that τ is a 2k 2 2 (h + 1)-DST, we show that before each -node, there are at most 2k (h + 1) open processes. Since there are at most tiles on each process and k blocks on each tile, there is always at most k blocks on each process.

First, consider some open process q of M τ , for a subterm τ of τ . Since processes are closed as soon as possible, some tile T i of q must still be missing in M τ (cf. Figure 10). In our construction, a tile is added as soon as all its processes have been added and uncolored in the tree-term, so this means that some process of T i must be missing or colored in G τ . Suppose for instance that some processes of T i are missing (represented by dotted lines in Figure 10). Using the fact that T Ti is connected, there must be processes u and v in T i such that u is in G τ , but v is not. Then u must be a colored process of G τ .

So in all cases, an open process q of M τ must share a tile with some colored process of G τ . Now, each colored process u is part of at most tiles, and each tile has at most k processes (see Figure 11). So there are at most k process sharing a tile with u. Moreover, there are at most (h + 1) colored process. So, at most k (h + 1) processes of M τ share a tile with (any) colored process of G τ . q u v T i Fig. 10. Tiles of an open process q Finally, observe that our reasoning about open processes of M τ also holds for processes q of G τ that are not in M τ . (All we need is that some tile of q is missing.) Thus, there are at most k (h + 1) processes of G τ that are either open processes of M τ or not in M τ .

≤ k processes ≤ k ≤ k ≤ tiles ≤ h + 1 colored processes
We are now ready to prove that τ is a 2k 2 2 (h + 1)-DST:

-All nodes of the t i 's have at most k blocks, since the t i 's are k-DSTs.

- Lemma 27. One can construct in space polynomial in k, , h a tree-automaton

A TB k, ,h with 2 O(k 2 h 2 ) states such that TB k, ,h = {M t | t ∈ L(A TB k, ,h ∩ A k msc )}, where k = 2k 2 2 (h + 1).
Proof. The idea is that A TB k, ,h recognizes DSTs of the form described in the proof of Lemma 18. In particular, using the same notations as in that proof, they are all of the form:

τ ::= (t i1 . . . t ij ) | (τ (t i1 . . . t ij )) | ((τ τ ) (t i1 . . . t ij )) ,
where t i1 , . . . , t ij denote k-tiles. Notice that in the proof of Lemma 18, some of the τ 1 , τ 2 may be empty and thus are not truly part of the complete DST (and then, neither is their father -node). This explain why we can have DST of the form (t i1 . . . t ij ). However, we assume that all -nodes described in the proof (except those such that there child node is empty) are actual nodes of the DST, though they may perform no action (i.e. be such that w p ∈ (B 1 ) * for any word of the label).

To check if a DST is of the above form, the bottom-up automaton A TB k, ,h remembers for each node a value stage ∈ {0, 1, 2}, with stage = 0 for the internal nodes of the t i 's, stage = 1 for the root of a t i or a shuffle of several t i 's, and stage = 2 for all other nodes. So initially, stage = 0, and at some point, A TB k, ,h guesses that a tile is complete and goes to stage = 1. Then only certain shuffles and merges are allowed, so that A TB k, ,h recognizes DSTs of the form described above (it uses some additional information to distinguish, among nodes such that stage = 2, those of the form τ , τ τ , τ t, or (τ τ ) t), where the root of t is in state stage = 1).

As long as stage = 0, A TB k, ,h checks that it is indeed reading some k-DST and not just any k -DST, and that no process is ever closed. This can be achieved with a slight modification of the automaton A k valid . Then, when stage ∈ {1, 2}, A TB k, ,h remembers the number of tiles currently intersecting with each open process, and checks that it never gets greater than . This ensures that all DSTs accepted by A TB k, ,h are (k, )-tile-bounded.

In addition, A TB k, ,h guesses an (h + 1)-term τ for the observable topology T of the current split MSC. Following the proof of Lemma 18, it guesses τ in such a way that all processes of T (open or closed) are uncolored processes of G τ . It forgets about the (h + 1)-term itself, as well as what happens on closed processes of T (all of them are uncolored in τ , and thus do not intervene in the remaining of the tree-term, nor naturally in the remaining of the DST). However, it keeps in its state the subgraph H τ of G τ induced by the other processes, i.e. colored vertices of G τ , uncolored vertices of G τ that are not part of T yet, and open processes of T . In the proof of Lemma 18, there are always at most m = 2k (h + 1) such processes.

First, for all nodes such that stage ∈ {0, 1} (i.e. when the current split MSC is a tile in construction, or a disjoint shuffle of tiles), A TB k, ,h remembers the observable topology T of the current split MSC. Recall that all processes of the split MSCs associated with such nodes are open, and thus can be identified with elements of [k ]. We ignore the interface names, and represent T by a subset of [k ] 2 .

Then, for each node such that stage = 2, A TB k, ,h keeps in its state a graph H τ with set of vertices included in [m], together with a partial coloring function c : [m] → [h+1], and a partial injective function num : [m] → [k], such that c and num have disjoint domains. The intuition is that num(v) = p when the vertex v of H τ is the p-th open process of T . When c(v) is defined, it gives the color of the vertex of H τ associated with v. We explain simultaneously the construction of H τ performed by A TB k, ,h , and how it can be associated inductively with an (h+1)-term τ , such that T a subgraph of G τ that uses only uncolored vertices, and H τ is the subgraph of G τ induced by all the vertices that are not closed processes of T .

-Consider a -node with child n where the value for stage goes from 1 to 2. This corresponds to a set of tiles being merged. (In the proof of Lemma 18, this happens when enough processes have finally been uncolored in the treeterm to cover all processes of some tiles.) A TB k, ,h must initialize H τ . To do so, it guesses a graph H τ = G τ of treewidth at most h and functions c and num such that the topology T stored at node n is a subgraph of H τ (the correspondence between the vertices being given by num). -Consider a shuffle between a node n 1 such that stage = 2 and a node n 2 such that stage = 1. This means that some tiles (denoted by n 2 ) are added to the current MSC (denoted by n 1 ). This can only happens when all the processes of n 2 are already uncolored in the tree-term. A TB k, ,h takes for H τ the graph stored for n 1 , and checks that the topology T 2 stored for n 2 is a subgraph of H τ . If a process of n 2 is shuffled with a process p 1 of n 1 , then it must correspond to the process num 1 (p 1 ). Other processes of n 2 (all of which are open) can be associated with any process of H τ for which num 1 is undefined. The function num 1 is then updated and extended into num to follow the possible additions of open processes from n 2 , and renumbering of the open processes of n 1 .

T 2 is thus a subgraph of G τ , and by induction hypothesis, so is the topology T 1 of the split MSC associated with n 1 (both respecting num). Thus, the topology T after the shuffle is still a subgraph of G τ . -Consider a shuffle between two nodes n 1 and n 2 for which stage = 2. Let H τ1 and H τ2 be the graphs stored respectively for the right and left child.

In the proof of Lemma 18, a node of this form correspond to a node τ 1 τ 2 in the tree-term. To construct the DST τ 1 τ 2 , the first step is to take the shuffle of τ 1 and τ 2 (afterwards, a second shuffle corresponding to the previous case is performed to add missing tiles). Recalled that the processes of τ 1 are uncolored processes of τ 1 , and similarly for τ 2 . Thus, they are not fused in τ 1 τ 2 , and the shuffle τ 1 τ 2 is disjoint (that is, w p ∈ B * ∪ B * r for each word of the label). At such a node, A TB k, ,h thus start by checking that the shuffle is disjoint. It also checks that H τ1 H τ2 contains at most m vertices, where H τ1 and H τ2 are the graphs stored respectively for the left and right children. It then takes H τ = H τ1 H τ2 . This correspond to taking τ = τ 1 τ 2 . By induction hypothesis, the topologies T 1 and T 2 for the left and right child are subgraphs of resp. G τ1 and G τ2 that only use uncolored vertices, hence are disjoint subgraphs of G τ . Moreover, the topology T is the disjoint union of T 1 and T 2 . Thus it is also a subgraph of G τ .

-Consider a -node such that stage = 2 for the child node n . Then A TB k, ,h may guess an uncoloring of a vertex of the graph H τ stored for n or a parallel union with a graph H of tree-width at most h and such that H τ H has at most m vertices. A TB k, ,h then removes from the resulting graph all the processes that are closed during the merge, and takes it as the new value for H τ . This corresponds to taking for τ = τ , τ = forget x (τ ), or τ = τ τ , where τ is an (h + 1)-term for H. Since T does not change, it is still a subgraph of G τ .

Any valid k'-DST accepted by A TB k, ,h then denotes a (k, )-bounded MSC over a topology of tree-width at most h. Conversely, all k -DSTs described in the proof of Lemma 18 are accepted by A TB k, ,h .

E.2 Equivalence with bounded split-width

Lemma 28. Let t be a valid k-DST, and M = M t . Let M be some sub-MSC of M (i.e., there exists N such that M ∈ (N N ), with b blocks. Then N has split-width at most k + b.

Proof. We write M = (P, O, E, →, , , π, λ), M = (P , O , E , → , , , π , λ ), and for a k-DST r, M r = (P r , O r , E r , → r , r , r , π r , λ r ). We define a (k + b)-DST t for M , by restricting t to the events that are in N . More precisely, for each subterm s of t, we define a

(k + b)-DST s such that M s is a sub-MSC of M s , E s = E s ∩ E , O s = P s ∩ (O s ∪ O ), and s = E 2 s ∩ ( s ∪ ).
-If s is a leaf of t, we let s = s if s denotes an event of N , and s = ∅ otherwise.

-If s = (wp) (s 1 ), we let s = (w p ) (s 1 ), where (w p ) is defined so that for all elastic edge e f of M s1 that are also in M s 1 , if e f is made rigid in M s , and is rigid in N , then it is also made rigid in M s .

-If s = s 1 (wp) s 2 , we let s = s 1 (w p ) s 2 , where (w p ) is defined so that the order in which the blocks of s 1 and s 2 are shuffled respect the order defined by s. The set of events covered by the previous tiles, Fr, is represented in blue. It consists of all events of the closed processes (here, the fourth process only), and some of the events of the open processes. All events that are not in Fr are added to the new tile Tp (in green), except e1 and e2, since the path from their processes to p (leftmost process) goes through a closed process.

the tiles are pairwise disjoint and since C t = P , by 2, they cover M . Hence, M ∈ ( p∈P T p ). It remains to show that each process q ∈ P intersects at most tiles (where is defined in the statement of the theorem). By 1, if a tile T p intersects process q then p is at distance at most k from q in T M . It is easy to check that the number of processes at distance at most k from q is at most .

We turn now to the definition of the tiles (T p ) p∈P . Assume that process p is closed at subterm s = (r) of t. We may assume that no blocks are merged on other processes and no other processes are closed. Hence, the set of closed processes is C s = C r {p}. By induction, T q is already defined for all q ∈ C r .

Let G be the set of events in E r \F r which are located on processes connected to p in T Mr via open processes of M r only: an event e ∈ E r \F r is in G if π(e) = p or π(e) = p 1 • • • p i = p in T Mr for some p 1 , . . . , p i ∈ O r . Let us show that G is -closed. So consider an edge e f with one end in G, say e ∈ G. Assume f ∈ F r . Since each tile is -closed, so is F r and we deduce e ∈ F r , a contradiction. Hence, f ∈ E r \ F r and by 2 we have π(f ) ∈ O r . Moreover, π(e) is connected to p via processes in O r only, and thus so is π(f ). Therefore, f ∈ G.

We define T p as the tile of M induced by G (see Fig. 12). We show that conditions 1, 2, and 3 are satisfied at s. Proof of condition 1. By definition, T p is disjoint from the existing tiles (T q ) q∈Cr .

Moreover, since t is a k-DST, there are at most k open processes in any subterm, in particular |O r | ≤ k. We deduce that T p contains at most k processes, each of which being at distance at most k from p in the topology T M .

It remains to show that T p has split-width at most k 2 + 2k. By Lemma 28, it is enough to show that T p has at most k 2 + k blocks.

A block of T p is an interval on some block of M r , delimited on each side either by (a) an end of the said block, or (b) by a block of the split MSC M Fr induced by F r (see Fig. 13). This is the case since for every process q ∈ O r , the set {e ∈ E r \ F r | π(e) = q} is either entirely contained in G or disjoint from G. Since M r has at most k blocks, there are at most 2k blocks of T p that are delimited on at least one side by the end of a block of M r (like the first two ones in Figure 13). Moreover, by induction hypothesis 3 at r, M Fr has at most k blocks on each process. Thus, on each process, there are at most (k -1) blocks of T p that are delimited on both sides by blocks of M Fr . Counting all processes, T p has at most k(k -1) blocks of this kind. Hence, T p has in total at most 2k + k(k -1) = k 2 + k blocks.

Proof of condition 2. Recall that C s = C r {p}. We have F s = F r G. By induction hypothesis, we know that {e ∈ E | π(e) ∈ C r } ⊆ F r ⊆ E r = E s . So we only need to show that {e ∈ E | π(e) = p} ⊆ F s = F r G. This is immediate, since by definition, G includes all events e ∈ E r \ F r which are on process p. This means all events in E \ F r which are on process p, since p is closed at s.

Proof of condition 3. Observe from the definition of G that on any process q of T p , the blocks of M Fs are the blocks of M r , and that on any other open process q, the blocks of M F are the blocks of M Fr .

F Satisfiability and Model-Checking

Monadic second-order logic. The set of monadic second-order formulas (over N ) is denoted by MSO N , and is given by the following syntax: where a ∈ N , x, y, . . . and u, v, . . . denote first-order variables ranging respectively over events and processes, and X, Y, . . . and U, V, . . . denote second-order variables ranging respectively over sets of events and sets of processes. MSO N formulas are interpreted over MSCs M = (P, E, →, , π, λ). Free variables are interpreted by a partial function I that maps a variable x to an event I(x) ∈ E, and X to a set I(X) ⊆ E. A variable u is mapped to a process I(u) ∈ P , and U to a set I(U ) ⊆ P . We write M, I |= x@u when π(I(x)) = I(u), and M, I |= u a b v when I(u) a b I(v) in the observable topology T M of M . The other cases are as expected. When ϕ is a closed formula, we simply write M |= ϕ instead of M, I |= ϕ.

Since T M is entirely determined by the events of M , the part of the logic that involves processes is redundant. Any formula ϕ ∈ MSO N can be translated into an equivalent formula over the syntax defined by the first two lines of (1).

G Complexity lower bounds

Notice that reachability reduces to non-emptiness, and satisfiability to modelchecking.

Lemma 34. When the set of interfaces N and the bound k on split-width are fixed rather than part of the input, and such that |N | ≥ 2 and k ≥ 3, SW-Reachability is Ptime-hard.

Similarly, when |N | ≥ 3, a bound k ≥ 3 on the number of contexts, and a bound h ≥ 1 on the tree-width of the topologies are fixed, CB-Reachability is Ptime-hard.

Proof. The proof is by reduction from the non-emptiness problem for binary tree automata. Without loss of generality, we assume here that tree automata accept only trees where the root and every internal node have exactly two children. Given a tree automaton A, we can construct in logarithmic space a PCA S over N = {father, child 1 , child 2 } with a distinguished state accept, such that there exists a MSC M ∈ SW 3 (resp. M ∈ CB 2 ) and a run ρ of S on M with ρ(e) = accept for some event of M iff L(A) = ∅. More precisely, we define S in such a way that for any connected MSC M , if there exist a run of S on M in which S reaches accept, then M has split-width at most 3 and is existentially 3-bounded, T M is a tree, and there exists a labeling of T M such that the labeled tree is accepted by A; and such that conversely, for any t ∈ L(A), there exists a MSC M with observable topology t, and such that there is a run ρ of S on M such that ρ(e) = accept for some event e of M .

The idea is that each process guesses (a) whether it is the a leaf, internal, or the root; and (b) a transition of A. More precisely, if a process guesses that it is a leaf, then it chooses a transition of A of the form a -→ q, and sends q to its father. If a process guesses that it is internal, it must start by receiving some message q 1 from its left child, then some q 2 from its right child. It then guesses a transition q 1 , q 2 a -→ q of A and sends q to its father. If a process guesses that it is a root, then it must receive some q 1 from its left child, then some q 2 from its right child, such that there exists a transition of A of the form q 1 , q 2 a -→ q with q accepting. In that case, it goes to state accept.

Let M be a connected MSC which allows for a run ρ of S such that ρ(e) = accept for some e. By definition of S, T M only contains edges of the form p father child i q. Moreover, there is no edge π(e) father child i q. Thus, T M is indeed a tree. Clearly, M is 3-context-bounded. It also has split-width at most 3: we can disconnect M by splitting the edge of its root, which create two blocks. In both of the resulting components, only one block (one event) remains on the root. We can disconnect the corresponding message by splitting the first process edge of the child node, leading to a total of 3 blocks. We are then back at the initial situation, except that the root of the subtree is already open. Next, any (I)CPDL formula Ψ over trees can be translated in polynomial time into an (I)CPDL formula Φ over MSCs, such that for any M ∈ L(Φ 0 ), M |= Φ ⇐⇒ T M |= Ψ . The formula Ψ is constructed inductively, by interpreting a node in t M by the first event of the corresponding process in M . For instance, a state formula σ ≡ x (for some x ∈ A) over trees is translated into the state formula ((x, father)? ∨ (x, child 1 )! ∨ (x, child 2 )!) ∧ ¬ → -1 over MSCs. a path formula π =↓ 1 over trees, denoting a path between a node and its left child, is translated into the path formula → * • test( x∈A (x, child 1 )!) • over MSCs.

We then have L(Φ 0 ∧ Φ) = ∅ ⇐⇒ L(Ψ ) = ∅.

Lemma 39. EB-CPDL-Sat is Pspace-hard. EB-ICPDL-Sat is Expspacehard.

Proof. The proof is an in Lemma 38, but using words instead of trees.

Fig. 2 .

 2 Fig. 1. An MSC with 3 processes

Definition 7 .

 7 A split (pre-)MSC is a tuple M = (P, O, E, →, , , π, λ), where (P, E, → ∪ , , π, λ) is a (pre-)MSC, ∩ → = ∅, O ⊆ P is the set of open processes of M , and every split process is open, i.e., {p ∈ P | (E p ) 2 ∩ = ∅} ⊆ O.

  The solution comes from the distinction between open and closed processes, and the fact that the number of open processes stays bounded. Merge and shuffle operations only act on open processes: a merge makes some elastic edges rigid (which are all located on open processes, by definition), and/or closes some open processes. Similarly, a shuffle of two split MSCs M 1 and M 2 may only combine some pairs of open processes of M 1 and M 2 by shuffling their blocks and adding elastic edges between them. It simply takes the disjoint union of closed processes.

Lemma 21 .

 21 One can construct in space polynomial in k and |N | a deterministic bottom-up tree automaton A k msc with 2 O(|N |k 4 ) states such that L(A k msc ) = DST k msc .

  which leads to an algorithm in time polynomial in |S| and exponential in k, |N | and |F | to decide the non-emptiness of L(S) ∩ SW k . This proves the upperbound of Theorem 11.

Fig. 7 .

 7 Fig. 7. Complexity results. All problems are only polynomial in the number of states and transitions of the input PCA.

  2 is (B , B B r ), which implies that the first open process is the first open process of the left child, and the second open process comes from the shuffle of the second open process of the left child, and of the first open process of the right child.

Fig. 9 .

 9 Fig. 9. A connected component of M1

Fig. 11 .

 11 Fig. 11. Number of open processes

Fig. 12 .

 12 Fig.12. Definition of Tp. The set of events covered by the previous tiles, Fr, is represented in blue. It consists of all events of the closed processes (here, the fourth process only), and some of the events of the open processes. All events that are not in Fr are added to the new tile Tp (in green), except e1 and e2, since the path from their processes to p (leftmost process) goes through a closed process.

Fig. 13 .

 13 Fig.[START_REF] Delzanno | On the power of cliques in the parameterized verification of ad hoc networks[END_REF]. Blocks of Tp (in green) and of MF r (in blue) on the third process of Figure12.

ϕ

  ::= x = y | x y | x → y | a!(x) | a?(x) | x ∈ X | ∃x.ϕ | ∃X.ϕ | ¬ϕ | ϕ ∨ ϕ (1) | x@u | u a b v | u = v | u ∈ U | ∃u.ϕ | ∃U.ϕ

Lemma 30 .

 30 For any closed formula ϕ ∈ MSO N , one can construct a tree automatonA k ϕ such that L(A k ϕ ) ∩ DST k msc = {t ∈ DST k msc | M t |= ϕ}. Proof.The construction is by induction on ϕ. The only non-trivial case for atomic formula is the → relation. It can be retrieved by a deterministic bottomup tree automaton with O(k 4 ) states, which accepts a valid k-DST t with two marked leaves e and f iff e → f in M t . It remembers the blocks B and B of the two marked leaves (that is, pairs in [k] 2 , where (p, i) represents the i-th block on the p-th open process), and checks that there is no merge on the right of B or the left of B until reaching a common ancestor where the two blocks are merged.The inductive cases are treated with standard constructions: union for disjunction, complementation for negation, and projection for existential quantifications.Theorem 31. For C ∈ {SW, EB, CB, TB}, the satisfiability and model-checking problems are decidable:C-MSO-Sat:Input: N , ϕ ∈ MSO N , i. Question: ∃M ∈ C i , M |= ϕ ? C-MSO-MC: Input: N , ϕ ∈ MSO N , S, i. Question: ∀M ∈ L(S) ∩ C i , M |= ϕ ?Proof. The bounded split-width satisfiability problem reduces to testing whether L(A k ϕ ∩ A k msc ) = ∅, and the bounded split-width model-checking problem to testing whether L(A k S ∩ A k ¬ϕ ∩ A k msc ) = ∅. For the other classes, we add the corresponding automaton to the intersection, as for the non-emptiness problem.

Lemma 35 .

 35 When |N | ≥ 2 and k ≥ 3 are fixed, the problem EB-Reachability is Nlogspace-hard.

  how the blocks of the p-th open process of its child are merged: B i stands for a block resulting from the merge of i consecutive blocks of the child. We use w p = ε to indicate that process p is closed, merging all its blocks if any. For instance, in Figures5 and 6the label (B 2 , B 2 ) of node n 3 indicates that on both process of M 3 , the two blocks are merged in M 3 .-For a -node, m ≤ 2 and the word w p ∈ {B ! , B

? } indicates that the p-th open process consists of the send (resp. receive) event. If m = 2 then w 1 = w 2 . For instance, n 7 is labeled (B ! ), which means that in M 7 the process of the send event is open whereas the process of the receive event is closed.

  Notice that each process of t , be it open or closed, is in P τ = P τ1 P τ2 . Hence, we show that t has at most k (h + 1) open processes in P τ1 , and at most k (h + 1) open processes in P τ2 . If an open process p ∈ P τ1 of t is also a process of τ 1 , then it must be open as well in τ 1 . Moreover, at most k (h + 1) processes of G τ1 are either not processes of τ 1 , or open processes of τ 1 . So t has at most k (h + 1) open processes in P τ1 . As in the previous case, t has at most k (h + 1) open processes in P τ . Since all processes of t are in P τ = P τ {p}, t has in total at most k (h + 1) + 1 open processes.

	Consider a subterm τ = (τ 1	τ 2	t i1	. . .	t ij ) of τ , as defined
	above. We show that t = τ 1	τ 2	t i1	. . .	t ij has at most 2k (h + 1)
	open processes. -Consider a subterm τ = (τ		t i1	. . . t ij ) of τ , as defined above. We
	show that t = τ	t i1	. . . t ij has at most k (h + 1) + 1 open processes.

B Tree-width

There are many equivalent definitions of tree-width. We use a definition in terms of a graph algebra [START_REF] Courcelle | Graph Structure and Monadic Second-Order Logic -A Language-Theoretic Approach[END_REF], which is closer to our definition of split-width.

We consider undirected simple graphs G = (V, E) equipped with a partial injective coloring function c : V → C of their vertices. We identify isomorphic graphs. Given a finite set of colors C and x, y ∈ C, we denote by -x the graph consisting of a single vertex colored x, -xy the graph with two vertices labeled x and y and one edge between them, -forget x the operation of uncoloring a vertex, -rename x,y (G, c) the graph (G, c ) obtained by permuting colors x and y in G:

) the union of G and G where the vertices with same color are fused.

A k-term is a term over the algebra

The semantics (G τ , c τ ) of a k-term is as expected. The tree-width of a graph G is the least k such that G = G τ for some (k + 1)-term τ .

Theorem 24. Let M be an MSC. If M has split-width at most k, then T M has tree-width at most k -1.

Proof. Let t be a k-DST for M . We construct by induction on t a k-term τ (t) for T M , such that the open processes of t are the colored vertices of G τ (t) . More precisely, the translation depends on the labels of the k-DST and is shown below:

) by renaming colors so that the pairs of processes from G τ (t1) and G τ 2 having the same color are exactly the pairs of processes being fused in the shuffle. τ ( (wp) (t 1 )) = forget x1 (. . . (forget xi (τ (t 1 ))) . . .), where x 1 , . . . , x i are the colors in G τ (t1) of the processes that are closed in the merge.

To prove that t is a (k + b)-DST, we need to show that for all subterm s of t, s has at most k blocks, i.e.

By definition, we have

Theorem 20 is obtained as the combination of Lemma 24 and 29.

Lemma 29. Let M be an MSC with split-width at most k. Define

Then M admits a (k 2 + 2k, )-tile decomposition where each tile contains at most k processes.

Proof. Let t be a valid k-DST such that M = M t = (P, E, →, , π, λ). We first introduce some notations. For each subterm s of t we consider the associated split MSC M s . We denote by O s (C s resp.) the set of open (closed resp.) processes of M s . In particular, O t = ∅ and C t = P . We also denote by E s the set of events of M s .

A subset F ⊆ E is -closed if for all e f , either both events are in F or none of them are in F . For a -closed subset F ⊆ E, we denote by M F the split MSC induced by F , i.e., the split MSC whose set of events is F , and such that two events of F are connected by a →-or -edge in M F iff they are in M . The open processes of M F are those on which some events of M are missing. The elastic edges are such that the order of the events in M F is compatible with M . Notice that M ∈ (M F M E\F ). We will define a tuple of tiles (T p ) p∈P which forms a (k 2 +2k, ) decomposition of M . These tiles will be defined below by induction on t. Intuitively, whenever a process p is closed at some subterm s of t, we define the tile T p as the split-MSC induced by the set of events that are not yet covered by some tile and that are connected to p via open processes.

For each p ∈ P , let X p ⊆ E be the subset of events of the tile T p . We will ensure the following, where s is an arbitrary subterm of t and F s = p∈Cs X p :

1. For all p ∈ P , T p is a (k 2 + 2k)-tile which contains at most k processes, each of which being at distance at most k from p in the topology T M . The tiles are pairwise disjoint: X p ∩ X q = ∅ for all p = q. 2. The tiles (T p ) p∈Cs are contained in M s and cover all events of the closed processes of

On the other hand, some events of M s located on open processes may not be in F s . 3. The split MSC M Fs induced by F s has at most k blocks on each process.

Before defining the tile-decomposition (T p ) p∈P , we first show that the above conditions allow to derive the theorem. First, by 1, each T p is a (k 2 + 2k)-tile, Propositional Dynamic Logic. The syntax of ICPDL N is given by

where a ∈ N . If intersection π ∩ π is not allowed, the fragment is PDL with converse (CPDL). If backward paths π -1 are not allowed the fragment is called PDL with intersection (IPDL). In simple PDL neither backward paths nor intersection are allowed. State formula and path formula are respectively evaluated over events and pairs of events of an MSC. We only give a few cases:

The operations +, •, * , ∩ and -1 correspond respectively to union, composition, reflexive and transitive closure, intersection, and converse of the relations defined by path formulas.

MSC properties are specified using global formulas. For the base case, M |= Eσ if there exists e ∈ E such that M, e |= σ.

Lemma 32. For any Φ ∈ CPDL N (resp. Φ ∈ ICPDL N ), one can construct in PSpace (resp. ExpSpace) a tree automaton

Proof. The construction is again by induction on the formula, but uses alternating two-way tree automata (A2A) rather than bottom-up automata. For any CPDL N (resp. ICPDL N ) formula Φ, we can construct an A2A of polynomial (resp. exponential) size that accepts a valid k-DST t iff M t |= Φ (see [START_REF] Aiswarya | Verifying communicating multipushdown systems via split-width[END_REF] for a more detailed and very similar proof). It can then be translated into an exponentially larger (ordinary) tree automaton.

Theorem 33. For bounded split-width, context-bounded or tile-bounded MSCs (resp. existentially-bounded MSCs), the CPDL satisfiability and model-checking problems are Exptime-complete (resp. Pspace-complete), and the ICPDL satisfiability and model-checking problems are 2-Exptime-complete (resp. Expspacecomplete). The model-checking problem is (in all cases) only polynomial in the number of states and transitions of the PCA.

Proof. The proof is the same as that of Lemma 34, but using word automata instead of tree automata, and pipelines instead of trees for topologies.

Lemma 36. SW-Reachability and CB-Reachability are Exptime-hard.

Proof. The proof is similar to that of Lemma 34, but we reduce the intersection problem for k tree automata. Each process simply repeats k times the behaviour described above. (More details can be found in the proof of Lemma 37, which uses the same kind of reduction but for word automata instead of tree automata.) Each process has at most 3k events, hence the MSC is 3k-context bounded, hence has split-width at most 6k + 2.

Lemma 37. EB-Reachability is Pspace-hard.

Proof. The proof is by reduction from the intersection problem for finite automata. Given finite automata A 1 , . . . , A k , we can construct in polynomial time a PCA S over N = {left, right}, with a distinguished state accept, such that

and a run ρ of S on M with ρ(e) = accept for some event of M . The idea is that if S accept some connected MSC M , then there exists a word w ∈ L(A 1 ) ∩ • • • ∩ L(A k ) such that T M is a pipeline with |w| processes, and conversely. Each process guesses a transition for each A i using the same (guessed) letter, and sends it to its right neighbor. The (guessed) leftmost process must choose transitions starting in initial states, and the (guessed) rightmost process checks for all A i that it can choose a transition ending in an accepting state. It then goes to state accept. More precisely, S only accepts MSCs of the form described in Figure 3 (or disjoint unions of such MSCs), with an arbitrary number of processes, but k events on the leftmost process. The fact that the topology does not contain any cycle is ensured by the fact that at least one process has no right neighbor (the process reaching accept).

Any MSC accepted by S is existentially (k + 2)-bounded: the linearization consists in taking first the events of the leftmost process (in order), then the events of its right neighbor, and so on.

Lemma 38. SW-CPDL-Sat and CB-CPDL-Sat are Exptime-hard, and SW-ICPDL-Sat and CB-ICPDL-Sat are 2-Exptime-hard.

Proof. The proofs are by reduction from the satisfiability problems for (I)CPDL over binary trees with labels in some finite alphabet A.

First, there is a PDL formula Φ 0 over N = A × {father, child 1 , child 2 } that recognizes the set of MSCs M such that T M is a tree (and each process has at most 3 interfaces, of the form (x, father), (x, child 1 ), (x, child 2 ) for some x ∈ A), and each process is composed of first a receive from its father (if any), then a send to its left child (if any), then a send to its right child (if any). We let t M be the tree whose nodes are those of T M , and such that the label x of each node is determined by its set of interfaces in T M . This defines a bijection between the set of labeled binary trees and L(Φ 0 ). Moreover, for any k ≥ 3, h ≥ 1, L(Φ 0 ) ⊆ SW k and L(Φ 0 ) ⊆ CB k,h .