Benedikt Bollig

Cinzia Di Giusto

Alain Finkel

Etienne Lozes

Amrita Suresh

A Unifying Framework for Deciding Synchronizability

Keywords: 2012 ACM Subject Classification Theory of computation → Formal languages and automata theory communicating finite-state machines, message sequence charts, synchronizability, MSO logic, special tree-width

Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.

Introduction

Communication systems. The model of concurrent processes communicating asynchronously through FIFO channels is used since the 1960s in applications such as communication protocols [28], hardware design, MPI programs, and more recently for designing and verifying session types [23], web contracts, choreographies, concurrent programs, Erlang, Rust, etc. Since communication systems use FIFO channels, it is well known that all non-trivial properties (e.g., are all channels bounded?) are undecidable [START_REF] Brand | On communicating finite-state machines[END_REF], essentially because a FIFO channel may simulate the tape of Turing machines and the counters of Minsky machines. However, there are many subclasses of communication systems for which the control-state reachability problem becomes decidable: e.g., synchronizable systems and existentially bounded systems (executions can be reorganized or decomposed into a finite number of sequences in which all channels are bounded), flat FIFO machines [START_REF] Esparza | A perfect model for bounded verification[END_REF][START_REF] Finkel | Verification of Flat FIFO Systems[END_REF] (the graph of the machine does not contain nested loops), channel-recognizable systems [START_REF] Boigelot | Symbolic verification of communication protocols with infinite state spaces using qdds (extended abstract)[END_REF], unreliable (lossy, insertion, duplication) FIFO systems [START_REF] Cécé | Unreliable channels are easier to verify than perfect channels[END_REF], input-bounded FIFO machines [START_REF] Bollig | Bounded reachability problems are decidable in FIFO machines[END_REF], and half-duplex systems [START_REF] Cécé | Verification of programs with half-duplex communication[END_REF].

On the boundedness problem. We focus on the boundedness problem, which is known to be undecidable. We could limit our analysis to decide whether for a given integer k ≥ 0, known in advance, the FIFO channels are k-bounded, and this property is generally decidable in PSPACE. Unfortunately, the k-boundedness property is too binding since we could want to design an unbounded system that is able, for example, to make unbounded iterations of sending and receiving messages. Hence, to cope with this limitation, one can find variants of the boundedness property that essentially reduce to say that every unbounded execution of a system (i.e., channels are unbounded along the execution) is equivalent (for instance, causally equivalent) to another bounded execution.

About synchronizability. To mention some examples, Lohrey and Muscholl introduced existentially k-bounded systems [25] (see also [START_REF] Genest | On communicating automata with bounded channels[END_REF][START_REF] Genest | A kleene theorem for a class of communicating automata with effective algorithms[END_REF]24]) where all accepting executions leading to a stable (with empty channels) final configuration can be re-ordered into a k-bounded execution. This property is undecidable, even for a given k [START_REF] Genest | On communicating automata with bounded channels[END_REF]. A more general definition, still called existentially bounded, is given in 2014 where the considered executions are not supposed to be final or stable [22]. In [21,25], the notion of universally k-bounded (all possible schedulings of an execution are k-bounded) is also discussed and the authors show that the property is undecidable in general. In 2011, Basu and Bultan introduced synchronizable systems [START_REF] Basu | Choreography conformance via synchronizability[END_REF], for which every execution is equivalent (for the projection on sending messages) to one of the same system but communicating by rendezvous; to avoid ambiguity, we call such systems send-synchronizable. In 2018, Bouajjani et al., called a system S k-synchronizable [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] (to avoid confusion we call such systems weakly k-synchronizable) if every MSC of S admits a linearization (which is not necessarily an execution) that can be divided into blocks of at most k messages. After each block, a message is either read, or will never be read. This constraint seems to imply that buffers are bounded to k messages. However, as the linearization need not be an execution, this implies that a weakly k-synchronizable execution, even with the more efficient reschedule, can need unbounded channels to be run by the system.

Communication architecture and variants.

A key difference between these works is that they consider different communication architectures. Existentially bounded systems have been studied for p2p (with one queue per pair of processes), whereas k-synchronizability has been studied for mailbox communication, for which each process merges all its incoming messages in a unique queue. The decidability results for k-synchronizability have been extended to p2p communications [START_REF] Di Giusto | On the k-synchronizability of systems[END_REF], but it is unknown whether the decidability results for existentially bounded systems extend to mailbox communication. Moreover, variants of those definitions can be obtained depending on if we consider messages that are sent but never read, called unmatched messages. Indeed the challenges that arise in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] are due to mailbox communication and unmatched messages blocking a channel so that all messages sent afterwards will never be read. To clarify and overcome this issue, we propose strong k-synchronizability, a new definition that is suitable for mailbox communication: an execution is called strongly k-synchronizable if it can be rescheduled into another k-bounded execution such that there are at most k messages in the channels before emptying them.

Contributions. Our contributions can be summarized as follows:

In order to unify the notions of synchronizability, we introduce a general framework based on monadic second-order (MSO) logic and (special) tree-width that captures most existing definitions of systems that may work with bounded channels. Moreover, reachability and model checking are shown decidable in this framework. We show that existentially bounded systems can be expressed in our framework and, as a consequence, the existentially k-bounded property is decidable by using the generic proof.

We generalize the existing notion of (weak) k-synchronizability in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] and we introduce three new classes of synchronizable systems: weakly synchronizable (which are more general than weakly k-synchronizable), strongly synchronizable and strongly k-synchronizable (which are particular cases of weakly synchronizable). We then prove that these properties all fit in our framework and are all shown decidable using the generic proof. We then deduce that reachability and model checking are decidable for these classes (only control-state reachability was shown to be decidable for weakly k-synchronizable in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] and it is clearly also decidable for existentially/universally bounded systems but reachability properties are generally not studied for these classes of systems). In order to obtain better complexity results for some classes (strongly and weakly synchronizable systems), we also use the fragment of propositional dynamic logic with loop and converse (LCPDL) instead of MSO logic in our framework. We provide a comparison between synchronizable classes both for p2p and mailbox semantics (see Fig. 8 for p2p systems and Fig. 9 for mailbox systems). In particular, we clarify the link between weakly synchronizable and existentially bounded systems for both p2p and mailbox systems, which was left open in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] and solved only for p2p systems in [23, Theorem 7] where weakly synchronizable systems are shown to be included into existentially bounded ones when considering executions (and not MSCs as in our case).

Outline. Section 2 defines some preliminary notions such as p2p/mailbox message sequence charts (MSCs), and communicating systems. Section 3 presents the unifying MSO framework and two general theorems on k-synchronizability and model checking. In Section 4, we apply the MSO framework to different existing definitions of synchronizability, and we introduce a new decidable one. Section 5 studies the relations between the classes. In Section 6, we conclude with some final remarks. Missing proofs are given in the appendix.

Preliminaries

Message Sequence Charts

Assume a finite set of processes P and a finite set of messages M. The set of (p2p) channels is C = {(p, q) ∈ P × P | p ̸ = q}. A send action is of the form send(p, q, m) where (p, q) ∈ C and m ∈ M. It is executed by p and sends message m to q. The corresponding receive action, executed by q, is rec(p, q, m). For (p, q) ∈ C, let Send(p, q, ) = {send(p, q, m) | m ∈ M} and Rec(p, q, ) = {rec(p, q, m) | m ∈ M}. For p ∈ P, we set Send(p, , ) = {send(p, q, m) | q ∈ P \ {p} and m ∈ M}, etc. Moreover, Σ p = Send(p, , ) ∪ Rec( , p, ) will denote the set of all actions that are executed by p. Finally, Σ = p∈P Σ p is the set of all the actions.

Peer-to-peer MSCs. A p2p MSC (or simply MSC ) over P and M is a tuple M = (E, →, ◁, λ) where E is a finite (possibly empty) set of events and λ : E → Σ is a labeling function. For p ∈ P, let E p = {e ∈ E | λ(e) ∈ Σ p } be the set of events that are executed by p. We require that → (the process relation) is the disjoint union p∈P → p of relations → p ⊆ E p × E p such that → p is the direct successor relation of a total order on E p . For an event e ∈ E, a set of actions A ⊆ Σ, and a relation

R ⊆ E × E, let # A (R, e) = |{f ∈ E | (f, e) ∈ R and λ(f ) ∈ A}|.
We require that ◁ ⊆ E × E (the message relation) satisfies the following:

(1) for every pair (e, f ) ∈ ◁, there is a send action send(p, q, m) ∈ Σ such that λ(e) = send(p, q, m), λ(f ) = rec(p, q, m), and # Send(p,q, ) (→ + , e) = # Rec(p,q, ) (→ + , f ),

(2) for all f ∈ E such that λ(f ) is a receive action, there is e ∈ E such that e ◁ f . Finally, letting ≤ M = (→ ∪ ◁) * , we require that ≤ M is a partial order.

Condition (1) above ensures that every (p2p) channel (p, q) behaves in a FIFO manner. By Condition (2), every receive event has a matching send event. Note that, however, there may be unmatched send events in an MSC. We let

SendEv(M ) = {e ∈ E | λ(e) is a send action}, RecEv(M ) = {e ∈ E | λ(e) is a receive action}, Matched(M ) = {e ∈ E | there is f ∈ E such that e ◁ f }, and Unm(M ) = {e ∈ E | λ(e)
is a send action and there is no f ∈ E such that e ◁ f }. We do not distinguish isomorphic MSCs and let MSC be the set of all MSCs over the given sets P and M.

▶ Example 1. For a set of processes P = {p, q, r} and a set of messages

M = {m 1 , m 2 , m 3 , m 4 }, M 1 = (E, →, ◁, λ) is an MSC where, for example, e 2 ◁ e ′
2 and e ′ 3 → e 4 . The dashed arrow means that the send event e 1 does not have a matching receive, so e 1 ∈ U nm(M 1 ). Moreover, e 2 ≤ M1 e 4 , but e 1 ̸ ≤ M1 e 4 . We can find a total order

⇝ ⊇ ≤ M1 such that e 1 ⇝ e 2 ⇝ e ′ 2 ⇝ e 3 ⇝ e ′ 3 ⇝ e 4 ⇝ e ′ 4 .
We call ⇝ a linearization, which is formally defined below. Mailbox MSCs. For an MSC M = (E, →, ◁, λ), we define an additional binary relation that represents a constraint under the mailbox semantics, where each process has only one incoming channel. Let ⊏ M ⊆ E × E be defined by: e 1 ⊏ M e 2 if there is q ∈ P such that λ(e 1 ) ∈ Send( , q, ), λ(e 2 ) ∈ Send( , q, ), and one of the following holds:

e 1 ∈ Matched(M ) and e 2 ∈ Unm(M ), or e 1 ◁ f 1 and e 2 ◁ f 2 for some f 1 , f 2 ∈ E q such that f 1 → + f 2 . We let ⪯ M = (→ ∪ ◁ ∪ ⊏ M ) * . Note that ≤ M ⊆ ⪯ M . We call M ∈ MSC a mailbox MSC if ⪯ M
is a partial order. Intuitively, this means that events can be scheduled in a way that corresponds to the mailbox semantics, i.e., with one incoming channel per process. Following the terminology in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF], we also say that a mailbox MSC satisfies causal delivery. The set of mailbox MSCs M ∈ MSC is denoted by MSC mb .

▶ Example 2. MSC M 1 is a mailbox MSC. Indeed, even though the order ⇝ defined in Example 1 does not respect all mailbox constraints, particularly the fact that e 4 ⊏ M1 e 1 , there is a total order ⇝ ⊇ ⪯ M1 such that e 2 ⇝ e 3 ⇝ e ′ 3 ⇝ e 4 ⇝ e 1 ⇝ e ′ 2 ⇝ e ′ 4 . We call ⇝ a mailbox linearization, which is formally defined below.

