On the Power of Alternating Local Certification with Constant-Size Certificates

On the Power of Alternating Local Certification with Constant-Size Certificates Pedro Montealegre1 , Martín Ríos-Wilson1 , Jukka Suomela2 , and Guillaume Theyssier3

arXiv:2610.23694v1 [cs.DC] 16 Oct 2026

1

Facultad de Ingeniería y Ciencias, Universidad Adolfo Ibáñez 2 Aalto University 3 I2M, CNRS, Marseille, France

Abstract We study a distributed decision model based on the interaction between a prover, a disprover, and a distributed verifier. During a constant number of alternating rounds, the prover and the disprover assign certificates to the nodes, responding to the preceding assignments. The verifier is a local distributed algorithm in which each node decides whether to accept from its own input and the certificates observed in its neighborhood. The instance is accepted if all nodes accept. Alternation hierarchies for distributed decision have been studied under different restrictions, with previous works exploring, for example, the impact of local computation (Reiter, PODC 2024) or logarithmic-size certificates (Feuilloley et al., ICALP 2016). In this paper, we study a restricted setting where certificates have constant size and the network is anonymous. Moreover, we consider three models limiting the information available to the verifier. In the first model, called the SET hierarchy, nodes observe only the set of certificate sequences assigned to their neighbors. In the second, strictly stronger model, called the MULTISET hierarchy, nodes observe the corresponding multiset. In the third model, called the PORTS hierarchy, nodes can additionally distinguish neighboring certificate sequences by local port numbers. We prove that PORTS is strictly stronger than MULTISET, and that MULTISET is strictly stronger than SET. Despite these severe restrictions, the resulting hierarchies remain surprisingly expressive. In particular, leader detection belongs to the third level of the SET hierarchy, together with several natural graph properties previously known to require logarithmic-size certificates or unique identifiers. Our main results are the following. • We characterize the SET hierarchy: over finite input alphabets, a distributed language belongs to SET if and only if it is definable in monadic second-order logic MSO1 . • Every language definable in counting monadic second-order logic CMSO1 belongs to the PORTS hierarchy. We also exhibit a language in MULTISET that is not CMSO1 definable, while the inclusion of CMSO1 in MULTISET remains open. • Each of the SET, MULTISET, and PORTS hierarchies is strict at every level. • We develop lower-bound techniques showing that neither Hamiltonicity nor the existence of a perfect matching belongs to PORTS. Since both properties are MSO2 definable, the containment of MSO1 in PORTS does not extend to MSO2 . • For unbounded input alphabets, verifying that every node is given the correct network size lies outside the PORTS hierarchy. These results motivate further study of weak models of alternating local certification, with open questions about how local information and alternation determine their expressive power. Use of AI tools. The authors used ChatGPT (OpenAI) to assist with the writing and editing of this paper and in finding a proof of Theorem 7. The authors take full responsibility for the correctness of all results and proofs.

1

Contents 1 Introduction 1.1 Alternation hierarchies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 Constant-size hierarchies in weak models . . . . . . . . . . . . . . . . . . . . . . . 1.3 Our results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.4 Structure of the article . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

1 1 3 4 7

2 High-level description of our results 7 2.1 The power of the SET model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.2 The power of the PORTS hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . 11 2.3 Equivalence of hierarchies on bounded-degree graphs . . . . . . . . . . . . . . . . 13 2.4 Explicit problems outside the constant hierarchy . . . . . . . . . . . . . . . . . . 13 3 Preliminaries 3.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 Distributed languages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.3 Local views and verification models . . . . . . . . . . . . . . . . . . . . . . . . . . 3.4 Constant-size certification hierarchies . . . . . . . . . . . . . . . . . . . . . . . . . 3.5 Counting monadic second-order logic (CMSO) . . . . . . . . . . . . . . . . . . . .

14 14 14 15 16 16

4 Fundamental Tools 4.1 Closure under union and intersection . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Coloring orientations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Surjectivity of XOR maps . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.4 ALOS is in the third level of the SET hierarchy . . . . . . . . . . . . . . . . . . . 4.5 AMOS is in the second level of the SET hierarchy . . . . . . . . . . . . . . . . . . 4.6 Leader, spanning-tree and closure operations. . . . . . . . . . . . . . . . . . . . .

17 18 19 20 21 23 23

5 The power of the SET hierarchy 5.1 The SET hierarchy contains MSO . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 MSO contains the SET hierarchy . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Trading horizon for interaction . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.4 Comparison with distributed graph automata . . . . . . . . . . . . . . . . . . . .

26 26 27 29 31

6 Counting in PORTS and comparison with CMSO 33 6.1 Counting modulo a constant . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 6.2 The PORTS hierarchy contains CMSO . . . . . . . . . . . . . . . . . . . . . . . . 36 7 The MULTISET hierarchy is not included in CMSO

36

8 Separating the MULTISET and PORTS hierarchies 37 8.1 Encoding words by graphs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 9 Equivalence of hierarchies on bounded-degree graphs

41

10 Explicit languages outside the PORTS hierarchy 44 10.1 Labeled complete bipartite graphs . . . . . . . . . . . . . . . . . . . . . . . . . . 45 10.2 Bounded-degree graphs with unbounded inputs . . . . . . . . . . . . . . . . . . . 46 11 Discussion

48

1

Introduction

In distributed local certification, the nodes of a network aim to collectively verify whether the network satisfies a given property, with the help of a prover. The prover is an untrusted oracle that tries to convince the nodes that the network satisfies the property. Several models of local certification have been studied. The first one was introduced by Korman, Kutten, and Peleg [14] under the name proof-labeling schemes (PLS). A PLS protocol proceeds in two stages. In the first stage, the prover assigns a certificate to each node. In the second stage, called the verification stage, every node inspects the certificates in its local neighborhood and decides whether to accept or reject. If the instance is legal then there must exist a certificate assignment that makes all nodes accept. Conversely, if the instance is not legal, then for every certificate assignment, at least one node must reject. The efficiency of a protocol is measured by the size of the certificates. A canonical example is the verification of bipartiteness. This property can be verified by assigning to each node a single bit, interpreted as its color in a purported proper 2-coloring. A node accepts if and only if all its neighbors receive a color different from its own. Thus, all nodes accept if and only if the input graph is bipartite. This should be contrasted with the situation without certificates: no constant-round local algorithm can decide bipartiteness, since detecting an odd cycle may require exploring arbitrarily large portions of the graph; equivalently, long even and odd cycles are locally indistinguishable for nodes whose view is restricted to a constant radius (see, e.g., [6]). Many graph properties admit efficient verification in the PLS model with logarithmic-sized certificates. Examples include planarity [8], bounded genus [9], graph classes defined by intersections of geometric objects [13], H-minor-freeness [3], model checking on bounded treewidth [4], etc. In all these cases, certificates make it possible to verify properties that cannot be recognized by constant-round local algorithms without the help of a prover. However, for most known local certification schemes, constant-size certificates are not sufficient; logarithmic or polylogarithmic certificates are typically used, and are often necessary. Let us illustrate why finding properties that can be verified with constant-size certificates is difficult. Consider the property ”there exists a node of degree 3 ”. Although this property is global, it can be verified in the PLS model by certifying a spanning tree rooted at a node of degree 3. The tree is encoded by giving each node, except the root, the identifier of its parent and its distance to the root, assuming that the input graph is connected. Each node checks that its parent’s distance is exactly one less than its own, while the root checks that its distance is 0 and that it has degree 3. Hence, by using a spanning tree, one can easily certify non-local properties. However, Korman, Kutten, and Peleg [14] showed that certifying such a spanning tree requires certificates of size Ω(log n). Moreover, this encoding relies on the existence of unique identifiers. In fact, in anonymous networks, even verifying whether a marked set of edges forms a spanning tree is impossible with the sole help of a prover [14]. Several variants of the local certification model have been considered. For example, one may allow nodes to inspect certificates at some fixed constant radius, or to access not only the certificates but also the input states of their neighbors [10]. Even in such strengthened variants, the certification of a spanning tree appears to require unique identifiers and certificates of logarithmic size.

1.1

Alternation hierarchies

A natural way to generalize the certification framework is to allow the nodes to interact with more than one global entity. If all these entities have the same goal, then this does not really change the model: their certificates can simply be concatenated and viewed as a single certificate provided by only one entity. The interesting case arises when the entities have opposite objectives. 1

This leads to an alternating model of local certification. Besides the prover, whose goal is to convince the nodes that the input instance is legal, a new player called the disprover is introduced. The goal of the disprover is to convince the nodes in the graph that the instance is illegal. The prover and the disprover take turns, which we call interaction rounds. In each interaction round, one of the two players assigns a label to every node in the network: labels assigned by the prover are called certificates, while labels assigned by the disprover are called challenges. After these interaction rounds, the verifier remains local: each node inspects only a constant-radius neighborhood, together with the labels provided by the players, and decides whether to accept or reject. As usual, the whole network accepts if and only if all nodes accept. The number of interaction rounds, together with the order in which the prover and the disprover provide their labels, induces a hierarchy of models. For instance, the usual PLS model corresponds to a single existential interaction round: there exists a certificate assignment that makes all nodes accept on legal instances, while no certificate assignment can make all nodes accept on illegal instances. In general, the semantics of this hierarchy is the following: each action of the disprover should be understood as a universal choice, while each action of the prover should be understood as an existential choice. Thus, when the disprover provides a challenge, the protocol must be correct for every possible challenge; when the prover provides a certificate, it is enough that there exists a certificate that successfully answers the previous challenges. In this way, an alternating protocol naturally gives rise to an alternating sequence of universal and existential choices, while the final verification step remains purely local. Let us illustrate this with the property of being non-3-colorable. The usual 3-colorability property has a simple local certificate: the prover assigns one of three colors to each node, and each node checks that all its neighbors have a different color. The complement property, namely non-3-colorability, is naturally expressed with one interaction of the disprover followed by one interaction of the prover. The disprover first provides a challenge, consisting of an alleged 3coloring of the graph. If the graph is indeed not 3-colorable, then every such challenge must fail: there is at least one edge whose endpoints receive the same color. The prover can then answer the challenge by certifying the existence of such an invalid edge. To make this witness visible to all nodes, the prover provides a spanning tree rooted at one endpoint of a monochromatic edge. The root checks that one of its neighbors has the same color in the challenge, while the remaining nodes verify the consistency of the spanning tree, as in a standard PLS certificate. Thus, for every coloring proposed by the disprover, there exists a certificate that makes all nodes accept. On the other hand, if the graph is 3-colorable, then the disprover can choose a proper 3-coloring as its challenge. In that case there is no monochromatic edge, and therefore no spanning-tree certificate rooted at a local defect can make all nodes accept. Several alternation hierarchies for local decision and local certification have been studied before, under different assumptions on certificate size, computational power, and the information available to each node. In the logarithmic-size hierarchy [7], nodes have globally unique identifiers and the players provide O(log n)-bit certificates. This model shows that alternation can drastically reduce certificate size: for instance, minimum spanning tree and nontrivial automorphism admit much more succinct protocols than in one-round certification. However, the logarithmic hierarchy is not known to be infinite, and it does not contain all computable distributed languages. Other hierarchies with global features have also been considered. The identifier-independent hierarchy of [2] collapses at the second interaction and already contains all Turing-decidable distributed languages. A polynomial-time variant was studied in [1]. These models are very powerful because certificates or local computations may still encode information depending on global parameters of the input graph. The closest point of comparison for our work is the strictly local line of research. In [16], the local polynomial and local bounded hierarchies are introduced in the LOCAL model with locally

2

unique identifiers. There, certificate sizes and local computation are bounded as functions of the constant-radius view of each node. This yields a hierarchy that preserves a strong notion of locality, admits logical characterizations in the spirit of descriptive complexity, and is known to be infinite. Alternation had also been studied earlier in finite-state anonymous models, where connections with monadic second-order logic were established [15]. Our work belongs to this strictly local side of the landscape, but focuses on an even weaker regime: anonymous networks, constant-size labels, and weak views of neighborhoods. Thus, our goal is not to revisit the previous models with some additional constraints such as smaller certificates, but to understand what alternation can express when the only information exchanged in each interaction has constant size and when nodes have only set, multiset, or port-numbering views of neighboring certificates. In fact, our work is not focused on the properties of a particular hierarchy of alternation but on understanding how alternation can impact the power and expressiveness of the model when the communication protocol and the size of the certificates are very limited.

1.2

Constant-size hierarchies in weak models

The weak views that we consider are inspired by the weak models of distributed computing studied in [12]. These models classify anonymous local computation according to what a node can observe from its neighbors. In the port-numbering view, each incident edge is assigned a distinct local port number, allowing a node to distinguish the different occurrences of neighboring labels. In contrast, in the multiset view, port information is lost, but multiplicities are preserved: a node can see how many neighbors carry each label. In the set view, even multiplicities are lost: a node only sees which labels appear among its neighbors. The connection with logic provides additional motivation for this distinction. The multiset and set models were characterized by modal logic in [12]: roughly speaking, the set view corresponds to ordinary modal logic, which can express the existence of a neighbor of a given type, while the multiset view corresponds to graded modal logic, which can also express counting statements about neighbors. Thus, losing or preserving multiplicities is not a technical detail; it changes the expressive power of the local model. Unless stated otherwise, we consider finite connected undirected graphs. A network configuration is a pair (G, x), where x : V (G) → {0, 1}∗ assigns an input to each node. A distributed language is a collection of such configurations. We combine these weak views with alternating local certification. This gives rise to three constant-size hierarchies, depending on whether nodes observe their neighborhoods as sets, multisets of neighboring label sequences, or pairs consisting of a local port number and a neighboring label sequence. We call them the SET hierarchy, the MULTISET hierarchy, and the PORTS hierarchy, respectively. These hierarchies are defined in anonymous networks and with constant-size labels. The protocol has two phases. First, there is a bounded interaction between the prover and the disprover: in each interaction round, one of the two players assigns a constant-size label to every node. Then, once the interaction is over, the nodes run a local verifier. The verifier is local in a weak sense: a node can use its own input and labels, but its information about the neighborhood is limited to the set of neighboring label sequences in the SET model, the multiset of neighboring label sequences in the MULTISET model, or the set of pairs consisting of a local port number and a neighboring label sequence in the PORTS model. At first sight, these restrictions may seem severe. The players can provide only constantsize information, the nodes are anonymous, and the verifier sees only a restricted view of each neighborhood. Nevertheless, the resulting hierarchies are surprisingly expressive. They capture many natural properties and exhibit clean connections with logic. At the same time, the weakness of the local views makes the models fine-grained enough to separate SET from MULTISET

3

and MULTISET from PORTS, to study the role of multiplicities and port information, and to identify natural properties that remain outside the hierarchies. Let us give a rough definition of our models in order to state our results (see Section 3.1 for more precise definitions). Given a graph G = (V, E) and a map x : V → {0, 1}∗ , we call the map x an input for G, and we call the pair (G, x) a network configuration. A distributed language is a collection of network configurations. A port numbering of G is a family π = (πv )v∈V , where each πv : E(v) → {1, . . . , deg(v)} is a bijection and E(v) denotes the set of edges incident to v. Port numbers are local: the numbers assigned to an edge at its two endpoints need not coincide. We denote by P(G) the set of all valid port numberings of G. We consider three verification models, denoted by M ∈ {SET, MULTISET, PORTS}, which differ in the information that a node can access about the certificates assigned to its neighbors. For each k ≥ 0 and each model M ∈ {SET, MULTISET, PORTS}, we define the k-th level of the M-hierarchy, denoted Mk , as the family of distributed languages L for which there exist a positive integer c and an anonymous one-round distributed algorithm A such that, for every network configuration (G, x) and every port numbering π ∈ P(G), (G, x) ∈ L ⇐⇒ Q1 ℓ1 , Q2 ℓ2 , . . . , Qk ℓk such that ∀v ∈ V (G),

A(v, x(v), ℓ1 (v), . . . , ℓk (v), viewM (v)) = accept.

Here, the quantifiers Q1 , . . . , Qk follow the alternating pattern defining level k, and each ℓi : V → {0, 1}∗ satisfies |ℓi (v)| ≤ c for every v ∈ V (G).
For each node u, let ℓ(u) = ℓ1 (u), ℓ2 (u), . . . , ℓk (u) denote its sequence of certificates over the k interaction rounds. The neighborhood views are defined by viewSET (v) = ℓ(u) : u ∈ N (v) , 

viewMULTISET (v) =



ℓ(u) : u ∈ N (v) ,

viewPORTS (v) = (πv (uv), ℓ(u)) : u ∈ N (v) . 

Thus, the SET model discards multiplicities, the MULTISET model preserves them, and the PORTS model additionally identifies the local port through which each certificate sequence is received. In the PORTS model, the port numbering is fixed before the certificate assignments are chosen, and the protocol must be correct for every valid port numbering. The views in the SET and MULTISET models are independent of the port numbering. Finally, we define the set hierarchy, the multiset hierarchy, and the port hierarchy as SET =