Linearizations, Prefixes, and Concatenation

. Consider M = (E, →, ◁, λ) ∈ MSC. A p2p linearization (or simply linearization) of M is a (reflexive) total order ⇝ ⊆ E × E such that ≤ M ⊆ ⇝. Similarly, a mailbox linearization of M is a total order ⇝ ⊆ E × E such that ⪯ M ⊆ ⇝.
That is, every mailbox linearization is a p2p linearization, but the converse is not necessarily true (Example 2). Note that an MSC is a mailbox MSC iff it has at least one mailbox linearization.

Let M = (E, →, ◁, λ) ∈ MSC and consider E ⊆ E such that E is ≤ M -downward- closed, i.e, for all (e, f ) ∈ ≤ M such that f ∈ E, we also have e ∈ E. Then, the MSC (E, → ∩ (E × E), ◁ ∩ (E × E), λ ′ ), where λ ′ is the restriction of E to E, is called a prefix of M .
In particular, the empty MSC is a prefix of M . We denote the set of prefixes of M by Pref (M ). This is extended to sets L ⊆ MSC as expected, letting Pref (L) = M ∈L Pref (M ).

▶ Lemma 3. Every prefix of a mailbox MSC is a mailbox MSC.

Let

M 1 = (E 1 , → 1 , ◁ 1 , λ 1 ) and M 2 = (E 2 , → 2 , ◁ 2 , λ 2 ) be two MSCs. Their concatenation M 1 • M 2 = (E, →, ◁, λ) is defined if, for all (p, q) ∈ C, e 1 ∈ Unm(M 1 )
, and e 2 ∈ E 2 such that λ(e 1 ) ∈ Send(p, q, ) and λ(e 2 ) ∈ Send(p, q, ), we have e 2 ∈ Unm(M 2 ). As expected, E is the disjoint union of E 1 and E 2 , ◁ = ◁ 1 ∪ ◁ 2 , λ is the "union" of λ 1 and λ 2 , and

→ = → 1 ∪ → 2 ∪ R.
Here, R contains, for all p ∈ P such that (E 1 ) p and (E 2 ) p are non-empty, the pair (e 1 , e 2 ) where e 1 is the maximal p-event in M 1 and e 2 is the minimal p-event in M 2 . Note that M 1 • M 2 is indeed an MSC and that concatenation is associative.

Communicating Systems

We now recall the definition of communicating systems (aka communicating finite-state machines or message-passing automata), which consist of finite-state machines A p (one for every process p ∈ P) that can communicate through the FIFO channels from C. ▶ Definition 4. A communicating system over P and M is a tuple S = (A p ) p∈P . For each p ∈ P, A p = (Loc p , δ p , ℓ 0 p ) is a finite transition system where Loc p is a finite set of local (control) states, δ p ⊆ Loc p × Σ p × Loc p is the transition relation, and ℓ 0 p ∈ Loc p is the initial state.

Given p ∈ P and a transition

t = (ℓ, a, ℓ ′ ) ∈ δ p , we let source(t) = ℓ, target(t) = ℓ ′ , action(t) = a, and msg(t) = m if a ∈ Send( , , m) ∪ Rec( , , m).
There are in general two ways to define the semantics of a communicating system. Most often it is defined as a global infinite transition system that keeps track of the various local control states and all (unbounded) channel contents. As, in this paper, our arguments are based on a graph view of MSCs, we will define the language of S directly as a set of MSCs. These two semantic views are essentially equivalent, but they have different advantages depending on the context. We refer to [START_REF] Aiswarya | Reasoning about distributed systems: WYSIWYG (invited talk)[END_REF] for a thorough discussion.

Let M = (E, →, ◁, λ) be an MSC. A run of S on M is a mapping ρ : E → p∈P δ p that assigns to every event e the transition ρ(e) that is executed at e. Thus, we require that (i) for all e ∈ E, we have action(ρ(e)) = λ(e), (ii) for all (e, f ) ∈ →, target(ρ(e)) = source(ρ(f )), (iii) for all (e, f ) ∈ ◁, msg(ρ(e)) = msg(ρ(f )), and (iv) for all p ∈ P and e ∈ E p such that there is no f ∈ E with f → e, we have source(ρ(e)) = ℓ 0 p . Letting run S directly on MSCs is actually very convenient. This allows us to associate with S its p2p language and mailbox language in one go. The p2p language of S is L p2p (S) = {M ∈ MSC | there is a run of S on M }. The mailbox language of S is L mb (S) = {M ∈ MSC mb | there is a run of S on M }.

Note that, following [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF][START_REF] Di Giusto | On the k-synchronizability of systems[END_REF], we do not consider final states or final configurations, as our purpose is to reason about all possible traces that can be generated by S. The next lemma is obvious for the p2p semantics and follows from Lemma 3 for the mailbox semantics.

▶ Lemma 5. For all com ∈ {p2p, mb}, L com (S) is prefix-closed: Pref (L com (S)) ⊆ L com (S).
▶ Example 6. Fig. 2 depicts S 1 = (A p , A q , A r ) such that MSC M 1 in Fig. 1 belongs to L p2p (S 1 ) and to L mb (S 1 ). There is a unique run ρ of S 1 on M 1 . We can see that (e ′ 3 , e 4 ) ∈ → and target(ρ(e ′

3 )) = source(ρ(e 4 )) = ℓ 1 r , (e 2 , e ′ 2 ) ∈ ◁ M1 , and msg(ρ(e 2 )) = msg(ρ(e ′ 2 )) = m 2 .

Conflict Graph

We now recall the notion of a conflict graph associated to an MSC defined in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF]. This graph is used to depict the causal dependencies between message exchanges. Intuitively, we have

ℓ 0 p ℓ 1 p ℓ 2 p send(p, q, m 1 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q ℓ 2 q ℓ 3 q send(q, p, m 2 ) send(q, r, m 3 ) rec(r, q, m 4 ) Aq ℓ 0 r ℓ 1 r ℓ 2 r rec(q, r, m 3 )
send(r, q, m 4 ) Ar a dependency whenever two messages have a process in common. For instance, an SS --→ dependency between message exchanges v and v ′ expresses the fact that v ′ has been sent after v, by the same process. This notion is of interest because it was seen in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] that the notion of synchronizability in MSCs (which is studied in this paper) can be graphically characterized by the nature of the associated conflict graph. It is defined in terms of linearizations in [START_REF] Di Giusto | On the k-synchronizability of systems[END_REF], but we equivalently express it directly in terms of MSCs.

For an MSC M = (E, →, ◁, λ) and e ∈ E, we define the type τ (e) ∈ {S, R} of e by τ (e) = S if e ∈ SendEv(M ) and τ (e) = R if e ∈ RecEv(M ). Moreover, for e ∈ Unm(M ), we let µ(e) = e, and for (e, e ′ ) ∈ ◁, we let µ(e) = µ(e ′ ) = (e, e ′ ).

▶ Definition 7 (Conflict graph). The conflict graph CG(M ) of an MSC M = (E, →, ◁, λ) is the labeled graph (Nodes, Edges), with Edges ⊆ Nodes × {S, R} 2 × Nodes, defined by Nodes = ◁ ∪ Unm(M ) and Edges = {(µ(e), τ (e)τ (f ), µ(f )) | (e, f ) ∈ → + }. In particular, a node of CG(M ) is either a single unmatched send event or a message pair (e, e ′ ) ∈ ◁.

Model Checking and Synchronizability

In this section, we survey two classical decision problems for communicating systems. The first problem is the model-checking problem, in which one checks whether a given system satisfies a given specification. A canonical specification language for MSCs is monadic second-order (MSO) logic. However, model checking in full generality is undecidable. A common approach is, therefore, to restrict the behavior of the given system to MSCs of bounded (special) tree-width. Next, we introduce MSO logic and special tree-width.

Logic and Special Tree-Width

Monadic Second-Order Logic. The set of MSO formulas over MSCs (over P and M) is given by the grammar φ ::

= x → y | x ◁ y | λ(x) = a | x = y | x ∈ X | ∃x.φ | ∃X.φ | φ ∨ φ | ¬φ,
where a ∈ Σ, 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. We assume that we have an infinite supply of variables, and we use common abbreviations such as ∧, ∀, etc. The satisfaction relation is defined in the standard way and self-explanatory. For example, the formula ¬∃x.( a∈Send( , , ) λ(x) = a ∧ ¬matched(x)) with matched(x) = ∃y.x ◁ y says that there are no unmatched send events. It is not satisfied by MSC M 1 of Fig. 1, as message m 1 is not received, but by M 4 from Fig. 6.

Given a sentence φ, i.e., a formula without free variables, we let L(φ) denote the set of (p2p) MSCs that satisfy φ. It is worth mentioning that the (reflexive) transitive closure of a binary relation defined by an MSO formula with free variables x and y, such as x → y, is MSO-definable so that the logic can freely use formulas of the form x → + y or x ≤ y (where ≤ is interpreted as ≤ M for the given MSC M ). Therefore, the definition of a mailbox MSC can be readily translated into the formula φ mb = ¬∃x.∃y.(¬(x = y) ∧ x ⪯ y ∧ y ⪯ x) so that

M |= Eσ if σ M ̸ = ∅ → M := → and ◁ M := ◁ a M := {e ∈ E | λ(e) = a} test(σ) M := {(e, e) | e ∈ σ M } ⟨π⟩σ M := {e ∈ E | ∃f ∈ σ M : (e, f ) ∈ π M } jump M := E × E Loop⟨π⟩ M := {e ∈ E | (e, e) ∈ π M } π 1 + π 2 M := π 1 M ∪ π 2 M π -1 M := {(e, f ) ∈ E × E | (f, e) ∈ π M } π * M := n∈N π n M π 1 • π 2 M := {(e, f ) ∈ E × E | ∃g ∈ E : (e, g) ∈ π 1 M and (g, f ) ∈ π 2 M } Figure 3 Semantics of LCPDL
we have L(φ mb ) = MSC mb . Here, x ⪯ y is obtained as the MSO-definable reflexive transitive closure of the union of the MSO-definable relations →, ◁, and ⊏. In particular, we may define x ⊏ y by

x ⊏ y = q∈P a,b∈Send( ,q, ) λ(x) = a ∧ λ(y) = b ∧ matched(x) ∧ ¬matched(y) ∨ ∃x ′ .∃y ′ .(x ◁ x ′ ∧ y ◁ y ′ ∧ x ′ → + y ′ ) .
Propositional Dynamic Logic (PDL). For better complexity, we also consider PDL with Loop and Converse, henceforth called LCPDL (cf. [START_REF] Bollig | Communicating finite-state machines, firstorder logic, and star-free propositional dynamic logic[END_REF][START_REF] Bollig | Non-sequential theory of distributed systems[END_REF]27] for more details). Its syntax is:

Φ ::= Eσ | Φ ∨ Φ | ¬Φ (sentence) σ ::= a | σ ∨ σ | ¬σ | ⟨π⟩σ | Loop⟨π⟩ (event formula) π ::= → | ◁ | test(σ) | jump | π + π | π • π | π * | π -1 (path formula)
where a ∈ Σ. We use the symbol ⊤ to denote a tautology event formula (such as a ∨ ¬a).

We describe the semantics for the logic in Fig. 3 (apart from the obvious cases). A sentence Φ is evaluated wrt. an MSC M = (E, →, ◁, λ). An event formula σ is evaluated wrt. M and an event e ∈ E so that it defines a unary relation σ M ⊆ E. Finally, a path formula π is evaluated over two events, and so it defines a binary relation π M ⊆ E × E. Finally, we let L(Φ) = {M ∈ MSC | M |= Φ}. Note that every LCPDL-definable property is MSO-definable.

It can be seen below that the mailbox semantics can be readily translated into the LCPDL formula Φ mb = ¬E (Loop⟨(◁ + → + ⊏) + ⟩) such that L(Φ mb ) = MSC mb . Hereby, we let

⊏ = ◁ • → + • ◁ -1 + q∈P a,b∈Send( ,q, ) test(a) • ◁ • jump • test(b ∧ ¬⟨◁⟩⊤) .
Special Tree-Width. Special tree-width [START_REF] Courcelle | Special tree-width and the verification of monadic second-order graph properties[END_REF], is a graph measure that indicates how close a graph is to a tree (we may also use classical tree-width instead). This or similar measures are commonly employed in verification. For instance, tree-width and split-width have been used in [26] and, respectively, [START_REF] Aiswarya | Verifying communicating multi-pushdown systems via split-width[END_REF][START_REF] Cyriac | MSO decidability of multi-pushdown systems via split-width[END_REF] to reason about graph behaviors generated by pushdown and queue systems. There are several ways to define the special tree-width of an MSC. We adopt the following game-based definition from [START_REF] Bollig | Non-sequential theory of distributed systems[END_REF].

Adam and Eve play a two-player turn based "decomposition game" whose positions are MSCs with some pebbles placed on some events. More precisely, Eve's positions are marked MSC fragments (M, U ), where M = (E, →, ◁, λ) is an MSC fragment (an MSC with possibly some edges from ◁ or → removed) and U ⊆ E is the subset of marked events. Adam's positions are pairs of marked MSC fragments. A move by Eve consists in the following steps:

1. marking some events of the MSC resulting in (M, U ′ ) with U ⊆ U ′ ⊆ E, 2. removing (process and/or message) edges whose endpoints are marked, 3. dividing (M, U ) in (M 1 , U 1 ) and (M 2 , U 2 ) such that M is the disjoint (unconnected) union of M 1 and M 2 and marked nodes are inherited.

When it is Adam's turn, he simply chooses one of the two marked MSC fragments. The initial position is (M, ∅) where M is the (complete) MSC at hand. A terminal position is any position belonging to Eve such that all events are marked. For k ∈ N, we say that the game is k-winning for Eve if she has a (positional) strategy that allows her, starting in the initial position and independently of Adam's moves, to reach a terminal position such that, in every single position visited along the play, there are at most k + 1 marked events.

▶ Fact 1 ([7]). The special tree-width of an MSC is the least k such that the associated game is k-winning for Eve.

The set of MSCs whose special tree-width is at most k is denoted by MSC k-stw .

Model Checking

In general, even simple verification problems, such as control-state reachability, are undecidable for communicating systems [START_REF] Brand | On communicating finite-state machines[END_REF]. However, they are decidable when we restrict to behaviors of bounded special tree-width, which motivates the following definition of a generic bounded model-checking problem for com ∈ {p2p, mb}: Input: Two finite sets P and M, a communicating system S, an MSO sentence φ, and k ∈ N (given in unary).

Question:

Do we have L com (S) ∩ MSC k-stw ⊆ L(φ)? ▶ Fact 2 ([7]
). The bounded model-checking problem for com = p2p is decidable. When the formulas φ are from LCPDL, then the problem is solvable in exponential time.

Note that [START_REF] Bollig | Non-sequential theory of distributed systems[END_REF] does not employ the LCPDL modality jump, but it can be integrated easily. Using φ mb or Φ mb , we obtain the corresponding result for mailbox systems as a corollary:

▶ Theorem 8. The bounded model-checking problem for com = mb is decidable. When the formulas φ are from LCPDL, then the problem is solvable in exponential time.

Synchronizability

The above model-checking approach is incomplete in the sense that a positive answer does not imply correctness of the whole system. The system may still produce behaviors of special tree-width greater than k that violate the given property. However, if we know that a system only generates behaviors from a class whose special tree-width is bounded by k, we can still conclude that the system is correct.

This motivates the synchronizability problem. Several notions of synchronizability have been introduced in the literature. However, they all amount to asking whether all behaviors generated by a given communicating system have a particular shape, i.e., whether they are all included in a fixed (or given) set of MSCs C. Thus, the synchronizability problem is essentially an inclusion problem, namely L p2p (S) ⊆ C or L mb (S) ⊆ C. We show that, for decidability, it is enough to have that C is MSO-definable and special-tree-width-bounded An important component of the decidability proof is the following lemma, which shows that we can reduce synchronizability wrt. an STW-bounded class to bounded model-checking.

(STW-bounded): We call C ⊆ MSC (i) MSO-definable if there is an MSO-formula φ such that L(φ) = C, (ii) LCPDL-definable if there is an an LCPDL-formula Φ such that L(Φ) = C, (iii) STW-bounded if there is k ∈ N such that C ⊆ MSC k-stw .
▶ Lemma 9. Let S be a communicating system, com ∈ {p2p, mb}, k ∈ N, and C ⊆ MSC k-stw . Then, L com (S) ⊆ C iff L com (S) ∩ MSC (k+2)-stw ⊆ C.
The result follows from the following lemma. Note that a similar property was shown in [START_REF] Genest | On communicating automata with bounded channels[END_REF]Proposition 5.4] for the specific class of existentially k-bounded MSCs.

▶ Lemma 10. Let k ∈ N and C ⊆ MSC k-stw . For all M ∈ MSC \ C, we have (Pref (M ) ∩ MSC (k+2)-stw ) \ C ̸ = ∅.
We now have all ingredients to state a generic decidability result for synchronizability: ▶ Theorem 11. Fix finite sets P and M. Suppose com ∈ {p2p, mb} and let C ⊆ MSC be an MSO-definable and STW-bounded class (over P and M). The following problem is decidable: Given a communicating system S, do we have L com (S) ⊆ C?

Proof. Consider the MSO-formula φ such that L(φ) = C, and let k ∈ N such that C ⊆ MSC k-stw . We have L com (S) ⊆ C Lemma 9 ⇐⇒ L com (S) ∩ MSC (k+2)-stw ⊆ C ⇐⇒ L com (S) ∩ MSC (k+2)-stw ⊆ L(φ)
. The latter can be solved thanks to Fact 2 and Theorem 8. ◀ ▶ Remark 12. Note that, in some cases (cf. Section 4), P and M are part of the input and the concrete class C may be parameterized by a natural number so that it is part of the input, too. Then, we need to be able to compute the MSO formula characterizing the class as well as the bound on the special tree-width.

Application to Concrete Classes of Synchronizability

In this section, we instantiate our general framework by specific classes. Table 1 gives a summary of the results.

A New General Class: Weakly Synchronous MSCs

We first introduce the class of weakly synchronous MSCs. This is a generalization of synchronous MSCs studied earlier, in [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF][START_REF] Di Giusto | On the k-synchronizability of systems[END_REF], which we shall discuss later. We say an MSC is weakly synchronous if it is breakable into exchanges where an exchange is an MSC that allows one to schedule all sends before all receives. Let us define this formally:

▶ Definition 13 (exchange). Let M = (E, →, ◁, λ) be an MSC. We say that M is an exchange if SendEv(M ) is a ≤ M -downward-closed set.
▶ Definition 14 (weakly synchronous). We say that

M ∈ MSC is weakly synchronous if it is of the form M = M 1 • . . . • M n such that every M i is an exchange.
We use the term weakly to distinguish from variants introduced later.

▶ Example 15. Consider the MSC M 2 in Fig. 4. It is is weakly synchronous. Indeed, m 1 , m 2 , and m 5 are independent and can be put alone in an exchange. Repetitions of m 3 and m 4 are interlaced, but they constitute an exchange, as we can do all sends and then all receptions.

An easy adaptation of a characterization from [START_REF] Di Giusto | On the k-synchronizability of systems[END_REF] yields the following result for weakly synchronous MSCs: It is easily seen that the characterization from Proposition 16 is LCPDL-definable: Proof. Let M be fixed, and let us sketch Eve's winning strategy. Let n = |P|. The first step for Eve is to split M in exchanges. She first disconnects the first exchange from the rest of the graph (2n pebbles are needed), then she disconnects the second exchange from the rest of the graph (2n pebbles needed, plus n pebbles remaining from the first round), and so on for each exchange.

q r p m 1 m 2 m 3 m 3 m 4 m 4
▶
So we are left with designing a winning strategy for Eve with 4n + 1 pebbles on the graph of an exchange M 0 , where initially there are (at most) n pebbles placed on the first event of each process and also (at most) n pebbles placed on the last event of each process. Eve also places (at most) n pebbles on the last send event of each process and also (at most) n pebbles on the first receive event of each process. Eve erases the (at most) n →-edges between the last send event and the first receive event.

We are now in a configuration that will be our invariant.

Let us fix a mailbox linearization of M 0 and let e be the first send event in this linearization.

if e is an unmatched send of process p, Eve places her last pebble on the next send event of p (if it exists), let us call it e ′ . Then Eve erases the →-edge (e, e ′ ), and now e is completely disconnected, so it can be removed and the pebble can be taken back. if e ◁ e ′ , with e ′ a receive event of process q, then due to the mailbox semantics e ′ is the first receive event of q, so it has a pebble placed on it. Eve removes the ◁-edge between e and e ′ , then using the extra pebble she disconnects e and places a pebble on the →-successor of e, then she also disconnects e ′ and places a pebble on the →-successor of e ′ .

After that, we are back to our invariant, so we can repeat the same strategy with the second send event of the linearization, and so on until all edges have been erased. ◀

We obtain the following result as a corollary. Note that it assumes the mailbox semantics.

▶ Theorem 19. The following problem is decidable in exponential time: Given P, M, and a communicating system S (over P and M), is every MSC in L mb (S) weakly synchronous?

Proof. According to Corollary 17, we determine the LCPDL formula Φ wsmb such that L(Φ wsmb ) is the set of weakly synchronous mailbox MSCs. Moreover, recall from Proposition 18 that the special tree-width of all weakly synchronous mailbox MSCs is bounded by 4|P|. By Lemma 9, L mb (S) ⊆ L(Φ wsmb ) iff L mb (S) ∩ MSC (4|P|+2)-stw ⊆ L(Φ wsmb ). The latter is an instance of the bounded model-checking problem. As the length of Φ wsmb is polynomial in |P|, we obtain that the original problem is decidable in exponential time by Theorem 8. ◀

For the same reasons, the model-checking problem for "weakly synchronous" systems is decidable. Interestingly, a reduction from Post's correspondence problem shows that decidability fails when adopting the p2p semantics:

▶ Theorem 20. The following problem is undecidable: Given finite sets P and M as well as a communicating system S, is every MSC in L p2p (S) weakly synchronous?

Weakly k-Synchronous MSCs

This negative result for the p2p semantics motivates the study of other classes. In fact, our framework captures several classes introduced in the literature.

▶ Definition 21 (k-exchange). Let M = (E, →, ◁, λ) be an MSC and k ∈ N. We call M a k-exchange if M is an exchange and |SendEv(M )| ≤ k.
Let us now recall the definition from [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF][START_REF] Di Giusto | On the k-synchronizability of systems[END_REF], but (equivalently) expressed directly in terms of MSCs rather than via executions. It differs from the weakly synchronous MSCs in that here, we insist on constraining the number of messages sent per exchange to be at most k.