[

SETk ,

k≥0

1.3

MULTISET =

[

MULTISETk ,

PORTS =

k≥0

[

PORTSk .

k≥0

Our results

We obtain several results on the expressive power of the SET, MULTISET, and PORTS hierarchies. Figure 1 summarizes their relationships with MSO and CMSO over finite input alphabets. In particular, increasing the information available about neighboring certificates yields strictly more expressive verification models: MSO = SET ⊊ MULTISET ⊊ PORTS. CMSO also lies strictly between SET and PORTS. Furthermore, we exhibit a language in MULTISET that is not CMSO-definable, while a separation in the reverse direction has not been established. Table 1 complements this overview with concrete languages and their placement in the SET and MULTISET hierarchies. 4

⊊

CMSO

SET = MSO

⊊

PORTS

? ⊊

MULTISET

⊊

Figure 1: Inclusions among the verification hierarchies and logics over finite input alphabets. All solid arrows denote strict inclusion. The dashed line marks the remaining uncertainty between CMSO and MULTISET: we know that MULTISET ⊈ CMSO, whereas the reverse non-inclusion CMSO ⊈ MULTISET has not been established. We first focus on the SET hierarchy. As discussed above, one might expect this model to be rather weak, since the verification process is highly restricted. Nevertheless, we show that it is expressive enough to contain several important languages. One important distributed language that also plays a key role in this paper is leader. This language consists of instances (G = (V, E), x) such that x : V → {0, 1} and there is a unique node v satisfying x(v) = 1. Formally, leader = {(G, x) : x ∈ {0, 1}V , ∃!v ∈ V, x(v) = 1}. The language leaderbelongs to the first level of the logarithmic hierarchy, where O(log n)bit certificates suffice. This bound is optimal: every protocol with a single prover assignment requires Ω(log n)-bit certificates, even when the verifier inspects a neighborhood of any fixed constant radius [10]. We show that three interaction rounds suffice with constant-size certificates in the SET model. Theorem 1. leader is in the third level of the SET hierarchy. For the proof of Theorem 1, we develop a technique to certify the existence of rooted spanning trees despite having no identifiers and only constant local communication. This technique relies on two main ingredients: coloring orientations, and acyclicity testing through the surjectivity of finite-state dynamics of the XOR map. It is a key component in proving the subsequent results of the paper, as it allows us to show that the hierarchy is closed under intersection, union, and complement. This closure phenomenon is perhaps surprising in such a restricted anonymous setting. Indeed, it means that the SET hierarchy is not merely a collection of ad hoc locally certifiable properties, but a robust formalism with the full Boolean structure. As a consequence, we obtain that the SET hierarchy defines exactly the languages definable in Monadic Second-Order Logic (MSO). Theorem 2. Over finite input alphabets, the SET hierarchy defines exactly the MSO-definable distributed languages. In other words, over finite input alphabets, the expressive power obtained by constant-size alternating certificates in the anonymous SET model coincides exactly with MSO definability. Thus, every MSO-definable distributed language admits a certificate system at some finite level of the SET hierarchy, and conversely every language recognized by the hierarchy has an MSO definition. A direct consequence of Theorem 2 is that (non-)k-colorability for each fixed k, planarity, and H-minor-freeness for each fixed graph H belong to the SET hierarchy. We next consider counting predicates. For every fixed modulus p ≥ 1 and residue 0 ≤ q < p, we show that the property of having q selected vertices modulo p belongs to the PORTS 5

hierarchy. The construction uses local port numbers to select a parent at each non-root vertex and verify modular sums over the resulting tree. This yields the following extension of our MSO containment. Theorem 3. Every CMSO-definable language belongs to the PORTS hierarchy. We also exhibit a graph language in MULTISET1 that is not CMSO-definable. Together with the preceding theorem, this implies that CMSO is strictly contained in the PORTS hierarchy. Whether every CMSO-definable language belongs to the MULTISET hierarchy remains open. Theorem 4. There is a language in MULTISET that is not CMSO-definable. We next compare the MULTISET and PORTS hierarchies. The inclusion MULTISET ⊆ PORTS follows by discarding port numbers. We prove that this inclusion is strict, even for graph languages without input labels. Theorem 5. There exists a decidable language of graphs, without input labels, that belongs to PORTS but not to MULTISET. Consequently, MULTISET ⊊ PORTS. The proof, given in Section 8, encodes binary words as graphs. On this encoding, PORTS can recognize every decidable word language closed under reversal. We then use a counting argument over finite tables of local views to construct such a word language whose graph encoding cannot be recognized by any MULTISET protocol. These results suggest that the expressive power of the PORTS hierarchy can be compared to that of the logarithmic hierarchy. However, the constant size of the certificates in our model, together with the absence of unique identifiers, also makes it possible to prove separation results whose analogues remain out of reach for the logarithmic hierarchy. More precisely, we show that the levels of the constant hierarchy form a strict hierarchy. Theorem 6. Let M ∈ {SET, MULTISET, PORTS}. The M-hierarchy consists of infinitely many levels. More precisely, for all k ≥ 0 there exists a language L ∈ Mk+1 such that L ̸∈ Mk . The proof compares corresponding levels of our hierarchies with those of the locally polynomial hierarchy on graphs of bounded degree and over finite input alphabets. For every k ≥ 2, this comparison transfers the separations of [16, Theorem 36 and Proposition 38], yielding a language in SETk+1 that does not belong to PORTSk . The first two inclusions are separated directly using 2-colorability and amos, respectively. Since SETk ⊆ MULTISETk ⊆ PORTSk at every level, the same witnesses establish strictness for all three hierarchies. Our containment results for MSO and CMSO concern MSO1 and CMSO1 , respectively, where second-order quantification ranges over sets of vertices. We show that the containment in the PORTS hierarchy cannot be extended to MSO2 , which also allows quantification over sets of edges. Theorem 7. Neither Hamiltonicity nor the existence of a perfect matching belongs to the PORTS hierarchy. Consequently, MSO2 ̸⊆ PORTS. Both properties are definable in MSO2 . For Hamiltonicity, one quantifies an edge set forming a connected spanning subgraph in which every vertex has degree two. For a perfect matching, one quantifies an edge set containing exactly one edge incident to each vertex. Thus, the failure of the containment already occurs for graph languages without input labels. The proof, given in Section 10.1, shows that a PORTS protocol on complete bipartite graphs induces a deterministic communication protocol of uniformly bounded cost between the two parts. For either property, such a protocol would decide whether the two parts have the same size, which requires unbounded communication. For languages with unbounded input alphabets, we prove a further limitation. Let size be the language consisting of all pairs (G, x) such that G has n vertices and x(v) = n for every v ∈ V (G). 6

Language

SET

MULTISET

PORTS

k-coloring At least one selected node (alos) At most one selected node (amos) Exactly one selected node (leader) MSO-definable languages CMSO-definable languages Degree-neighbor counting Hamiltonicity Existence of a perfect matching Graph size verification (size)

SET1 MULTISET1 PORTS1 Folklore SET3 MULTISET3 PORTS3 Lemma 9 SET2 MULTISET2 PORTS2 Lemma 11 SET3 MULTISET3 PORTS3 Theorem 1 ⊆ SET ⊆ MULTISET ⊆ PORTS Theorem 2 ̸⊆ SET ? ⊆ PORTS Theorem 3 ∈ / SET MULTISET1 PORTS1 Theorem 4 ∈ / SET ∈ / MULTISET ∈ / PORTS Theorem 7 ∈ / SET ∈ / MULTISET ∈ / PORTS Theorem 7 ∈ / SET ∈ / MULTISET ∈ / PORTS Theorem 8

Result

Table 1: Examples of languages studied in this paper and their placement in the SET, MULTISET, and PORTS hierarchies. The indicated levels are upper bounds obtained by our constructions and are not necessarily optimal. For logical classes, inclusions refer to all languages definable in the corresponding logic. “Open” denotes an unresolved inclusion. Theorem 8. size is not in the PORTS hierarchy. In fact, our result holds for a much larger set of languages. We say that a word s ∈ {0, 1}∗ is d-fragile if there exists a yes-instance (G, x) and a node v of degree d in G such that the input of v is s, i.e., x(v) = s but any perturbation of the input value of v produces a no-instance. We show that, for every language L ∈ PORTS and every fixed degree d > 0, only finitely many input values are d-fragile. For size, the cycles Cn , with n ≥ 3 and input n at every node, give infinitely many 2-fragile input values. Therefore, size ∈ / PORTS. Finally, Table 1 provides an overview of our main results, summarizing the expressive power and limitations of the three hierarchies through representative languages and their corresponding levels. The table also highlights the relationships between the models and the questions that remain open.

1.4

Structure of the article

The rest of the paper is organized as follows. In Section 2, we provide a high-level overview of our results and the main ideas behind the proofs. The detailed proofs are given in Sections 4 to 6, 9 and 10. We conclude in Section 11 with a discussion of possible directions for future work.

2

High-level description of our results

In this section, we provide a high-level description of the ideas and techniques used to obtain our results.

2.1

The power of the SET model

We first focus on proving Theorem 2, showing that the SET hierarchy has the same expressive power as MSO. We begin developing a series of fundamental tools. First, we show that the language leader is in the third level of the SET hierarchy. Remember that this language consists of instances (G, x) such that x : V → {0, 1} and |M (x)| = 1, where M (x) = {u ∈ V : x(u) = 1}. It is known that leader admits a PLS with certificates of size O(log n) [14], but this result heavily relies

7

on node identifiers and logarithmic certificates. Instead, we consider a different approach based on graph colorings and finite-state dynamics on graphs. First, we divide the task of showing that leader is in the hierarchy by considering two auxiliary languages: the language alos, consisting of instances (G, x) such that at least one node is selected (i.e., |M (x)| ≥ 1), and the language amos, consisting of instances (G, x) such that at most one node is selected (i.e., |M (x)| ≤ 1). 2.1.1

ALOS is in the third level of the SET hierarchy

We begin showing that alos is at the third level of the SET hierarchy Lemma 9. alos is in the third level of the SET hierarchy. The idea of the proof consists of two ingredients. The first ingredient is the use of coloring orientations. Given an instance (G, x), the prover assigns a root mark and a 3-coloring c : V → {0, 1, 2}. A node v colored c(v) considers as possible successors the neighbors with color c(v) − 1 mod 3. The root is required to be a selected node and to have no successor, while every other node is required to have at least one possible successor. In the SET model, the coloring c alone does not define a unique successor: nodes can detect which colors appear among their neighbors, but they cannot distinguish or count neighbors with the same color. For this reason, in the second round the disprover chooses a set R ⊆ V of red nodes, and in the third round the prover gives an auxiliary constant-size mark. A red node v looks at its red successors, that is, red neighbors with color c(v) − 1 mod 3. If v sees a unique red-successor type, then it uses this type as its successor. If it sees no red-successor type, or if the auxiliary marks make two different red-successor types visible, then v treats itself as having no successor. In this way, each red node locally decides whether to use one visible red-successor value in its XOR equation or no successor value at all. The key remark is that (G, x) ∈ alos if and only if there exists a valid rooted 3-coloring (c, ρ) such that, for every set R ⊆ V , the graph DR = D(G, c, ρ, R) is acyclic. In a yes-instance, the prover can take a BFS coloring modulo 3 rooted at a selected node. Then every directed edge decreases the distance to the root, so no such graph DR contains a directed cycle. Conversely, if no node is selected, then every valid coloring forces each node to have at least one possible successor, and the disprover can choose a red directed cycle in which each red node has exactly one red successor. The second ingredient comes from a finite-state dynamics on directed graphs. In this context, an element of {0, 1}V is called a configuration. Given a directed graph D = (V, E), we define the map XORD : {0, 1}V → {0, 1}V by 

 X

XORD (z)v = zv +

zw 

mod 2.

w∈N + (v)

We show that, restricted to directed graphs of maximum out-degree at most 1, the map XORD is surjective if and only if D contains no directed cycle. Putting everything together, the protocol for alos has three rounds. First, the prover gives a rooted 3-coloring (c, ρ). Second, the disprover chooses a red set R ⊆ V and a bit labeling y. Third, the prover gives auxiliary bits a and a bit labeling z. At each red vertex v, the verifier considers the set of distinct visible red-successor types A(v) = {(a(u), z(u)) : u ∈ SR (v)}. If A(v) = {(α, b)}, the verifier checks y(v) = z(v) + b (mod 2). Otherwise, it checks y(v) = z(v). These equations are locally checkable in the SET model, but they do not necessarily coincide with those of XORDR : several red successors may carry the same pair (a, z) and therefore appear as a single type in the local view. 8

Nevertheless, when R is the vertex set of a shortest directed cycle in the successor relation, every red vertex has exactly one red successor. In this case, the equations checked by the verifier coincide with those of XORDR , regardless of the auxiliary bits. This is the key observation used in the soundness proof. If (G, x) is a yes-instance, the prover chooses a BFS coloring modulo 3 rooted at a selected node. Hence every possible successor is strictly closer to the root. For any challenge (R, y), the prover can then construct the final configuration z in increasing order of distance from the root, choosing each bit so that the local XOR equation at that vertex is satisfied. If (G, x) is a no-instance, the disprover chooses a red directed cycle on which every red node has exactly one red successor, and then chooses a configuration with no preimage under the corresponding XOR map. Hence at least one node must reject. We refer to Section 4.4 for the full proof. Remark 10. Similar ideas are used in [16] to establish the expressiveness of the local second-order logic characterizing the locally polynomial hierarchy (see Example 4 therein). Our models, however, are substantially weaker, and such constructions must be revisited with care. In particular, Hamiltonicity, which is expressible in the local second-order logic considered in [16, Example 6], cannot be recognized even in our strongest model, PORTS, as established in Theorem 7. 2.1.2

AMOS is in the second level of the SET hierarchy

Next, in Section 4.5, we study the problem amos and show that it belongs to the second level of the SET hierarchy. Lemma 11. amos is in the second level of the SET hierarchy. The protocol has quantifier pattern ∀∃. The disprover assigns bits d(v), and the prover responds with bits a(v). Each vertex checks that its a-value agrees with those of all its neighbors and, if selected, that a(v) = d(v). Since G is connected, a must be constant. If at most one vertex is selected, the prover can satisfy every challenge; otherwise, the disprover assigns different bits to two selected vertices, forcing rejection. See Section 4.5. 2.1.3

MSO is contained in the SET hierarchy

Now we use the previous constructions to show that every graph property expressible in monadic second-order logic belongs to the SET hierarchy. More precisely, we show the following lemma: Lemma 12. Every MSO-definable distributed language over a finite input alphabet belongs to the SET hierarchy. The proof follows the natural interpretation of logical variables as certificate assignments. A monadic second-order variable X is represented by a bit labeling of the nodes: a node v receives value 1 if and only if v ∈ X. A first-order variable x is also represented by a bit labeling, but in this case the labeling must select exactly one node. This condition is precisely the language leader, which we have already shown to belong to the third level of the SET hierarchy. Thus, whenever a first-order variable is introduced, the protocol also verifies that the corresponding labeling is a valid singleton assignment. Each logical quantifier is simulated by quantifying over the corresponding bit labeling. Set variables require no additional condition. For a first-order variable, however, the labeling must select exactly one node. This condition has to be treated differently for existential and universal quantifiers. An existential choice is accepted only if the labeling is a valid leader labeling, whereas an invalid labeling chosen by a universal quantifier must be ignored. Thus, schematically,
∃x ψ −→ ∃ℓx leader(ℓx ) ∧ ψb , 9

whereas ∀x ψ

−→

∀ℓx ¬leader(ℓx ) ∨ ψb .

Since leaderand its complement belong to the hierarchy, these validity conditions can be incorporated using the closure properties proved above. It remains to explain how the quantifier-free part of the formula is verified. The atomic formulas of MSO are of three types: x = y,

x ∼ y,

x ∈ X.

Each of these can be checked locally once the corresponding variable assignments are encoded by node labelings. Equality x = y is verified by checking that the two singleton labelings mark the same node. Adjacency x ∼ y is verified by the unique node marked by x, which checks whether it sees a neighbor marked by y. Membership x ∈ X is verified by the node marked by x, which checks whether it also belongs to the set X. Boolean combinations of atomic formulas are handled using the closure of the hierarchy under finite intersections, unions, and complement. Therefore the whole quantifier-free part of the MSO formula can be verified inside the SET hierarchy. Combining this with the simulation of the quantifier prefix shows that every MSO-definable language belongs to the SET hierarchy. We refer to Section 5.1 for the complete proof. 2.1.4

The SET hierarchy is contained in MSO

We next prove the converse direction: every language in the SET hierarchy is MSO-definable. Lemma 13. Let L ∈ SETk be a language over a finite input alphabet. Then L is MSO-definable. The key observation is that a SET verifier has access only to a finite local view: its own input and certificate sequence, together with the set of certificate sequences assigned to its neighbors. Since the input and certificate alphabets are finite, there are only finitely many such views. Importantly, the verifier cannot read the inputs of its neighbors, and the neighborhood view does not preserve multiplicities. This information can be described in MSO. Each certificate labeling is encoded by a finite tuple of monadic second-order variables, one set for each possible certificate value. These sets are required to form a partition of the vertex set, so that every node receives exactly one certificate in each round. Then, for every possible node type, there is an MSO formula saying that a node has that type. Similarly, for every finite set T of neighboring certificate types, there is an MSO formula expressing that the set of certificate sequences appearing among the neighbors of a node is exactly T . This formula requires every type in T to appear at least once and excludes all other neighboring certificate types. Crucially, it does not inspect the input values of neighboring nodes. Since the verifier is fixed, there are only finitely many accepting local views. Hence the condition that a node accepts is a finite disjunction of MSO formulas, one for each accepting view. Finally, the quantifier rounds of the distributed hierarchy are translated into MSO quantifiers over the corresponding certificate sets: existential certificate rounds become existential monadic quantifiers, and universal certificate rounds become universal monadic quantifiers. Thus, the whole statement “there exist/for all certificate assignments, every node accepts” can be translated into an MSO sentence. We refer to Section 5.2 for the complete proof. We obtain that every language in the SET hierarchy is MSO-definable. Consequently, the SET hierarchy and MSO have the same expressive power.

10

2.1.5

Trading horizon for interaction

We also consider fixed-radius versions of SET. In the weak r-horizon model, a vertex sees its own input and certificates together with the set of certificate sequences at other vertices within distance r. This model is not monotone: at radius two, every vertex of both K1,n and Kn+1 sees all other vertices, so stars cannot be recognized, although they can at radius one. The strong r-horizon model retains the original neighborhood view and additionally provides, for each 2 ≤ j ≤ r, the set of certificate sequences in the radius-j ball. We denote by SETkr the class of languages recognized with k alternating certificate assignments in this model. It is monotone in r, and SETk1 = SETk . We prove that, in this strong model, larger constant horizons do not add expressive power to the hierarchy. More precisely, we show the following theorem: Theorem 14. For every fixed r ≥ 1, SET r =

S

S r 1 k≥0 SETk = k≥0 SETk = SET.

The prover certifies the sets Tj (v) of certificate sequences appearing in Bj (v), for 0 ≤ j ≤ r. Writing γ(v) for the certificate sequence of v, the verifier checks T0 (v) = {γ(v)} and [

Tj (v) = T0 (v) ∪

Tj−1 (u).

u∈N (v)

These checks use only the ordinary SET view, since multiplicities are irrelevant. The certified sets reconstruct the additional horizon information and can be merged into the last existential assignment, or supplied in one additional existential round.

2.2

The power of the PORTS hierarchy

Next, we focus on understanding the expressive power of the PORTS hierarchy. Clearly, this hierarchy contains both the SET and MULTISET hierarchies, since a PORTS verifier can recover the corresponding views by ignoring port numbers and, if necessary, multiplicities. Therefore, the languages amos, alos, and leader also belong to the PORTS hierarchy. Moreover, the closure properties proved for the SET hierarchy, namely closure under finite intersections, finite unions, and complement, extend directly to the PORTS hierarchy. In particular, every MSOdefinable language belongs to the PORTS hierarchy. To go beyond MSO, we introduce an additional ingredient: the ability to count selected nodes modulo a fixed constant. This is where port numbering becomes useful. By distinguishing neighbors through their local ports, nodes can select a unique parent in a certified spanning tree and verify local aggregation constraints involving the contributions of all their children. More precisely, for every fixed p ≥ 2 and 0 ≤ q < p, we define the language Count(q, p) of instances in which the number of selected nodes is congruent to q modulo p, and show that Count(q, p) belongs to the PORTS hierarchy. Lemma 15. For all q, p ∈ N, with p ≥ 1, and 0 ≤ q < p, Count(q, p) belongs to PORTS9 . For the proof of Lemma 15, we combine leader with the coloring orientations used for alos. In the PORTS model, each non-root vertex selects a unique parent among its eligible neighbors using the smallest local port. We then certify that this functional orientation is acyclic and has exactly one root. Consequently, the selected edges form a rooted spanning tree of G. This rooted tree allows us to count by collecting information from the leaves towards the root. Given an instance (G, x), the prover assigns to each node a value sv ∈ {0, . . . , p − 1}, intended to represent the number of marked nodes in the subtree rooted at v, modulo p. Each node v should then verify that sv ≡ x(v) +

X u∈Tv

11

su

(mod p),

(1)

where Tv denotes the set of children of v in T . This bottom-up aggregation is standard in distributed certification [7, 14]. In our setting, however, one must be careful about what is locally visible: every non-root node knows its unique parent in the certified tree, but a node v does not identify its children individually. To make the verification of Equation (1) local, we use two additional interactions. Once T and the values {sv }v∈V are fixed, the disprover marks a node v ∗ at which Equation (1) is to be tested. The prover responds by marking precisely the children of v ∗ . This is locally checkable: a node is marked by the prover if and only if its parent is the node marked by the disprover. Then v ∗ uses the multiset of marked neighboring certificates to compute x(v ∗ ) +

X

su

(mod p)

u∈Tv∗

and checks that this value is equal to sv∗ . If the assignment {sv }v∈V is incorrect, the disprover chooses a node v ∗ for which Equation (1) fails. Then some node rejects: either the prover marks the children inconsistently, or v ∗ receives exactly the values of its children and detects that the modular equation is false. It remains to deal with the case where the disprover does not select a unique node v ∗ . As before, this can be handled using leader: the verifier accepts when the challenge is not unique, and performs the modular check only when the challenge selects a single node. This is implemented by a Boolean combination of the previously studied languages. We obtain that Count(q, p) is recognized at a constant level of the PORTS hierarchy. In our explicit construction, the resulting Boolean combination places the language at level 9. See Section 6.1 for the complete proof. 2.2.1

The PORTS hierarchy strictly extends CMSO

Combining the previous techniques, we show that every language expressible in counting monadic second-order logic (CMSO) belongs to the PORTS hierarchy. Theorem 3. Every CMSO-definable language belongs to the PORTS hierarchy. The proof of Theorem 3 follows the same general approach as Lemma 12, with the additional simulation of counting predicates using the certification of Count(q, p) as a subroutine. This allows us to extend the correspondence between logical quantification and alternating certificates to CMSO formulas. We then show that this inclusion is strict by exhibiting a language in the MULTISET hierarchy that is not definable in CMSO. Since the MULTISET hierarchy is contained in the PORTS hierarchy, this also establishes that the expressive power of PORTS goes beyond CMSO. Theorem 4. There is a language in MULTISET that is not CMSO-definable. For this separation, we consider the language L consisting of graphs in which every node of degree at least 3 has the same number of neighbors of degree 1 and degree 2. This language belongs to the first level of the MULTISET hierarchy. The prover assigns to each node its degree truncated at 3, and the nodes locally verify these labels. Nodes of degree at least 3 additionally check that the numbers of neighbors labeled 1 and 2 coincide. These checks are possible because the MULTISET model preserves multiplicities. To prove that L is not definable in CMSO, we show that any CMSO formula defining L would induce a CMSO formula over finite words recognizing a non-regular language. This contradicts the fact that CMSO-definable word languages are regular [5]. Together, these results establish that CMSO is strictly contained in the PORTS hierarchy. Whether every CMSO-definable language also belongs to the MULTISET hierarchy remains open. 12

2.3

Equivalence of hierarchies on bounded-degree graphs

In Section 9, we study the expressive power of our hierarchies when restricted to boundeddegree graphs. We show that, from sufficiently high levels onward, the SET, MULTISET, and PORTS hierarchies coincide level-wise with the locally polynomial hierarchy introduced in [16], assuming a fixed finite input alphabet. The main challenge is to simulate the additional information available in [16], where nodes are equipped with locally unique identifiers. On bounded-degree graphs, the identifiers needed within a constant horizon can be represented using constant-size labels. The key idea is to certify an appropriate coloring of a power of the graph, ensuring that nearby nodes receive distinct colors. These colors allow even a SET verifier to recover the distinctions between neighboring nodes that are normally lost when multiplicities are ignored. The proof uses alternating certificates to verify the validity of the coloring, with different constructions depending on whether the protocol starts with an existential or a universal quantifier. An important consequence is that our hierarchies have infinitely many distinct levels. Indeed, [16] established strict separations in the locally polynomial hierarchy even on graphs of bounded degree. By transferring these separations through our equivalence result, we conclude that the SET, MULTISET, and PORTS hierarchies are all infinite.

2.4

Explicit problems outside the constant hierarchy

Finally, in Section 10, we establish explicit limitations of the PORTS hierarchy. We identify two different obstacles to verification with constant-size certificates: the limited information that can be exchanged in graphs of unbounded degree, and the presence of unbounded local inputs, even on bounded-degree graphs. We first show that neither Hamiltonicity nor the existence of a perfect matching belongs to the PORTS hierarchy. The proof of Theorem 7 relies on a connection with communication complexity. More precisely, we show that every language over a fixed finite input alphabet belonging to the PORTS hierarchy induces a uniformly bounded deterministic communication protocol on complete bipartite graphs. To obtain the separation, we consider complete bipartite graphs Kn,m , where Alice knows n and Bob knows m. Such a graph admits a perfect matching if and only if n = m, and a Hamiltonian cycle if and only if n = m ≥ 2. However, deciding equality between two arbitrarily large integers requires an unbounded amount of deterministic communication. This contradiction shows that neither language belongs to the PORTS hierarchy. We then consider a different limitation, arising from unbounded input alphabets. We define the language size, consisting of all pairs (G, x) such that G is an n-node graph and x(v) = n for every v ∈ V . Theorem 8. size is not in the PORTS hierarchy. For the proof of Theorem 8, we introduce a lemma based on fragile inputs. Let (G, x) be a network configuration. A perturbation at a node v consists of changing its input x(v) to a different value, while leaving the rest of the configuration unchanged. For a fixed d > 0, we say that L has a fragile d-degree input value s if there exists an instance (G, x) ∈ L and a node v ∈ V of degree d with x(v) = s, such that every perturbation at v produces a no-instance. Given a distributed language L, we denote by Fragiled (L) the number, possibly infinite, of fragile d-degree input values of L. We establish the following lemma. Lemma 16. For every language L in the PORTS hierarchy and every d > 0, Fragiled (L) is finite. 13

The proof of Lemma 16 relies on a counting argument. Since the degree d is fixed and certificates have constant size, there are only finitely many possible local certificate views, including port information. Consequently, infinitely many fragile input values would imply that two distinct values induce the same local verification behavior for every possible certificate view. Replacing one by the other would then preserve the acceptance of the entire protocol, contradicting fragility. As a consequence, size cannot belong to the PORTS hierarchy, since it has infinitely many fragile input values. Indeed, it suffices to consider cycles Cn , where every node has degree 2 and input n. Changing the input of any node produces a no-instance, showing that Fragile2 (size) is infinite. For the complete proofs of these results, refer to Section 10.

3

Preliminaries

In this section, we introduce the basic definitions and the distributed verification models used throughout the paper. We then formally define the corresponding hierarchies of constant-size certificates and recall the counting monadic second-order logic on graphs.

3.1

Basic definitions

For integers s < t, we denote by [s, t] the set of all integers k such that s ≤ k ≤ t. We also use [t] as shorthand for [1, t], with [0] = ∅. Throughout this paper, graphs are finite, simple, and undirected. Unless stated otherwise, all graphs are connected. Given a graph G = (V, E), we write n = |V | for its number of nodes and N (v) for the neighborhood of a node v ∈ V . The degree of v is denoted by δ(v) = |N (v)|, and ∆(G) denotes the maximum degree of G. We also write V (G) and E(G) for the vertex and edge sets of G, respectively.

3.2

Distributed languages

Given a graph G = (V, E), an input is a mapping x : V → {0, 1}∗ . The pair (G, x) is called a network configuration. A distributed language is a set of network configurations, that is, L ⊆ {(G, x) : G = (V, E), x : V → {0, 1}∗ }. The complement of L is the distributed language L = {(G, x) : (G, x) ∈ / L}. A graph language is a set of graphs. When treating a graph language as a distributed language, we fix a singleton input alphabet {⊥} and identify each graph G with the configuration (G, x⊥ ), where x⊥ (v) = ⊥ for every v ∈ V (G). For example, the language of 3-colorable graphs is defined by 3-colorable = {G : ∃c : V (G) → [3], ∀uv ∈ E(G), c(u) ̸= c(v)}. We say that a distributed language has a finite input alphabet if the input values of its nodes belong to a fixed finite set. For each positive integer ∆, let B(∆) denote the class of graphs of maximum degree at most ∆, that is, G ∈ B(∆) ⇐⇒ ∆(G) ≤ ∆. Given a class of graphs G and a distributed language L, we define the restriction of L to G as LG = {(G, x) ∈ L : G ∈ G}. For example, restricting 2-colorable to B(2) yields the language consisting of paths and even cycles. 14

3.3

Local views and verification models

We consider three anonymous models of local verification, denoted by SET, MULTISET, and PORTS. Nodes do not have unique identifiers, and the models differ in the information they provide about neighboring certificates. Given a graph G = (V, E), a labeling is a mapping ℓ : V → {0, 1}∗ . A labeling list is a tuple ℓ = (ℓ1 , . . . , ℓk ) of labelings. For a positive integer c, we say that ℓ is c-bounded if P |ℓ(v)| = ki=1 |ℓi (v)| ≤ c for every v ∈ V . Let ℓ be a labeling list. We define the following three local views: • In the SET model, a node observes the set of neighboring labeling lists: viewSET (v) = {ℓ(u) : u ∈ N (v)}. In particular, multiplicities are not visible. • In the MULTISET model, a node observes the multiset of neighboring labeling lists: viewMULTISET (v) = {{ℓ(u) : u ∈ N (v)}}. Thus, multiplicities are preserved, but neighboring nodes carrying identical labeling lists cannot be distinguished. • In the PORTS model, every node v is equipped with a local port numbering, given by an injective map πv : N (v) → [δ(v)]. Port assignments are local: distinct neighbors of a node receive distinct port numbers, but the assignments at opposite endpoints of an edge are independent. The PORTS-view of v is the set of port-certificate pairs viewPORTS (v) = (πv (u), ℓ(u)) : u ∈ N (v) . 

Hence, a node can distinguish its neighbors through their local port numbers, even when several neighbors carry identical labeling lists. The three models satisfy the natural information ordering SET ⪯ MULTISET ⪯ PORTS, since a set view can be recovered from a multiset view, and a multiset view can be recovered from a port-ordered tuple. Local verifiers. A local verification algorithm, also called a distributed verifier, for model M ∈ {SET, MULTISET, PORTS} is a computable function A which, for every network configuration (G, x), every labeling list ℓ, and every node v ∈
V , produces an output A(G, x, v, ℓ) ∈ {0, 1} depending only on the tuple x(v), ℓ(v), viewM (v) . In particular, a node can read its own input and its own certificates, but it cannot directly read the inputs of neighboring nodes. Only their certificate labels are available through the corresponding local view. For the PORTS model, the output may depend on the local port numbering. However, the distributed languages recognized by the model must be independent of the particular choice of port numbering. We interpret output 1 as accept and output 0 as reject. When the configuration and labeling list are clear from the context, we simply write A(v) instead of A(G, x, v, ℓ). The verifier accepts a configuration with labeling list ℓ if every node accepts, that is, A(G, x, ℓ) = 1 ⇐⇒ ∀v ∈ V, 15

A(G, x, v, ℓ) = 1.

Otherwise, we write A(G, x, ℓ) = 0. Notice that even with constant-size certificates, the local verifier need not have a finite input domain, since the original input x(v) may have arbitrary length. Nevertheless, the set of possible certificate views is finite in the SET model. For MULTISET and PORTS, this is also the case when the degree is bounded. In particular, port numbering does not provide additional unbounded information at a fixed degree.

3.4

Constant-size certification hierarchies

We now formally define the hierarchy of distributed decision with constant-size certificates for each model M ∈ {SET, MULTISET, PORTS}. Let k ≥ 0. A distributed language L belongs to the k-th level of the hierarchy if there exist a constant c > 0 and a distributed verifier A for model M such that (G, x) ∈ L ⇐⇒ Q1 ℓ1 Q2 ℓ2 · · · Qk ℓk ,

A(G, x, ℓ) = 1,

where the quantifiers Q1 , . . . , Qk ∈ {∀, ∃} alternate, and the labeling list ℓ = (ℓ1 , . . . , ℓk ) is c-bounded. Each labeling ℓi ranges over assignments from a fixed finite certificate alphabet Ci , chosen independently of the graph size. The alphabets and their encodings are fixed as part of the protocol, with a total of at most c bits per node across all certificate assignments. We distinguish the two possible choices of the first quantifier. We write M(Σk ) for the class of languages recognized by protocols starting with an existential quantifier, and M(Πk ) for those starting with a universal quantifier. In both cases, the remaining quantifiers alternate. For k = 0, there are no certificate assignments, and both classes coincide with local decision in model M. We write Mk for the union of the two classes at level k, and define the full hierarchy by M=

[

Mk .

k≥0

For the PORTS hierarchy, the equivalence defining membership must hold for every valid port numbering of the graph. Thus, port numbers may influence the local verification procedure and the certificates chosen by the provers and disprovers, but not the language recognized by the protocol. The information ordering between the three models immediately implies that, for every k ≥ 0, SETk ⊆ MULTISETk ⊆ PORTSk . The same inclusions hold separately for the Σk and Πk levels.

3.5

Counting monadic second-order logic (CMSO)

Finally, we consider graph languages expressible in counting monadic second-order logic (CMSO), also referred to as CMS1 [5]. This logic extends monadic second-order logic (MSO) with counting predicates. Both logics allow quantification over vertices (first-order quantification, usually denoted by lowercase variables) and over sets of vertices (monadic second-order quantification, usually denoted by uppercase variables).1 In addition to Boolean connectives and quantifiers, CMSO formulas are built from the following atomic formulas, with their corresponding interpretations: • xi = xj : equality of vertices; 1

We do not allow quantification over sets of edges. Allowing such quantification yields the more expressive logics MSO2 and CMSO2 , respectively.

16

• xi ∼ xj : adjacency of vertices; • xi ∈ Xj : membership of a vertex in a set; • Cardqp (Xi ): the cardinality of Xi is congruent to q modulo p, where p ≥ 2 and 0 ≤ q < p are fixed integers. For languages over a fixed finite input alphabet, we also allow a unary predicate for each input symbol, interpreted by the vertices carrying that symbol. MSO is the fragment of CMSO obtained by excluding the counting predicates Cardqp (Xi ). These logics are also commonly denoted MSO1 and CMSO1 , respectively, to emphasize that second-order quantification is restricted to sets of vertices. For a CMSO sentence ϕ, we define the graph language Lϕ = {G : G |= ϕ}. Many natural graph properties can be expressed in MSO. For instance, the language of 3colorable graphs is defined by the following formula: 

∃X1 ∃X2 ∃X3



∀x

_

(x ∈ Xi )

i∈[3]



∧

! ^

∀x ∀y (x ∈ Xi ∧ y ∈ Xi ) → ¬(x ∼ y)  .

i∈[3]

Other examples of MSO-definable graph properties include connectivity, planarity, and exclusion of a fixed graph H as a minor. Every CMSO formula can be transformed into an equivalent formula in prenex normal form, consisting of a sequence of first-order or second-order quantifiers followed by a quantifier-free formula: Q1 z1 Q2 z2 · · · Qk zk ψ, where Qi ∈ {∃, ∀} and ψ is quantifier-free. The quantifier rank (or quantifier depth) of a formula is the maximum nesting depth of its quantifiers. In particular, a formula in prenex normal form with k quantified variables has quantifier rank k. This should not be confused with quantifier alternation depth, which measures the number of alternations between existential and universal quantifiers. In the results relating logical definability to our distributed hierarchies, we use the number of quantified variables in a prenex representation as the relevant complexity parameter. This allows us to simulate each logical quantifier by a corresponding certificate quantifier, with an additional constant number of hierarchy levels.

4

Fundamental Tools

In this section we show the core construction for our results. A key element that we need in our proofs is to be able to verify that at least (resp. at most) one node is marked in a graph. More precisely, we study three languages: 1. alos = {(G, x) : x : V 7→ {0, 1}, |{v ∈ V : x(v) = 1}| ≥ 1}. 2. amos = {(G, x) : x : V 7→ {0, 1}, |{v ∈ V : x(v) = 1}| ≤ 1}. 3. leader = alos ∩ amos. The language alos corresponds to the set of network configurations such that there is at least one node selected. In addition, amos corresponds to the set of network configurations such that there is at most one node selected. Finally, leader is the set of network configurations in which there is exactly one node selected. 17

4.1

Closure under union and intersection

In this section, we establish closure under finite intersections and unions for the SET, MULTISET, and PORTS hierarchies. The proof applies to all three models, so we write M ∈ {SET, MULTISET, PORTS}. We now prove the closure result. Lemma 17. Let M ∈ {SET, MULTISET, PORTS}. Let L1 , . . . , Ls be languages such that Li ∈ Mki for every i ∈ {1, . . . , s}, and let k = maxi ki . Then s \

Li ∈ MK

and

i=1

s [

Li ∈ Mk+1 ,

i=1

where K = k if there is a single i with ki = k, and K = k + 1 otherwise. Proof. We first prove closure under finite intersection. We give the proof for the case s = 2; the generalization to larger s is straightforward. By adding dummy certificate rounds, we can suppose that both languages are recognized by protocols with exactly K rounds and the same sequence of quantifiers: K = k is enough when there is a single i with ki = k, and K = k + 1 is enough otherwise (in particular, when two protocols use k rounds but start with different quantifiers). We have L1 , L2 ∈ MK . Thus, for each i ∈ {1, 2}, there exists a local verifier Ai such that (G, x) ∈ Li if and only if i

Q1 ℓi1 , Q2 ℓi2 , . . . , QK ℓiK , ∀v ∈ V, Ai (G, x, v, ℓ ) = 1, i

where ℓ = (ℓi1 , . . . , ℓiK ). We define a new verifier A for L1 ∩ L2 . In each round j, the certificate assigned to a node is the pair (ℓ1j (v), ℓ2j (v)). The verifier A locally simulates both A1 and A2 on the corresponding coordinates and accepts at v if and only if both simulations accept: 1

2

1

2

A(G, x, v, ℓ , ℓ ) = A1 (G, x, v, ℓ ) ∧ A2 (G, x, v, ℓ ). This construction is valid in all three models. From the neighborhood view of pairs of certificate sequences, a node can recover the view corresponding to each coordinate. In the PORTS model, the local port numbers are preserved in both projections. Hence the verifier can simulate both original verifiers. It follows directly that (G, x) ∈ L1 ∩ L2 if and only if all nodes accept in this combined protocol. Hence L1 ∩ L2 ∈ MK . The argument extends to any finite number of languages by taking tuples of certificates and conjoining all verifiers. We now prove closure under finite union. Let L1 , L2 ∈ Mk . Consider an alternating quantifier prefix of length k + 1 starting existentially: ∃∀∃ ··· . Every k-round protocol starting existentially can be embedded in the first k rounds of this prefix. Similarly, every k-round protocol starting universally can be embedded in rounds 2, . . . , k + 1. In the first round, the prover assigns a selector b(v) ∈ {1, 2} to each vertex. Every vertex checks that its selector agrees with those of all its neighbors. Since the graph is connected, acceptance requires b to be constant throughout the graph. The remaining certificate fields simulate the protocol corresponding to the selected language, using the appropriate positions in the common quantifier prefix. Unused certificate fields are ignored. If (G, x) ∈ L1 ∪ L2 , the prover selects a language containing (G, x) in the first round and follows a winning strategy for that language. The selected protocol therefore accepts against every subsequent universal challenge. 18

Conversely, suppose that (G, x) ∈ / L1 ∪L2 . Any nonconstant selector causes a local rejection. If the selector is constant, it specifies a language that does not contain (G, x). Since the selection was made before the universal challenges, the disprover can follow a winning strategy against the selected protocol. Thus some vertex rejects. Therefore, L1 ∪ L2 ∈ Mk+1 . The same construction works for any fixed finite union, using a constant-size selector. All certificates have constant size, and the argument applies to the SET, MULTISET, and PORTS models.

4.2

Coloring orientations

First, we show an auxiliary result regarding orientations. Given a graph G, we would like to encode, using constant-size certificates, a local orientation induced by a coloring modulo 3. Let G = (V, E) be a graph and let x : V → {0, 1} be an input function. Given a map c : V → {0, 1, 2}, we define the set of successors of a node v ∈ V , with respect to the coloring c, as S(v) = {u ∈ N (v) : c(u) = c(v) − 1 mod 3}. The prover will also mark some nodes as roots. Let ρ : V → {0, 1} be this root marking, and let B(ρ) = {v ∈ V : ρ(v) = 1}. We say that the pair (c, ρ) is a valid rooted coloring for (G, x) if the following conditions hold. • For every v ∈ B(ρ), we have x(v) = 1 and S(v) = ∅. • For every v ∈ / B(ρ), we have S(v) ̸= ∅. Observe that these conditions are locally checkable in the SET model, since a node only needs to know whether the set of certificates received from its neighbors contains a node with color c(v) − 1 mod 3. Later, the disprover will choose a set R ⊆ V of red nodes. For every node v, define SR (v) = S(v) ∩ R. Intuitively, SR (v) is the set of red successors of v. Given a valid rooted coloring (c, ρ) and a set R ⊆ V , we define a directed graph DR = D(G, c, ρ, R) as follows. • The vertex set of DR is R. • For every v ∈ R, if SR (v) = {u}, then DR contains the directed edge (v, u). • If SR (v) = ∅ or |SR (v)| > 1, then v has no outgoing edge in DR . Thus, every node in DR has out-degree at most 1. Lemma 18. Let (G, x) be a network configuration with x : V → {0, 1}. Then (G, x) ∈ alos if and only if there exists a valid rooted coloring (c, ρ) such that, for every set R ⊆ V , the graph DR = D(G, c, ρ, R) has no directed cycle. Proof. First, suppose that (G, x) ∈ / alos. Then no node is selected, that is, x(v) = 0 for every v ∈ V . Let (c, ρ) be any valid rooted coloring. Since every root must satisfy x(v) = 1, we have B(ρ) = ∅. Therefore, by validity, every node v ∈ V satisfies S(v) ̸= ∅. Now consider the directed relation that connects each node v to all nodes in S(v). Since every node has at least one successor, this relation contains a directed cycle, and we can consider a minimal such cycle. More precisely, there exist distinct nodes R = {v0 , . . . , vk−1 } such that SR (vi ) = {vi+1 } for every i, with indices taken modulo k. Indeed, if vj ∈ S(vi ) for j ̸= i + 1, we could form a cycle avoiding vi+1 by connecting vi to vj instead of vi+1 (taking indices modulo k), which would contradict minimality of cycle R. Hence DR contains the directed cycle (v0 , v1 , . . . , vk−1 , v0 ). 19

Conversely, suppose that (G, x) ∈ alos. Let r be a selected node, and let T be a BFS tree of G rooted at r. Define ρ(r) = 1, ρ(v) = 0 for every v ̸= r, and c(v) = dT (r, v) mod 3, where dT (r, v) denotes the distance from r to v in T . We claim that (c, ρ) is a valid rooted coloring. Since r is selected, x(r) = 1. Moreover, S(r) = ∅, because no neighbor of the root has distance −1 from r. For every node v ̸= r, the parent of v in the BFS tree has distance dT (r, v) − 1, and therefore belongs to S(v). Hence S(v) ̸= ∅. Now let R ⊆ V be arbitrary. We prove that DR is acyclic. If (v, u) is an edge of DR , then u ∈ S(v). Since the coloring comes from BFS distances, this implies dT (r, u) = dT (r, v) − 1. Therefore, the distance to the root strictly decreases along every directed edge of DR . Hence DR cannot contain a directed cycle. In the next sections, we use this fact to verify that alos belongs to the hierarchy. The remaining difficulty is to express, in the SET model, the XOR verification associated with such red orientations, without relying on ports or on multiplicities of identical neighboring certificates.

4.3

Surjectivity of XOR maps

Given a directed graph D = (V, E), we define the XOR map over D, denoted by XORD : {0, 1}V → {0, 1}V , as follows: X

XORD (z)v = zv +

zu

mod 2.

+ (v) u∈ND

We sometimes refer to maps z : V → {0, 1} as state configurations, or simply as configurations. In this paper we will apply this map only to directed graphs of maximum out-degree at most 1. For such a graph D, we define the function parentD : V → V ∪ {⊥} by setting parentD (v) = u + + if ND (v) = {u}, and parentD (v) = ⊥ if ND (v) = ∅. Then, for every node v, we have (

XORD (z)v =

zv zv + zparentD (v)

if parentD (v) = ⊥, mod 2 otherwise.

For the sake of simplicity, we write XOR instead of XORD whenever the underlying directed graph is clear from the context. The following lemma links the surjectivity of the XOR map with the acyclicity of the underlying directed graph. Lemma 19. Let D = (V, E) be a directed graph with maximum out-degree at most 1. Then XORD is surjective if and only if D contains no directed cycle. Proof. First, suppose that D contains no directed cycle. Since every node has out-degree at most 1, every directed path eventually reaches a node of out-degree 0. Thus, D is a collection of directed trees whose edges point toward roots of out-degree 0. Let y ∈ {0, 1}V be arbitrary. We construct a configuration z ∈ {0, 1}V such that XOR(z) = y. Let B0 be the set of nodes of out-degree 0. For every v ∈ B0 , set zv = yv . Now suppose that z has already been defined for all nodes at directed distance at most i from B0 . Let v be a node at directed distance i + 1 from B0 , and let u = parentD (v). Then zu has already been defined, so we set zv = yv + zu mod 2. This guarantees that XOR(z)v = yv . Proceeding inductively, we define z for every node of D, and therefore XOR is surjective. Conversely, suppose that D contains a directed cycle C. Let A(C) be the set of nodes that can reach C by following directed edges. That is, v ∈ A(C) if and only if there exists a directed path from v to some node of C. 20

Let 0 be the all-zero configuration, and define a configuration y ∈ {0, 1}V by setting yv = 1 if v ∈ A(C), and yv = 0 otherwise. Clearly XOR(0) = 0. We claim that also XOR(y) = 0. Indeed, if v ∈ A(C), then v has exactly one outgoing neighbor u, and this neighbor also belongs to A(C). Hence XOR(y)v = 1+1 = 0 mod 2. If v ∈ / A(C), then either v has no outgoing neighbor, in which case XOR(y)v = yv = 0, or its outgoing neighbor also lies outside A(C), in which case again XOR(y)v = 0 + 0 = 0 mod 2. Thus XOR(0) = XOR(y), while y ̸= 0. Therefore, XOR is not injective. Since {0, 1}V is finite, XOR is not surjective.

4.4

ALOS is in the third level of the SET hierarchy

Now, we put all the pieces together and show that alos is in the third level of the SET hierarchy. We start by stating the following immediate consequence of Lemma 18 and Lemma 19. Lemma 20. Let G = (V, E) be a graph and let x : V → {0, 1} be an input function. Then (G, x) ∈ alos if and only if there exists a valid rooted coloring (c, ρ) such that, for every set R ⊆ V , the XOR map defined over DR = D(G, c, ρ, R) is surjective. Proof. By Lemma 18, (G, x) ∈ alos if and only if there exists a valid rooted coloring (c, ρ) such that, for every set R ⊆ V , the graph DR = D(G, c, ρ, R) has no directed cycle. By Lemma 19, the map XOR over DR is surjective if and only if DR contains no directed cycle. Lemma 20 characterizes alos in terms of the surjectivity of XOR maps on the graphs DR . However, a SET verifier cannot directly check the equations of XORDR , since determining whether a vertex has exactly one red successor requires distinguishing neighbors that may carry identical certificates. Instead, our protocol uses locally checkable XOR-style equations determined by the distinct certificate types visible among red successors. We prove completeness by showing that, for a BFS coloring rooted at a selected vertex, the prover can satisfy these equations for every challenge. For soundness, the disprover chooses the vertex set of a shortest directed cycle in the successor relation. Every red vertex then has exactly one red successor, so the local equations coincide with those of XORDR . The non-surjectivity of this map provides a challenge that no prover response can satisfy. Lemma 9. alos is in the third level of the SET hierarchy. Proof. The protocol has three rounds. In the first round, the prover assigns to every node a rooted coloring (c, ρ), where c(v) ∈ {0, 1, 2} and ρ(v) ∈ {0, 1}. In the second round, the disprover assigns to every node a red bit r(v) ∈ {0, 1}, defining the set R = {v ∈ V : r(v) = 1}, and a bit y(v) ∈ {0, 1}. The bit y(v) is interpreted as a challenge configuration on the red nodes. In the third round, the prover assigns to every node a bit z(v) ∈ {0, 1} and an auxiliary bit a(v) ∈ {0, 1}. Each node v first checks that x(v) ∈ {0, 1}, rejecting otherwise. It then verifies that (c, ρ) is a valid rooted coloring: 1. if ρ(v) = 1, then v checks that x(v) = 1 and S(v) = ∅; 2. if ρ(v) = 0, then v checks that S(v) ̸= ∅. These checks are valid in SET: the input conditions are local, and the successor conditions only require testing the presence of neighboring colors.

21

If v ∈ / R, then v performs no further check. Suppose then that v ∈ R. Let A(v) be the set of pairs (a(u), z(u)) that appear among red successors of v, that is, among nodes u ∈ SR (v). The verifier now checks the local XOR equation as follows: • if A(v) = ∅, then v checks that y(v) = z(v); • if A(v) = {(α, b)}, then v checks that y(v) = z(v) + b mod 2; • if |A(v)| > 1, then v checks that y(v) = z(v). In other words, if v sees a unique red-successor type, it uses that type as its successor in the XOR equation. If it sees either no red-successor type or at least two different red-successor types, it treats itself as having no successor. The auxiliary bit is precisely what allows the last prover to exhibit that two red successors should be distinguished, in which case the outgoing edge of v is cut. We now prove soundness and completeness. First, assume that (G, x) ∈ alos. Let r be a selected node. In the first round, the prover chooses ρ(r) = 1, ρ(v) = 0 for every v ̸= r, and a BFS coloring c(v) = dist(r, v) mod 3. This is a valid rooted coloring. Moreover, for every non-root vertex v, S(v) = {u ∈ N (v) : dist(r, u) = dist(r, v) − 1}. In particular, every successor of v is strictly closer to r. Now consider an arbitrary challenge (R, y) chosen by the disprover. In the third round, the prover sets a(v) = 0 for every v ∈ V , and constructs z in increasing order of distance from r. Suppose that the values z(u) have already been defined for all vertices u with dist(r, u) < dist(r, v). Since every successor of v is closer to r, all values z(u) for u ∈ SR (v) are already fixed. If v ∈ / R, choose z(v) arbitrarily. If v ∈ R, define z(v) =

 y(v), y(v) + b

if {z(u) : u ∈ SR (v)} is empty or contains both bits, (mod 2),

if {z(u) : u ∈ SR (v)} = {b}.

Since a ≡ 0, the set A(v) seen by a red vertex is A(v) = {(0, z(u)) : u ∈ SR (v)}. Therefore, if the successor values are empty or contain both 0 and 1, the verifier uses the equation y(v) = z(v); if all red successors have the same value b, it uses the equation y(v) = z(v) + b (mod 2). By construction, the corresponding equation is satisfied at every red vertex. Hence, for every challenge (R, y), the prover has a third-round response (a, z) that makes all vertices accept. Now assume that (G, x) ∈ / alos. If some vertex has input outside {0, 1}, it rejects regardless of the certificates. Otherwise, x ∈ {0, 1}V , so no vertex is selected. Consider any first-round certificate (c, ρ) proposed by the prover. If (c, ρ) is not a valid rooted coloring, then at least one node rejects in the verification step, independently of the remaining certificates. Suppose then that (c, ρ) is valid. By Lemma 18, there exists a set R ⊆ V such that DR = D(G, c, ρ, R) contains a directed cycle. The disprover chooses R to be the vertex set of such a cycle, so that every red node has exactly one red successor. By Lemma 19, the map XORDR is not surjective. Hence there exists a configuration y : R → {0, 1} with no preimage under XORDR . The disprover chooses this configuration y. Now consider any third-round answer of the prover, including any auxiliary bits and any configuration z. Since every red node has exactly one red successor, the auxiliary bits do not affect the local equation checked by the verifier: each red node v checks precisely y(v) = z(v) + z(parentDR (v)) mod 2. Thus, if all red nodes accepted, we would have XORDR (z) = y, contradicting the choice of y. Therefore at least one red node rejects. All certificates have constant size: c(v), ρ(v), r(v), y(v), z(v), and a(v) are all taken from fixed finite alphabets. We conclude that alos belongs to the third level of the SET hierarchy. 22

4.5

AMOS is in the second level of the SET hierarchy

In this section, we show that amos belongs to the second level of the SET hierarchy. Let G = (V, E) be a graph and let x : V → {0, 1} be an input function. We write M (x) = {v ∈ V : x(v) = 1}. The language amos consists of all configurations (G, x) such that |M (x)| ≤ 1. The idea is to use a universal challenge to force two marked nodes, if they exist, to disagree on a globally constant labeling. Since the graph is connected, the prover can enforce such a labeling using only local equality checks. Lemma 11. amos is in the second level of the SET hierarchy. Proof. We describe a two-round protocol in the SET model. In the first round, the disprover assigns a bit d(v) ∈ {0, 1} to every node v ∈ V . In the second round, the prover answers with a bit a(v) ∈ {0, 1} at every node. The local verifier at each node v first checks that x(v) ∈ {0, 1}, rejecting otherwise. It then checks the following conditions: 1. For every neighbor u ∈ N (v), a(v) = a(u). 2. If x(v) = 1, then a(v) = d(v). Both conditions are locally checkable in the SET model. Indeed, a node knows its own input and certificates, and can verify whether all neighboring certificates have the same a-value as its own. We now prove correctness. Suppose first that (G, x) ∈ amos. Let d : V → {0, 1} be an arbitrary challenge of the disprover. If M (x) = ∅, the prover assigns a(v) = 0 to every node. Both conditions are satisfied. If M (x) = {r}, the prover assigns a(v) = d(r) to every node v ∈ V . The first condition holds because a is constant, and the second holds because r is the only marked node. Thus, for every challenge d, there exists a response a such that all nodes accept. Conversely, suppose that (G, x) ∈ / amos. If some vertex has input outside {0, 1}, it rejects V immediately. Otherwise, x ∈ {0, 1} , and there exist two distinct marked nodes u, v ∈ M (x). The disprover chooses a challenge d such that d(u) = 0 and d(v) = 1. Assume, for contradiction, that the prover can produce a labeling a accepted by every node. By the first verification condition and the connectivity of G, the labeling a must be constant over V . However, the second condition requires a(u) = d(u) = 0

and

a(v) = d(v) = 1,

a contradiction. Therefore, for this challenge, every response of the prover causes at least one node to reject. Finally, both certificates consist of a single bit per node. Hence the protocol uses constantsize certificates and has the quantifier pattern ∀d ∃a. We conclude that amos ∈ SET2 .

4.6

Leader, spanning-tree and closure operations.

Now we state some corollaries of the previous results. The first important corollary is that the problem leader is in the hierarchy SET. Theorem 1. leader is in the third level of the SET hierarchy. Proof. Since leader = alos ∩ amos, as a consequence of the first result in Lemma 17 we have that leader ∈ SET3 .

23

A direct application of the latter corollary and of the coloring orientations used in the proof of Lemma 9 is that a suitable spanning-tree-like language belongs to the SET hierarchy. It is important to notice that we use a slightly unconventional definition of this language. Traditionally, see, e.g. [14], the language SpanningTree consists of graphs with marked edges, where the marked edges encode a spanning tree T of G. This definition does not suit our model, since in the SET model we have no identifiers or ports that would allow nodes to refer to individual incident edges. Instead, we define a SET-induced spanning tree language, denoted by SetTree, whose instances are network configurations of the form (G, (x, c)), where x : V → {0, 1} and c : V → {0, 1, 2}. The map x is intended to mark the root, and the coloring c is intended to define local successor relations through the sets S(v) = {u ∈ N (v) : c(u) = c(v) − 1 mod 3}. Formally, we say that (G, (x, c)) ∈ SetTree if the following conditions hold: 1. there exists a unique node r ∈ V such that x(r) = 1; 2. the pair (c, x) is a valid rooted coloring; 3. for every set R ⊆ V , the graph DR = D(G, c, x, R) is acyclic. Equivalently, 

  

 (G, x) ∈ leader,  SetTree = (G, (x, c)) : (c, x) is a valid rooted coloring, .    for every R ⊆ V, DR is acyclic 

Observe that the first condition is exactly (G, x) ∈ leader. The second condition is locally checkable in the SET model. The third condition can be verified using the XOR characterization of acyclicity from Lemma 19, exactly as in the proof of Lemma 9. More precisely, we obtain the following corollary. Corollary 21. SetTree ∈ SET3 . Proof. We verify the three conditions in the definition of SetTree. The first condition, (G, x) ∈ leader, belongs to SET3 by Theorem 1. For the remaining conditions, the prover uses a certificate cb : V → {0, 1, 2} copying the input coloring c. Every vertex checks locally that cb(v) = c(v). Hence neighboring values of c become visible through the certificates. The validity of the rooted coloring (c, x) can then be checked locally: a vertex with x(v) = 1 checks that it has no successor, while every vertex with x(v) = 0 checks that it has at least one successor. It remains to verify that, for every R ⊆ V , the graph DR = D(G, c, x, R) is acyclic. Consider the directed relation H = {(v, u) : u ∈ S(v)}. We first observe that H is acyclic

⇐⇒

DR is acyclic for every R ⊆ V.

The forward implication is immediate. Conversely, suppose that H contains a directed cycle, and choose one of minimum length. Let R be its vertex set. By minimality, each vertex of the cycle has exactly one successor in R; otherwise an additional edge between two vertices of the cycle would produce a shorter directed cycle. Hence this cycle also appears in DR . We now give a two-round protocol for the acyclicity condition. The disprover chooses R ⊆ V and a bit labeling y. The prover responds with a bit labeling z, an auxiliary bit labeling a, and the copy cb described above. If H is acyclic, process its vertices in an order in which every successor of a vertex has already been processed. Set a ≡ 0, and define z(v) exactly as in the completeness proof of Lemma 9: if the set of z-values of red successors of v is empty or contains both bits, set z(v) = y(v); if all 24

red successors have the same value b, set z(v) = y(v) + b (mod 2). Thus every local equation checked by the verifier is satisfied. Conversely, if some DR contains a directed cycle, the disprover chooses R to be the vertex set of such a cycle and chooses a configuration y with no preimage under XORDR . Every red vertex then has exactly one red successor, so the auxiliary bits cannot change the equation being checked. Hence no response of the prover makes all vertices accept. Therefore the second and third conditions can be verified with the quantifier pattern ∀(R, y) ∃(cb, a, z). They belong to SET2 . Intersecting this language with leader ∈ SET3 , using Lemma 17, gives SetTree ∈ SET3 . Now we show that the complement of a language in the SET hierarchy also belongs to the hierarchy, with a constant increase in the level. More precisely, for k ≥ 0, let co-SETk = {L : L ∈ SETk }. Corollary 22. co-SETk ⊆ SETk+3 . Proof. Let L ∈ co-SETk . Then L ∈ SETk . By definition, there exists a SET local verifier A such that (G, x) ∈ L ⇐⇒ Q1 ℓ1 Q2 ℓ2 · · · Qk ℓk ∀v ∈ V, A(G, x, v, ℓ) = 1, where ℓ = (ℓ1 , . . . , ℓk ). Taking the complement of this statement, we obtain (G, x) ∈ L ⇐⇒ Q1 ℓ1 Q2 ℓ2 · · · Qk ℓk ∃v ∈ V, A(G, x, v, ℓ) = 0, where ∃ = ∀ and ∀ = ∃. The existential quantifier over nodes can be expressed by means of a non-empty set of marked nodes. More precisely, introduce an additional labeling ℓ′ : V → {0, 1}. The condition ∃v ∈ V such that A(G, x, v, ℓ) = 0 is equivalent to the existence of a labeling ℓ′ such that: 1. (G, ℓ′ ) ∈ alos; 2. for every node v, if ℓ′ (v) = 1, then A(G, x, v, ℓ) = 0. Therefore, (G, x) ∈ L ⇐⇒ Q1 ℓ1 Q2 ℓ2 · · · Qk ℓk ∃ℓ′ ∈ {0, 1}V (

such that

(G, ℓ′ ) ∈ alos, ∀v ∈ V, ℓ′ (v) = 1 ⇒ A(G, x, v, ℓ) = 0.

The condition (G, ℓ′ ) ∈ alos is in SET3 by Lemma 9. The second condition is locally checkable without adding any new alternation: each node only has to verify that, if it is marked by ℓ′ , then the original verifier A rejects at that node. Thus, after the k complemented quantifier rounds, we can append the three-round SET protocol for alos. This gives a protocol in SETk+3 . Hence L ∈ SETk+3 , and therefore co-SETk ⊆ SETk+3 .

Example 23. Since 3-colorability belongs to SET1 , Corollary 22 implies that non-3-colorability belongs to SET4 . We remark that [10] shows that non-3-colorability requires certificates of size Ω̃(n2 ) at the first level of the hierarchy, even when the nodes of the network have unique identifiers and the verification algorithm is allowed to inspect a constant-radius neighborhood. 25

The same argument applies to the MULTISET and PORTS hierarchies. Indeed, the proof only uses the fact that alos belongs to the third level and that the local rejection condition of the original verifier can be checked in the underlying model. Since SET3 ⊆ MULTISET3 ⊆ PORTS3 , we obtain co-MULTISETk ⊆ MULTISETk+3 , co-PORTSk ⊆ PORTSk+3 . The construction is uniform in the port numbering and also applies to predicates of portnumbered configurations.

The power of the SET hierarchy

5

In this section, we show that the SET hierarchy equals MSO. Recall that MSO on graphs uses quantification over vertices, called first-order quantification, and over sets of vertices, called monadic second-order quantification. Its atomic formulas are: • xi = xj , expressing equality of vertices; • xi ∼ xj , expressing adjacency; • xi ∈ Xj , expressing membership of a vertex in a set. We show first that any graph language expressible in MSO belongs to some level of the SET hierarchy. Later, we show the opposite direction.

5.1

The SET hierarchy contains MSO

We first prove the containment for MSO in the SET hierarchy. Lemma 12. Every MSO-definable distributed language over a finite input alphabet belongs to the SET hierarchy. Proof. Let ϕ be an MSO sentence. We prove the result by induction on the structure of ϕ. Variable assignments are represented by bit labelings. A set variable X is represented by an arbitrary labeling ℓX : V → {0, 1}, where ℓX (v) = 1 means v ∈ X. A first-order variable x is represented by a bit labeling ℓx : V → {0, 1}, intended to mark exactly one vertex. We prove the stronger claim that, for every subformula ψ, its truth can be verified uniformly for any fixed assignment of its free variables, represented by bit labelings. These labelings are treated as previously assigned certificate fields: they remain visible to the verifier and its neighbors through the usual SET view, and are not quantified again by the subprotocol. We assume that the labelings of free first-order variables mark exactly one vertex. Under this invariant, the atomic formulas are locally checkable. For x = y, every vertex checks that ℓx (v) = ℓy (v). For x ∼ y, the unique vertex marked by ℓx checks that the type ℓy = 1 appears among its neighbors. For x ∈ X, the unique vertex marked by ℓx checks that ℓX (v) = 1. If the vocabulary contains input predicates Pσ , corresponding to a fixed finite input alphabet, then Pσ (x) is checked by the unique vertex marked by ℓx , which verifies that its own input is σ. Negations of atomic formulas, as well as conjunctions and disjunctions, can be handled using closure of the SET hierarchy under complement, intersection, and union. It remains to simulate quantification. For a set variable there is no validity restriction. Thus ∃X ψ is simulated by an existentially quantified bit labeling ℓX , followed by the protocol for ψ, and similarly ∀X ψ is simulated using a universally quantified bit labeling. 26

For a first-order variable, the labeling must represent a single vertex. Let Sing(ℓx ) denote the property that (G, ℓx ) ∈ leader. By Theorem 1, Sing belongs to the SET hierarchy.
An existential first-order quantifier is simulated as ∃ℓx Sing(ℓx ) ∧ ψb . Thus an invalid labeling cannot witness an existential quantifier. A universal first-order quantifier is simulated
b as ∀ℓx ¬ Sing(ℓx ) ∨ ψ . Hence labelings that do not represent a vertex impose no requirement, while every singleton labeling must satisfy the translation of ψ. This is exactly the semantics of universal first-order quantification. By Lemma 17 and corollary 22, Boolean combinations can be implemented uniformly while preserving all previously assigned certificate fields. Likewise, each logical quantifier introduces a new bit labeling before the auxiliary rounds verifying its scope. Consecutive quantifiers of the same type can be merged, and dummy rounds can be added when needed. The induction therefore yields a finite-round SET protocol for every subformula, uniformly in its free-variable assignments. Since ϕ is a sentence, the resulting protocol has no free variables and recognizes precisely Lϕ . Hence every MSO-definable distributed language over a finite input alphabet belongs to the SET hierarchy.

5.2

MSO contains the SET hierarchy

We now show that the SET hierarchy captures exactly MSO-definable languages. Combined with Lemma 12, this gives an exact correspondence between MSO and the SET hierarchy. Let A be a local verifier in the SET model using certificate alphabets Γ1 , . . . , Γk , and let Σ be the finite input alphabet. The local view of a node consists of its own input and certificate sequence, together with the set of certificate sequences appearing among its neighbors. In particular, a node does not observe the input values of its neighbors. We therefore distinguish two types of local information. An own type is a tuple Y

τ = (σ, a1 , . . . , ak ) ∈ Σ ×

Γi ,

i∈[k]

while a neighbor certificate type is a tuple α = (a1 , . . . , ak ) ∈

Y

Γi .

i∈[k]

Each certificate assignment is encoded by a finite tuple of monadic second-order variables, one set for each possible certificate value. These sets are required to form a partition of the vertex set. We then construct MSO formulas describing the own type of a node and the set of neighbor certificate types it observes. Since all alphabets are finite, there are only finitely many possible local views, and the acceptance condition of the verifier can be expressed as a finite disjunction of MSO formulas. Lemma 13. Let L ∈ SETk be a language over a finite input alphabet. Then L is MSO-definable. Proof. Let L ∈ SETk . By definition, there exists a local verifier A, finite certificate alphabets Γ1 , . . . , Γk , and quantifiers Qi ∈ {∃, ∀}, for i ∈ [k], such that (G, x) ∈ L if and only if Q1 ℓ1 : V → Γ1 Q2 ℓ2 : V → Γ2 · · · Qk ℓk : V → Γk ∀v ∈ V, A(G, x, v, ℓ1 , . . . , ℓk ) = 1. Let Σ be the finite input alphabet. For every input symbol σ ∈ Σ, we use a unary predicate Pσ , where Pσ (v) means that x(v) = σ.

27

For each certificate round i ∈ [k], we encode a labeling ℓi : V → Γi by a tuple of monadic i second-order variables X = (Xai )a∈Γi . The intended meaning is that v ∈ Xai if and only if ℓi (v) = a. We enforce this intended meaning with the partition formula       ^  _ i i i i   v ∈ X ∧ ¬ v ∈ X ∧ v ∈ X Parti (X ) := ∀v  a a b  . a∈Γi

a,b∈Γi a̸=b

i

Thus, Parti (X ) says that every vertex receives exactly one certificate from Γi . We now define the MSO translation of the quantifier prefix. For a formula ψ, define recursively Tk+1 (ψ) := ψ, and, for i ∈ [k], 
∃X i Parti (X i ) ∧ Ti+1 (ψ) , Ti (ψ) :=
i i 

if Qi = ∃,

∀X Parti (X ) ⇒ Ti+1 (ψ) ,

if Qi = ∀.

This ensures that existential and universal quantifiers range only over valid certificate labelings. It remains to express the local acceptance predicate of A in MSO. We distinguish the finite sets of own types and neighboring certificate types: Town = Σ ×

Y

Y

Tnbr =

Γi ,

Γi .

i∈[k]

i∈[k]

For every own type τ = (σ, a1 , . . . , ak ), define Typeτ (v) := Pσ (v) ∧

^

v ∈ Xai i .

i∈[k]

For every neighboring certificate type α = (a1 , . . . , ak ), define Certα (u) :=

^

u ∈ Xai i .

i∈[k]

Notice that Certα (u) does not refer to the input of u, since neighboring input values are not visible in the SET model. For every T ⊆ Tnbr , define SetViewT (v) :=

^

∃u u ∼ v ∧ Certα (u)

α∈T

!

∧ ∀u

u∼v⇒

_

Certα (u) .

α∈T

The first condition requires every certificate type in T to appear among the neighbors of v, while the second excludes all other types. Thus SetViewT (v) describes exactly the neighboring information available to the SET verifier. Since A is fixed and all alphabets are finite, its accepting local views form a finite set W A ⊆ Town × 2Tnbr . We define AcceptA (v) := (τ,T )∈A (Typeτ (v) ∧ SetViewT (v)) . By construction, AcceptA (v) holds if and only if the original SET verifier A accepts at v.
Finally, define the MSO sentence φL := T1 ∀v AcceptA (v) . By the construction above, for every input graph (G, x), (G, x) ∈ L

if and only if 28

(G, x) |= φL .

Therefore L is MSO-definable. We can also bound the quantifier depth of the resulting formula in terms of the certificate alphabets. The formula ∀v AcceptA (v) has quantifier depth at most 2. For each round i, the i i tuple X contains |Γi | monadic second-order variables, while the partition condition Parti (X ) has quantifier depth 1. Since this condition is combined with the remaining translation by conjunction or implication, the recursive definition of Ti gives a quantifier depth of at most 2+

k X

|Γi |

i=1

for φL . Thus the bound depends on the certificate alphabets of the chosen protocol, as well as on the number of certificate rounds.

5.3

Trading horizon for interaction

In this subsection, we discuss extensions of the SET model in which the verifier can inspect certificates beyond its immediate neighborhood. We first explain that there are two natural ways to define such a model, denoted the weak r-horizon SET model and the strong r-horizon SET model. The weak model need not become more expressive as the horizon increases. For the strong model, we show that any fixed horizon can be simulated at horizon one with at most one additional interaction. In the weak r-horizon SET model, a node v always has access to its own input x(v) and its own certificate sequence ℓ(v), n separately from theocertificates of other vertices. In addition, it observes the set Wr (v) = ℓ(u) : u ∈ Br (v) \ {v} , where Br (v) = {u ∈ V : dist(u, v) ≤ r}. Thus, the node observes the set of certificate sequences appearing at other vertices within distance at most r, without distinguishing their distances or multiplicities. In particular, for r = 1, W1 (v) = {ℓ(u) : u ∈ N (v)}, so the weak 1-horizon model coincides exactly with the original SET model. The power of the weak model is not monotone in the horizon. In particular, the weak 2horizon model does not necessarily simulate the usual radius-one model. Consider the language Star = {G : G ≃ K1,n for some n ≥ 2}. This language is recognizable in the weak 1-horizon SET model with two alternating certificate assignments. In the first round, the prover assigns each vertex a role in {C, L0 , L1 }, where C denotes a center and L0 , L1 denote two types of leaves. In the second round, the disprover assigns an arbitrary bit d(v) to each vertex. Each vertex performs the following checks using its own certificates and the set of certificate sequences of its neighbors. A vertex marked C checks that it has no neighbor marked C, and that it has at least one neighbor of type L0 and at least one of type L1 . A vertex marked L0 or L1 checks that all its neighbors are marked C, and that the set {d(u) : u ∈ N (v), σ(u) = C} contains exactly one element, where σ denotes the first-round role assignment. If G = K1,n with n ≥ 2, the prover marks the center with C, one leaf with L0 , and all remaining leaves with L1 . Every verification condition then holds, regardless of the disprover’s bits. Conversely, suppose that a first-round role assignment is accepted for every assignment of the disprover’s bits. There can be no edge between two centers or between two leaves, by the local role checks. Moreover, every leaf has exactly one center neighbor: it must have at least 29

one, and if it had two distinct center neighbors, the disprover could assign different bits to them, causing the leaf to reject. Since G is connected, these conditions imply that there is exactly one center and that every other vertex is adjacent only to this center. Finally, the center must have at least two leaves, since it sees both types L0 and L1 . Therefore, G ≃ K1,n for some n ≥ 2. However, Star is not recognizable in the weak 2-horizon model. Consider, for every n ≥ 2, the graphs K1,n and Kn+1 on the same vertex set. Both graphs have diameter at most 2. Hence, in the weak 2-horizon model, for every node v in either graph, the ball B2 (v) is the whole vertex set. It follows that no weak 2-horizon SET protocol can distinguish K1,n from Kn+1 . Thus Star is not recognizable in the weak 2-horizon SET hierarchy. To obtain a monotone extension of the original SET model, we introduce the following definition. Let r ≥ 1. In the strong r-horizon SET model, suppose that a protocol uses k certificate assignments ℓi : V → Γi for i ∈ [k]. Write γ(v) = (ℓ1 (v), . . . , ℓk (v)) for the certificate sequence of vertex v. After the certificate assignments have been made, each vertex v has access to its own input x(v) and its own certificate sequence γ(v), separately from the certificates of other vertices. In addition, the vertex observes the tuple (SN (v), S≤2 (v), . . . , S≤r (v)) , where SN (v) = {γ(u) : u ∈ N (v)} is the usual SET neighborhood view, and, for every 2 ≤ j ≤ r, S≤j (v) = {γ(u) : u ∈ Bj (v)}. The sets S≤j (v) include the certificate sequence of v, since v ∈ Bj (v). However, the immediate neighborhood view SN (v) is provided separately. Thus, a vertex can always distinguish its own certificates from the presence of the same certificates among its immediate neighbors. As usual in the SET model, multiplicities are not visible in any of these sets. When r = 1, the tuple consists only of SN (v). Hence the strong 1-horizon model coincides exactly with the original SET model. We denote the corresponding k-th level by SETkr , so that SETk1 = SETk . Moreover, for every r ≥ 1 and every k ≥ 0, SETk1 ⊆ SETkr , since a strong r-horizon verifier can ignore the additional ball information and use only SN (v). We now prove the converse inclusion with at most one additional interaction. Theorem 14. For every fixed r ≥ 1, SET r =

S

S r 1 k≥0 SETk = k≥0 SETk = SET.

Proof. Let L ∈ SETkr , and let A be a strong r-horizon SET verifier recognizing L. We construct a radius-one SET protocol using at most one additional certificate round. Let ℓi : V → Γi , for i ∈ [k], be the certificate assignments of the original protocol. Write C = Γ1 × · · · × Γk for the finite alphabet of complete certificate sequences, and let γ(v) = (ℓ1 (v), . . . , ℓk (v)) ∈ C. For k = 0, we take C to consist of the unique empty sequence. The prover supplies to every vertex v a tuple (T0 (v), T1 (v), . . . , Tr (v)), where each Tj (v) ⊆ C. These sets are intended to satisfy Tj (v) = {γ(u) : u ∈ Bj (v)} for 0 ≤ j ≤ r. The tuple is supplied in an existential certificate assignment after all original certificate fields have been determined. If the original protocol ends with an existential assignment, these additional fields are merged into that assignment. Otherwise, we append one existential round. We claim that the intended values of the sets Tj (v) can be verified using only radius-one SET information. First, every vertex v checks T0 (v) = {γ(v)}. Then, for every j ∈ [r], it checks Tj (v) = S T0 (v) ∪ u∈N (v) Tj−1 (u). This condition is locally checkable in the SET model: the vertex reads its own set T0 (v) and the set of values Tj−1 (u) appearing among its neighbors. Multiplicities are irrelevant because the operation is set union. We now show that if all vertices pass these checks, every claimed set is correct. The assertion S holds for j = 0 by the first check. Suppose it holds for j−1. Since Bj (v) = {v}∪ u∈N (v) Bj−1 (u),

30

we obtain Tj (v) = {γ(v)} ∪

[

Tj−1 (u)

u∈N (v)

= {γ(u) : u ∈ Bj (v)}. Thus the assertion follows by induction for every 0 ≤ j ≤ r. Once these sets have been verified, the radius-one verifier reconstructs the strong r-horizon view required by A. The vertex already knows its own input x(v) and original certificate sequence γ(v). Moreover, it directly observes the original SET neighborhood view SN (v) = {γ(u) : u ∈ N (v)} by projecting the certificate sequences of its neighbors onto the fields of the original k rounds. For each 2 ≤ j ≤ r, the remaining component of the strong view is S≤j (v) = Tj (v). Therefore the verifier can reconstruct exactly the tuple (SN (v), S≤2 (v), . . . , S≤r (v)) and simulate the original verifier A. If any consistency check fails, the new verifier rejects. We now establish correctness. Fix any assignment of the original k certificate fields. If the original verifier accepts at every vertex, the prover can supply the correct sets Tj (v) = {γ(u) : u ∈ Bj (v)}. Every consistency check succeeds, and the new verifier reconstructs the exact strong r-horizon view at every vertex. Hence all vertices accept. Conversely, suppose that some assignment of the additional sets makes all vertices accept. The consistency checks force all the sets Tj (v) to have their intended values. Consequently, the new verifier simulates exactly the strong r-horizon verifier A, which must therefore accept at every vertex. Thus, for every fixed assignment of the original certificate fields, there exists an accepting assignment of the additional sets if and only if the original verifier accepts everywhere. This equivalence preserves the entire alternating quantifier prefix of the original protocol. Finally, all certificates have constant size: the alphabet C is finite, r is fixed, and each additional certificate consists of r + 1 subsets of C. If the original protocol ends with a universal assignment, the new existential round extends its alternating prefix by one round. If it ends with an existential assignment, the additional fields are merged into that round, so no extra round is needed. For k = 0, one existential round suffices. Whenever necessary, a dummy round can be appended to obtain exactly k + 1 alternating rounds. S 1 Therefore, SETkr ⊆ SETk+1 . Together with SETk1 ⊆ SETkr , this implies k≥0 SETkr = S 1 k≥0 SETk = SET.

5.4

Comparison with distributed graph automata

In [15], an equivalence is established between languages recognized by MSO formulae and those recognized by alternating distributed graph automata. Alternating distributed graph automata are automata using a finite set of states Q with a local transition of the form2 : Q × 2Q → 2Q . This local transition map is applied uniformly at each node of the input graph on the state of the node together with the set of states of neighbors. Together with the initialization map used to read input labels on nodes locally, it implements the same mode of communication as in the SET model. Moreover, states are leveled and typed level-wise as existential, universal or permanent. The transition map can only increase the level until reaching a permanent state, so that there is convergence after a bounded number of applications. Universal and existential states have the same interpretation as in classical alternating automata. Since the type of states is the same at each level, this is equivalent to alternating a bounded number of prover/disprover rounds 2

This is the simplified form from [15] when restricting to graph without edge labeling, to fit the formalism of the present paper.

31

and letting a local SET algorithm decide whether it (locally) accepts or not given all the local labelings introduced by the prover/disprover interaction. The key difference between these two models lies in the accepting condition: for alternating distributed graph automata, a global condition on the set of permanent states present in the graph after convergence is used, whereas in the SET model the unanimity condition is used (all nodes must accept locally) as in the LOCAL model and other hierarchies based on it [16, 7]. In the formalism of [15], the unanimity condition is an accepting condition consisting of one “accepting set” which is the singleton {accept} (meaning that a run is accepting if and only if the set of permanent sets in the graph once stabilized is exactly {accept}). Thus, the SET model can be seen as a particular case of alternating distributed graph automata, and Theorem 2 can be seen as a strengthened version of the equivalence result of [15] using a simpler accepting condition, which is natural in the context of distributed computing. This difference in accepting condition is not just a technical convention, and we would like to point out three noticeable differences between the two models. Levels and number of alternations. The two models involve quantifier alternation (or levels) but they are not equivalent level-wise. In particular, the ALOS problem which is key in establishing Theorem 2 is at level three of the SET hierarchy (Theorem 9), but it is trivial in the formalism of alternating distributed graph automata: just take the initialization map that read the local input label into states and use as accepting condition the two sets {1} and {1, 0} (thus requiring at least one 1 among input labels on nodes). Thus ALOS doesn’t require any kind of alternation in the formalism of [15], which places it at the same level as purely LOCAL languages. Non-connected graphs. If one extends the SET model to non-connected graphs, the accepting condition is such that a graph is accepted if and only if all of its connected components are accepted. In particular ALOS on non-connected graphs cannot be recognized in the SET model. With the global accepting condition of [15], there is no such limitation and ALOS is recognized on non-connected graphs using the same distributed graph automaton as above. Deciding if a graph is connected (still a MSO property) is easy with distributed graph automata. Indeed, with one level of universal states one can put a random bit on each node and goes to permanent state b ∈ {0, 1} if b is the only random bit seen in the neighborhood and to the reject permanent state otherwise. Then the accepting condition is made of sets {1}, {0} and all possible sets containing reject. This characterizes connectedness because non-connected graphs can lead to the set of permanent states {0, 1}, and a connected graph will never produce {0, 1} as final set of permanent states because if both bits 0 and 1 are present in the graph, then a node will see them both in its neighborhood and turn into reject. Connectedness is however impossible to capture with model SET. Infinite graphs. In both models, no identifier are used on nodes to distinguish them, so they both make perfect sense on arbitrary infinite graphs. Although [15] only deals with finite graphs, it seems clear that the equivalence with MSO holds on infinite graphs (in particular one can check that the automaton for ALOS above perfectly works on infinite graphs). We would like to stress that the equivalence between SET and MSO breaks on infinite graphs for a deep reason: recognized language with the unanimity acceptance condition are topologically closed, but some MSO languages like ALOS are not. Although it goes beyond the scope of the present paper, let us make this statement more precise. Fix G = Z, the bi-infinite line graph (i ∈ Z is connected to i + 1 and i − 1), and let us restrict to languages made only of labelings of G, or equivalently, languages of bi-infinite words. For a finite alphabet Σ, the space ΣZ , equipped with the product of the discrete topology on Σ, is compact. The language ALOS restricted to G is not a closed set in this topology: indeed, 32

the sequence of yes-instances where the unique occurrence of 1 is at position i converges, when i → ∞, to the all 0 configuration which is a no-instance. However, we claim that any language of bi-infinite words recognized in the SET hierarchy is closed, and hence that ALOS is not recognizable in SET for infinite graphs. This closedness property roughly holds for the following reasons: first, acceptance at a given node i is a closed condition because it depends on finitely many positions (neighbors of i). So unanimous acceptance is an intersection of closed set, hence a closed set. This is true even in the context of a fixed free variable not part of the input labeling. Second, the property is preserved when climbing up in the hierarchy because quantification has the following topological interpretation: on one hand, universal quantification corresponds to intersection, and, on the other hand, existential quantification corresponds to a continuous projection (hence sending closed sets to closed sets by the closed map lemma since the ambient space is compact). As an alternative proof, one can check that SET-recognized languages belongs to the u-MSO fragment of [17] and then use Corollary 1 therein. This topological constraint disappears on finite graphs (which do not form a compact set), and the finiteness property is crucially used in lemmas 18 (all nodes having a successor implies existence of a cycle) and 19 (injectivity is equivalent to surjectivity for finite maps). Both lemmas are false on infinite graphs.

Counting in PORTS and comparison with CMSO

6

We now turn to CMSO. Recall that CMSO extends MSO with counting predicates Cardqp (Xi ), which express cardinality modulo a fixed positive integer. Here we prove their verification in PORTS; the weaker MULTISET model is considered separately below.

6.1

Counting modulo a constant

The key point is not merely to count neighboring certificates but to obtain a rooted tree on every connected graph with constant-size vertex labels. Demanding that each non-root vertex have exactly one neighbor of the preceding color modulo three does not suffice: such a coloring need not exist (already on K3,3 ). Instead, in PORTS every node selects the first eligible neighbor according to its fixed local ordering of ports. Fix an arbitrary port numbering π of G = (V, E), a root marking r : V → {0, 1}, and a coloring t : V → {0, 1, 2}. Define St (v) = {u ∈ N (v) : t(u) = t(v) − 1

(mod 3)}.

If St (v) ̸= ∅, let parentπ (v) be the neighbor in St (v) incident to the smallest local port of v. This selects a single neighbor regardless of how many eligible neighbors share the same labels. At a root, or if no eligible neighbor exists, set parentπ (v) = ⊥. Let PortTree denote the property of a port-numbered configuration (Gπ , (r, t)) satisfying: 1. exactly one node r0 has r(r0 ) = 1; 2. St (r0 ) = ∅, and St (v) ̸= ∅ for every v ̸= r0 ; 3. the functional digraph Tr,t,π , with edges v → parentπ (v) for v ̸= r0 , is acyclic. The selected parent relation, and hence PortTree, may depend on the port numbering π. We use PortTree only as an auxiliary condition in the counting protocol, which must recognize the same language for every port numbering. We say that such a predicate admits a uniform k-round PORTS protocol if the same verifier and certificate alphabets recognize it for every fixed port numbering, using k alternating certificate assignments. 33

Under these conditions Tr,t,π is a spanning tree directed toward r0 : in a finite acyclic functional digraph every path reaches a vertex without a parent, and this vertex must be the unique root. Corollary 24. The predicate PortTree admits a uniform three-round PORTS protocol with quantifier pattern ∃∀∃. Moreover, for every connected graph G and every port numbering π, there exist r, t satisfying PortTree. Proof. The unique-root requirement is the language leader, which belongs to SET3 ⊆ PORTS3 . The first existential round can also copy the bounded input r, t into certificates and locally check that the copies are faithful, as in Remark 25. Each vertex can then inspect the copies at its ports, verify the second condition, and identify its selected parent. The universal round supplies y, and the final existential round supplies z. For acyclicity, use Lemma 19 on Tr,t,π . For a universal bit labeling y, the final prover supplies a bit labeling z. A root checks y(v) = z(v), while every other node checks y(v) = z(v) + z(parentπ (v))

(mod 2).

Each equality is local in PORTS: a node reads z at the first eligible port. The condition ∀y ∃z holds exactly when the selected functional digraph is acyclic. Hence this condition lies at level two. Combining these checks with the three-round protocol for leader gives a uniform ∃∀∃ protocol for PortTree. All checks use the same fixed port numbering. Finally, let r0 be any node and put t(v) = distG (r0 , v) mod 3, with r marking r0 . Every non-root vertex has a neighbor one step closer to the root, while the root has no preceding-color neighbor. Along every eligible edge v → u, BFS distance strictly decreases: adjacent vertices have distances differing by at most one, and the preceding-color condition forces the difference to be exactly one. Consequently every port-selected parent relation is acyclic, for every π. This proves the existence assertion. For p ≥ 1 and 0 ≤ q < p, define Count(q, p) = {(G, x) : x ∈ {0, 1}V ,

|M (x)| ≡ q

(mod p)},

M (x) = {v ∈ V : x(v) = 1}.

Any other integer representative q is handled by replacing it with its residue modulo p. As usual, a fixed finite alphabet can be copied into a constant-size certificate in an existential round, making that information visible to neighbors; cf. the following observation. Remark 25. When the input alphabet is bounded, one existential quantifier can make bounded input information locally visible to the verifier. For example, if x ∈ {0, 1}k for fixed k, then ∀v ∀u ∈ N (v),

x(v) = x(u)

holds if and only if there exists a labeling ℓ such that each node checks ℓ(v) = x(v) and ℓ(u) = ℓ(v) at all its neighbors. This works in each of the three local models. Lemma 15. For all q, p ∈ N, with p ≥ 1, and 0 ≤ q < p, Count(q, p) belongs to PORTS9 . Proof. Fix an arbitrary port numbering π. The initial prover supplies ℓr : V → {0, 1} and ℓt : V → {0, 1, 2}, intended to certify PortTree. By the preceding corollary, a suitable pair exists for all connected yes-instances, independently of π. The prover also supplies ℓc : V → {0, . . . , p − 1}. For each vertex v, the intended recurrence is X ℓc (v) ≡ x(v) + ℓc (u) (mod p). (2) u:parentπ (u)=v

34

Here the sum ranges over the children of v in the port-selected tree, not over all its neighbors. The prover must also satisfy the local condition ℓr (v) = 1 ⇒ ℓc (v) = q. If all recurrences hold, induction from the leaves gives ℓc (r0 ) ≡ |M (x)| (mod p). To test all these equations without allowing a vertex to inspect the port choices of its neighbors, the disprover marks a challenge vertex by a bit labeling ℓp : V → {0, 1}. When (G, ℓp ) ∈ leader, let v ∗ be the uniquely marked node. If the challenge is not in leader, it is ignored. The final prover supplies ℓ : V → {0, . . . , p − 1}. We require (

ℓ(u) =

ℓc (u), 0,

if u ̸= r0 and ℓp (parentπ (u)) = 1, otherwise.

(3)

This equation is locally checkable in PORTS: a non-root node selects its parent using the first eligible port, reads the parent’s challenge bit, and checks its own value ℓ(u). The root checks ℓ(r0 ) = 0. At any challenged vertex v the verifier also checks ℓc (v) ≡ x(v) +

X

ℓ(u)

(mod p).

(4)

u∈N (v)

This sum is local in PORTS, which presents one certificate value per incident port (including repeated values). If the challenge is unique and (3) holds, the sum in (4) is exactly the sum of ℓc over the children of v ∗ . Thus (4) tests (2) at v ∗ . We now combine these conditions. Fix a port numbering π. The protocol uses the outer quantifier prefix ∃(ℓr , ℓt , ℓc ) ∀ℓp ∃ℓ. After these assignments, the remaining verification requires: 1. (Gπ , (ℓr , ℓt )) ∈ PortTree. 2. Every vertex v checks that x(v) ∈ {0, 1} and that ℓr (v) = 1 ⇒ ℓc (v) = q. 3. Either (G, ℓp ) ∈ / leader, or (3) holds at every vertex and (4) holds at the unique vertex marked by ℓp . The first condition is verified by the uniform protocol of Corollary 24. The second is directly local. In the third condition, the two equations are also directly checkable in PORTS: all the labelings involved have already been chosen in the outer rounds and are therefore available as neighboring certificate fields. Although the first and third conditions may depend on π, the complete protocol uses the same verification algorithms for every port numbering. For every fixed π, these conditions are equivalent to membership in Count(q, p). Here the outer existential labels have constant size because p is fixed. For completeness, use a BFS-distance coloring and the true subtree sums; for each valid challenge the final prover uses the uniquely determined values in (3). For soundness, invalid inputs are rejected locally, and invalid tree certificates are caught by the PortTree check. For a valid binary input and a valid tree, an incorrect root value causes rejection; otherwise, the disprover challenges a vertex where the recurrence fails. Equation (3) forces exactly its children’s contributions, and (4) rejects for every final reply. We now make the number of rounds explicit. By Corollary 24, PortTree has an ∃∀∃ protocol. Since leader has the same quantifier pattern, Corollary 22 gives a ∀∃∀∃∀∃ protocol for leader. Denote their certificate assignments by α1 , α2 , α3 and β1 , . . . , β6 , respectively. Let E denote the local condition requiring (3) everywhere and (4) at every challenged vertex. Condition (3) above is precisely leader(ℓp )∨E. We implement this disjunction using a globally constant existential selector b, chosen before the universal challenges of the leader protocol. 35

The complete alternating prefix is ∃(ℓr , ℓt , ℓc ) ∀ℓp ∃(ℓ, b, α1 ) ∀(α2 , β1 ) ∃(α3 , β2 ) ∀β3 ∃β4 ∀β5 ∃β6 . The α-fields verify PortTree. If b = 0, the β-fields verify leader(ℓp ); if b = 1, the verifier checks E directly. The root condition is checked locally. Correctness follows from the preceding argument: on yes-instances, the prover certifies a valid tree and correct subtree sums, choosing the appropriate branch for each challenge. On noinstances, either the tree or root check fails, or the disprover selects a vertex with an incorrect recurrence. In the latter case, neither branch can succeed. All certificate alphabets are finite, and the construction is uniform in the port numbering. Thus Count(q, p) ∈ PORTS9 .

This bound is an upper bound only. In particular, we do not assert that the same protocol works in MULTISET: an unnumbered multiset does not let a node choose the first eligible port when several neighbors carry the same certificate.

6.2

The PORTS hierarchy contains CMSO

Theorem 3. Every CMSO-definable language belongs to the PORTS hierarchy. Proof. Let ϕ be a CMSO sentence. We use the same inductive translation as in the proof of Lemma 12. First-order variables are represented by singleton bit labelings, and set variables by arbitrary bit labelings. The non-counting atomic formulas x = y, x ∼ y, x ∈ X are handled exactly as in the SET case, since a PORTS verifier can simulate a SET verifier. For a counting atom Cardqp (X), the bit labeling representing X defines an instance of Count(q ′ , p), where q ′ = q mod p. By Lemma 15, this language belongs to the PORTS hierarchy. Negated atoms and Boolean combinations are handled using closure under complement, finite intersection, and finite union. The logical quantifiers are treated as in Lemma 12. Set quantifiers range over arbitrary bit labelings. For a first-order variable x, let Sing(ℓx ) denote the property that ℓx marks
exactly one vertex. Then ∃x ψ is simulated by ∃ℓx Sing(ℓx ) ∧ ψb , whereas ∀x ψ is simulated by
∀ℓx ¬ Sing(ℓx ) ∨ ψb . Since leader ∈ SET ⊆ PORTS, these guards are available in the PORTS hierarchy. Applying the construction recursively yields a constant-size alternating certification protocol with finitely many rounds. Therefore every CMSO-definable language over a finite input alphabet belongs to PORTS.

7

The MULTISET hierarchy is not included in CMSO

In this section we exhibit a problem in the MULTISET hierarchy that is not expressible in CMSO, thereby proving that this hierarchy is not contained in CMSO, and also showing that the PORTS hierarchy is strictly more expressive than CMSO. Theorem 4. There is a language in MULTISET that is not CMSO-definable. Proof. Consider the language L of graphs (without input labels) such that each node of degree 3 or more has an equal number of neighbors of degree 1 and of degree 2. It is clear that L ∈ MULTISET1 because each node can make publicly available whether its degree is 1 or 2 36

through an existential certificate (see Remark 25); then each node can check locally the desired property on its local view. We now show that L is not CMSO-definable. Suppose, for a contradiction, that there exists a CMSO sentence ϕ defining L. Consider words of the form w = #am (bc)k , where m, k ≥ 2. We associate with each such word a graph Gw whose vertices are the positions of w. The first position, labeled #, is adjacent to every position labeled a or b. In addition, each position labeled b is adjacent to the position labeled c immediately following it. There are no other edges. The resulting graph is simple and connected. Its first vertex r has degree m + k. Every vertex labeled a or c has degree one, while every vertex labeled b has degree two. Thus r is the only vertex of degree at least three, and it has exactly m neighbors of degree one and k neighbors of degree two. Consequently, Gw ∈ L if and only if m = k. The graph Gw is first-order interpretable in the word w. Indeed, its vertices are the positions of the word, and its adjacency relation is defined by

E(x, y) ≡ P# (x) ∧ (Pa (y) ∨ Pb (y))

∨ P# (y) ∧ (Pa (x) ∨ Pb (x))

∨ Pb (x) ∧ Pc (y) ∧ succ(x, y)

∨ Pb (y) ∧ Pc (x) ∧ succ(y, x) , where Pσ (x) means that position x carries symbol σ, and succ(x, y) means that y immediately follows x. Replacing each adjacency atom in ϕ by this formula yields a CMSO sentence ϕ′ over words, such that w |= ϕ′ if and only if Gw |= ϕ for every word of the form #am (bc)k with m, k ≥ 2. Since the language W = {#am (bc)k : m, k ≥ 2} is regular, it is MSO-definable. Therefore, intersecting ϕ′ with a formula defining W gives a CMSO sentence defining {#ak (bc)k : k ≥ 2}. However, this language is not regular: the prefixes #ak , for k ≥ 2, are pairwise distinguishable by the suffixes (bc)k . This contradicts the fact that every CMSO-definable language of finite words is regular (see [5, Theorem 1.16 and Section 5.2.7]). Hence L is not CMSO-definable.

8

Separating the MULTISET and PORTS hierarchies

We now show that port numbers strictly increase the expressive power of constant-size alternating certification. The separation already holds for graph languages without input labels. Theorem 5. There exists a decidable language of graphs, without input labels, that belongs to PORTS but not to MULTISET. Consequently, MULTISET ⊊ PORTS. The inclusion is immediate: a PORTS verifier can discard port numbers and recover the multiset of neighboring certificate sequences. To prove strictness, we encode binary words by graphs. We show that PORTS can recognize every decidable word language on this encoding, provided that it is closed under reversal. We then construct such a language that no MULTISET protocol recognizes.

8.1

Encoding words by graphs.

For a word w = w1 · · · wn ∈ {0, 1}n , with n ≥ 6, let Gw be obtained from the path v1 , . . . , vn by adding a vertex r adjacent to every path vertex, and by attaching one leaf to vi if and only if wi = 1. Figure 2 illustrates this construction for w = 1011010. The vertex r has degree n, whereas every other vertex has degree at most four. Hence r is uniquely determined by the graph, and its neighborhood induces the original path. It follows 37

r

v1

wi :

1

v2

0

v3

v4

1

1

v5

0

v6

1

v7

0

Figure 2: The graph Gw for w = 1011010. The vertices v1 , . . . , v7 induce a path, and the hub r is adjacent to every path vertex. A pendant leaf is attached to vi exactly when wi = 1. Vertex names and bits are shown for illustration only; the word is encoded entirely by the structure of the unlabeled graph. that Gw ∼ = Gw ′

w′ = w or w′ = wrev ,

⇐⇒

where wrev denotes the reversal of w. S For a language D ⊆ n≥6 {0, 1}n closed under reversal, define the graph language LD = {G : G ∼ = Gw for some w ∈ D}. Lemma 26. If D is decidable and closed under reversal, then LD ∈ PORTS. Proof. Fix an arbitrary port assignment. The prover first marks two vertices r, s, two sets P, F ⊆ V (G), and chooses a bit labeling b : P → {0, 1}. Each vertex marking is represented by one bit per vertex. We require that exactly one vertex receives each of the marks for r and s, and impose the following conditions: 1. {r}, P, F partition V (G), and N (r) = P . 2. G[P ] is a path on at least six vertices, and s is one of its endpoints. 3. Every vertex in F has degree one and its neighbor belongs to P ; every vertex in P has at most one neighbor in F . These conditions are MSO-definable and characterize the graphs Gw , together with a choice of an endpoint s. Write the path order starting at s as v1 , . . . , vn , and let wi = 1 if and only if vi has a neighbor in F . Let pi be the neighbor of r at its local port i. The order p1 , . . . , pn may differ from the path order v1 , . . . , vn . The labeling b defines the word z = b(p1 ) · · · b(pn ). Vertex r can read z from its PORTS view and decide whether z ∈ D. It remains to verify that z = w. The disprover chooses a vertex set U , and the prover responds with a vertex set T and two bit labelings a, h. In addition to the conditions on the initial markings, we require: 1. If U = {u} for some u ∈ P , then h ≡ 1 and T is exactly the vertex set of the subpath from s to u in G[P ], including both endpoints. 2. Otherwise, h ≡ 0.

38

Here h ≡ ε means that every vertex receives the bit ε. In the second case, there is no restriction on T . Let φ be the conjunction of the conditions on the initial markings, including the uniqueness of the marks for r and s, and these requirements on U, T, h. This is an MSO condition. In particular, the condition on T can be expressed as follows: if s = u, require T = {s}; otherwise, require that T ⊆ P induces a connected path whose endpoints are exactly s and u. In addition to verifying φ, the final verifier performs the following local checks: 1. Every vertex checks that its bit a agrees with the bits a of all its neighbors. 2. If h(v) = 1 and v ∈ U , vertex v checks that a(v) = 1 if and only if it has a neighbor in F . 3. Vertex r always checks that z ∈ D. If h(r) = 1, it also computes i = |N (r) ∩ T | and checks that 1 ≤ i ≤ n and b(pi ) = a(r). Every vertex carrying the mark for r performs the third check; the condition φ ensures that there is exactly one such vertex. These checks use only a vertex’s own markings and the markings of its neighbors indexed by its local ports. Since the graph is connected, the first check forces a to be constant. The protocol therefore uses the prefix ∃r, s, P, F, b, ∀U, ∃T, a, h, where quantification over r, s abbreviates the choice of the binary markings described above. This prefix is followed by a SET protocol for φ, which exists by Theorem 2. The markings chosen before this additional protocol are treated as fixed finite input labels. The final PORTS verifier conjoins the outcome of that protocol with the local checks above. All earlier markings remain available in the certificate sequences. The resulting protocol uses a constant number of rounds and a constant number of certificate bits per vertex, including those needed to verify φ. For completeness, suppose that G = Gw with w ∈ D. Mark r, P, F according to the construction of Gw , and choose an endpoint s of the path. Let v1 , . . . , vn be the order starting at s, and write w for the word read in this order. Since D is closed under reversal, this word belongs to D. Choose b so that b(pi ) = wi for every i ∈ [n]. Thus z = w, and vertex r accepts its membership check. If U is not a singleton contained in P , choose h ≡ 0, a ≡ 0, and T = ∅. Then φ and all local checks hold. If U = {vj }, choose h ≡ 1, T = {v1 , . . . , vj }, a ≡ wj . Again φ holds. The check at vj succeeds by the definition of wj , and the check at r succeeds because |N (r) ∩ T | = j and b(pj ) = wj = a(r). In both cases, the prover can win the appended SET protocol because φ is true. This proves completeness. For soundness, suppose that the prover has a winning strategy. The appended SET protocol forces the conditions on the initial markings. Thus these markings determine a graph Gw and a path order v1 , . . . , vn . The initial labeling b fixes the word z = b(p1 ) · · · b(pn ), and the unconditional check at r gives z ∈ D. For each j ∈ [n], consider the choice U = {vj }. The condition φ forces h ≡ 1 and T = {v1 , . . . , vj }. The local check at vj gives a(vj ) = wj , and the checks along the edges force a to be constant. Hence a(r) = wj . Since |N (r) ∩ T | = j, the check at r then gives zj = b(pj ) = a(r) = wj . The labeling b was chosen before U , so the same word z satisfies this equality for every j. Thus z = w. Since z ∈ D, we conclude that G ∈ LD . The port assignment was arbitrary. The initial labeling b may depend on it, and the argument works for every assignment. The decider for D is used only in the local computation at r, whose running time is unrestricted in our model. 39

Lemma 27. There exists a decidable language D ⊆ that LD ∈ / MULTISET.

S

n n≥6 {0, 1} , closed under reversal, such

Proof. Every MULTISET protocol can be represented using a finite sequence of quantified binary labelings Q1 β1 · · · Qc βc , Qi ∈ {∃, ∀}, βi : V → {0, 1}, where we do not require consecutive quantifiers to alternate. Indeed, for each original certificate alphabet Γ, choose a surjection {0, 1}d → Γ, replace its quantified labeling by d consecutive binary labelings with the same quantifier, and let the verifier decode each complete certificate sequence. The induced map on global labelings is surjective, so this replacement preserves both existential and universal quantification. An ignored binary labeling allows us to assume c ≥ 1. Fix c, and put q = 2c . On a graph of maximum degree at most n, the information available to a MULTISET verifier at a vertex is determined by its own certificate sequence and the multiplicity of each of the q possible neighboring sequences. Since every multiplicity lies in {0, . . . , n}, the number of possible local views is at most pc (n) = q(n + 1)q . There are no input labels. In particular, this bound applies to every graph Gw with |w| = n ≥ 6. Let Rn contain the lexicographically smaller word in each reversal class of {0, 1}n , listed in lexicographic order, and let rn = |Rn |. Since each class has at most two elements, rn ≥ 2n−1 . These representatives encode pairwise nonisomorphic graphs. For a fixed quantifier sequence, the behavior of any verifier on these graphs is determined by a Boolean table on at most pc (n) local views. Thus there are at most 2pc (n) possible tables. Including the 2c quantifier sequences, protocols with c binary labelings induce at most 2pc (n)+c acceptance vectors on {Gw : w ∈ Rn }. This bound does not impose any restriction on the verifier’s computation time. Choose a strictly increasing computable sequence n1 , n2 , . . ., with nc ≥ 6, such that pc (nc ) + c < 2nc −1 . This is possible because pc is a polynomial for each fixed c: at stage c, take the least integer larger than the previous term, and at least six, satisfying the inequality. At stage c, enumerate every quantifier sequence of length c and every Boolean table on the finite set of possible local views of degree at most nc . Evaluate the resulting finite quantification games on every Gw with w ∈ Rnc . This computation terminates, since all labeling domains are finite and every local decision is supplied by the enumerated table. There are at most 2pc (nc )+c resulting acceptance vectors, whereas nc −1

2pc (nc )+c < 22

≤ 2rnc .

Let ηc ∈ {0, 1}rnc be the lexicographically first vector not obtained in this enumeration. Define D to reject all words whose length is not one of the nc . At length nc , include a word w precisely when the coordinate of ηc indexed by the representative of its reversal class is one. This language is closed under reversal. It is also decidable: given w, generate the increasing sequence nc until its first term satisfying nc ≥ |w|. If nc > |w|, reject; otherwise, compute ηc by the finite procedure above and inspect the coordinate corresponding to the reversal class of w. Every step of this procedure terminates. Suppose now that a MULTISET protocol recognizes LD , and put it into binary form with c ≥ 1 labelings. Its restriction to {Gw : w ∈ Rnc } is described by one of the quantifier sequences and tables enumerated at stage c. Its acceptance vector therefore cannot be ηc . But the definition of D requires precisely this vector, a contradiction. Proof of Theorem 5. Take the language D supplied by Lemma 27. By Lemma 26, LD ∈ PORTS, whereas LD ∈ / MULTISET. The graph language LD is decidable: recognize the encoding, extract either orientation of the word, and run the decider for D. Together with the immediate inclusion MULTISET ⊆ PORTS, this proves the theorem. 40

9

Equivalence of hierarchies on bounded-degree graphs

We compare the expressiveness of our constant-size certification hierarchies with the locally polynomial hierarchy of [16]. This comparison is useful specifically on graphs of bounded degree; we therefore introduce the model here, rather than alongside the weak neighborhood views that are the subject of this paper. In the model of [16], a node may communicate for a fixed number of rounds and perform a polynomial amount of local computation. Nodes have identifiers that are unique within a fixed radius (not necessarily globally), and the players alternately assign certificates whose sizes are polynomially bounded in the information contained in constant-radius neighborhoods. LP Write ΣLP m and Πm for the levels with m alternating certificate assignments, beginning with an existential and a universal assignment, respectively. The protocol is required to be correct for every admissible identifier assignment. We use the formal definition and the bounded-degree normalization results of [16]. M For M ∈ {SET, PORTS}, we similarly write ΣM m and Πm for the two possible starting quanM tifiers at level m of our hierarchy; in particular, Mm = Σm ∪ ΠM m for m ≥ 1. For a fixed ∆ ≥ 1, let B(∆) denote the class of connected graphs of maximum degree at most ∆. Throughout this section we compare languages over a fixed finite input alphabet; this qualification is essential, since the certificate-size bound in the locally polynomial hierarchy model can depend on the length of an unbounded input label. We use the notation C|B(∆) for the restrictions of the languages in C to B(∆). Lemma 28. Fix ∆ ≥ 1 and a finite input alphabet. For every m ≥ 3, PORTS ΣSET |B(∆) = ΣLP m |B(∆) = Σm m |B(∆) .

For every m ≥ 4, PORTS ΠSET |B(∆) = ΠLP m |B(∆) = Πm m |B(∆) .

The assertion is uniform over each fixed choice of the communication radius and the identifieruniqueness radius of the locally polynomial verifier. Proof. A SET verifier is simulated by a PORTS verifier simply by discarding port order. A constant-time locally polynomial machine can in turn simulate a PORTS verifier: it orders the neighbors according to the available LOCAL interface (or, equivalently, their locally distinct identifiers). This is legitimate because the PORTS protocol must recognize the same language for every local port numbering. Its certificates are constant-size and hence satisfy the local polynomial bound in [16]. Thus only the inclusion from LP into SET requires proof. Coloring and locally certified views. Let M be a locally polynomial verifier for a language L on B(∆). Fix its communication time, identifier-uniqueness radius, certificate-bound radius, and finite input alphabet. We choose a constant R ≥ 1 large enough that a correctly reconstructed radius-R view contains everything needed to simulate M and that uniqueness of identifiers within distance 2R implies its identifier assumption. An auxiliary labeling χ will serve as a synthetic identifier assignment. We require it to be a proper coloring of G2R , with colors from the constant-size palette [C∆,R ], where C∆,R = 1 + ∆

2R−1 X

(∆ − 1)j .

j=0

Indeed, the number of vertices at distance at most 2R from any vertex is at most C∆,R ; greedily coloring G2R gives the bound. For example, if ∆ = 2, this is 4R + 1. The palette is fixed independently of the number of vertices. 41

We record how a radius-R LOCAL view can be simulated with radius-one SET checks. Let κ1 , . . . , κm be the original certificate assignments and let ρ be an additional bit labeling when needed. An existential certificate, issued after these assignments, supplies finite descriptions Uj (v), for 0 ≤ j ≤ R, of the labeled radius-j unfoldings at each node. The base description contains the node’s own input, color χ(v), original certificates, and ρ(v). For definiteness, one may choose the recursively defined descriptions U0 (v) = (χ(v), x(v), κ1 (v), . . . , κm (v), ρ(v)),

Uj (v) = (U0 (v), {Uj−1 (u) : u ∈ N (v)}) .

Each node checks the base description against its own labels and checks every recurrence using the set of neighboring descriptions. We now explain why these descriptions contain enough information to reconstruct the local topology required by M . Fix a vertex v and suppose that χ is a proper coloring of G2R . Since any two vertices in BR (v) are at distance at most 2R, distinct vertices in this ball have distinct colors. The recursive description UR (v) contains the labeled unfoldings along all walks of length at most R starting at v. Consequently, every vertex in BR (v) appears in this description. Moreover, two occurrences correspond to the same vertex if and only if they carry the same χ-color. Thus the colors allow us to identify repeated occurrences of vertices reached through different walks. For every vertex u ∈ BR−1 (v), the description also contains U1 (u), which records the colors and labels of all neighbors of u. Therefore, we can recover all adjacencies between vertices of BR−1 (v). It follows that UR (v) determines the labeled induced subgraph G[BR−1 (v)], with χ serving as an injective identifier assignment within this ball. Choosing R strictly larger than the communication radius of M , and large enough to satisfy its identifier-uniqueness requirements, ensures that the reconstructed view contains all the information needed to simulate M . If a local ordering of neighbors is needed, we use the order induced by their distinct χ-colors. Because ∆, R, and all label alphabets are fixed, these unfoldings have bounded size. More importantly, if all local recurrence checks accept, induction on j proves that every claimed unfolding is correct. This is a global conjunction of local checks; we do not assume that one vertex can independently inspect a distant vertex’s true label. Thus a final existential assignment can provide and validate the necessary higher-radius information without adding a quantifier round. For later use, a universal challenge ρ : V → {0, 1} can test χ. At a node v, inspect the certified radius-R unfolding and reject if it contains two vertex occurrences of the same χ-color carrying different ρ-bits. If χ is proper on G2R , this never happens: any two vertices in BR (v) are at distance at most 2R. Conversely, if distinct vertices u, w at distance at most 2R have the same color, choose a midpoint v on a shortest u–w path so that u, w ∈ BR (v). Assign ρ(u) = 0 and ρ(z) = 1 for all z ̸= u. The correct unfolding at v now reveals a collision. An existentially supplied false unfolding cannot circumvent this challenge, because some recurrence or base check would reject. Protocols beginning existentially. First let m ≥ 3 be odd, so the m-th assignment is existential. In the first round the prover chooses χ in addition to the first certificate κ1 of M . In the second round the adversary chooses ρ together with κ2 . The remaining rounds carry the respective original certificates. In the final existential round, the prover also supplies the unfoldings Uj . The one-hop verifier checks all unfolding recurrences, tests the ρ-challenge on χ, and simulates the local acceptance predicate of M with the reconstructed view. If χ is valid, every challenge passes and the simulation has exactly the truth value of the original locally polynomial protocol for that admissible identifier assignment. If χ is invalid, the second player can choose a challenge exposing a collision; no later existential reply can 42

make all vertices accept. The quantifier pattern is unchanged, and all certificates are bounded. SET Therefore ΣLP m |B(∆) ⊆ Σm |B(∆) for odd m ≥ 3. For even m ≥ 4, we use the bounded-degree elimination of a trailing universal certificate LP (Proposition 38 of [16]): ΣLP m |B(∆) = Σm−1 |B(∆) . Apply the preceding construction at the odd level m − 1 ≥ 3 and append a dummy universal assignment. This establishes the claimed Σm inclusion for all m ≥ 3. Protocols beginning universally. Suppose first that m ≥ 4 is even, so the last certificate assignment is existential. The first (universal) assignment now contains both χ and κ1 . The second (existential) assignment contains κ2 , a bit b, and an auxiliary witness. All nodes check that b has the same value at both ends of every edge; connectedness makes b global. The meaning of the bit is the following. If b = 1, the prover claims that χ is valid. The third (universal) round adds the challenge ρ to κ3 . The verifier tests the coloring exactly as above and, using unfoldings supplied in the last existential round, simulates M . An invalid coloring is therefore refuted by a suitable ρ. If b = 0, the prover claims that χ is invalid. Its second-round witness consists of a number d ∈ [2R], a color a, and node roles from {⊥, 0, . . . , d} (the values d, a are required to be uniform). Every vertex with role i < d checks that it has a neighbor with role i + 1; a vertex with role 0 or d checks that its χ-color is a. Because each vertex has only one role, the existence of a role-0 vertex forces a path with d distinct vertices after its start, whose two distinct endpoints have the same χ-color. Thus a locally valid witness with a role-0 vertex certifies a violation of proper coloring of G2R . Conversely, a shortest path between two equally colored vertices at distance d ≤ 2R provides such a witness. It remains to require at least one role-0 vertex. This is the language alos, which has a three-round SET protocol with quantifier sequence ∃ ∀ ∃ (Lemma 9). Its rounds are merged with rounds two, three, and four of the present protocol. The one-hop verifier enforces the path constraints and the alos protocol in the b = 0 branch; when b = 0 it ignores M . The auxiliary challenge and response can be padded with dummy fields in any subsequent rounds. If χ is valid, choosing b = 0 cannot succeed: every candidate path either fails a local constraint or has no role-0 vertex, in which case the third-round adversary defeats the alos test. The prover must choose b = 1, where the correct simulation of M determines acceptance. If χ is invalid, the prover can choose b = 0 and certify an actual color collision, so the invalid identifier assignment does not affect membership. Therefore the universal first-round choice ranges, effectively, only over valid identifiers. In the b = 1 branch, the last existential assignment supplies and validates the necessary radius-R unfoldings, exactly as in the Σ case. The original m quantifier rounds suffice. LP For odd m ≥ 5, Proposition 38 in [16] gives ΠLP m |B(∆) = Πm−1 |B(∆) . The even-level construction applies to m − 1 ≥ 4 and can be padded by one dummy universal round. This completes the Πm inclusion and the proof of the lemma. The restriction m ≥ 3 in the Σ statement is deliberate: our radius-one reconstruction uses a final existential assignment, which is not available in the two-round ∃∀ pattern. The separation argument below does not require an equivalence at that level. Likewise, the lower levels of the Π hierarchy are not needed here. Notice also that the horizon R is a fixed constant depending on the simulated verifier, not a common radius imposed on all languages. Theorem 6. Let M ∈ {SET, MULTISET, PORTS}. The M-hierarchy consists of infinitely many levels. More precisely, for all k ≥ 0 there exists a language L ∈ Mk+1 such that L ̸∈ Mk . Proof. We prove the stronger statement that, for every k ≥ 0, there exists a language Lk ∈ SETk+1 \ PORTSk . This implies the theorem, since SETj ⊆ MULTISETj ⊆ PORTSj for every j ≥ 0.

43

We first consider k ≥ 2. Fix B = B(4), the class of connected graphs of maximum degree at most four, and restrict all the classes below to B. By Theorem 36 of [16], for every even integer ℓ ≥ 2, LP LP ΣLP ℓ−1 ⊊ Πℓ ⊊ Σℓ+1 .

These separations also hold on our class of connected graphs: the graph encodings of rectangular pictures used to establish them are connected and have maximum degree four. By Proposition 38 of [16], the final universal quantifier can be eliminated on boundedLP LP degree graphs. Consequently, for even k ≥ 2, we have ΣLP k = Σk−1 ⊆ Πk , while for odd k ≥ 3, LP LP ΠLP k = Πk−1 ⊆ Σk . The inclusions follow by adding a dummy initial quantifier. Since a PORTS verifier can be simulated in the locally polynomial model, we obtain PORTSk ⊆ LP Πk when k is even, and PORTSk ⊆ ΣLP k when k is odd. LP Suppose first that k ≥ 2 is even. By Theorem 36, there exists a language L ∈ ΣLP k+1 \Πk . By Lemma 28, the restriction of L to B coincides with the restriction of some language Lk ∈ ΣSET k+1 . LP If Lk belonged to PORTSk , then its restriction to B would belong to Πk , a contradiction. Hence Lk ∈ SETk+1 \ PORTSk . LP Now suppose that k ≥ 3 is odd. Theorem 36 gives a language L ∈ ΠLP k+1 \ Σk . Since SET k + 1 ≥ 4, Lemma 28 provides a language Lk ∈ Πk+1 whose restriction to B coincides with that of L. The same argument gives Lk ∈ SETk+1 \ PORTSk . It remains to consider k = 0 and k = 1. For k = 0, consider the language of bipartite graphs. It belongs to SET1 , since the prover can assign a proper 2-coloring. On the other hand, a PORTS verifier without certificates cannot distinguish C3 from C4 : in both graphs every node has degree two and receives the same trivial input. Thus Bipartiteness ∈ SET1 \ PORTS0 . For k = 1, consider amos. By Lemma 11, we have amos ∈ SET2 . We show that amos ∈ / PORTS1 . First, amos ∈ / ΣPORTS . Consider a cycle Cn , with n ≥ 4, containing exactly one marked 1 vertex. Suppose that an existential one-round PORTS protocol accepts this instance. Fix a port numbering and an accepting certificate assignment. Take the double cover C2n of Cn , lifting the input marks, port numbering, and certificates. The covering preserves every local PORTS view, so every vertex of C2n accepts. However, the lifted instance has two marked vertices and does not belong to amos, a contradiction. Second, observe that ΠPORTS = PORTS0 . Indeed, a universally quantified certificate assign1 ment can be eliminated locally. Each vertex enumerates all possible certificates for itself and its neighbors, indexed by its local ports, and accepts if the original verifier accepts for every such assignment. Every local assignment extends to a global one, so this test preserves the universal acceptance condition. Since local computation is unrestricted, the test can be performed without certificates. Finally, amos ∈ / PORTS0 . On cycles, a verifier without certificates sees only its own input and its two ports. An accepting cycle with one marked vertex therefore forces acceptance of both possible local input values, and the same verifier accepts a cycle with two marked vertices. Consequently, amos ∈ SET2 \ PORTS1 . We have thus established, for every k ≥ 0, the existence of a language Lk ∈ SETk+1 \PORTSk . By the level-wise inclusions between our three models, this proves that every consecutive inclusion is strict in each hierarchy.

10

Explicit languages outside the PORTS hierarchy

In this section, we give explicit examples of languages outside the PORTS hierarchy. We identify two limitations of constant-size alternating certification in this model. The first arises on highly

44

symmetric graphs of unbounded degree, even with a finite input alphabet; the second arises from unbounded local inputs, even on bounded-degree graphs.

10.1

Labeled complete bipartite graphs

Let L be a distributed language over a fixed finite input alphabet Q. We associate with L the following two-party communication problem, defined for every n, m ≥ 1: KL = (u, v) ∈ Qn × Qm : (Kn,m , xu,v ) ∈ L . 

Here Alice receives u = (u1 , . . . , un ), the inputs of the n vertices in one bipartition class, and Bob receives v = (v1 , . . . , vm ), the inputs of the m vertices in the other. Each player knows the size of their own input but not necessarily that of the other player. Communication complexity is measured uniformly over all n, m. We show that an arbitrary fixed number of alternating rounds with constant-size certificates in the PORTS model yields a uniformly bounded deterministic communication protocol on these graphs. We use the fact that nondeterministic communication protocols of constant cost can be replaced by deterministic protocols of constant cost (the equality P0 = N P0 ; see [11]). Lemma 29. Let L be a distributed language over a fixed finite input alphabet Q. If L ∈ PORTS, then KL has uniformly bounded deterministic communication complexity. That is, there exists a constant B, independent of n, m, such that Alice and Bob can decide membership in KL by exchanging at most B bits. Proof. Fix a PORTS protocol for L, with a finite number of alternating certificate assignments, each over a finite alphabet. Membership is independent of the choice of local port numbering, so on Kn,m we may fix a convenient one: at every vertex of Alice’s class, port j leads to Bob’s vertex j, and at every vertex of Bob’s class, port i leads to Alice’s vertex i. We argue by induction on the number of certificate quantifiers that remain to be evaluated. For precision, we allow certificate fields whose quantifiers have already been removed to be supplied as additional, finite-valued distributed inputs to the communication problem, while retaining their original visibility at neighboring ports. This strengthened induction statement is useful because a certificate visible to neighboring vertices cannot simply be treated as an ordinary local input in the definition of PORTS. All the additional alphabets remain finite. Equivalently, such information could be copied into visible certificates and checked against the corresponding local inputs with an existential certificate assignment. For the base case, all certificate fields are fixed. Each player knows the inputs and the certificate fields of the vertices in their own class. Let TA be the set of local types occurring in Alice’s class, where a type consists of a vertex input and all its own certificate fields; define TB analogously. Both sets range over a fixed finite universe. Alice sends TA to Bob, and Bob sends TB to Alice, using a constant number of bits. Because of the chosen port numbering, all vertices of Alice’s class see the same port-ordered tuple of certificate fields from Bob’s class. Bob knows that tuple, as well as its length m. He can therefore evaluate the local verifier on every type in TA and determine whether all vertices of Alice’s class accept. Symmetrically, Alice can determine whether all vertices of Bob’s class accept. They exchange the resulting two bits and decide whether every vertex accepts. This is a deterministic protocol with uniformly bounded communication. Notice that the verifier does not need to read the original inputs of neighboring vertices: it reads only their visible certificate fields, exactly as specified by PORTS. For the induction step, first suppose that the next certificate assignment is existential. Write the residual condition as R(u, v) ⇐⇒ ∃y R′ ((u, yA ), (v, yB )),

45

where yA and yB are the restrictions of the finite-alphabet labeling y to Alice’s and Bob’s vertices, respectively. The induction hypothesis provides a deterministic communication protocol P ′ , of uniformly bounded cost, for R′ , with the new certificate field still visible at neighboring ports. Alice and Bob now use the following nondeterministic protocol for R. First, they guess an accepting communication transcript µ of P ′ . There are only finitely many possible transcripts, since P ′ communicates at most a constant number of bits. Alice checks, using only her own input and µ, whether there exists some assignment yA for which all messages she would send in P ′ are consistent with µ. Bob independently performs the analogous check for some yB . They accept if both checks succeed. If they accept, the two local assignments together define a global labeling y, and the complete transcript µ is consistent with the deterministic protocol P ′ on that input. Since the transcript is accepting, R′ holds, hence R holds. Conversely, if R holds, take a witnessing labeling y and the accepting transcript of P ′ on that labeling. Both local consistency checks then succeed. Thus this nondeterministic protocol decides R with constant cost. By P0 = N P0 , R also has a deterministic constant-cost protocol. If the next certificate assignment is universal, use ∀y R′ (u, v, y)

⇐⇒

¬∃y ¬R′ (u, v, y).

By induction, R′ has a bounded deterministic protocol; complementation preserves its cost. The existential case therefore applies to ¬R′ , and a final complementation gives a bounded deterministic protocol for the universal case as well. Applying the induction through the entire fixed quantifier prefix proves the lemma. Corollary 30. Let L be a graph language such that, for some constant n0 ≥ 1, Kn,m ∈ L

⇐⇒

n=m

for all n, m ≥ n0 .

Then L ∈ / PORTS. In particular, neither the language of Hamiltonian graphs nor the language of graphs admitting a perfect matching belongs to the PORTS hierarchy. Proof. Suppose L ∈ PORTS. Since L is a graph language, its input alphabet can be taken to be a singleton. By Lemma 29, Alice and Bob could decide whether n = m for all n, m ≥ n0 using a uniformly bounded number of bits. This is impossible. Indeed, a deterministic protocol exchanging at most B bits has only finitely many accepting transcripts, and each accepting transcript defines a combinatorial rectangle. A rectangle contained in the equality relation cannot contain two distinct diagonal pairs (n, n) and (m, m), since it would then also contain the non-diagonal pair (n, m). Thus equality on arbitrarily large positive integers requires infinitely many accepting rectangles and cannot have uniformly bounded deterministic communication complexity. Finally, Kn,m admits a perfect matching exactly when n = m. It admits a Hamiltonian cycle exactly when n = m ≥ 2. The corollary follows by taking n0 = 1 and n0 = 2, respectively. This obstruction is specific to the information available in our constant-certificate port model. It does not automatically extend to the locally polynomial hierarchy of [16], which allows locally unique identifiers and more general certificate-size bounds.

10.2

Bounded-degree graphs with unbounded inputs

We now consider a different obstruction. Local verifiers can process arbitrarily long inputs at their own vertices, but in PORTS they cannot read neighboring inputs directly. For a fixed degree, the information provided by constant-size certificates and their port-ordered neighboring tuples ranges over a finite set. 46

Let L be a distributed language with inputs in {0, 1}∗ . Given an instance I = (G, x), a ev,s′ ) by vertex v ∈ V (G) with input s = x(v), and any s′ ̸= s, define the perturbation Ie = (G, x ( ev,s′ (u) = x

x(u) if u ̸= v, s′ if u = v.

For a fixed degree d > 0, we say that s ∈ {0, 1}∗ is a fragile degree-d input value of L if there exists a yes-instance I = (G, x) ∈ L with a degree-d vertex v satisfying x(v) = s, such that every perturbation of I at v produces a no-instance. We say that I witnesses the fragility of s. Let Fragiled (L) be the number, possibly infinite, of fragile degree-d input values of L. Lemma 16. For every language L in the PORTS hierarchy and every d > 0, Fragiled (L) is finite. Proof. Let L ∈ PORTS, and fix d > 0. There are a finite number k of certificate quantifiers and a local verifier A such that (G, x) ∈ L ⇐⇒ Q1 ℓ1 · · · Qk ℓk ∀v ∈ V (G),

A x(v), ℓ(v), viewPORTS (v) = 1,

where ℓ = (ℓ1 , . . . , ℓk ) and all certificate alphabets are finite. Let C be the finite alphabet of complete certificate tuples ℓ(v). At a degree-d vertex, the certificate information seen by A belongs to the finite set Vd = C × C d , consisting of its own certificate tuple and the ordered tuples of neighboring certificates indexed by its local ports. In particular, for each possible input value s, the verifier determines a Boolean function Fs : Vd −→ {0, 1}. Only finitely many such functions exist. If Fragiled (L) = ∞, we can therefore choose distinct fragile values s ̸= s′ for which Fs = Fs′ . Let I = (G, x) ∈ L witness the fragility of s at a degree-d vertex v, and replace only x(v) = s by s′ . By fragility, the resulting instance Ie is not in L. However, for every possible assignment of all certificates, the local output at v is unchanged because Fs = Fs′ , and the local output at every other vertex is unchanged because those vertices do not read x(v) directly. Hence the statement that all vertices accept has exactly the same truth value on I and Ie for every certificate assignment. The entire alternating quantified statement therefore has the same truth value on both instances, contradicting I ∈ L and Ie ∈ / L. Thus Fragiled (L) is finite. We now consider the distributed language size = {(G = (V, E), x) : ∀v ∈ V, x(v) = |V |}, where integers are represented by their binary encodings. This language asks every vertex to hold the correct number of vertices of the graph. Theorem 8. size is not in the PORTS hierarchy. Proof. We show that Fragile2 (size) = ∞. For each n ≥ 3, consider the cycle Cn with input n at every vertex. This is a yes-instance of size. Every vertex has degree 2, and changing the input at any one vertex to a different value makes the instance a no-instance. Consequently, every n ≥ 3, encoded in binary, is a fragile degree-2 input value. Hence Fragile2 (size) = ∞, and Lemma 16 implies size ∈ / PORTS. 47

Remark 31. The same argument applies to other size-dependent inputs. For example, let f : N → N be an unbounded computable function, and define 

Lf = (G = (V, E), x) : ∀v ∈ V, x(v) = f (|V |) . The values f (n), for n ≥ 3, are infinite in number, and the cycle argument shows that each distinct value is a fragile degree-2 input. Thus Lf ∈ / PORTS. For languages over a fixed finite input alphabet, this particular fragility argument does not apply. Indeed, several finite-alphabet properties, including agreement on a fixed input value and counting modulo a fixed constant, can be verified within the hierarchy.

11

Discussion

Our results leave several natural questions open. While the SET hierarchy is exactly characterized by MSO, a logical characterization of the MULTISET and PORTS hierarchies remains unknown. We have established the strict inclusions SET ⊊ MULTISET ⊊ PORTS, showing that both multiplicities and port numbering strictly increase expressive power. Moreover, the PORTS hierarchy strictly contains CMSO, while the MULTISET hierarchy can express properties that are not CMSO-definable. Whether every CMSO-definable language belongs to the MULTISET hierarchy remains open. More generally, finding logical characterizations of these two hierarchies is an important direction for future research. Our negative results provide some insight into their limitations. In particular, we have shown that Hamiltonicity and the existence of a perfect matching cannot be recognized in the PORTS hierarchy, and therefore neither in the weaker MULTISET hierarchy. Since Hamiltonicity is expressible in MSO2 , this establishes that even port numbering and arbitrarily many alternating rounds of constant-size certificates do not suffice to capture all properties definable using edgeset quantification. This raises the question of which fragments of MSO2 , beyond CMSO, can be captured by these hierarchies. Our result concerning size provides a different limitation, showing that unbounded input alphabets can obstruct verification even on bounded-degree graphs. A second direction concerns the internal structure of the hierarchies. Although we establish that the hierarchies have infinitely many distinct levels, explicit separations between small levels remain open. In particular, it would be interesting to determine the exact level of the language leader. We show that leader belongs to the third level, and it is known that it does not belong to the first level [10]. Proving that it does not belong to the second level would provide a natural and explicit separation between the second and third levels. Another natural direction is to understand what happens between constant-size and logarithmicsize certificates. In the hierarchy with logarithmic-size certificates, unique identifiers can be assigned and certified at some level of the hierarchy. Once identifiers are available, nodes can distinguish their neighbors, and multiplicities can be recovered from sets of decorated local types. Consequently, the distinction between the SET and MULTISET views essentially disappears in that setting. This raises the question of what happens for intermediate certificate sizes, for instance in the regime o(log n). Is there a threshold below which multiplicities still provide additional expressive power? Or can one already recover enough symmetry-breaking information to collapse the different hierarchies? Understanding this intermediate regime could help clarify which aspects of their separation are genuinely due to constant-size certificates, and which are consequences of anonymity itself. Finally, larger certificates allow us to approach stronger logical formalisms. Certificates of size O(n log n) are sufficient to encode arbitrary edge-set assignments and capture MSO2 . On 48

the other hand, logarithmic-size certificates already suffice to recognize Hamiltonicity [7]. It remains open whether such certificates are sufficient to capture every MSO2 -definable graph language, or whether some properties require larger certificates

References [1] Eden Aldema Tshuva and Rotem Oshman. On Polynomial Time Local Decision. In Alysson Bessani, Xavier Défago, Junya Nakamura, Koichi Wada, and Yukiko Yamauchi, editors, 27th International Conference on Principles of Distributed Systems (OPODIS 2023), volume 286 of Leibniz International Proceedings in Informatics (LIPIcs), pages 27:1–27:17, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. URL: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs. OPODIS.2023.27, doi:10.4230/LIPIcs.OPODIS.2023.27. [2] Alkida Balliu, Gianlorenzo D’Angelo, Pierre Fraigniaud, and Dennis Olivetti. What can be verified locally? In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2017. [3] Nicolas Bousquet, Laurent Feuilloley, and Théo Pierron. Local certification of graph decompositions and applications to minor-free classes. Journal of Parallel and Distributed Computing, 193:104954, 2024. [4] Linda Cook, Eun Jung Kim, and Tomáš Masařík. A tight meta-theorem for local certification of mso2 properties within bounded treewidth graphs. In Proceedings of the ACM Symposium on Principles of Distributed Computing, pages 110–120, 2025. [5] Bruno Courcelle and Joost Engelfriet. Graph structure and monadic second-order logic. A language-theoretic approach. Encyclopedia of Mathematics and its applications, Vol. 138. Cambridge University Press, June 2012. Collection Encyclopedia of Mathematics and Applications, Vol. 138. [6] Laurent Feuilloley. Introduction to local certification. Discrete Mathematics & Theoretical Computer Science, 23(Distributed Computing and Networking), 2021. [7] Laurent Feuilloley, Pierre Fraigniaud, and Juho Hirvonen. A hierarchy of local decision. Theoretical Computer Science, 856:51–67, 2021. [8] Laurent Feuilloley, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, Éric Rémila, and Ioan Todinca. Compact distributed certification of planar graphs. Algorithmica, 83(7):2215–2244, 2021. [9] Laurent Feuilloley, Pierre Fraigniaud, Pedro Montealegre, Ivan Rapaport, Eric Rémila, and Ioan Todinca. Local certification of graphs with bounded genus. Discrete Applied Mathematics, 325:9–36, 2023. [10] Mika Göös and Jukka Suomela. Locally checkable proofs. In Proceedings of the 30th annual ACM SIGACT-SIGOPS symposium on Principles of distributed computing, pages 159–168, 2011. [11] Hamed Hatami and Pooya Hatami. Guest column: Structure in communication complexity and constant-cost complexity classes. SIGACT News, 55(1):67–93, March 2024. [12] Lauri Hella, Matti Järvisalo, Antti Kuusisto, Juhana Laurinharju, Tuomo Lempiäinen, Kerkko Luosto, Jukka Suomela, and Jonni Virtema. Weak models of distributed computing, with connections to modal logic. In Proceedings of the 2012 ACM Symposium on Principles of distributed computing, pages 185–194, 2012. 49

[13] Benjamin Jauregui, Pedro Montealegre, Diego Ramírez-Romero, and Ivan Rapaport. Local certification of some geometric intersection graph classes. arXiv preprint arXiv:2309.04789, 2023. [14] Amos Korman, Shay Kutten, and David Peleg. Proof labeling schemes. In Proceedings of the twenty-fourth annual ACM symposium on Principles of distributed computing, pages 9–18, 2005. [15] Fabian Reiter. Distributed graph automata. In 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, July 2015. doi:10.1109/lics.2015.27. [16] Fabian Reiter. A local view of the polynomial hierarchy. In Proceedings of the 43rd ACM Symposium on Principles of Distributed Computing, pages 347–357, 2024. [17] Ilkka Törmä. Subshifts, MSO Logic, and Collapsing Hierarchies, pages 111–122. Springer Berlin Heidelberg, 2014. doi:10.1007/978-3-662-44602-7_10.

50

Related documents

• Distributed Statistical Zero-Knowledge Proofs via Sumcheck#187288
• Efficient Zero-Knowledge Proofs for Set Membership in Blockchain-Based Sensor Networks: A Novel OR-Aggregation Approach#131252
• Verifiable Secure Aggregation via Dual Servers with Linear Tags in Federated Learning#665777
• Verifiable Secure Aggregation via Dual Servers with Linear Tags in Federated Learning#664277
• Multiscale Dynamic Dependence Estimation over Networks#615080