▶ Definition 22 (weakly k-synchronous). Let k ∈ N. We say that M ∈ MSC is weakly k-synchronous if it is of the form M = M 1 • . . . • M n such that every M i is a k-exchange.
▶ Example 23. MSC M 3 in Fig. 5 is weakly 1-synchronous, as it can be decomposed into three 1-exchanges (the decomposition is depicted by the horizontal dashed lines). We remark that M 3 ∈ MSC mb . Note that there is a p2p linearization that respects the decomposition. On the other hand, a mailbox linearization needs to reorganize actions from different MSCs: the sending of m 3 needs to be done before the sending of m 1 . Note that M 1 in Fig. 1 is also weakly 1-synchronous. In fact, MSO-definability essentially follows from the following known theorem: ▶ Theorem 25 ([14]). Let M be an MSC. Then, M is weakly k-synchronous iff every SCC in its conflict graph CG(M ) is of size at most k and no RS edge occurs on any cyclic path. This property is similar to the graphical characterization of weakly synchronous MSCs, except for the condition that every SCC in the conflict graph is of size at most k. Furthermore, it is easy to establish a bound on the special tree-width: ▶ Proposition 26. Let k ∈ N. The set of MSCs that are weakly k-synchronous have special tree-width bounded by 2k + |P|.

Hence, we can conclude that the class of weakly k-synchronous MSCs is MSO-definable and STW-bounded. As a corollary, we get the following (known) decidability result, but via an alternative proof:

▶ Theorem 27 ([8, 14]). For com ∈ {p2p, mb}, the following problem is decidable: Given finite sets P and M, a communicating system S, and k ∈ N, is every MSC in L com (S) weakly k-synchronous?

Proof. We proceed similarly to the proof of Theorem 19. For the given P, M, and k, we first determine, using Proposition 24, the MSO formula φ k such that L(φ k ) is the set of weakly k-synchronous p2p/mailbox MSCs. From Proposition 26, we know that the special tree-width of all weakly k-synchronous MSCs is bounded by 2k + |P|. By Lemma 9, we have

L com (S) ⊆ L(φ k ) iff L com (S) ∩ MSC (2k+|P|+2)-stw ⊆ L(φ k ).
The latter is an instance of the bounded model-checking problem. By Fact 2 and Theorem 8, we obtain decidability. ◀ ▶ Remark 28. The set of weakly k-synchronous MSCs is not directly expressible in LCPDL (the reason is that LCPDL does not have a built-in counting mechanism). However, its complement is expressible in the extension of LCPDL with existentially quantified propositions (we need k + 1 of them). The model-checking problem for this kind of property is still in EXPTIME and, therefore, so is the problem from Theorem 27 when k is given in unary. It is very likely that our approach can also be used to infer the PSPACE upper bound from [START_REF] Bouajjani | On the completeness of verifying message passing programs under bounded asynchrony[END_REF] by showing bounded path width and using finite word automata instead of tree automata. Finally, note that the problem to decide whether there exists an integer k ∈ N such that all MSCs in L com (S) are weakly k-synchronous has recently been studied in [20] and requires different techniques.

Observe also that we can remove the constraint of all the sends preceding all the receives in a k-exchange, and still have decidability. We then have the following definition.

▶ Definition 29 (modified k-exchange). Let M = (E, →, ◁, λ) be an MSC and k ∈ N. We call M a modified k-exchange if |SendEv(M )| ≤ k.
We extend this notion to consider modified weakly k-synchronous executions as before, and the graphical characterization of this property is that there are at most k nodes in every SCC of the conflict graph. Hence, this class is also MSO-definable, and since each modified k-exchange has at most 2k events, it also has bounded special tree-width.

Strongly k-Synchronous MSCs and Other Classes

Our framework can be applied to a variety of other classes. Here we show how the decidability results can be shown for a variant of the class of weakly k-synchronous MSCs.

▶ Definition 30. Let M = (E, →, ◁, λ) ∈ MSC mb . We call M strongly k-synchronous if it can be written as M = M 1 •. . .•M n such that every MSC M i = (E i , → i , ◁ i , λ i ) is a k-exchange
and, for all (e, f ) ∈ ⊏ M , there are 1 ≤ i ≤ j ≤ n such that e ∈ E i and f ∈ E j .

▶ Example 31. MSC M 4 ∈ MSC mb in Fig. 6 is strongly 1-synchronous. Indeed, we can decompose it into 1-exchanges and this decomposition allows for a total order compatible with ⊏ M4 . Moreover, MSC M 3 in Fig. 5, which is weakly 1-synchronous, is strongly 3-synchronous. Indeed, we need to put the three messages in the same k-exchange to regain our total order. Finally, for all k, MSC M 1 in Fig. 1 is not strongly k-synchronous, as we cannot put all messages in the same k-exchange, where all sends are followed by all receptions. Here, this is not possible as the reception of m 3 has to take place before the sending of m 4 . The proof proceeds similarly to what has been shown in the previous cases, but MSOdefinability now relies on an extended conflict graph. As a corollary, we thus obtain:

▶ Theorem 33. The following problem is decidable: Given finite sets P and M, a communicating system S, and k ∈ N, is every MSC in L mb (S) strongly k-synchronous? ▶ Remark 34. Only mailbox MSCs are considered for the definition of strongly k-synchronous MSCs for the following reason: A natural p2p analogue of Definition 30 would require from the decomposition that, for all (e, f ) ∈ ≤ M , there are indices 1 ≤ i ≤ j ≤ n such that e ∈ E i and f ∈ E j . But this is always satisfied. So the natural definition of "strongly k-synchronous MSCs" would coincide with weakly k-synchronous MSCs.

Like the variant for the case of weakly synchronous MSCs, we can also generalize strongly k-synchronous MSCs by removing the restriction on the number of messages per exchange:

▶ Definition 35. Let M = (E, →, ◁, λ) ∈ MSC mb . We call M strongly synchronous if it can be written as M = M 1 • . . . • M n such that every MSC M i = (E i , → i , ◁ i , λ i
) is an exchange and, for all (e, f ) ∈ ⊏ M , there are indices 1 ≤ i ≤ j ≤ n such that e ∈ E i and f ∈ E j .

Similarly to the constructions for strongly k-synchronous MSCs, we can obtain a graphical characterization where we only look for the absence of RS-edges in a cycle. Hence, this class is also MSO-definable (in fact, even LCPDL-definable) and STW-bounded.

Existentially k-Bounded MSCs

Now, we turn to existentially k-bounded MSCs [START_REF] Genest | On communicating automata with bounded channels[END_REF][START_REF] Genest | A kleene theorem for a class of communicating automata with effective algorithms[END_REF]24]. Synchronizability has been studied for the p2p case in [START_REF] Genest | On communicating automata with bounded channels[END_REF], so we only consider the mailbox case here. A linearization ⇝ of an MSC M = (E, →, ◁, λ) ∈ MSC is called k-mailbox-bounded if, for all e ∈ Matched(M ), say with λ(e) = send(p, q, m), we have # Send( ,q, ) (⇝, e) -# Rec( ,q, ) (⇝, e) ≤ k .

▶ Definition 36. Let M = (E, →, ◁, λ) ∈ MSC and k ∈ N. We call M existentially k- mailbox-bounded if it has some mailbox linearization that is k-mailbox-bounded.
Note that every existentially k-mailbox-bounded MSC is a mailbox MSC.

▶ Example 37. MSC M 5 in Fig. 7 is existentially 1-mailbox-bounded, as witnessed by the (informally given) linearization s(q, p, m 2 ) ⇝ s(p, q, m 1 ) ⇝ s(q, r, m 3 ) ⇝ r(q, r, m 3 ) ⇝ r(p, q, m 1 ) ⇝ s(p, q, m 1 ) ⇝ r(q, p, m 2 ) ⇝ s(q, r, m 3 ) . . . Note that M 5 is neither weakly nor strongly synchronous as we cannot divide it into exchanges. This extension is also valid for the p2p definition of existentially k-bounded MSCs, which were addressed in [START_REF] Genest | On communicating automata with bounded channels[END_REF]. Finally, our framework can also be adapted to treat universally bounded systems [21, 24].

Relations Between Classes

In this section we study how the classes introduced and recalled so far are related to each other. Notably, depending on the semantics (p2p or mailbox), we obtain two different classifications. The results are summed up in Figures 8 and9. Here, we define existentially k-p2p-bounded MSCs and universally bounded counterparts as expected (formal definitions are available in Appendices C.8 and C.9).

To refer to those systems we use the following terminology: a system S is called weakly synchronizable (resp. strongly synchronizable) if all MSCs M in the respective language are weakly synchronous (resp. strongly synchronous). A system is called weakly k-synchronizable (resp. strongly k-synchronizable, existentially bounded or universally bounded) if all MSCs are weakly k-synchronous (resp. strongly k-synchronous, existentially k-bounded or universally k-bounded). A similar comparison relating existentially bounded systems, weakly k-synchronizable systems, as well as other systems that have not been described here, can also be found in [23] for p2p systems.

We give some results showing the inclusion of certain classes. Recall that strong ksynchronizability is tailored to mailbox systems (cf. also Remark 34) so that, for p2p systems, we only consider the case of weak (k-)synchronizability.

▶ Proposition 39. Every weakly k-synchronous MSC is existentially k-p2p-bounded. Moreover, every strongly k-synchronous mailbox MSC is existentially k-mailbox-bounded.

Finally, if a system is weakly synchronizable and universally k-bounded then, there is a k ′ such that it is also weakly k ′ -synchronizable. The equivalent property is also valid for strong classes.

▶ Proposition 40. Every weakly (resp. strongly) synchronizable and universally k-bounded system is weakly (resp. strongly) k ′ -synchronizable for a k ′ .

Conclusion and Perspectives

We have presented a unifying framework based on MSO logic and (special) tree-width, that brings together existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability. Let us notice that the send-synchronizability does not fit in our framework because the question L p2p (S) ⊆ C 0 would be decidable (by Theorem 11), where C 0 is the set of send-synchronizable MSCs, but this property is equivalent to checking whether the system S is send-synchronizable and this last property is undecidable [START_REF] Finkel | Synchronizability of communicating finite state machines is not decidable[END_REF].

Many other related questions could be studied in the future. For example, we could think about the hypotheses to add to our general framework to make the problem "does there exist an k ≥ 0 such that L p2p (S) ⊆ C k ?" decidable. From very recent work [20], one knows that the problem "does there exist an k ≥ 0 such that the system is (weakly/strongly) k-synchronizable?" is decidable; but it remains to be seen if it would be possible to obtain these results by showing that these properties can be expressed in a decidable extension of our framework. Let us remark that the decidability of the question whether there exists an k ≥ 0 such that L p2p (S) ⊆ C k allows us to build a bounded model checking strategy by first deciding whether there exists such an k ≥ 0 and then by testing if L p2p (S) ⊆ C k for k = 0, 1, 2 . . . . One may use this strategy for weakly/strongly synchronizable systems, but not for existentially bounded systems (except for deadlock-free systems) or for deterministic deadlock-free universally bounded systems. In [23], Lange and Yoshida introduced an asynchronous compatibility property and it would also be interesting to verify whether this property could be expressed into our framework.

Auckland, New Zealand, December [START_REF] Cyriac | MSO decidability of multi-pushdown systems via split-width[END_REF][START_REF] Di Giusto | On the k-synchronizability of systems[END_REF][START_REF] Esparza | A perfect model for bounded verification[END_REF][START_REF] Finkel | Synchronizability of communicating finite state machines is not decidable[END_REF][START_REF] Finkel | Verification of Flat FIFO Systems[END_REF]2004

A Proof for Section 2

A.1 Proof of Lemma 3

▶ Lemma 3. Every prefix of a mailbox MSC is a mailbox MSC.

Proof. Let M = (E, →, ◁, λ) ∈ MSC mb and M 0 = (E 0 , → 0 , ◁ 0 , λ 0 ) be a prefix of M , i.e., E 0 ⊆ E. By contradiction, suppose that M 0 is not a mailbox MSC. Then, there are distinct e, f ∈ E 0 such that e Proof. Using the mailbox semantics and the MSO formula φ mb , we get

⪯ M0 f ⪯ M0 e with ⪯ M0 = (→ 0 ∪ ◁ 0 ∪ ⊏ M0 ) * . As E 0 ⊆ E, we have that → 0 ⊆ →, ◁ 0 ⊆ ◁,
L mb (S) ∩ MSC k-stw ⊆ L(φ) ⇐⇒ L p2p (S) ∩ MSC k-stw ∩ L(φ mb ) ⊆ L(φ) ⇐⇒ L p2p (S) ∩ MSC k-stw ⊆ L(φ ∨ ¬φ mb ) .
The latter is decidable due to Fact 2. Similarly, we can use the LCPDL formula Φ mb , whose size is polynomial in the number of processes and messages. ◀ We obtain such an MSC by successively removing maximal events. If M ′ is the empty MSC, we are done, since then M ′ ∈ (Pref (M ) ∩ MSC k+2-stw ) \ C. Otherwise, let e be ≤ M ′ -maximal and let M ′′ = M ′ \ {e}.

Since M ′ was taken minimal in terms of number of events, M ′′ ∈ C. So Eve has a winning strategy with k + 1 pebbles for M ′′ . Let us design a winning strategy with k + 3 pebbles for Eve for M ′ , which will show the claim.

Observe that the event e occurs at the end of the timeline of a process (say p), and it is part of at most two edges: one with the previous p-event (if any) one with the corresponding send event (if e is a receive event)

Let e 1 , e 2 be the two neighbors of e. The strategy of Eve is the following: in the first round, mark e, e 1 , e 2 , then erase the edges (e 1 , e) and (e 2 , e), then split the remaining graph in two parts: M ′′ on the one side, and the single node graph {e} on the other side. Then Eve applies its winning strategy for M ′′ , except that initially the two events e 1 , e 2 are marked (so she may need up to k + 3 pebbles). ◀

C Proofs for Section 4

C.1 Proof of Proposition 16

▶ Proposition 16. Let M be an MSC. Then, M is weakly synchronous iff no RS edge occurs on any cyclic path in the conflict graph CG(M ).

Proof. =⇒ Let M be an MSC. If M is weakly synchronous, then M = M 1 • . . . • M n such that every M i is an exchange. Hence, for every vertex v of the conflict graph, there is exactly one index ι(v) ∈ {1, . . . , n} such that ∃λ -1 (e) ∈ M ι (v) , where e ∈ Send( , , v). Note that if there is an edge from v to v ′ in the conflict graph, some action of v must happen before some action of v ′ , i.e., ι(v

) ≤ ι(v ′ ). Furthermore, note that if v RS --→ v ′ , then ι(v) < ι(v ′
), since within an exchange all the sends precede all the receives. So an RS edge cannot occur on a cyclic path.

⇐= Let M be an MSC. We assume now that the conflict graph of M does not contain a cyclic path with an RS edge. Let V 1 , . . . , V n be the set of maximal SCCs of the conflict graph, listed in some topological order. For a fixed i, let M i = s 1 . . . s m r 1 . . . r m ′ be the enumeration of the actions of the message exchanges of V i defined by first taking all send actions of V i obeying the relation ≤ M , and then all the receive actions of V i in the same order as in ≤ M . Let M ′ = M 1 . . . M n . Then the conflict graph of M ′ is the same as that of M , as the permutation of actions we defined could only postpone a receive after a send of a same SCC, therefore it could only replace some v RS --→ v ′ edge with an v SR --→ v ′ edge between two vertices v, v ′ of a same SCC. However, since we assumed that the cycles (hence by extensions SCCs) do not contain RS edges, this cannot happen. Therefore M and M ′ have the same conflict graph, and correspond to the same MSC. Furthermore, since each M i is a downward-closed set, M ′ is weakly synchronous, and so is M . ◀

C.2 Proof of Corollary 17

▶ Corollary 17. The sets of weakly synchronous MSCs and weakly synchronous mailbox MSCs are LCPDL-definable. Both formulas have polynomial size.

Proof. LCPDL can be used to express the graphical characterization of weakly synchronous MSCs. This follows from the formulas below. Here, we let R = a∈Rec( , , ) a.

SS --→ = test(¬R)• → + •test(¬R) RR --→ = test(¬R) • ◁• → + • ◁ -1 •test(¬R) RS --→ = test(¬R) • ◁• → + •test(¬R) SR --→ = test(¬R)• → + • ◁ -1 •test(¬R) CG --→ = ( SS --→ + RR --→ + RS --→ + SR --→)
The absence of RS edges in any cycle in the conflict graph can be expressed by the following formula:

Φ wsync = ¬Loop⟨( CG --→) * • RS --→ •( CG --→) * ⟩ ◀ C.

Proof of Theorem 20

▶ Theorem 20. The following problem is undecidable: Given finite sets P and M as well as a communicating system S, is every MSC in L p2p (S) weakly synchronous?

Proof. We show that the control state reachability problem for p2p weakly synchronizable systems is not decidable. This immediately shows that the model-checking problem for p2p weak synchronizable systems is not decidable. With some extra coding, it also shows that the membership problem (decide whether a given system is p2p weakly synchronizable) also is undecidable: indeed, it is enough to add a non weak synchronizable behavior after the control states for which reachability is undecidable: the system will be not weakly synchronizable iff the control states are reached. We reduce from Post correspondence problem (PCP). Let us recall that a PCP instance consists of N pairs (u i , v i ) of finite words over an alphabet A, and that PCP undecidability holds already for N = 7 and A = {0, 1}. We let the set of messages be {1, . . . , N } ⊎ A ⊎ {♯}, and we consider a system with four machines: Prover1, Prover2, Verifier1, and Verifier2. We have unidirectional communication channels from provers to verifiers, so the system is weakly synchronous by construction.

Informally, the system works as follows:

Prover1 guesses a solution u i1 . . . u im of the PCP instance, and Prover2 also guesses the same solution v i1 ...v im .

Prover1 sends u i1 . . . u in to Verifier1 and sends simultaneously i 1 . . . i m to Verifier2

Prover2 sends v i1 . . . v im to Verifier1 and sends simultaneously i 1 . . . i m to Verifier 2

Verifier1 checks that the two words are equal and Verifier2 checks that the sequences of indices are equal.

Let us now formally define these machines. We describe them with regular expressions. For w = a 1 • • • a n , we write send * (p, q, w) (resp rec * (p, q, w)) for send(p, q, a 1 ) • • • send(p, q, a n ) (resp rec(p, q, a 1 ) • • • rec(p, q, a n )). We abbreviate Prover1 as P1, Prover2 as P2, Verifier1 as V1, and Verifier2 as V2 Prover1 is

N i=1 send(P 1 , V 1 , i)send * (P 1 , V 2 , u i ) + send(P 1 , V 1 , ♯)send(P 1 , V 2 , ♯) Prover2 is N i=1 send(P 2 , V 1 , i)send * (P 2 , V 2 , v i ) + send(P 2 , V 1 , ♯)send(P 2 , V 2 , ♯) Verifier1 is N i=1 rec(P 1 , V 1 , i)rec(P 2 , V 1 , i) * rec(P 1 , V 1 , ♯)rec(P 2 , V 1 , ♯) Verifier2 is a∈Σ rec(P 1 , V 2 , a)rec(P 2 , V 2 , a) * rec(P 1 , V 2 , ♯)rec(P 2 , V 2 , ♯)
It can be checked that all machines reach their own final state if and only if the PCP instance has a solution. ◀

C.4 Proof of Proposition 24

▶ Proposition 24. Let k ∈ N. The set of weakly k-synchronous p2p (mailbox, respectively) MSCs is effectively MSO-definable.

Proof. The formula for the property that there is no strongly connected component of size greater than k in the conflict graph is as follows: Proof. Let M be a k-synchronous MSC. By definition, we know that

M = M 1 • . . . • M n such that every M i is a k-exchange.
Eve's strategy is to mark the vertices belonging to the set M 1 . Hence, she marks at most 2k vertices. We can remove the edges between these vertices. Let the new marked MSC fragment be (G, U ), where G is the new MSC fragment (with the edges between marked vertices removed), and U the set of marked vertices.

Notice that |U | ≤ 2k. Furthermore, since every vertex corresponding to a send message in U is either unmatched or matched with a reception in U (by definition), we can be sure that there are no message edges between vertices of U and any other vertex. Moreover, we can also be sure that there are at most |P| process edges between vertices in U and vertices outside this set. Let us mark these |P| vertices. We call these vertices U ′ . Let the new marked MSC fragment be (G ′ , U ∪ U ′ ), where G ′ is the new MSC fragment (with the edges between all vertices in U ∪ U ′ removed). Now, we see that there are no edges between any of the vertices in U and any other vertex, i.e. all the vertices in U are isolated. We can divide the MSC fragment to consist of the vertices U and V \ U and the corresponding edges.

Let the MSC fragment with vertices in U be (G 1 , U 1 ). It consists of at most 2k isolated colored vertices. Let the MSC fragment with vertices in V \ U be (G 2 , U 2 ). We observe that |U 2 | = n. Adam trivially loses if he chooses (G 1 , U 1 ), hence, he has to choose (G 2 , U 2 ). Now, we mark the vertices corresponding to M 2 , which are again, at most 2k. We have two possibilities for each vertex in U 2 , either they belong to the set M 2 or belong to another set M p where p > 2. However, if they belong to M p , we can be sure that there is no other event on the same process that belongs to M 2 -this is because it was the successor of some event in M 1 . Hence, we see once again, that marking all the vertices in M 2 and the immediate successors along each process will result in marked vertices of size at most 2k + |P|. And once again, we see that we can separate into MSC fragments (G ′ 1 , U ′ 1 ) and (G ′ 2 , U ′ 2 ) such that every vertex in U ′ 1 is isolated, and |U ′ 1 | ≤ 2k. We do this for all i ∈ [n], and hence, we can effectively use 2k + |P| colors. Therefore, set of MSCs over |P| processes which are k-synchronous have bounded special tree-width. ◀

C.6 Proof of Proposition 32

As was shown in [START_REF] Di Giusto | On the k-synchronizability of systems[END_REF], in order to capture the mailbox semantics, we need extended edges.

We recall from [START_REF] Di Giusto | On the k-synchronizability of systems[END_REF] the extended edge relation XY with X, Y ∈ {S, R} in Figure 10. We call the conflict graph along with the new extended edges the extended conflict graph (ECG). This graph is also used to characterize some classes of MSCs in Section 4.3. ▶ Theorem 41 (Graphical Characterization of strongly k-synchronous MSCs). Let M ∈ MSC mb . M is strongly k-synchronous iff every strongly connected component (SCC) in the ECG is of size at most k and no RS edge occurs on any cycle in the ECG.

v 1 XY --→ v 2 v 1 XY v 2 (Rule 1) v ∈ ◁ v SR v (Rule 2) v 1 RR --→ v 2 v 1 SS v 2 (Rule 3) v 1 XY Y Z v 2 v 1 XZ v 2 (Rule 4) e 1 ∈ Matched(M ) e 2 ∈ Unm(M ) e 1 ∈ Send(p 1 , q, ), e 2 ∈ Send(p 2 , q, ), p 1 , p 2 , q ∈ P µ(e 1 )
Proof. ( =⇒ ) Assume that we have an MSC M that is strongly k-synchronous. Hence, we can divide M = M 1 . . . M n such that each M i is a k-exchange. By contradiction, suppose that there is an SCC of size k ′ > k in ECG(M ). As there are at most k messages in each k-exchange, there are v, v ′ which belong to the SCC such that v ∈ M i and v ′ ∈ M j , 1 ≤ i < j ≤ n. Then, we have v * v ′ * v. By induction, we prove that v ′ * v implies that j ≤ i.

Base There are two cases.

Suppose that v ′ XY --→ v then an action of v ′ is done by the same process than an action of v and it is done before it. Then, j ≤ i.

Suppose that v ′ SS

v, built by Rule 5 (because others rules do not add any edges between vertices that are not already connected), then, v ′ is matched and v is unmatched, such that, v ∈ Send(q, p, v) and v ′ ∈ Send(q ′ , p, v ′ ), q, q ′ ∈ P. Then, the send of v ′ has to be done before the send of v and so j ≤ i.

Step By hypothesis, there is

v ′ * v 1 v such that v 1 ∈ M l , j ≤ l ≤ n.
There are also two cases.

Either v 1 XY --→ v. Then, an action of v 1 is done before and by the same process than an action of v. Then, l ≤ i and so j ≤ i.

Or v 1 SS v.
Then, similarly as before, v 1 has to be sent before v and so l ≤ i. Therefore, j ≤ i.

Finally, we have that v ′ * v implies that j ≤ i and so there is a contradiction. Now, we show that there is no RS edge in any SCC. By contradiction, suppose that we have v RS --→ v ′ * v in the extended conflict graph. Then, as proved before, v and v ′ have to be in the same M i , 1 ≤ i ≤ n. However, v RS --→ v ′ implies that the reception of v has to be done before the send of v ′ , but a k-exchange can, by definition, be linearized with all the sends followed by all the receptions. So we have a contradiction.

( ⇐= ) Conversely, assume that every SCC in the extended conflict graph of M is of size at most k and no RS edge occurs on any cyclic path in the ECG. Then, we first show that every SCC in the extended conflict graph is k-synchronous. Let C be an SCC formed of a set of nodes v 1 , • • • , v n , for some 1 ≤ n ≤ k such that s i ∈ Send( , , v i ), for all 1 ≤ i ≤ n. W.l.o.g., assume that the indexing of the nodes in C is consistent with the edges labeled by SS (note that there is no cycle formed only of edges labeled by SS), i.e., for every 1 ≤ i 1 < i 2 ≤ n, C doesn't contain an edge labeled by SS from i 2 to i 1 , and for every 1 ≤ i < j < k ≤ n, if s i , s k ∈ Send(p, , ) for p ∈ P then s j ∈ Send(p, , ). Let i 1 , • • • , i m be the maximal subsequence of 1, . . . , n such that r ℓ ∈ Rec( , , v i ) for every ℓ = i j where 1 ≤ j ≤ m. We have that C is the graph of the execution e

= s i1 • • • s in r i1 • • • r im .
The fact that all sends can be executed before the receives is a consequence of the fact that C doesn't contain edges labeled by RS. Then, the order between receives is consistent with the one between sends because C satisfies causal delivery. By definition, e is the label of an n-exchange transition, and therefore, C is strongly k-synchronous.

To complete the proof we proceed by induction on the number of strongly connected components of the extended conflict graph. The base case is for an MSC with a single SCC, which can be deduced from above. For the induction step, assume that the claim holds for every MSC whose extended conflict graph has at most n strongly connected components, and let M be a MSC with n + 1 strongly connected components. Let C be a strongly connected component of M such that C has no outgoing edges towards another strongly connected component of M . By the definition of the extended conflict-graph, M = M ′ • M ′′ is the MSC corresponding to the nodes of C. We have shown above that M ′′ is k-synchronous, and by the induction hypothesis, M ′ is also k-synchronous. As there is no outgoing edges from M ′′ , we know that all messages in it have not to be done before a message of M ′ . Therefore, M is strongly k-synchronous. ◀

For the extended conflict graph, we use the following MSO formulas to express the edge relation. For instance, the extended SR edge relation includes all SR edges along with the set of self loops around each message that ensures that the sends are before the corresponding receives.

ESR(e 1 , e 2 ) = SR(e 1 , e 2 ) ∨ (∃f 1 . [e 1 ◁ f 1 ∧ (e 1 = e 2 )])
Similarly, the extended send edge relation includes the SS edges along with the edges produced from Rule 3 and Rule 5.

ESS(e 1 , e 2 ) = SS(e 1 , e 2 ) ∨ RR(e 1 , e 2 ) ∨ ∃f 1 . [e 1 ◁ f 1 ∧ ∄f 2 . [e 2 ◁ f 2 ]] ∧ p,p ′ ,q∈P [(λ(e 1 ) = Send(p, q, ) ∧ λ(e 2 ) = Send(p ′ , q, ))]
The extended RR and RS edges are the same as in the conflict graph.

ERR(e 1 , e 2 ) = RR(e 1 , e 2 )

ERS(e 1 , e 2 ) = RS(e 1 , e 2 )

The transitive closure of each of these formulas is defined as follows. It essentially takes care of Rule 4. For all X, Y, Z ∈ {R, S}, we have:

EXY(e 1 , e 2 ) ∧ EYZ(e 2 , e 3 ) =⇒ EXZ * (e 1 , e 3 ) EXZ(e 1 , e 2 ) =⇒ EXZ * (e 1 , e 2 )

We then extend the rest of the results, as in the case of the conflict graph in the previous section.

And finally, for the condition of the bounded STW, we observe that the set of strongly k-synchronizable MSCs are included in the set of weakly k-synchronizable MSCs. Hence, the decomposition strategy as used for the weakly k-synchronizable MSCs can be applied to the set of strongly k-synchronizable MSCs.

Therefore, the family (C k ) k∈N is MSO-definable and STW-bounded.

C.7 Proof of Proposition 38

We define the following relation in order to characterize k-mailbox-bounded MSCs.

Let k ≥ 1, and let M be a fixed mailbox MSC. Let rev --→ k be the binary relation among events of M defined as follows:

r rev --→ k s if 1.
r is a receive event of a process p; 2. let r ′ be the k-th receive event of process p after r; then s ◁ r ′ .

▶ Lemma 42. M is existential k-mailbox-bounded if and only if ⪯

M ∪ rev --→ k is acyclic.
Proof. Assume that M is existential k-mailbox-bounded. Let ⇝ be a mailbox linearisation of M such that for all e ∈ Matched(M ), say with λ(e) = send(p, q, m),

# Send(-,q, ) (⇝, e) -# Rec(-,q, ) (⇝, e) ≤ k .
Then ⇝ is also a linearisation of (⪯ M ∪ rev --→ k ) * . Indeed, if it was not the case, there would be a pair of events r, s such that r rev --→ k s and s ⇝ r. But then we would have # Send(-,q, ) (⇝, s) -# Rec(-,q, ) (⇝, s) > k , and the contradiction. So ⇝ is a linearisation of (⪯ M ∪ rev --→ k ) * and ⪯ M ∪ rev --→ k is acyclic. Conversely, assume that ⪯ M ∪ rev --→ k , and let ⇝ be a linearisation of (⪯ M ∪ rev --→ k ) * . In particular, ⇝ is a mailbox linearisation of M . Let us show that for all s ∈ Matched(M ), say with λ(s) = send(p, q, m),

# Send(-,q, ) (⇝, s) -# Rec(-,q, ) (⇝, s) ≤ k .
Let s ∈ Matched(M ) be fixed, and let r ′ be such that s ◁ r ′ . There are two cases:

# Rec(-,q, ) (→, r ′ ) ≤ k. Then # Send(-,q, ) (⇝, s) ≤ k ,
because all sends before s are matched. So # Send(-,q, ) (⇝, s) -# Rec(-,q, ) (⇝, s) ≤ k , # Rec(-,q, ) (→, r ′ ) ≤ k. Then there is r on process q such that r rev --→ k s. So r ⇝ s, and there are at most k messages in the buffer of q at the time of event s, or in other words, # Send(-,q, ) (⇝, e) -# Rec(-,q, ) (⇝, e) ≤ k . Finally, let us show that existentially k-mailbox-bounded is also LCPDL definable. This follows from the following formulas:

≺ M = (◁+ →) + R = ⟨◁ -1 ⟩⊤ next R ----→= (→ ∧test(¬R)) * • (→ ∧test(R)) rev --→ k = ( next R ----→) k .(◁) -1 . Φ ∃k mb-bounded = ¬ELoop⟨(≺ M + rev --→ k ) + ⟩ ◀ C.8 Existentially k-p2p-bounded MSCs ▶ Definition 43. Let M = (E, →, ◁, λ) ∈ MSC and k ∈ N. A linearization ⇝ of M is called k-p2p-bounded if,
for all e ∈ Matched(M ), say with λ(e) = send(p, q, m), # Send(p,q, ) (⇝, e) -# Rec(p,q, ) (⇝, e) ≤ k ,

We call M existentially k-p2p-bounded if it has some p2p linearization that is k-p2pbounded, ▶ Proposition 44. For all k ∈ N, the set of existentially k-p2p-bounded MSCs is MSOdefinable and STW-bounded.

Proof. The set of existentially k-p2p-bounded MSCs was shown to be MSO-definable (in fact, even FO-definable) in [25]. Note that there are minor differences in the definitions (in particular, the fact that we deal with unmatched messages), which, however, do not affect FO-definability. In [7, Proposition 5.4, page 163], it was shown that their special tree-width is bounded by k|P| 2 + |P|. ◀ ▶ Theorem 45. For com ∈ {p2p, mb}, the following problem is decidable: Given finite sets P and M, a communicating system S, and k ∈ N, is every MSC in L com (S) existentially k-p2p-bounded?

Proof. Again, the proof follows exactly the same lines as that or Theorem 27, now using Proposition 44. ◀

Note that this is similar to the problem considered in [START_REF] Genest | On communicating automata with bounded channels[END_REF]22], though there is a subtle difference: in [START_REF] Genest | On communicating automata with bounded channels[END_REF]22], there are a notion of deadlock and distinguished final configurations.

C.9 Definition of universally bounded MSCs Proof. We begin by considering a p2p MSC. Let M ∈ MSC be such that M is strongly k-synchronous. Then, there is

M = M 1 • • • M n , M i which is a k-exchange, 1 ≤ i ≤ n.
By induction on M :

1. Base M = M 1 then M is a k-exchange and by definition |Matched(M ) ∪ Unm(M )| ≤ k.
Then, for all e ∈ M atched(M ) s.t. λ(e) = send(p, q, m), we have # Send(p,q, ) (⇝, e) -# Rec(p,q, ) (⇝, e) ≤ k.

Then, M is k-p2p-bounded.

2.

Step M = M ′ • M n and we suppose that

M ′ = M 1 • • • M n-1 is k-p2p-bounded.
For all 1 ≤ i ≤ n, M i is a k-exchange, and so an MSC, and by definition we know that any reception belongs to the same MSC as its matched send. Let ⇝ be a linearization and f ∈ M atched(M ′ ) s.t. λ(f ) = send(p, q, m) and, for all e ∈ M atched(M ′ ) s.t. λ(e) = send(p, q, m),

# Send(p,q, ) (⇝, f ) > # Send(p,q, ) (⇝, e).
Then, we have:

# Send(p,q, ) (⇝, f ) -# Rec(p,q, ) (⇝, f ) = 0.
Note that there is no unmatched message sent to q before f as f is matched. As M n is a k-exchange, we have for all e ∈ M atched(M n ) s.t. λ(e) = send(p, q, m) # Send(p,q, ) (⇝, e) -# Rec(p,q, ) (⇝, e) ≤ k.

Finally, for all e ′ ∈ M atched(M ) s.t. λ(e ′ ) = send(p, q, m), there is e ∈ M atched(M n ) such that we can decompose: # Send(p,q, ) (⇝, e ′ ) = # Send(p,q, ) (⇝, f ) + # Send(p,q, ) (⇝, e) and # Rec(p,q, ) (⇝, e ′ ) = # Rec(p,q, ) (⇝, f ) + # Rec(p,q, ) (⇝, e).

Therefore # Send(p,q, ) (⇝, e ′ ) -# Rec(p,q, ) (⇝, e ′ ) ≤ k.

Then, M is k-p2p-bounded. Now, we move to mailbox MSCs. Let M ∈ MSC mb be a strongly k-synchronous MSC. By definition,

M = M 1 • • • M n such that every M i = (E i , → i , ◁ i , λ i ) is a k-exchange
and, for all (e, f ) ∈ ⊏ M , there are indices 1 ≤ i < j ≤ n such that e ∈ E i and f ∈ E j .

By induction of M , we show that M is k-mailbox-bounded.

1. Base M = M 1 then M is a k-exchange and |Matched(M ) ∪ Unm(M )| ≤ k.
Let ⇝ be any linearization of M and so, for all e ∈ M atched(M ) s.t. λ(e) = send(p, q, m), we have # Send( ,q, ) (⇝, e) -# Rec( ,q, ) (⇝, e) ≤ k. Then, M is k-mailbox-bounded.

2.

Step M = M ′ • M n and we suppose that

M ′ = M 1 • • • M n-1 is k-mailbox-bounded. For all 1 ≤ i ≤ n, M i is a k-exchange,
and so an MSC, and by definition we know that any reception belongs to the same MSC as its matched send. Let ⇝ be a linearization and f ∈ M atched(M ′ ) s.t. λ(f ) = send(p, q, m) and, for all e ∈ M atched(M ′ ) s.t. λ(e) = send(p, q, m),

# Send( ,q, ) (⇝, f ) > # Send( ,q, ) (⇝, e).
Then, we have:

# Send( ,q, ) (⇝, f ) -# Rec( ,q, ) (⇝, f ) = 0.
Note that there is no unmatched message sent to q before f as f is matched. As M n is a k-exchange, we have for all e ∈ M atched(M n ) s.t. λ(e) = send(p, q, m)

# Send( ,q, ) (⇝, e) -# Rec( ,q, ) (⇝, e) ≤ k.

Finally, for all e ′ ∈ M atched(M ) s.t. λ(e ′ ) = send(p, q, m), there is e ∈ M atched(M n ) such that we can decompose:

# Send( ,q, ) (⇝, e ′ ) = # Send( ,q, ) (⇝, f ) + # Send( ,q, ) (⇝, e) and # Rec( ,q, ) (⇝, e ′ ) = # Rec( ,q, ) (⇝, f ) + # Rec( ,q, ) (⇝, e). Therefore # Send( ,q, ) (⇝, e ′ ) -# Rec( ,q, ) (⇝, e ′ ) ≤ k.
Then, M is k-mailbox-bounded.

◀ ▶ Proposition 40. Every weakly (resp. strongly) synchronizable and universally k-bounded system is weakly (resp. strongly) k ′ -synchronizable for a k ′ .

Proof. Let S be a system such that, for all M ∈ MSC,

M = M 1 • • • M n where M i is an exchange, 1 ≤ i ≤ n. Moreover, for all e ∈ M atched(M ) s.t. λ(e) = send(p, q, m), if M ∈ MSC \ MSC mb , for all ⇝⊆ ≤ M , # Send(p,q, ) (⇝, e) -# Rec(p,q, ) (⇝, e) ≤ k. if M ∈ MSC mb , for all ⇝⊆ ⪯ M , # Send( ,q, ) (⇝, e) -# Rec( ,q, ) (⇝, e) ≤ k. 1. Base Suppose that M = M 1 so M is an exchange. Either M ∈ MSC \ MSC mb and, as M is k-p2p-bounded, | M |= k 1 ≤ k× | P | 2 . So M is weakly k 1 -synchronous. Or M ∈ MSC mb and, as M is k-mailbox-bounded, | M |= k 2 ≤ k× | P |. So M is strongly k 2 -synchronous.

Step Suppose now that

M = M ′ • M ′′ such that M ′ is weakly k-synchronous for a k ′ ∈ N. Then, if M ∈ MSC \ MSC mb , for all linearizations ⇝⊆≤ M , let f ∈ M atched(M ′ ) s.t. λ(f ) = send(p, q, m) and, for all e ∈ M atched(M ′ ) s.t. λ(e) = send(p, q, m), # Send(p,q, ) (⇝, f ) > # Send(p,q, ) (⇝, e).
Then, we have:

# Send(p,q, ) (⇝, f ) -# Rec(p,q, ) (⇝, f ) = 0.
As S is universally k-bounded, | M ′′ |≤ k 1 , and as M ′′ is an exchange, we know that M ′′ is a k 1 -exchange. if M ∈ MSC mb , for all linearizations ⇝⊆⪯ M , let f ∈ M atched(M ′ ) s.t. λ(f ) = send(p, q, m) and, for all e ∈ M atched(M ′ ) s.t. λ(e) = send(p, q, m),

# Send( ,q, ) (⇝, f ) > # Send( ,q, ) (⇝, e).
Then, we have:

# Send( ,q, ) (⇝, f ) -# Rec( ,q, ) (⇝, f ) = 0.
As S is universally k-bounded, | M ′′ |≤ k 2 , and as M ′′ is an exchange, we know that

M ′′ is a k 2 -exchange. Then, M is at least weakly k 1 -synchronous (k 1 > k 2 ).
Finally, as all MSCs are weakly k 1 -synchronous, S is weakly k 1 -synchronizable. The equivalent proposition for strong properties can be shown in the same way. As an MSC is strongly synchronizable, it can be divided while maintaining the mailbox order. In a recursive way, as MSC is universally k-bounded, we have that each exchange of the MSC is bounded. Finally, each MSC is strongly k ′ -synchronous for a k ′ depending of k and the number of channels, and so the system is strongly k ′ -synchronizable. ◀

D.2 Examples D.2.1 p2p systems

For p2p semantics, weakly synchronizable and strongly synchronizable systems form a single class, as strongly k-synchronizable and weakly k-synchronizable form a single class too. Indeed, as a consequence of Proposition 47, weakly k-synchronizable systems are strongly k-synchronizable, and weakly synchronizable are strongly synchronizable. Therefore, for this p2p part, we will only talk about weak classes. We will see that this is not the case for mailbox systems.

However, universally bounded and existentially bounded classes are not equal, an universally bounded system is existentially bounded by definition but we can find a existentially bounded system, as system S 5 in Fig. 11 where, as we can see in a corresponding MSC in Fig. 7, an unbounded number of m 3 can be sent before be read by r, which prevent the system to be universally bounded.

ℓ 0 p ℓ 1 p ℓ 2 p send(p, q, m 1 ) send(p, q, m 1 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q send(q, p, m 2 ) rec(p, q, m 1 ) send(q, r, m 3 ) send(q, r, m 3 ) Aq ℓ 0 r rec(q, r, m 3 ) Ar Figure 11 System S5
By definition, weakly k-synchronizable systems are weakly synchronizable. Also, strongly k-synchronizable systems are included into existentially k-bounded systems, as proved by Proposition 39, so weakly k-synchronizable are included into existentially k-bounded.

We can see that weakly synchronizable systems and existentially bounded systems are incomparable. System S 6 in Fig. 12 is weakly synchronizable because we can send all messages before read them, and existentially 1-bounded because each MSC of L p2p (S 6 ) has a linearization of the form send(q, p, m 2 ) • (send(p, q, m 1 ) • rec(p, q, m 1 )) * rec(q, p, m 2 ), allowing to have in each channel only one pending message.

ℓ 0 p ℓ 1 p send(p, q, m 1 ) rec(q, r, m 2 ) Ap ℓ 0 q ℓ 1 q send(q, r, m 2 ) rec(p, q, m 1 ) Aq Figure 12 System S6 p q m 1 m 1 m 2 Figure 13 MSC M6
But, system S 7 in Fig. 14 is only weakly synchronizable. Indeed, for each execution we can add an iteration of message m 1 or m 2 , or both, and, as we can see in Fig. 15, we need to send all messages before begin to read, and so each execution need a bigger channel than the previous one.

0 p ℓ 1 p send(p, q, m 1 ) send(p, q, m 1 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q send(q, p, m 2 ) send(q, p, m 2 ) rec(p, q, m 1 ) Aq Figure 14 System S7 p q m 1 m 1 m 2 m 2 Figure 15 MSC M7
For system S 8 in Fig. 16, we can see an example of MSC in Fig. 17 which cannot be divided into exchanges as send and receptions are intertwined and so S 8 is not weakly synchronizable.

ℓ 0 p ℓ 1 p ℓ 2 p send(p, q, m 1 ) send(p, q, m 1 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q send(q, p, m 2 ) rec(p, q, m 1 ) Aq Figure 16 System S8 p q m 1 m 1 m 1 m 2 m 2 Figure 17 MSC M8
We can observe that S 8 is universally 3-bounded as each time a message is sent, one is received and the maximal number of messages in a buffer is 3. As we said, S 7 is weakly synchronizable but not existentially bounded and so not universally bounded, so weakly synchronizable and universally bounded systems are incomparable. However, as proved in Proposition 40, a system which is both is also weakly k-synchronizable (not necessarly for the same k).

Finally, weakly k-synchronizable and universally k-bounded systems are incomparable. System S 1 in Fig. 2 is both weakly 1-synchronizable and universally 1-bounded. But, we have, for example, system S 3 below which is weakly 1-synchronizable but not universally k-bounded for any k. Indeed, each execution can be rescheduled to have all the receptions just after the respective sends. Then each MSC can be divided into 1-exchanges (for an example, see MSC M 3 in Fig. 5). However, as we can send an unbounded number of m 2 messages before reading them, the size of channel c p can also be unbounded thus the system is not universally bounded. Conversely, as we have seen, system S 8 is universally 3-bounded but not weakly k-synchronizable for any k.

ℓ 0 p ℓ 1 p ℓ 2 p send(p, q, m 1 ) rec(q, p, m 2 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q ℓ 2 q send(q, p, m 2 ) send(q, p, m 2 ) rec(r, q, m 3 ) Aq ℓ 0 r ℓ 1 r send(r, q, m 3 ) Ar Figure 18 System S3 D.2.

Mailbox systems

Now consider mailbox semantics. As depicted in Fig. 9, we can now distinguish between weakly and strongly synchronizable systems.

Some inclusions are obvious, by definition of the classes:

universally bounded systems are existentially bounded, but it is a proper inclusion. Indeed, a system, as system S 5 in Fig. 11, can be existentially 1-bounded, but not universally bounded. In this case, as in p2p semantics, an unbounded number of message m 3 can be sent before be read, as we can see in MSC M 5 in Fig. 7.

strongly k-synchronizable systems are strongly synchronizable. As well, a system can be strongly synchronizable without have a bound on the size of its exchange, as system S 7 in Fig 14 weakly k-synchronizable systems are weakly synchronizable. We can also find a weakly synchronizable system without bound on the size of its exchange. Let see S 2 in Fig. 19 with MSC M 2 in Fig. 4, which can be divided into exchanges, each message can be in a separate exchange, except messages m 2 and m 3 that have to be all in the same exchange.

As we can have as many repetitions of them, this exchange no have bound on its size and prevent the system to be weakly k-synchronizable for a precise k. send(p, q, m 1 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q ℓ 2 q send(q, r, m 3 ) send(q, r, m 3 ) rec(r, q, m 4 ) rec(r, q, m 5 ) Aq ℓ 0 q ℓ 1 q ℓ 2 q send(r, q, m 4 ) send(r, q, m 4 ) rec(q, r, m 3 ) send(r, q, m 5 )

Ar

Figure [START_REF] Genest | A kleene theorem for a class of communicating automata with effective algorithms[END_REF] System S2

The classes of weakly synchronizable and weakly k-synchronizable systems are incomparable with the classes of existentially bounded and universally bounded systems. Indeed, let see system S 8 in Fig. 16 which is universally 3-bounded. It cannot be weakly synchronizable (and so weakly k-synchronizable for a k) as we cannot divide a corresponding MSC, as M 8 in Fig. 17, into exchanges, where all sends have to be before all receptions, as in p2p semantics. We see a difference with the p2p semantics looking at S 9 in Fig. 20 which is weakly synchronizable but not existentially bounded. Indeed, we can see in Fig. 21 that M 9 can be divided easily into 1-exchange but, as m 1 has to be sent before m 4 , and m 2 has to be sent to send m 4 , it means that all messages m 2 have to wait the send of m 4 to be read. Then, each execution is x-mailbox-bounded, where x is the number of repetitions of m 2 . Then, there is no bound on the buffers and S 9 cannot be existentially bounded (and so universally bounded). send(p, q, m 2 ) send(p, s, m 3 ) Ap ℓ 0 q ℓ 1 q ℓ 2 q send(q, r, m 1 ) rec(p, q, m 2 ) rec(p, q, m 2 ) Aq Finally, as proved in Proposition 40, if a system is weakly synchronizable and universally bounded system, there is a k such that it is also strongly k-synchronizable. In all the other intersections, we can find a system: weakly synchronizable and existentially bounded (but not weakly k-synchronizable or universally bounded): S 10 in Fig. 22 is existentially 1-bounded but there is no bound on the size of the exchange containing messages m 3 and m 4 and so S 10 cannot be weakly k-synchronizable, and repetitions of m 3 prevent it to be universally bounded;

ℓ 0 p ℓ 1 p ℓ 2 p send(p, q, m 1 )
rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q ℓ 2 q send(q, r, m 3 ) rec(r, q, m 4 ) rec(r, q, m 5 ) Aq ℓ 0 q ℓ 1 q ℓ 2 q send(r, q, m 4 ) rec(q, r, m 3 ) send(r, q, m 5 ) send(p, q, m 1 ) rec(q, p, m 2 ) Ap ℓ 0 q ℓ 1 q ℓ 2 q send(q, r, m 3 ) send(q, p, m 2 ) rec(r, q, m 4 ) Aq ℓ 0 q ℓ 1 q rec(q, r, m 3 ) send(r, q, m 4 ) weakly k-synchronizable and universally bounded as S 8 in Fig. 2. Now, focus on the strong classes. We know by Proposition 39 that a strongly k-synchronizable is existentially bounded. So let compare strongly k-synchronizable systems with universally bounded ones. We can see that there are incomparable. S 4 in Fig. 26 is strongly 1-synchronizable, as we can see with M 4 in Fig. 6, but cannot be universally bounded as the unbounded iterations of m 1 can be stored before begin to read. As we see before S 7 is only universally bounded and cannot have any synchronizable property. But, S 12 in Fig. 27 is both strongly 1-synchronizable and universally 1-bounded. Similarly, strongly synchronizable systems are incomparable with existentially bounded ones. S 13 in Fig. 29 is strongly synchronizable (and also weakly 1-synchronizable) but, to get an execution from M 13 we need to send message m 5 before m 1 and, as we see with M 6 previously, the number of iterations of m 2 becomes the bound of the channels for this execution. As it is unbounded, the system cannot be existentially bounded. send(q, r, m 1 ) rec(p, q, m 2 ) rec(s, q, m 3 ) Aq ℓ 0 q ℓ 1 q rec(s, r, m 5 ) Ar ℓ 0 q ℓ 1 q ℓ 2 q ℓ 3 q send(s, q, m 3 ) send(s, p, m 4 ) send(s, r, m 5 ) S 10 in Fig. 22 is existentially bounded and weakly synchronizable, but, again, message m 5 have to be sent before m 1 , so all messages in M 10 have to be in the same exchange. However, on process r, receptions of m 3 precedes send of m 5 and so this is not an exchange, and the system is not strongly synchronizable.

Aq

Aq

As

For the intersection, as with weak, a strongly synchronizable and existentially bounded systems is always strongly k-synchronizable for a k, by Proposition 40. We can have for example, S 2 which is strongly synchronizable, universally bounded, weakly 1-synchronizable but, as an exchange have to contain all messages that we have in M 3 , and we can repeat m 2 as many times we want, an exchange in mailbox is no bounded, and the system is not strongly k-synchronizable for any k. We can also have S 6 in Fig. 12 which is strongly synchronizable and existentially bounded but, as one execution is always an exchange, and it can grow without limits, we cannot be neither strongly k-synchronizable nor weakly k-synchronizable for any k.

4 Figure 1

 41 Figure 1 MSC M1

Figure 2

 2 Figure 2 System S1

m 5 Figure 4 ▶ Proposition 16 .

 5416 Figure 4 MSC M2 ▶ Proposition 16. Let M be an MSC. Then, M is weakly synchronous iff no RS edge occurs on any cyclic path in the conflict graph CG(M ).

3 Figure 5

 35 Figure 5 MSC M3

1 Figure 6

 16 Figure 6 MSC M4

3 Figure 7

 37 Figure 7 MSC M5

B. 2 Proof of Lemma 10 ▶ 10 .

 21010 Lemma Let k ∈ N and C ⊆ MSC k-stw . For all M ∈ MSC \ C, we have (Pref (M ) ∩ MSC (k+2)-stw ) \ C ̸ = ∅. Proof. Let k and C be fixed, and let M ∈ MSC \ C. Let M ′ ∈ Pref (M ) \ C such that, for all ≤ M ′ -maximal events e of M ′ , removing e (and its adjacent edge(s)) creates an MSC in C.

∄e 1 ,▶

 1 . . . , e k+1 . [ i̸ =j CG * (e i , e j )] ◀ C.5 Proof of Proposition 26 Proposition 26. Let k ∈ N. The set of MSCs that are weakly k-synchronous have special tree-width bounded by 2k + |P|.

SS e 2 (Rule 5 )Figure 10

 2510 Figure 10 Additional rules for extended conflict graph; XY --→ refers to an edge in the conflict graph

  ℓ

2 p

 2 send(p, q, m 2 )

2 sAsFigure 4 Figure 21

 2421 Figure 20 System S9

Figure 5 Figure 23

 523 Figure 22 System S10

Figure 4 Figure 25

 425 Figure 24 System S11

1 qAqFigure 2 Figure 28

 1228 Figure 26 System S4

ℓ 0 p ℓ 1 p

 1 send(p, q, m 2 ) rec(s, p, m 4 )

Figure 5 Figure 30

 530 Figure 29 System S13

Table 1

 1 Summary of the decidability of the synchronizability problem in various classes

		Peer-to-Peer	Mailbox
	Weakly synchronous	Undecidable [Thm. 20]	EXPTIME [Thm. 19]
	Weakly k-synchronous	Decidable [8, 14] and [Thm. 27]
	Strongly k-synchronous	-	Decidable [Thm. 33]
	Existentially k-p2p-bounded	Decidable [18, Prop. 5.5]
	Existentially k-mailbox-bounded	-	Decidable [Prop. 38]

  , Proceedings, volume 3340 of Lecture Notes in Computer Science, pages 30-48. Springer, 2004. doi:10.1007/978-3-540-30550-7\_4. 20 Cinzia Di Giusto, Laetitia Laversa, and Étienne Lozes. Guessing the buffer bound for k-synchronizability. In Implementation and Application of Automata -25th International

	Conference, CIAA 2021, Proceedings, Lecture Notes in Computer Science. Springer, 2021. To
	appear.
	21 Jesper G. Henriksen, Madhavan Mukund, K. Narayan Kumar, Milind Sohoni, and P.S.
	Thiagarajan. A theory of regular msc languages. Information and Computation, 202(1):1-38,
	2005.
	22 Dietrich Kuske and Anca Muscholl. Communicating automata, 2014.
	23 Julien Lange and Nobuko Yoshida. Verifying asynchronous interactions via communicating
	session automata. CoRR, abs/1901.09606, 2019. URL: http://arxiv.org/abs/1901.09606,
	arXiv:1901.09606.
	24 Markus Lohrey and Anca Muscholl. Bounded MSC communication. In Mogens Nielsen and
	Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th
	International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on
	Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings,
	volume 2303 of Lecture Notes in Computer Science, pages 295-309. Springer, 2002. doi:
	10.1007/3-540-45931-6\_21.
	25 Markus Lohrey and Anca Muscholl. Bounded MSC communication. Inf. Comput., 189(2):160-
	181, 2004.

doi:10.1016/j.ic.2003.10.002. 26 P. Madhusudan and Gennaro Parlato. The tree width of auxiliary storage. In Thomas Ball and Mooly Sagiv, editors, Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 283-294. ACM, 2011. 27 Robert S. Streett. Propositional dynamic logic of looping and converse. In Proceedings of the 13th Annual ACM Symposium on Theory of Computing, May 11-13, 1981, Milwaukee, Wisconsin, USA, pages 375-383. ACM, 1981. 28 Gregor von Bochmann. Communication protocols and error recovery procedures. Operating Systems Review, 9(3):45-50, 1975.

  and ⊏ M0 ⊆ ⊏ M . Finally, ⪯ M0 ⊆ ⪯ M and M is not a mailbox MSC, which is a contradiction. ◀

	B Proofs for Section 3
	B.1 Proof of Theorem 8

▶ Theorem 8. The bounded model-checking problem for com = mb is decidable. When the formulas φ are from LCPDL, then the problem is solvable in exponential time.

  So ⇝ is a mailbox linearisation with k bounded buffers, and M is existential k-mailboxbounded. ◀ ▶ Proposition 38. For all k ∈ N, the set of existentially k-mailbox-bounded MSCs is MSOdefinable and STW-bounded. M was already shown MSO definable and acyclicity is easily MSO definable, it is enough to show that rev --→ k is MSO definable. It is indeed the case, as demonstrated by this formula φ(r, s) = ∃r 1 , r 2 , . . . , r n .r → r 1 → r 2 → . . . → r n ∧ s ◁ r n .

	Proof. Let k ≥ 1 be fixed. Since every existentially k-mailbox-bounded MSCs is also
	existentially k-p2p-bounded, and since the class of existentially k-p2p-bounded MSCs is STW
	bounded (cf Proposition 44), the class of existentially k-mailbox-bounded MSCs is also STW
	bounded.
	Let us show that it is moreover MSO definable.
	By Lemma 42, it is enough to show that the acyclicity of ⪯ M ∪	rev --→ k is MSO definable,
	and since ⪯

▶

  Definition 46 (Universally bounded MSC). Let M = (E, →, ◁, λ) and k ∈ N. We call M universally k-p2p-bounded (resp., universally k-mailbox-bounded) if every p2p (resp., mailbox) linearization⇝ ⊆ E × E is k-p2p-bounded (resp., k-mailbox-bounded). Consider an MSC of the form M = M 1 • . . . • M n such that every MSC M i = (E i , → i , ◁ i , λ i ) is a (k-)exchange. Then, for all (e, f ) ∈ ≤ M , there are 1 ≤ i ≤ j ≤ n such that e ∈ E i and f ∈ E j .Proof. If e ≤ M f , then there is a sequence of events e = e 0 ▷◁ 1 e 1 ▷◁ 2 . . . ▷◁ m e m = f where ▷◁ is either → or ◁. Clearly, for every ℓ ∈ {0, . . . , m -1}, there are 1 ≤ i ≤ j ≤ n such that e ℓ ∈ E i and e ℓ+1 ∈ E j . By transitivity, this proves the statement. ◀ ▶ Proposition 39. Every weakly k-synchronous MSC is existentially k-p2p-bounded. Moreover, every strongly k-synchronous mailbox MSC is existentially k-mailbox-bounded.

	D Additional Material for Section 5
	D.1 Proofs
	Proof of the property from Remark 34:
	▶ Proposition 47.

  . See an example of MSC of S 7 in Fig 15, where we can always build a bigger adding iterations of messages m 1 or m 2 .