IRIF, Université Paris Cité and CNRS,
<EMAIL_ADDRESS>support for ANR projects QuData and
DUCAT. LaBRI, Université de Bordeaux<EMAIL_ADDRESS>Facultad
de Ingeniería y Ciencias, Universidad Adolfo Ibáñez, Santiago,
<EMAIL_ADDRESS>work was supported by Centro de Modelamiento
Matemático (CMM), FB210005, BASAL funds for centers of excellence from ANID-
Chile, and ANID-FONDECYT 1230599. DIM-CMM (UMI 2807 CNRS), Universidad de
Chile<EMAIL_ADDRESS>work was supported by Centro de
Modelamiento Matemático (CMM), FB210005, BASAL funds for centers of excellence
from ANID-Chile, and ANID-FONDECYT 1220142. LIFO, Université d’Orléans and
INSA Centre-Val de Loire<EMAIL_ADDRESS>Pierre
Fraigniaud, Frédéric Mazoit, Pedro Montealegre, Ivan Rapaport and Ioan Todinca
[500]Theory of computation Distributed algorithms

# Distributed Certification for Classes of Dense Graphs

Pierre Fraigniaud  Frédéric Mazoit  Pedro Montealegre  Ivan Rapaport  Ioan
Todinca

###### Abstract

A _proof-labeling scheme_ (PLS) for a boolean predicate $\Pi$ on labeled
graphs is a mechanism used for certifying the legality with respect to $\Pi$
of global network states in a distributed manner. In a PLS, a _certificate_ is
assigned to each processing node of the network, and the nodes are in charge
of checking that the collection of certificates forms a global proof that the
system is in a correct state, by exchanging the certificates once, between
neighbors only. The main measure of complexity is the _size_ of the
certificates. Many PLSs have been designed for certifying specific predicates,
including cycle-freeness, minimum-weight spanning tree, planarity, etc.

In 2021, a breakthrough has been obtained, as a “meta-theorem” stating that a
large set of properties have compact PLSs in a large class of networks.
Namely, for every $\mathrm{MSO}_{2}$ property $\Pi$ on labeled graphs, there
exists a PLS for $\Pi$ with $O(\log n)$-bit certificates for all graphs of
bounded _tree-depth_. This result has been extended to the larger class of
graphs with bounded _tree-width_ , using certificates on $O(\log^{2}n)$ bits.

We extend this result even further, to the larger class of graphs with bounded
_clique-width_ , which, as opposed to the other two aforementioned classes,
includes dense graphs. We show that, for every $\mathrm{MSO}_{1}$ property
$\Pi$ on labeled graphs, there exists a PLS for $\Pi$ with $O(\log^{2}n)$-bit
certificates for all graphs of bounded clique-width. As a consequence,
certifying families of graphs such as distance-hereditary graphs and (induced)
$P_{4}$-free graphs (a.k.a., cographs) can be done using a PLS with
$O(\log^{2}n)$-bit certificates, merely because each of these two classes can
be specified in $\mathrm{MSO}_{1}$. In fact, we show that certifying
$P_{4}$-free graphs can be done with certificates on $O(\log n)$ bits only.
This is in contrast to the class of $C_{4}$-free graphs (which does not have
bounded clique-width) which requires $\tilde{\Omega}(\sqrt{n})$-bit
certificates.

###### keywords:

CONGEST, Proof Labelling Schemes, clique-width, MSO

##  1 Introduction

Checking whether a distributed system is in a legal global state with respect
to some boolean predicate occurs in several domains of distributed computing,
including the following.

  * •

Fault-tolerance: the occurrence of faults may turn the system into an illegal
state that needs to be detected for allowing the system to return to a legal
state.

  * •

The use of subroutines as black boxes: some of these subroutines may contain
bugs, and produce incorrect outputs that need to be checked before use in the
protocol calling the subroutines.

  * •

Algorithm design for specific classes of systems: an algorithm dedicated to
some specific class of networks (e.g., algorithms for trees, or for planar
networks) may cause deadlocks or live-locks whenever running on a network
outside the class. The membership to the class needs to be checked before
running the algorithm.

In all three cases above, the checking procedure may be impossible to
implement without significant communication overhead. A typical example is
bipartiteness, whether it be applied to the network itself, or to an overlay
network produced by some subroutine.

###  1.1 Proof-Labeling Schemes

_Proof-labeling scheme_ (PLS) [46] is a popular mechanisms enabling to certify
correctness w.r.t. predicates involving some global property, like
bipartiteness. A PLS involves a _prover_ and a _verifier_. The prover has
access to the global state of the network (including its structure), and has
unlimited computational power. It assigns _certificates_ to the nodes. The
verifier is a distributed algorithm running at each node, performing in a
single round, which consists for each node to send its certificate to its
neighbors. Upon reception of the certificates of its neighbors, every node
performs some local computation and outputs accept or reject. To be correct, a
PLS for a predicate $\Pi$ must satisfy:

$\begin{array}[]{c}\mbox{the global state of the network satisfies $\Pi$}\\\
\Updownarrow\\\ \mbox{the prover can assign certificates such that the
verifier accepts at all nodes.}\end{array}$

For instance, for bipartiteness, the prover assigns a color 0 or 1 to the
nodes, and each node verifies that its color is 0 or 1, and is different from
the color of each of its neighbors. If the network is bipartite then the
prover can properly 2-color the nodes such that they all accept, and if the
network is not bipartite then, for every 2-coloring of the nodes, some of them
reject as this coloring cannot be proper.

The PLS certification mechanism has several desirable features. First, if the
certificates are small then the verification is performed efficiently, in a
single round consisting merely of an exchange of a small message between every
pair of adjacent nodes. As a consequence, verification can be performed
regularly and frequently without causing significant communication overhead.
Second, if the network state does not satisfy the predicate, then at least one
node rejects. Such a node can raise an alarm or launch a recovery procedure
for allowing the system to return to a correct state, or can stop a program
running in an environment for which it was not designed. Third, the prover is
an abstraction, for the certificates can be computed offline, either by the
nodes themselves in a distributed manner, or by the system provider in a
centralized manner. For instance, a protocol constructing an overlay network
that is supposed to be bipartite, may properly 2-color the overlay for
certifying its bipartiteness. It follows from their features that PLSs are
versatile certification mechanisms that are also quite efficient whenever the
certificates for legal instances are small.

Many PLSs have been designed for certifying specific predicates on labeled
graphs, including cycle-freeness [46], minimum-weight spanning tree (MST)
[45], planarity [31], bounded genus [25], $H$-minor-freeness for small $H$
[6], etc. In 2021, a breakthrough has been obtained, as a “meta-theorem”
stating that a large set of properties have compact PLSs in a large class of
networks (see [27]). Namely, for every $\mathrm{MSO}_{2}$ property111Monadic
second-order logic (MSO) is the fragment of second-order logic where the
second-order quantification is limited to quantification over sets.
$\mathrm{MSO}_{1}$ refers to MSO on graphs with quantification over sets of
vertices, whereas $\mathrm{MSO}_{2}$ refers to MSO on graphs with
quantification over sets of vertices and sets of edges.  $\Pi$, there exists a
PLS for $\Pi$ with $O(\log n)$-bit certificates for all graphs of bounded
_tree-depth_ , where the tree-depth of a graph intuitively measures how far it
is from being a star. This result has been extended to the larger class of
graphs with bounded _tree-width_ (see [35]), using certificates on
$O(\log^{2}n)$ bits, where the tree-width of a graph intuitively measures how
far it is from being a tree. Although the class of all graphs with bounded
tree-width includes many common graph families such as trees, series-parallel
graphs, outerplanar graphs, etc., it does not contain families of _dense_
graphs. In this paper, we focus on the families of graphs with bounded
_clique-width_ , which include families of dense graphs.

###  1.2 Clique-Width

Intuitively, the definition of clique-width is based on a “programming
language” for constructing graphs, using only the following four instructions
(see [16] for more details):

  * •

Creation of a new vertex $v$ with some color $i$, denoted by
$\mathsf{color}(v,i)$;

  * •

Disjoint union of two colored graphs $G$ and $H$, denoted by $G\parallel H$;

  * •

Joining by an edge every vertex colored $i$ to every vertex colored $j\neq i$,
denoted by $i\Join j$;

  * •

Recolor $i$ into color $j$, denoted by $\mathsf{recolor}(i,j)$.

For instance, the $n$-node clique can be constructed by creating a first node
with color blue, and then repeating $n-1$ times the following: (1) the
creation of a new node, with color red, (2) joining red and blue, and (3)
recoloring red into blue. Therefore, cliques can be constructed by using two
colors only. Similarly, trees can be constructed with three colors only. This
can be proved by induction. The induction statement is that, for every tree
$T$, every vertex $r$ of $T$, and every two colors
$c_{1},c_{2}\in\\{\mbox{blue, red, green}\\}$, $T$ can be constructed with
colors blue, red, and green such that $r$ is eventually colored $c_{1}$, and
every other vertex is colored $c_{2}$. The statement is trivial for the
single-node tree. Let $T$ be a tree with at least two nodes, let $r$ be one of
its vertices, and let $c_{1},c_{2}$ be two colors. Given an arbitrary neighbor
$s$ of $r$, removing the edge $\\{r,s\\}$ results in two trees $T_{r}$ and
$T_{s}$. By induction, construct $T_{r}$ and $T_{s}$ separately so that $r$
(resp., $s$) is eventually colored $c_{1}$ (resp., $c_{2}$) and all the other
nodes of $T_{r}$ and $T_{s}$ are colored $c_{3}\notin\\{c_{1},c_{2}\\}$. Then
form the graph $T_{r}\parallel T_{s}$, and, in this graph, join colors $c_{1}$
and $c_{2}$, and recolor $c_{3}$ into $c_{2}$.

The clique-width of a graph $G$, denoted by $\mathsf{cw}(G)$, is the smallest
$k\geq 0$ such that $G$ can be constructed by using $k$ colors. For instance,
$\mathsf{cw}(K_{n})\leq 2$ for every $n\geq 1$, and, for every tree $T$,
$\mathsf{cw}(T)\leq 3$. A family of graphs has bounded clique-width if there
exists $k\geq 0$ such that, for every graph $G$ in the family,
$\mathsf{cw}(G)\leq k$. Any graph family with bounded tree-depth or bounded
tree-width has bounded clique-width [12, 49]. However, there are important
graph families with unbounded tree-width (and therefore unbounded tree-depth)
that have bounded clique-width. Typical examples (see [17]) are cliques (i.e.,
complete graphs), $P_{4}$-free graphs (i.e., graphs excluding a path on four
vertices as an induced subgraph, a.k.a., cographs), and distance hereditary
graphs (the distances in any connected induced subgraph are the same as they
are in the original graph).

Many NP-hard optimization problems can be solved efficiently by dynamic
programming in the family of graphs with bounded clique-width. In fact, every
$\mathrm{MSO}_{1}$ property on graphs has a linear-time algorithm for graphs
of bounded clique-width [16]. In this paper we show a similar form of “meta-
theorem”, regarding the size of certificates of PLS for monadic second-order
properties of graphs with bounded clique-width.

###  1.3 Our Results

Our main result is the following. Recall that a labeled graph is a pair
$(G,\ell)$, where $G$ is a graph, and $\ell:V(G)\to\\{0,1\\}^{\star}$ is a
function assigning a label to every node in $G$.

######  Theorem 1.1.

Let $k$ be a non-negative integer, and let $\Pi$ be an $\mathrm{MSO}_{1}$
property on node-labeled graphs with constant-size labels. There exists a PLS
certifying $\Pi$ for labeled graphs with clique-width at most $k$, using
$O(\log^{2}n)$-bit certificates on $n$-node graphs.

The same way several NP-hard problems become solvable in polynomial time in
graphs of bounded clique-width, Theorem 1.1 implies that several predicates
for which every PLS has certificates of polynomial size in arbitrary graphs
have a PLS with certificates of polylogarithmic size on graphs with bounded
clique-width. This is for instance the case of non-3-colorability (which is a
$\mathrm{MSO}_{1}$ predicate), for which every PLS has certificates of size
$\tilde{\Omega}(n^{2})$ bits in arbitrary graphs [42]. Theorem 1.1 implies
that non-3-colorability has a PLS with certificates on $O(\log^{2}n)$ bits in
graphs with bounded clique-width, and therefore in graphs of bounded tree-
width, cographs, distance-hereditary graphs, etc. This of course is extended
to non-k-colorability, as well as other problems definable in
$\mathrm{MSO}_{1}$ such as detecting whether the input graph does not contain
a fixed subgraph $H$ as a subgraph, induced subgraph, minor, etc.

In fact, Theorem 1.1 can be extended to properties including certifying
solutions to maximization or minimization problems whose admissible solutions
are defined by $\mathrm{MSO}_{1}$ properties. For instance maximum independent
set, minimum vertex cover, minimum dominating set, etc.

In the proof of Theorem 1.1, we provide a PLS that constructs a particular
decomposition using at most $k\cdot 2^{k-1}$ colors (the clique-width of the
decomposition). It is through that decomposition that the PLS certifies that
the input graph satisfies $\Pi$.

An application of Theorem 1.1 is the certification of certain families of
graphs. That is, given a graph family $\mathcal{F}$, designing a PLS for
certifying the membership to $\mathcal{F}$. Interestingly, there are some
graph classes $\mathcal{F}$ that are expressible in $\mathrm{MSO}_{1}$ and, at
the same time, have clique-width at most $k$. Theorem 1.1 provides a PLS for
certifying the membership to $\mathcal{F}$ in such cases. Indeed, the PLS
first tries to build a decomposition of clique-width at most $k\cdot 2^{k-1}$.
If there is no such decomposition, then the input graph does not belong to
$\mathcal{F}$. Otherwise, the PLS uses the decomposition to check the
$\mathrm{MSO}_{1}$ property that defines $\mathcal{F}$.

######  Corollary 1.2.

Let $k$ be a non-negative integer, and let $\mathcal{F}$ be graph family
expressible in $\mathrm{MSO}_{1}$ such that all graphs of the family have
clique-width at most $k$. Membership to $\mathcal{F}$ can be certified with a
PLS using $O(\log^{2}n)$-bit certificates in $n$-node graphs.

For instance, for every $k\geq 0$, the class of graphs with tree-width at most
$k$ can be certified with a PLS using $O(\log^{2}n)$-bit certificates. Indeed,
“tree-width at most $k$” is expressible in $\mathrm{MSO}_{1}$, and the class
of graphs with tree-width at most $k$ forms a family with clique-width at most
$3\cdot 2^{k-1}+1$ [12]. Another interesting application is the certification
of $P_{4}$-free graphs. Indeed, “excluding $P_{4}$ as induced subgraph” is
expressible in $\mathrm{MSO}_{1}$, and $P_{4}$-free graphs form a family with
clique-width at most 2 [17]. It follows that $P_{4}$-free graphs can be
certified with a PLS using $O(\log^{2}n)$-bit certificates. This is in
contrast to the class of $C_{4}$-free graphs (i.e. graphs not containing a
cycle on four vertices, whether it be as induced subgraph or merely subgraph),
which requires certificates on $\tilde{\Omega}(\sqrt{n})$ bits [20]. In fact,
in the case of cographs, the techniques in the proof of Theorem 1.1 can be
adapted so that to save one log-factor, as stated below.

######  Theorem 1.3.

The class of (induced) $P_{4}$-free graphs can be certified with a PLS using
$O(\log n)$-bit certificates in $n$-node graphs.

Note that there is a good reason for the huge gap in terms of certificate-size
between $P_{4}$-free graphs and $C_{4}$-free graphs. The point is that, for
any graph pattern $H$, the class of $H$-free graphs has bounded clique-width
if and only if $H$ is an induced subgraph of $P_{4}$ [19]. Therefore,
$C_{4}$-free graphs (as well as triangle-free graphs) do not have bounded
clique-width, as opposed to $P_{4}$-free graphs (and $P_{3}$-free graphs,
which are merely cliques).

###  1.4 Related Work

Proof-Labeling Schemes (PLSs) have been introduced and thoroughly studied in
[46]. Variants have been been considered in [42] and [34], which slightly
differ from PLSs: the former allows each node to transfer no only its
certificates, but also its state, and the latter restricts the power of the
oracle, which is bounded to produce certificates independent of the IDs
assigned to the nodes. All these forms of distributed certifications have been
extended in various directions, including tradeoffs between the size of the
certificates and the number of rounds of the verification protocol [30], PLSs
with computationally restricted provers [24], randomized PLSs [37], quantum
PLSs [33], PLSs rejecting at more nodes whenever the global state is “far”
from being correct [28], PLSs using global certificates in addition to the
local ones [32], and several hierarchies of certification mechanisms,
including games between a prover and a disprover [1, 29], interactive
protocols [18, 44, 48], and even recently zero-knowledge distributed
certification [3], and distributed quantum interactive protocols [40].

All the aforementioned distributed certification mechanisms have been used for
certifying a wide variety of global system states, including MST [45], routing
tables [2], and a plethora of (approximated) solutions to optimization
problems [11, 23]. A vast literature has also been dedicated to certifying
membership to graph classes, including cycle-freeness [46], planarity [31],
bounded genus [25], absence of symmetry [42], $H$-minor-freeness for small $H$
[6], etc. In 2021, a breakthrough has been obtained, as a “meta-theorem”
stating that, for every $\mathrm{MSO}_{2}$ property $\Pi$, there exists a PLS
for $\Pi$ with $O(\log n)$-bit certificates for all graphs of bounded _tree-
depth_ [27]. This result has been extended to the larger class of graphs with
bounded _tree-width_ , using certificates on $O(\log^{2}n)$ bits [35]. To our
knowledge, this is the largest class of graphs, and the largest class of
boolean predicates on graphs for which it is known that PLSs with
polylogarithmic certificates exist.

The class of $H$-free graphs (i.e., the absence of $H$ as a subgraph), for a
given fixed graph $H$, has attracted lot of attention in the distributed
setting, mostly in the CONGEST model. Two main approaches have been
considered. One, called distributed property testing, aims at deciding between
the case where the input graph is $H$-free, and the case where the input graph
is “far” from being $H$-free (see, e.g., [7, 9, 26, 38]). In this setting, the
objective is to design (randomized) algorithms performing in a constant number
of rounds. Such algorithms have been designed for small graphs $H$, but it is
not known whether there is a distributed algorithm for testing
$K_{5}$-freeness in a constant number of rounds. The other approach aims at
designing algorithms deciding $H$-freeness performing in a small number of
rounds. For instance, it is known that deciding $C_{4}$-freeness can be done
in $\tilde{O}(\sqrt{n})$ rounds, and this is optimal [20]. The
$\tilde{\Omega}(\sqrt{n})$-round lower bounds for $C_{4}$-freeness also holds
for deciding $C_{2k}$-freeness, for every $k\geq 4$. Nevertheless, the best
known algorithm performs in essentially $\tilde{O}(n^{1-\Theta(1/k^{2})})$
rounds [22], even if faster algorithms exists for $k=2,3,4,5$, running in
$\tilde{O}(n^{1-\Theta(1/k)})$ rounds [10, 21]. Deciding $P_{k}$-freeness (as
subgraph) can be done efficiently for all $k\geq 0$ [36]. However, this is not
the case of deciding the absence of an _induced_ $P_{k}$, and no efficient
algorithms are known apart for the trivial cases $k=1,2,3$. The first non-
trivial case is deciding cographs, i.e., $P_{4}$-freeness (as induced
subgraph).

The terminology _meta-theorem_ is used in logic to refer to a statement about
a formal system proven in a language used to describe another language. In the
study of graph algorithms, Courcelle’s theorem [13] is often referred to as a
meta-theorem. It says that every graph property definable in the monadic
second-order logic $\mathrm{MSO}_{2}$ of graphs can be decided in linear time
on graphs of bounded treewidth. This theorem was extended to clique-width, but
for a smaller set of graph properties. Specifically, every graph property
definable in the monadic second-order logic $\mathrm{MSO}_{1}$ of graphs can
be decided in linear-time on graphs of bounded clique-width [16]. Note that
the classes of languages in $\mathrm{MSO}_{1}$ and $\mathrm{MSO}_{2}$ include
languages that are NP-hard to decide (e.g., 3-colorability and Hamiltonicity,
respectively). We remind that $\mathrm{MSO}_{2}$ is as an extension of
$\mathrm{MSO}_{1}$ which also allows quantification on sets of edges – see
Footnote 1 for a short description, or [14] for full details. Some graph
properties, e.g., Hamiltonicity, are expressible in $\mathrm{MSO}_{2}$ but not
in $\mathrm{MSO}_{1}$, nevertheless $\mathrm{MSO}_{1}$ captures a large set of
properties, including many classical NP-hard problems as explained above.
Eventually, we emphasize again that, when comparing the two most famous meta-
theorems, (1) _$\mathrm{MSO}_{2}$ properties are decidable in linear time on
bounded treewidth graphs_ vs. (2) _$\mathrm{MSO}_{1}$ properties are decidable
in linear time on bounded clique-width graphs_, the former concerns a larger
class of properties, but the latter concerns larger classes of graphs.

##  2 Models

In this section, we recall the main concepts used in this paper, including
proof-labeling scheme, and cographs.

###  2.1 Proof-Labeling Schemes for MSO Properties

For a fixed integral parameter $\lambda\geq 0$, we consider vertex-labeled
graphs $(G,\ell)$, where $G=(V,E)$ is a connected simple $n$-node graph, and
$\ell:V\to\\{0,\dots,\lambda-1\\}$. The label may indicate a solution to an
optimization problem, e.g., a minimum dominating set ($\ell(v)=0$ or $1$
depending on whether $v$ is in the set or not), a $\lambda$-coloring, an
independent set, etc. A labeling may also encode global overlay structures
such as spanning trees or spanners, in bounded-degree graphs or in graphs
provided by a distance-2 $k$-coloring, for $k=O(1)$. In the context of
distributed computing in networks, nodes are assumed to be assigned distinct
identifiers (ID) in $[1,n^{c}]$ for some $c\geq 1$, so that IDs can be stored
on $O(\log n)$ bits. The identifier of a node $v$ is denoted by
$\mathsf{id}(v)$. We denote by $N_{G}(v)$ the set of neighbors of node $v$ in
a graph $G$, and we let $N_{G}[v]=N_{G}(v)\cup\\{v\\}$ be the closed
neighborhood of $v$.

Given a boolean predicate $\Pi$ on vertex-labeled graphs, a _proof-labeling
scheme_ (PLS) for $\Pi$ is a prover-verifier pair. The _prover_ is a non-
trustable computationally unbounded oracle. Given a vertex-labeled graph
$(G,\ell)$ with ID-assignment $\mathsf{id}$, the prover assigns a
_certificate_ $c(v)$ to every node $v$ of $G$. The _verifier_ is a distributed
algorithm running at every node $v$ of $G$. It performs a single round of
communication consisting of sending $c(v)$ to all neighboring nodes $w\in
N_{G}(v)$, and receiving the certificates of all neighbors. Given
$\mathsf{id}(v)$, $\ell(v)$, and $\\{c(w):w\in N_{G}[v]\\}$, every node $v$
outputs _accept_ or _reject_. A PLS is correct if the following two conditions
are satisfied:

  * •

Completeness: If $(G,\ell)$ satisfies $\Pi$ then the prover can assign
certificates to the nodes such that the verifier accepts at all nodes;

  * •

Soundness: If $(G,\ell)$ does not satisfy $\Pi$ then, for every certificate
assignment to the nodes by the prover, the verifier rejects in at least one
node.

The main parameter measuring the quality of a PLS is the _size_ (i.e., number
of bits) of the certificates assigned by the prover to each node of vertex-
labeled graphs satisfying the predicate, and leading all nodes to accept.

#### MSO Predicates.

We focus on predicates expressible in $\mathrm{MSO}_{1}$. Recall that
$\mathrm{MSO}_{1}$ is the fragment of monadic second-order (MSO) logic on
(vertex-labeled) graphs that allows quantification on vertices and on sets of
(labeled) vertices, and uses the adjacency predicate ($\mathsf{adj}$). For
instance non 3-colorability is in $\mathrm{MSO}_{1}$. Indeed, for every graph
$G=(V,E)$, it can be expressed as: for all $A,B,C\subseteq V$, if $A\cup B\cup
C=V$ and $A\cap B=A\cap C=B\cap C=\varnothing$ then

$\exists(u,v)\in(A\times A)\cup(B\times B)\cup(C\times C):(u\neq
v)\land\mathsf{adj}(u,v).$

We shall show that, although some $\mathrm{MSO}_{1}$ predicates, like
non-3-colorability, require certificates on $\tilde{\Omega}(n^{2})$ bits in
$n$-node graphs (see [42]), PLSs with certificates of polylogarithmic size can
be designed for all $\mathrm{MSO}_{1}$ predicates in a rich class of graphs,
namely all graphs with bounded clique-width.

###  2.2 Cographs and Cotrees

We conclude this section by introducing a graph class that plays an important
role in this paper. Recall that a graph is a cograph (see, e.g., [8]) if it
can be constructed by a sequence of parallel operations (disjoint union of two
vertex-disjoint graphs) and join operations (connecting two vertex-disjoint
graphs $G$ and $H$ by a complete bipartite graphs between $V(G)$ and $V(H)$).
Therefore, by definition, cographs have clique-width 2. In particular, cliques
are cographs.

It is known [8] that cographs capture precisely the class of induced
$P_{4}$-free graphs. We shall show that, as opposed to $C_{4}$-free graphs,
which require $\tilde{\Omega}(\sqrt{n})$-bit certificates to be certified by a
PLS [20]222The lower bound in [20] is expressed for the CONGEST and Broadcast
Congested Clique models, but it extends directly to PLSs since Set-
Disjointness has non-deterministic communication complexity $\Omega(N)$ on
$N$-bit inputs., $O(\log n)$-bit certificates are sufficient for certifying
$P_{4}$-free graphs. This result is of interest on its own, but proving this
result will also play the role of a warmup before establishing our general
result about graphs with bounded clique-width. Note that the class of
$P_{4}$-free graphs (i.e., cographs) can be specified by an $\mathrm{MSO}_{1}$
formula. Roughly, the formula states that if there exists four vertices
$v_{1},v_{2},v_{3},v_{4}$ such that $\mathsf{adj}(v_{i},v_{i+1})$ for
$i=1,2,3$, then
$\mathsf{adj}(v_{1},v_{3})\lor\mathsf{adj}(v_{1},v_{4})\lor\mathsf{adj}(v_{2},v_{4}).$
$C_{4}$-freeness could be expressed in $\mathrm{MSO}_{1}$ as well. However,
$P_{4}$-free graphs have clique-width 2 whereas $C_{4}$-free graphs have
unbounded clique-width — this is because there are $2^{\Omega(n\sqrt{n})}$
different $C_{4}$-free graphs of size $n$, but only $2^{\mathcal{O}(n\log n)}$
$n$-vertex graphs of bounded clique-width.

Given a cograph $G$, there is actually a canonic way of constructing $G$ by a
sequence of parallel and join operations [8]. As explained before, this
construction can be described as a tree $T$ whose leaves are the vertices of
$G$, and whose internal nodes are labeled $\parallel$ or $\Join$. This tree is
called a _cotree_ , and will be used for our PLS.

##  3 Overview of our Techniques

The objective of this section is to provide the reader with a general idea of
our proof-labeling scheme. Our construction bears some similarities with the
approach used in [35] for the certification of $\mathrm{MSO}_{2}$ properties
on graphs of bounded tree-width, with certificates of size $O(\log^{2}n)$
bits. However, extending this approach to a proof-labeling scheme for graphs
with bounded clique-width requires to overcome several significant obstacles.
We therefore start by summarizing the main tools used for the certification of
$\mathrm{MSO}_{2}$ properties on graphs of bounded tree-width (see Section
3.1), and then proceed with the description of the new tools required for
extending the result to graphs of bounded clique-width, to the cost of
reducing the class of certified properties from $\mathrm{MSO}_{2}$ to
$\mathrm{MSO}_{1}$ (see Sections 3.2-3.6).

###  3.1 Certifying $\mathrm{MSO}_{2}$ Properties in Graphs of Bounded Tree-
Width

Recall that a tree-decomposition of a graph $G$ is a tree $T$ where each node
$x$ of $T$, also called _bag_ , is a subset of $V(G)$, satisfying the
following three conditions: (1) for every vertex $v\in V(G)$ there is a bag
$x\in V(T)$ that contains $v$, (2) for every edge $\\{u,v\\}\in E(G)$, there
is a bag $x$ containing both its endpoints, and (3) for each vertex $v\in
V(G)$, the set of bags that contains $v$ forms a (connected) subtree of $T$.
Let $\Pi$ be an $\mathrm{MSO}_{2}$ property, and let $T$ be a tree-
decomposition of the graph $G$. The proof-labeling scheme aims at providing
each vertex with sufficient information for certifying the correctness of $T$,
as well as the fact that $G$ satisfies $\Pi$. To do so, the certificate of
each vertex is divided into two parts, one called _main messages_ , and the
other called _auxiliary messages_.

#### Main messages.

The main message of a node $v$ is a sequence $\textrm{seq}_{v}$ representing a
path of bags in $T$ that connects a leaf with the root, such that $v$ is
contained in at least one bag of $\textrm{seq}_{v}$. For each bag
$x\in\textrm{seq}_{v}$, the main message includes, roughly: the set of
vertices contained in $x$, the identifier of a vertex $\ell_{x}$ in $x$,
called the _leader_ of $x$, and a data structure $c_{x}$ used to verify the
$\mathrm{MSO}_{2}$ property $\Pi$ on $G$. The leader $\ell_{x}$ of $x$ is
chosen arbitrarily among the vertices of $x$ that are adjacent to a vertex $u$
belonging to the parent bag $p(x)$ of $x$ in $T$. The vertex $u$ is said to be
_responsible_ for $x$ in $p(x)$. Let us assume the following consistency
condition: for every bag $x$ of $T$, every vertex in $x$ received the same
information about all the bags from $x$ to the root of $T$. Under the promise
that the consistency condition holds, it is possible to show that the vertices
can collectively verify that $T$ is indeed a tree-decomposition of $G$, and
that $G$ satisfies $\Pi$.

#### Auxiliary messages.

The role of the auxiliary messages is precisely to check the above consistency
condition. For each bag $x$, let $\tau_{x}$ be a Steiner tree (i.e. a minimal
tree connecting a set of vertices denoted _terminals_) in $G$ rooted at the
leader $\ell_{x}$, with all the nodes of $x$ as terminals. Every vertex in
$\tau_{x}$ receives an auxiliary message containing the certification of
$\tau_{x}$ (each vertex of $\tau_{x}$ receives the identifier of a root, of
its parent and the distance to the root), and a copy of the information about
$x$ given to the nodes in the bag $x$, through their main messages. By using
the auxiliary messages, the leader $\ell_{x}$ can verify whether the subgraph
$G[x]$ of $G$ induced by the union of the bags in $T[x]$ satisfies $\Pi$,
where $T[x]$ the subtree of $T$ containing $x$ and all its descendants.
Specifically, this verification is performed by simulating the dynamic
programming algorithm in Courcelle’s Theorem [13] as in the version of Boire,
Parker and Tovey [5]. This uses a constant-size data structure $c_{x}$ stored
in the auxiliary messages that “encodes” the predicate $\Pi(G[x])$. Its
correctness can be verified by a composition of the values $c_{y}$ for each
child $y$ of $x$ in $T$. The tree $\tau_{x}$ is actually used to transfer the
information about $c_{y}$ from the node $\ell_{y}$ in $x$ responsible for $y$,
to the leader $\ell_{x}$.

#### Certificate size.

If $T$ is of depth $d$, then the main messages are of size $O(d\log n)$ bits.
Crucially, for every graph $G$, there is a tree-decomposition $T$ satisfying
that, for every bag $x$, there is a Steiner tree $\tau_{x}$ completely
contained in $G[x]$. Such a decomposition is called _coherent_ in [35] (Lemma
3). It follows that every node participates in a Steiner tree with at most $d$
bags, which implies that the auxiliary messages can be encoded in $O(d\log n)$
bits. Thanks to a construction by Bodlaender [4], it is possible to choose a
coherent tree-decomposition with depth $d=O(\log n)$, up to increasing the
sizes of the bags by a constant factor only. It follows that the certificates
are of size $O(\log^{2}n)$ bits.

Our construction also follows the general structure described above. However,
each element of this construction has to be adapted in a highly non-trivial
way. Indeed, the grammar of clique-with, and the related structure of NLC
decomposition, differ in several significant ways from the grammar of tree-
width. The rest of the section is dedicated to providing the reader with a
rough idea of how this can be done.

###  3.2 Clique-Width and NLC-Width

First, instead of working with clique-width, it is actually more convenient to
work with the NLC-width, where NLC stands for _node-label controlled_. Every
graph of clique-width at most $k$ has NLC-width at most $k$, and every graph
of NLC-width at most $k$ has clique-width at most $2k$ [43]. As clique-width,
NLC-width can be viewed as the following grammar for constructing graphs,
bearing similarities with the grammar for clique-width:

  * •

Creation of a new vertex $v$ with color $i\in\mathbb{N}$, denoted by
$\mathsf{newVertex}_{i}$;

  * •

Given a set $S$ of ordered pairs of colors, and an ordered pair $(G,H)$ of
vertex-disjoint colored graphs, create a new graph as the union of $G$ and
$H$, then join by an edge every vertex colored $i$ of $G$ to every vertex
colored $j$ of $H$, for all $(i,j)\in S$; this operation is denoted by
$G\Join_{S}H$;

  * •

Recolor the graph, denoted by $\mathsf{recolor}_{R}$ where
$R:\mathbb{N}\to\mathbb{N}$ is any function.

If $k\geq 1$ colors are used, a recoloring function $R$ is a function
$R:[k]\to[k]$. When $R$ is used, for every $i\in[k]$, vertices with color $i$
are recolored $R(i)\in[k]$ (all colors are treated simultaneously, in
parallel). Note that the recoloring operation in the definition of clique-
width is limited to functions $R$ that preserve all colors but one. Note also
that, for $S=\varnothing$, the operation $G\Join_{S}H$ is merely the same as
$G\parallel H$ for clique-width. We therefore use $G\Join_{\varnothing}H$ or
$G\parallel H$ indistinctly. The NLC-width of a graph $G$ is the smallest
number of colors such that $G$ can be constructed using the operations above.
It is denoted by $\mathsf{nlcw}(G)$. For instance, the $n$-node clique can be
constructed by creating a first node $v_{1}$ with color 1, and then repeating,
for all $i=1,\dots,n-1$, (1) the creation of a new node $v_{i+1}$, with color
1 as well, and (2) applying $v_{i+1}\Join_{\\{(1,1)\\}}K_{i}$ to get the
clique $K_{i+1}$ on $i+1$ vertices. Therefore, cliques can be constructed by
using one color only, i.e., $\mathsf{nlcw}(K_{n})=1$ for every $n\geq 1$.

#### NLC-decomposition.

For every $k\geq 1$, the construction of a graph $G$ with
$\mathsf{nlcw}(G)\leq k$ can be described by a binary tree $T$, whose leaves
are the (colored) vertices of $G$. In $T$, every internal node $x$ has an
identified left child $x^{\prime}$ and an identified right child
$x^{\prime\prime}$, and is labeled by $\parallel$ or $\Join_{S}$ for some non-
empty set $S\subseteq[k]\times[k]$. This label indicates the operation
performed on the (left) graph $G^{\prime}$ with vertex-set equal to the leaves
of the subtree $T_{x^{\prime}}$ of $T$ rooted at $x^{\prime}$, and the (right)
graph $G^{\prime\prime}$ with vertex-set equal to the leaves of the subtree
$T_{x^{\prime\prime}}$ of $T$ rooted at $x^{\prime\prime}$. That is, node $x$
corresponds to the operation $G_{x^{\prime}}\parallel G_{x^{\prime\prime}}$ or
$G_{x^{\prime}}\Join_{S}G_{x^{\prime\prime}}$, depending on the label of $x$.
In addition to its label ($\parallel$ or $\Join_{S}$ for some
$S\neq\varnothing$), a node may possibly also include a recoloring function
$R:[k]\to[k]$, which indicates a recoloring to be performed _after_ the join
operation, see Figure 1 for an example.

Figure 1: An NLC decomposition tree $T$. Next to each node $x$ of the tree is
displayed the colored graph $G[x]$ corresponding to subtree $T[x]$ of $T$
rooted at $x$.

###  3.3 From Tree-Width to NLC-Width: The Main Messages

Let $\Pi$ be an $\mathrm{MSO}_{1}$ property, and let $T$ be an NLC-
decomposition tree of a graph $G$ with $\mathsf{cw}(G)\leq k$. That is, we can
choose the tree $T$ as one using at most $k$ colors. In the following, to
avoid confusion, we call _vertices_ the elements of the vertex set of $G$, and
_nodes_ the elements of the vertex-set of the decomposition tree $T$. The
structure of our certificates differ from the one in [35], and now we
decompose the certificate assigned to each node $v$ into three parts: _main
messages_ , _auxiliary messages_ , and _service messages_. This subsection
focuses on the main messages.

Our main messages have, to some extent, a structure similar to the main
messages used in [35] for the tree-width. In particular, vertex $v$ receives a
sequence $\textsf{path}(v)$, listing all the nodes, i.e., the whole set of
operations, in the path from the root of $T$ to the leaf of $T$ where $v$ was
created. For each node $x$ in $\textsf{path}(v)$, the main message also
includes the vertex identifier of a leader for $x$, called _exit vertex of
$x$_, and denoted by $\textsf{exit}(x)$. The main message also includes a data
structure $h(x)$ that encodes the truth value of the $\mathrm{MSO}_{1}$
property on $G[x]$. However, unlike the case of tree-width, where the nodes of
the tree-decomposition are sets of vertices (i.e., bags) of bounded size, the
contents of a non-leaf node in an NLC-decomposition tree $T$ does not
necessarily include information about the vertices created in $T[x]$. For that
reason, our proof-labeling scheme includes additional information in the main
message of $v$ in order to verify the correctness of the given decomposition.
It may actually be worth providing a concrete example to explain the need for
additional information.

#### Example.

Let us pick an arbitrary edge $\\{u,v\\}\in E(G)$, and denote by
$(x_{1}(u),\dots,x_{t_{1}}(u))$ and $(x_{1}(v),\dots,x_{t_{2}}(v))$ the
sequences $\textsf{path}(u)$ and $\textsf{path}(v)$, respectively, where
$x_{1}(u)=x_{1}(v)$ is the root of $T$, and $x_{t_{1}}(u)$ and $x_{t_{2}}(v)$
are the nodes where $u$ and $v$ are respectively created. Let
$x_{1},\dots,x_{t_{3}}$ be the longest common prefix of these two sequences,
i.e., the information contained in their main messages coincide on the first
$t_{3}$ elements, but $x_{t_{3}+1}(u)\neq x_{t_{3}+1}(v)$. In the tree $T$,
$x_{t_{3}+1}(u)$ and $x_{t_{3}+1}(v)$ are two children of $x_{t_{3}}$. The
sequence of operations described in $x_{t_{1}}(u),\dots,x_{t_{3}+1}(u)$
defines the color $c(u)$ that $u$ has in $x_{t_{3}+1}(u)$. Similarly, the
color $c(v)$ of $v$ in $x_{t_{3}+1}(v)$ is defined by
$x_{t_{2}}(v),\dots,x_{t_{3}+1}(v)$. In order to create the edge $\\{u,v\\}$,
the operations described in $x_{t_{3}}$ must specify a $\Join$ operation
between vertices with color $c(u)$ and vertices with color $c(v)$. However,
the join operations described in an NLC-decomposition tree make a clear
distinction between the left and right children of a node. Therefore, in our
example, for checking that the edge $\\{u,v\\}$ is indeed correctly created in
the given decomposition tree, the vertices $u$ and $v$ must be able to
distinguish which of the two children $x_{t_{3}+1}(u)$ and $x_{t_{3}+1}(v)$ of
$x_{t_{3}}$ is the left child, and which one is the right child.

For a node $x$ different from the root, let us denote by $p(x)$ the parent of
$x$ in $T$. The main message of $v$ includes a sequence $\textsf{links}(v)$
that specifies, for each node $x$ in $\textsf{path}(v)$ different from the
root, whether $x$ is the left or right child of $p(x)$. For instance, in the
example of Figure 1, we have $\textsf{links}(c)=(1,0)$, indicating that, to
reach the leaf creating vertex $c$ from the root, one must follow the right
child (1), and then the left child (0). S imilarly,
$\textsf{links}(d)=(1,1,0)$. The sequences links are also used to determine
the longest common prefixes of the main messages, when the same operations are
repeated between two children of a same node (consider for instance the case
where the same operation is performed at all the nodes of the decomposition
tree). Back to our example above, let us suppose that the sequences
$\textsf{links}(u)$ and $\textsf{links}(v)$ specify that $x_{t_{3}+1}(u)$ is
the left neighbor of $x_{t_{3}}$, and $x_{t_{3}+1}(v)$ is the right neighbor
of $x_{t_{3}}$. Using this information, $u$ and $v$ can infer that it is an
operation $\Join_{S}$, with $(c(u),c(v))\in S$ that is specified in the
description of $x_{t_{3}}$. With the given information, each vertex can thus
check that all its incident edges are indeed created at some node of the
decomposition tree $T$.

It remains to check that the decomposition does not define non-existent edges.
To do so, the main message of every vertex $v$ also includes, for each node
$x$ in $\textsf{path}(v)$, and for each $i\in[k]$, the integers
$\textsf{color}_{i}(x)$ representing the number of vertices of $G[x]$ that are
colored $i$ in the root of $T[x]$. (Recall that the subgraph $G[x]$ is the
subgraph of $G$ induced by the vertices created in the subtree $T[x]$ of $T$).
Returning to our example, vertex $v$ checks that it has exactly
$\textsf{color}_{c(u)}(x_{t_{3}+1}(u))$ neighbors with the same longest common
prefix as $u$ colored $c(u)$ in the left children of $x_{t_{3}}$. Also, vertex
$v$ checks, for each $i\in[k]$, that the number of vertices colored $i$ in
node $x_{t_{3}}$ corresponds to the sum of the number of vertices colored $j$
in $x_{t_{3}+1}(u)$ and $x_{t_{3}+1}(v)$, for each color $j$ that is recolored
$i$ by the recoloring operation defined in $x_{t_{3}}$. So, let us assume that
the following consistency condition (analogous to the one for the
certification of tree-decompositions) holds:

C1:

For every pair of vertices $u,v\in V(G)$, and for every node $x$ in both
$\textsf{path}(u)$ and $\textsf{path}(v)$, $u$ and $v$ receive the same
information about all nodes in the path from $x$ to the root of $T$ in their
main messages, and

C2:

If $x$ is the root of $T$, then the data structure $h(x)$ describes an
accepting instance (i.e., $G$ satisfies $\Pi$).

Assuming that the consistency condition is satisfied, it is not difficult to
show that the vertices can collectively check that the given certificates
indeed represent an NLC-decomposition tree, and that $G$ satisfies $\Pi$. The
difficulty is however in checking that the consistency condition holds. This
is the role of the auxiliary and service messages, described next.

###  3.4 Checking Consistency: Auxiliary, and Service Messages

We use auxiliary and service messages for allowing our proof-labeling scheme
to check the first condition C1 of the consistency condition defined at the
end of the previous subsection.

Auxiliary messages can easily be defined for every node $x$ of $T$ satisfying
that $G[x]$ is connected. In that case, the auxiliary messages of all the
vertices $v$ in $T[x]$ contain the certificates for certifying a spanning tree
$\tau_{x}$ of $G[x]$ rooted at the exit vertex of $x$. Each vertex $v$ can
verify that the longest common prefix common to $v$ and its parent in
$\tau_{x}$ contains all the nodes from the root up to $x$, and that the
information given in the main messages coincide for all such nodes. Observe
that every vertex $v$ may potentially contain one auxiliary message for each
node in $\textsf{path}(v)$.

The case where $G[x]$ is not connected is fairly more complicated, and we need
to introduce another type of decomposition.

#### NLC+ decompositions trees.

Observe that $G$ itself is connected. Therefore, there must exist an ancestor
$z$ of $x$ for which $G[z]$ is connected. We could provide the vertices in
$G[z]$ with a spanning tree of $G[z]$ for checking the consistency in $T[x]$.
However, the vertices in $G[z]$ do not necessarily contain $x$ in the prefixes
of their node sequences, so we would have to put a copy of the main message
associated to $x$ on every node participating in the spanning tree. Since an
NLC-decomposition tree does not allow to provide a bound on the distance
between $z$ and $x$ in the tree, we have no control on how many copies of main
messages a vertex should handle.

Therefore, to cope with the case where $G[x]$ is disconnected, we define a
specific type of NLC decompositions trees, called NLC+ decompositions trees.
The NLC+ decomposition trees are similar to NLC-decomposition trees, up to two
important differences.

  * •

First, we allow the nodes corresponding to a $\parallel$ operation to have
arbitrary large arity, and thus NLC+ decomposition trees are not binary trees,
as opposed to NLC-decomposition trees.

  * •

Second, if a node $x$ induces a disconnected subgraph $G[x]$, then its parent
node $p(x)$ must satisfy that $G[p(x)]$ is connected. Observe that $p(x)$ must
then correspond to a $\Join$ operation, and thus $p(x)$ has only two children:
$x$ and another child, denoted by $y$.

#### Service trees.

A _service tree_ $S_{x}$ for a node $x$ such that $G[x]$ is disconnected is a
Steiner tree in $G[p(x)]$ rooted at the exit vertex of $x$, and with all the
vertices of $G[x]$ as terminals. Each vertex of $S_{x}$ (i.e., all vertices in
$G[x]$, plus some vertices in $G[y]$ is given a _service message_ , which
contains the certificate for the tree $S_{x}$, as well as a copy of the
information about $x$ given in the main messages of the vertices in $G[x]$.
Each vertex in $S_{x}$ can then check that it shares the same information
about $x$ than its parent. The properties of the NLC+ decomposition guarantee
that a vertex $v$ participates to at most two service trees, for each node $x$
in the sequence $\textsf{path}(v)$. Indeed, vertex $v$ necessarily
participates in $S_{x}$ when $x$ is of type $\parallel$, and may also
participate in $S_{y}$ whenever the sibling $y$ of $x$ is of type $\parallel$.
There are significantly more subtle details concerning service trees, but they
will be described in Section 5.

It remains to check the second condition C2 of the consistency condition
defined at the end of the previous subsection, which consists in verifying the
correctness of $h(x)$, for every node $x$ of $T$. This is explained next.

###  3.5 Dealing with $\mathrm{MSO}_{1}$ Predicates

In their seminal work, Courcelle, Makowsky and Rotics [16] proved that every
$\mathrm{MSO}_{1}$ predicate $\Pi$ on vertex-labeled graphs can be decided in
linear time on graphs of bounded clique-width, and hence on graphs of bounded
NLC-width, whenever a decomposition tree is part of the input. The running
time of the algorithm is $O(n)$, i.e., linear in the number $n$ of vertices of
the input graph, with constants hidden in the big-O notation that depend on
the clique-width bound, on the number of labels, and on the $\mathrm{MSO}_{1}$
formula encoding the predicate $\Pi$. Note that this result does not hold for
$\mathrm{MSO}_{2}$ predicates, which is why our proof-labeling scheme applies
to $\mathrm{MSO}_{1}$ predicates only. We discuss the possible extension to
$\mathrm{MSO}_{2}$ properties in the conclusion (see Section 7).

For our purpose it is convenient to see the linear-time decision algorithm as
a dynamic programming algorithm over the NLC-decomposition tree of the input
graph. We formalize this dynamic programming approach following the vocabulary
and notations used by Borie, Parker and Tovey [5]. Note that the latter
provided an alternative proof of Courcelle’s theorem, but for graphs of
bounded tree-width, i.e., specific to a graph grammar defining tree-width. To
design our proof-labeling scheme, we adapt their approach to a graph grammar
defining NLC-width.

#### Homomorphism Classes.

For a fixed property $\Pi$ and a fixed parameter $k$, there is a finite set
$\mathcal{C}$ of _homomorphism classes_ (whose size depends only on $\Pi$ and
$k$) such that we can associate to each graph $G$ of clique-width at most $k$
its class $h(G)\in\mathcal{C}$ (for more details see Proposition 5.2).
Whenever $G$ is obtained from two graphs $G_{1}$ and $G_{2}$ by a $\Join_{S}$
operation potentially followed by a recoloring operation $R$, the class $h(G)$
only depends on $h(G_{1})$, $h(G_{2})$, $S\subseteq[k]\times[k]$, and
$R:[k]\to[k]$. This property also holds whenever $\Join_{S}$ is replaced by
$\parallel$. Moreover, we also extend the notion to arbitrary arity so that it
holds for the NLC+ decomposition trees. Importantly, Courcelle’s theorem [16]
provides a "compiler" allowing to compute $h(G)$ whenever $G$ is formed by a
single vertex of color $j\in[k]$, and to compute $h(G)$ from $h(G_{1})$,
$h(G_{2})$, $S$ and $R$ whenever $G=R(G_{1}\Join_{S}G_{2})$.

#### Checking Condition C2.

In our proof-labeling scheme, for each node $x$ of the NLC+ decomposition
tree, we specify $h(x)$ as the class $h(G[x])$. Following the same principles
as before, the consistency of these classes can be checked by simulating a
bottom-up parsing of the decomposition tree, in a way very similar to what we
described before for checking the consistency of $\textsf{color}(x)$, but
replacing the mere additions by updates of the homomorphism classes as
described above.

This completes the rough description of our proof-labeling scheme.

###  3.6 Certificate Size

For each vertex $v$, the main, auxiliary, and service messages of $v$ can be
encoded using $O(\log n)$ bits for each node $x$ in $\textsf{path}(v)$, for
the following reasons.

  * •

The main message associated to a node $x$ contains the following information.
First, the list of operations described in the node, which can be encoded in
$O(k^{2})$ bits. Second, the corresponding index of links, which is just one
bit representing whether $x$ is the left or right children of its parent.
Third, the homomorphism class $h(x)$ that can be encoded in $f(k)$ bits for
some function $f$ depending on the $\mathrm{MSO}_{1}$ property under
consideration — see the remark further in the text for a discussion about $f$.
Finally, it includes the node identifier of the exit vertex of $x$, and the
integers $\textsf{color}_{i}$ for each $i\in[k]$. All these latter items can
be encoded on $O(\log n)$ bits.

  * •

The auxiliary message associated to node $x$ (whenever $G[x]$ is connected)
corresponds to the certification of a spanning tree of $G[x]$, which can be
encoded in $O(\log n)$ bits (see [46]).

  * •

For the service messages, note that vertex $v$ participates in at most two
service trees associated to $x$: the one of $x$ (whenever $G[x]$ is
disconnected), plus the one of the sibling $y$ of $x$ (when $G[y]$ is
disconnected). Again, each of these trees can be certified using $O(\log n)$
bits.

Therefore, the total size of the certificates is $O(d\cdot\log n)$ bits, where
$d$ is the depth of the NLC+ decomposition tree $T$. Our final certificate
size depends then on how much we can bound the depth $d$ of $T$. Courcelle and
Kanté [15] show that there always exists an NLC decomposition tree of
logarithmic depth, but it comes with a price: the width of the small depth
decomposition can be exponentially larger than the width of the original
decomposition. Specifically, Courcelle and Kanté have shown that every
$n$-node graph of NLC-width $k$ admits an NLC-decomposition of width $k\cdot
2^{k+1}$ such that the corresponding decomposition tree $T$ has depth
$\mathcal{O}(\log n)$. Fortunately, our construction of NLC+ decomposition
trees does not increase the depth of a given NLC-decomposition tree. In other
words, we can use the result of Courcelle and Kanté to also show that NLC+
decomposition trees have logarithmic depth. Overall, we conclude that the
certificate size is $O(\log^{2}n)$ bits.

#### Remark.

Our asymptotic bound on the size of the certificates hides a large dependency
on the clique-width $k$ of the input graph. For certifying the NLC+
decomposition only, the constant hidden in the big-O notation is single-
exponential in $k$, given that the width of the NLC+ decomposition tree with
logarithmic depth grows to $k\cdot 2^{k+1}$. However, for certifying an
$\mathrm{MSO}_{1}$ property, the dependency on $k$ can be much larger, as it
depends on the number of homomorphism classes. It is known that, for
$\mathrm{MSO}_{1}$ properties, the number of homomorphism classes is at most a
tower of exponentials in $k$, where the height of the tower depends on the
number of quantifiers in the $\mathrm{MSO}_{1}$ formula. Moreover, this non-
elementary dependency on $k$ can not be improved significantly [39]. This
exponential or even super-exponential dependency on the clique-width $k$ is
however inherent to the theory of algorithms for graphs of bounded clique-
width. The same type of phenomenon occurs when dealing with graphs of bounded
tree-width (see [39]), and the proof-labeling scheme in [35] is actually
subject to the same type of dependencies in the bound $k$. On the other hand,
the certificate size of our proof-labeling scheme grows only
polylogarithmically with the size of the graphs.

##  4 Certifying Cographs

In this section we describe a PLS for the recognition of cographs, using
$O(\log n)$-bit certificates in $n$-node graphs. That is, this section is
entirely dedicated to proving Theorem 1.3. Our scheme uses two known technical
lemmas. The first lemma (Theorem 4 in [15]) states that every graph of NLC-
width $k$ admits an NLC-decomposition of _logarithmic_ depth, and width still
bounded by a function of $k$.

######  Lemma 4.1 (Courcelle and Kanté [15]).

Every $n$-node graph of NLC-width $k$ admits an NLC-decomposition of width
$k\cdot 2^{k+1}$ such that the corresponding decomposition tree $T$ has depth
$\mathcal{O}(\log n)$.

The second technical lemma used to establish Theorem 1.3 states that every
cograph has a spanning tree with very small diameter.

######  Lemma 4.2 (Montealegre, Ramírez-Romero, and Rapaport [47]).

Every cograph has a rooted spanning tree of depth 2 in which every node at
depth 1 in the tree has at most one child.

Our proof of Theorem 1.3 is structured as follows. First, we describe the
certificates assigned by the prover at each node. Next, we describe the
verification algorithm, and we prove that the scheme satisfies soundness and
completeness. Finally, we establish the desired upper bound on the size of the
certificates.

###  4.1 Certificate Assignment

Let $G=(V,E)$ be the considered graph, and let $u\in V$. The certificate
$c(u)$ is divided in two parts, respectively called _main message_ and
_auxiliary message_.

#### Main messages.

Lemma 4.1 states that there exists an NLC-decomposition of cographs, with
width 4, and such that the corresponding decomposition tree $T_{dec}$ has
depth $\mathcal{O}(\log n)$. These main messages are used to encode such an
NLC-decomposition tree $T_{dec}$. At every node $u$, the main message contains
the following data:

  * •

The identifier $\mathsf{id}(u)$, and an integer $\textsf{deg}(u)$ representing
the degree of $u$ in $G$.

  * •

A sequence $\textsf{path}(u)=(x_{1}(u),\dots,x_{d}(u))$ of values,
representing a path in $T_{dec}$ from the root of $T_{dec}$ to the leaf of
$T_{dec}$ where $u$ is created thanks to $\mathsf{newVertex}$. Here $d=d(u)$
represents the length of $\textsf{path}(u)$. For each $i\in\\{1,\dots,d\\}$,
the value $x_{i}(u)$ is a list of all the operations (type of join, potential
recoloring, etc.) performed at the $i$th node of the path, starting from the
root. For simplicity, we also refer to $x_{i}(u)$ as this $i$th node.

  * •

A sequence
$\textsf{links}(u)=(\ell_{1}(u),\dots,\ell_{d}(u))\in\\{0,1\\}^{d}$,
representing the sequence of edges that are followed to reach the $i$th node
$x_{i}(u)$ of the path $\textsf{path}(u)$ from the root $x_{1}(u)$. More
precisely, $\ell_{1}(u)=0$ and for each $i\in\\{2,\dots,d\\}$, $\ell_{i}(u)=0$
if $x_{i}(u)$ is the left child of $x_{i-1}(u)$, and $\ell_{i}(u)=1$
otherwise.

Note that since the prover provides $u$ with the whole list of
$\mathcal{O}(\log n)$ operations from the node of $T_{dec}$ where $u$ is
created to the root of $T_{dec}$, there is not enough space for assigning a
unique identifier to each nodes of the tree $T_{dec}$, as this would results
in consuming $O(\log^{2}n)$ bits in $\textsf{path}(u)$. Instead, a node of the
decomposition will be uniquely identified by the sequence $\textsf{links}(u)$
and by the content of the values stored in $\textsf{path}(u)$. We shall show
that this is sufficient.

#### Auxiliary messages.

Lemma 4.2 states that there is a rooted spanning tree $T_{span}$ of $G$, with
depth 2, and in which every node at depth 1 in the tree has at most one child.
The auxiliary messages are used to gather all the main messages on a single
node $r\in V$. Each node receives the information required to certify a
depth-2 spanning tree $T_{span}$ rooted at $r$. In addition, every node at
depth 1 in $T_{span}$ receives the main messages of its child in $T_{span}$.
Formally, the auxiliary message provided by the prover to a node $u$ contains
the following data:

  * •

The identifier $\rho(u)=\mathsf{id}(r)$ of the root $r$ of $T_{span}$.

  * •

An integer $\textsf{depth}(u)\in\\{0,1,2\\}$ representing the depth of $u$ in
$T_{span}$.

  * •

If $\textsf{depth}(u)=2$, a node identifier $\textsf{parent}(u)$ representing
the parent of $u$ in $T_{span}$.

  * •

If $\textsf{depth}(u)=1$, a variable $\textsf{child}(u)$, either representing
the node identifier of the child of $u$ in $T_{span}$, or $\bot$ if $u$ has no
children in $T_{span}$.

  * •

If $\textsf{depth}(u)=1$, and $\textsf{child}(u)\neq\bot$, then $u$ receives a
variable $\textsf{M}(u)$ representing the main message of $\textsf{child}(u)$.

###  4.2 Verification Scheme

We now describe the verification algorithm performed by every vertex $u$ of
the actual graph. First, $u$ verifies that $\textsf{deg}(u)$ corresponds to
its degree, and that all the values stored in
$\textsf{path}(u)=(x_{1}(u),\dots,x_{d}(u))$ effectively correspond to a list
of operations of an NLC-decomposition of width 4. In particular, $u$ checks
that $x_{d}(u)$ contains the unique operation $\textsf{NewVertex}_{i}$ for
some $i\in\\{1,\dots,4\\}$. Concretely, after having shared its certificate
with its neighbors, $u$ checks the following conditions, for each $v\in N(u)$:

  1. 1.

$\textsf{links}(u)$ and $\textsf{links}(v)$ have a common prefix. More
precisely, $u$ checks that there exists an index $i\in\\{1,\dots,d(u)\\}$ such
that $\ell_{j}(u)=\ell_{j}(v)$ for every $j\leq i$. Over all such indices we
denote by $i^{*}$ the maximum one.

  2. 2.

$\textsf{path}(u)$ and
$\textsf{path}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}{v}})$
share the same the first $i^{*}$ coordinates. More precisely, $u$ verifies
that $x_{j}(u)=x_{j}(v)$ for every $j\leq i^{*}$.

  3. 3.

Let $\mathsf{currentcolor}(u,i^{*})$ be the color of $u$ resulting from the
$\mathsf{NewVertex}$ operation specified in $x_{d(u)}$, and all the
$\mathsf{recolor}$ operations in all the nodes in $\textsf{path}(u)$ up to
$x_{i^{*}}(u)$, but not including the $\mathsf{recolor}$ operations in
$x_{i^{*}}$). The value $\mathsf{currentcolor}(v,i^{*})$ is defined the same
for node $v$. The following holds:

     * •

If $\ell_{i^{*}}(u)=0$ then $u$ checks that the join operation $\Join_{S}$ in
$x_{i^{*}}$ satisfies

$(\mathsf{currentcolor}(u,i^{*}),\mathsf{currentcolor}(v,i^{*}))\in S.$

     * •

If $\ell_{i^{*}}(u)\neq 0$ then $u$ checks that the join operation $\Join_{S}$
in $x_{i^{*}}$ satisfies

$(\mathsf{currentcolor}(v,i^{*}),\mathsf{currentcolor}(u,i^{*}))\in S.$

  4. 4.

Nodes $u$ and $v$ agree on the root of $T_{span}$, i.e., $\rho(u)=\rho(v)$.

  5. 5.

If $\textsf{depth}(u)=2$ then $u$ checks that there exists $v\in N(u)$ such
that ${\textsf{parent}(u)=v}$.

  6. 6.

If $\textsf{depth}(u)=1$, then $u$ checks that

     * •

$\rho(u)\in\\{\mathsf{id}(v):v\in N(u)\\}$;

     * •

If $\textsf{child}(u)\neq\bot$ then (1) $\textsf{child}(u)\in N(u)$, (2)
$\textsf{depth}(\textsf{child}(u))=2$, and (3) every $v\in
N(u)\smallsetminus\\{\textsf{child}(u)\\}$ with $\textsf{depth}(v)=2$
satisfies that $\textsf{parent}(v)\neq u$;

     * •

If $\textsf{child}(u)\neq\bot$ then $\textsf{M}(u)$ equals the main message of
$\textsf{child}(u)$.

  7. 7.

If $\mathsf{id}(u)=\rho(u)$ then, $u$ checks that the following holds333If all
previous conditions are satisfied, then the root $r=u$ obtains from its
neighbors all the main messages of the nodes in $G$:

     * •

The information in $\\{\textsf{path}(v):v\in V\\}$ and
$\\{\textsf{links}(v):v\in V\\}$ is consistent, that is, for every
$v_{1},v_{2}\in V$, and for every $i\in\mathbb{N}$,

$\Big{(}\forall j\leq
i,\;\ell_{j}(v_{1})=\ell_{j}(v_{2})\Big{)}\Longrightarrow\Big{(}\forall j\leq
i,\;x_{j}(v_{1})=x_{j}(v_{2})\Big{)}.$

Observe that if this condition is satisfied, then necessarily
$\\{\textsf{path}(v):v\in V\\}$ and $\\{\textsf{links}(v):v\in V\\}$ describe
a unique NLC-decomposition tree. Let us denote this tree by $T(u)$, and let
$G^{*}$ be the graph corresponding to the realization of the NLC-decomposition
tree given by $T(u)$. Note that $u$ can obtain all the vertices and edges of
$G^{*}$ from $T(u)$.

     * •

Node $u$ checks that $G^{*}$ is a cograph.

     * •

Finally $u$ checks that, for every node $v\in V$, the number of neighbors of
$v$ in $G^{*}$ equals $\textsf{deg}(v)$.

###  4.3 Completeness and Soundness

The completeness of our scheme directly follows from the fact that, thanks to
Lemma 4.1, every cograph admits a NLC-decomposition of width $4$, and, by
Lemma 4.2, one can define the main and auxiliary messages in a way that every
node accepts.

For the soundness, let us assume that all nodes of a graph $G$ accept in the
verification protocol. From condition 4, we have that all nodes agree on the
same root $r$ of $T_{span}$. From the first item of condition 6, all nodes of
depth 1 in $T_{span}$ are adjacent to $r$. From condition 5, and from the
second item of condition 6, we have that every node at depth $2$ is adjacent
to a node of depth 1. Finally, the third item of condition 6 guarantees that
the root $r$ receives all the main messages of the nodes $G$. Then, by the
first item of condition 7, we have that $r$ can recover all the vertices and
all the edges of $G^{*}$, and by the second item of condition 7, we have that
$G^{*}$ is a cograph. From conditions 1-3, we get that every edge
$\\{u,v\\}\in E(G)$ is necessarily included in $G^{*}$, meaning that $G$ is a
spanning subgraph of $G^{*}$. Finally, the third item of condition 7
guarantees that the number of edges in $G^{*}$ equals the number of edges in
$G$, and thus $G=G^{*}$. It follows that $G$ is indeed a cograph.

###  4.4 Certificate Size

By Lemma 4.1, every cograph admits an NLC-decomposition tree of depth
$\mathcal{O}(\log n)$. Therefore, in the certificate assigned to node $u$, we
have $d(u)=\mathcal{O}(\log n)$. Each value $x_{i}(u)$ can be encoded using
$O(1)$ bits as every operation involves a constant number of colors. It
follows that $\textsf{path}(u)$ can be encoded on $O(\log n)$ bits. The
variable $\textsf{links}(u)$ can be encoded with $\mathcal{O}(\log n)$ bits as
well, by construction. Every node identifier, and every node degree can be
encoded with $\mathcal{O}(\log n)$ bits. Therefore, all the main messages can
be encoded with $\mathcal{O}(\log n)$ bits. This also implies that the
auxiliary messages can be encoded with $\mathcal{O}(\log n)$ bits. We conclude
that, in total, our PLS uses certificates on $\mathcal{O}(\log n)$ bits, which
completes the proof of Theorem 1.3.

##  5 $\mathrm{MSO}_{1}$ Properties on Labeled Graphs of Bounded Clique-Width

This section is dedicated to the proof of Theorem 1.1. To avoid overloading
the notation, a labeled graph is simply denoted by $G=(V,E,\ell)$ where $\ell$
is the vertex-labeling function. We will often simply speak of "graphs"
instead of "vertex-labeled graphs". Before describing the certificates and the
verification protocol, let us first establish some preliminary technical
results.

###  5.1 Regularity of $\mathrm{MSO}_{1}$ predicates

In their seminal work [16], Courcelle, Makowsky and Rotics proved that any
$\mathrm{MSO}_{1}$ predicate $\Pi$ can be decided in linear time on graphs of
bounded clique-width, and hence on graphs of bounded NLC-width, whenever a
decomposition tree is part of the input. The running time of the algorithm is
linear in the number $n$ of vertices of the input graph, but the constant
hidden in the big-O notation depends on $k$, on the number of labels and on
the $\mathrm{MSO}_{1}$ formula encoding the predicate $\Pi$. The algorithm in
[16] is described using tools from automata theory. For our purpose it is more
convenient to see it as a dynamic programming algorithm over the decomposition
tree of the input graph. Let us formalize this dynamic programming approach
following the vocabulary and notations that Borie, Parker and Tovey [5]. Note
that [5] is alternative proof of Courcelle’s theorem on bounded treewidth
graphs, specific to a graph grammar defining treewidth; here we simply adapt
the definitions to NLC-width and the NLC grammar.

Let $\mathrm{NLC}_{k}$ denote the class of labeled graphs of graphs of
$\mathrm{NLC}$-width at most $k$ and let $\Pi$ be a graph property, assigning
to each graph $G$ a boolean value $\Pi(G)$. Intuitively, two graphs
$G_{1},G_{2}\in\mathrm{NLC}_{k}$ can be considered as equivalent w.r.t. $\Pi$
if, whenever a graph $G^{\prime}_{1}\in\mathrm{NLC}_{k}$ is obtained by a
sequence of NLC operations performed on $G_{1}$, then the graph
$G^{\prime}_{2}$ obtained from the same sequence of operations but performed
on $G_{2}$ has the same behaviour w.r.t. property $\Pi$ as $G^{\prime}_{1}$.
Informally again, a property $\Pi$ is said to be _NLC-regular_ if the number
of such equivalence classes, that will be called _homomorphism classes_ as in
[5], is upper bounded by a constant: the number of such classes does not
depend on the size of the graphs, but only on parameter $k$ and the property
$\Pi$ itself. As we shall see, if $\Pi$ is an $\mathrm{MSO}_{1}$-definable
boolean predicate, then it is also NLC-regular, and this is the crux for
deciding $\mathrm{MSO}_{1}$ properties for graphs of bounded NLC-width.

######  Definition 5.1 (NLC-regular property).

A graph property $\Pi$ is called _NLC-regular_ if, for any value $k$, we can
associate a finite set $\mathcal{C}$ of _homomorphism classes_ and a
_homomorphism function_ $h$, assigning to each graph $G\in\mathrm{NLC}_{k}$ a
class $h(G)\in\mathcal{C}$ such that:

  1. 1.

If $h(G_{1})=h(G_{2})$ then $\Pi(G_{1})=\Pi(G_{2})$.

  2. 2.

For each operation $\Join_{S}$ there exists a function
$\odot_{\Join_{S}}:\mathcal{C}\times\mathcal{C}\rightarrow\mathcal{C}$ such
that, for any two graphs $G_{1}$ and $G_{2}$ in $\mathrm{NLC}_{k}$,

$h(\Join_{S}(G_{1},G_{2}))=\odot_{\Join_{S}}(h(G_{1}),h(G_{2})),$

and for each operation $\mathsf{recolor}_{R}$ of there is a function
$\odot_{\mathsf{recolor}_{R}}:\mathcal{C}\rightarrow\mathcal{C}$ such that,
for any graph $G\in\mathrm{NLC}_{k}$,

$h(\mathsf{recolor}_{R}(G))=\odot_{\mathsf{recolor}_{R}}(h(G)).$

Observe that NLC-regularity of property $\Pi$ not only implies that the set of
homomorphism classes does not depend on the size of the graph, but also that,
given an NLC-decomposition of some graph $G\in NLC_{k}$, the class $h(G)$ can
be computed by dynamic programming from the leaves to the root. At each node
$x$ of the decomposition tree $T$, the class of $G[x]$, the subgraph of $G$
corresponding to the subtree $T[x]$ rooted at $x$ only depends on the classes
at the children nodes, and the operations at node $x$. The first condition of
Definition 5.1 partitions $\mathcal{C}$ into a set of accepting classes, i.e.,
classes $c\in\mathcal{C}$ such that $h(G)=c\rightarrow\Pi(G)$, and rejecting
classes, corresponding to graphs that do not satisfy the property.

We illustrate Definition 5.1 on the predicate $\Pi$ corresponding to
non-3-colorability, in order to prove that this predicate is NLC-regular, and
how this regularity allows to decide the non-3-colorability on graphs in
$\mathrm{NLC}_{k}$. It is convenient to view a proper 3-coloring of a graph
$G$ as a partition of its vertex $V$ set into three independent sets
$(X_{1},X_{2},X_{3})$. For such a partition $(X_{1},X_{2},X_{3})$ of a graph
$G\in\mathrm{NLC}_{k}$, $i\in[k]$, we encode this partition as a triple
$(b_{1},b_{2},b_{3})$ of boolean vectors of length $k$. Vector $b_{j}$ encodes
the intersection of set $X_{j}$ with the $k$ possible colours of the NLC
decomposition of $G$. That is, $b_{j}[i]=1$ if set $X_{j}$ contains some
vertex coloured $i\in[k]$, otherwise $b_{j}[i]=0$. Eventually, the
homomorphism class $h(G)$ of graph $G$ is the set of all triples
$(b_{1},b_{2},b_{3})\in\\{0,1\\}^{k}\times\\{0,1\\}^{k}\times\\{0,1\\}^{k}$,
such that there is some partition of the vertices $G$ into three independent
sets $(X_{1},X_{2},X_{3})$ and $(b_{1},b_{2},b_{3})$ is the encoding of this
partition as described above. In particular, observe that $G$ is
non-3-colourable iff $h(G)=\emptyset$, so $\emptyset$ is the only accepting
class.

It is a matter of exercise to see that the number of homomorphism classes is
upper bounded by a function on $k$, and even to understand how to construct
the class of graphs with a single vertex, and how functions
$\odot_{\Join_{S}}$ and $\odot_{\mathsf{recolor}_{R}}$ of Definition 5.1 can
be obtained for all $\Join_{S}$ and $\mathsf{recolor}_{R}$ operations. For the
sake of completeness, we give the construction in full details.

If $G$ consists of a single vertex $x$ coloured $i$, then the possible
partitions of $G$ into three independent sets are
$(\\{x\\},\emptyset,\emptyset)$, $(\emptyset,\\{x\\},\emptyset)$ and
$(\emptyset,\emptyset,\\{x\\})$. Thus $h(G)$ is formed by three triples:
$(u_{i,k},0^{k},0^{k})$, $(0^{k},u_{i,k},0^{k})$, and $(0^{k},0^{k},u_{i,k})$,
where $0^{k}$ denotes the boolean vector of $k$ zeros, and $u_{i,k}$ is formed
of $k-1$ zeros, and a one at position $i$.

Consider now two graphs $G_{1},G_{2}\in\mathrm{NLC}_{k}$ and let
$G=G_{1}\Join_{S}G_{2}$ for some $S\in[k]\times[k]$. We describe function
$\odot_{\Join_{S}}$, constructing $h(G)$ from $h(G_{1})$ and $h(G_{2})$. Note
that for each 3-partition $(X_{1},X_{2},X_{3})$ of $G$ into three independent
sets, the intersection of $X_{1},X_{2},X_{3}$ with the vertex set of $G_{1}$
(resp. $G_{2}$) induces a 3-partition $(Y_{1},Y_{2},Y_{3})$ (resp.
$(Z_{1},Z_{2},Z_{3})$) into independent sets. Conversely, given partitions
$(Y_{1},Y_{2},Y_{3})$ of $G_{1}$ and $(Z_{1},Z_{2},Z_{3})$ of $G_{2}$ into
independent sets, $(X_{1}=Y_{1}\cup Z_{1},X_{2}=Y_{2}\cup
Z_{2},X_{3}=Y_{3}\cup Z_{3})$ forms a partition into independent sets of $G$
unless operation $\Join_{S}$ creates an edge between $Y_{1}$ and $Z_{1}$, or
$Y_{2}$ and $Z_{2}$, or $Y_{3}$ and $Z_{3}$. Therefore, the homomorphism class
of $h(G)$ can be constructed as follows. For each triple of boolean vectors
$(y_{1},y_{2},y_{3})\in h(G_{1})$ and $(z_{1},z_{2},z_{3})\in h(G_{2})$
(corresponding to partitions $(Y_{1},Y_{2},Y_{3})$ of $G_{1}$ and
$(Z_{1},Z_{2},Z_{3})$ of $G_{2}$ respectively), we add to $h(G)$ the triple
$(y_{1}\lor z_{1},y_{2}\lor z_{2},y_{3}\lor z_{3})$ (where $x\lor y$ denotes
the bit-wise OR operation), unless there is some pair $(p,q)\in S$ such that
$y_{1}[p]\land z_{1}[q]$ or $y_{2}[p]\land z_{2}[q]$ or $y_{3}[p]\land
z_{2}[q]$ is true. The latter condition verifies that operation $\Join_{S}$
does not create an edge in $X_{1}$ or in $X_{2}$ or in $X_{3}$ in graph $G$.

Eventually, let $G^{\prime}=\mathsf{recolor}_{R}(G)$ for some
$G\in\mathrm{NLC}_{k}$, and $R:[k]\to[k]$. We describe function
$\odot_{recolor_{R}}$. Note that $(X_{1},X_{2},X_{3})$ is a partition of
$G^{\prime}$ into independent sets iff it is also a partition of $G$ into
independent sets. Therefore we only need to describe how the recoloring $R$
changes the encoding of $(X_{1},X_{2},X_{3})$ from $G$ to $G^{\prime}$. For
each $(b_{1},b_{2},b_{3})\in h(G)$, we add
$(\mathsf{recolor}_{R}(b_{1}),\mathsf{recolor}_{R}(b_{2}),\mathsf{recolor}_{R}(b_{3}))$
to $h(G^{\prime})$, where $b^{\prime}=\mathsf{recolor}_{R}(b)$ is defined as
follows on boolean vector $b\in\\{0,1\\}^{k}$: for each $q\in[k]$ we set
$b^{\prime}[q]=1$ if and only if there is some $p\in[k]$ such that $R(p)=q$
and $b[p]=1$. In full words, $b^{\prime}[q]$ is set to true iff the set $X$
encoded by $b$ contains some vertex colored $p$ in $G$, recolored $q$ in
$G^{\prime}$.

This does not only prove that property $\Pi(G)$: “$G$ is non-3-colourable” is
NLC-regular, but provides all ingredients to decide the property for graphs
$G\in\mathrm{NLC}_{k}$, when a decomposition tree is part of the input. Indeed
we need to compute, at each node $x$ of the decomposition tree, the
homomorphism class of $G[x]$, the induced subgraph corresponding to thee
$T[x]$. At the leaves, graph $G[x]$ is formed by a unique vertex, and as
described above the homomorphism class is defined by the colour of that
vertex. Then, for each node of the tree, the homomorphism class can be updated
from the classes of its children using functions $\odot_{\Join_{S}}$ and
$\odot_{\mathsf{recolor}_{R}}$. Finally, at the root, we accept if and only if
the homomorphism class of the whole graph is the empty set. The running time
is linear in the number of nodes of the tree, so it is $O(n)$ — of course it
also depends (exponentially) in parameter $k$.

The result of Courcelle, Makowsky and Rotics [16], although expressed in terms
of automata theory (see also Theorem 4.2 in [41] for an alternative proof),
can be restated as follows:

######  Proposition 5.2.

Any graph property $\Pi$ expressible by an $\mathrm{MSO}_{1}$ predicate is
NLC-regular. Moreover, given the corresponding $\mathrm{MSO}_{1}$ formula and
parameter $k$, one can explicitely compute the set of homomorphism classes
$\mathcal{C}$, as well as functions $\odot_{\Join_{S}}$ and
$\odot_{\mathsf{recolor}_{R}}$ for any $S\in[k]\times[k]$ and any
$R:[k]\to[k]$, and the homomorphism class of the graph formed by a unique
vertex coloured $i$, for any $i\in[k]$.

Therefore all $\mathrm{MSO}_{1}$ properties can be decided in $O(n)$ time on
graphs of bounded NLC-width, if a decomposition tree is part of the input;
again, the big-Oh notation hides a dependency in $k$ and the
$\mathrm{MSO}_{1}$ formula. We also use these ingredients for our proof
labeling scheme.

###  5.2 General description $\mathrm{NLC}_{+}$-Width

Before getting into the full details of our PLS, let us give a general
description of the certification algorithm for an $\mathrm{MSO}_{1}$ property
$\Pi$ on graphs of $\mathrm{NLC}$-width at most $k$. As in the case of
cographs (cf. Section 4), given a graph $G\in\mathrm{NLC}_{k}$, we use an NLC-
decomposition tree $T_{dec}$ of depth $\mathcal{O}(\log n)$ and of width
$k^{\prime}\leq k\cdot 2^{k+1}$, provided by Lemma 4.1. For any vertex $u$ of
$G$, recall that $\textsf{path}(u)=(x_{1}(u),\dots,x_{d}(u))$ denotes the path
in $T_{dec}$ from the root $x_{1}(u)$ to the leaf $x_{d}(u)$ corresponding to
the node where vertex $u$ is created (again, we abuse notation by identifying
the nodes of the tree with the values describing the operations performed in
those nodes).

As in Section 4, the so-called main message of $u$ contains its identifier
$\mathsf{id}(u)$, the sequence $\textsf{path}(u)$, as well as the sequence
$\textsf{links}(u)=(\ell_{1}(u),\dots,\ell_{d}(u))$, where, for $i\geq 2$,
$\ell_{i}(u)\in\\{0,1\\}$ indicates whether $x_{i}(u)$ is the left or right
child of $x_{i-1}(u)$ in $T_{dec}$, when $x_{i-1}(u)$ is of type $\Join$ . For
certifying a predicate $\Pi$, let $h_{i}(u)$ denote the homomorphism class at
node $x_{i}(u)$ w.r.t. ${\Pi}$ restricted to graphs of $\mathrm{NLC}$-width at
most $k^{\prime}$. That is, for $i=1,\dots,d$,

$h_{i}(u)=h(G[x_{i}(u)]).$

The sequence

$\textsf{h}(u)=(h_{1}(u),\dots,h_{d}(u))$ (1)

is added to the main message of $u$. Note that, since $d\in\mathcal{O}(\log
n)$, each sequence is of logarithmic length. Moreover, for every
$i\in\\{1,\dots,d\\}$, $(x_{i}(u),\ell_{i}(u),h_{i}(u))$ can be encoded on
$O(1)$ bits. Therefore the total size of the main message is $\mathcal{O}(\log
n)$.

Unlike the case of cographs, the diameter of a graph of bounded NLC-width is
not necessarily bounded by a constant (i.e., Lemma 4.2 does not hold in
general for such graphs). It follows that the main messages cannot be gathered
in a single vertex as in cographs. To overcome this difficulty, the prover
places additional information in the main message of $u$. First, for each
color $j\in[k^{\prime}]$ and $i\in[d(u)]$ let $\textsf{color}_{i}^{j}(u)$
denote the number of vertices colored $j$ in $G[x_{i}(u)]$ after the
recoloring operations performed at node $x_{i}(u)$. The sequence

$\textsf{color}^{j}(u)=(\textsf{color}^{j}_{1}(u),\dots,\textsf{color}^{j}_{d}(u))$

is also added to the main message of $u$, for all $j\in[k^{\prime}]$.

Finally, we need to guarantee that, for each node $x$, every vertex that
belongs to $G[x]$ receives the same information about the operations performed
in $x$, as well as the number of vertices colored with each one of the colors.
This verification is especially hairy for nodes $x$ where $G[x]$ is
disconnected, where this consistency verification is done with the help of
vertices outside $G[x]$. In order to cope with this issue, let us slightly
modify the notion of NLC-decomposition tree by allowing nodes $\parallel$
(i.e., nodes of $T_{dec}$ at which a disjoint union operation is performed) to
be of arbitrarily large arity (in the original decomposition $T_{dec}$, the
arity of an internal node is 2). Moreover all disconnected graphs $G[x]$ will
correspond to parallel nodes $x$, and for the parent $y$ of such a node,
$G[y]$ has to be connected. Such a decomposition tree will be called an
$\mathrm{NLC}_{+}$-decomposition tree.

######  Definition 5.3.

Let $k\geq 1$. A rooted tree $T$ is an $\mathrm{NLC}_{+}$-decomposition tree
of width $k$ if the following conditions holds:

  1. 1.

Every leaf of $T$ is labeled $\mathsf{newVertex}_{i}$, for some $i\in[k]$;

  2. 2.

Every internal node of $T$ is labelled $\Join$ or $\parallel$;

  3. 3.

Every node labeled $\Join$ has exactly $2$ children, and such a node is
associated to a set $S\in[k]\times[k]$ and to a function
$\mathsf{recolor}_{R}$ where $R:[k]\to[k]$;

  4. 4.

Every node labeled $\parallel$ has at least 2 children, and, for every node
labeled $\parallel$ distinct from the root, its parent is labeled $\Join$;

  5. 5.

Every graph defined by the subtree rooted in a $\Join$ node is connected.

In Definition 5.3, the nodes labeled $\Join$ represent the join and recoloring
operations performed as in $\mathrm{NLC}$-decomposition trees, i.e., first
join, and then recolor. Similarly, the nodes $\parallel$ represent the
disjoint union of the graphs defined by their children. However, a crucial
difference compare to $\mathrm{NLC}$-decomposition is that instead of
systematically involving two vertex-disjoint graphs, the
$\mathrm{NLC}_{+}$-decomposition allows an arbitrary number of vertex-disjoint
graphs. Another crucial difference with $\mathrm{NLC}$-decomposition is
Condition 5, which imposes connectivity of the subgraph hanging at every
$\Join$ node.

To cope with the notion of $\mathrm{NLC}_{+}$-decomposition, we merely extend
the functions $\odot$ given in Definition 5.1 by introducing the operator
$\odot_{\parallel}$ with arbitrary arity. Specifically, let $G$ be a graph
obtained from the disjoint union of a set of $\mathrm{NLC}_{+}$ graphs
$\\{G_{1},\dots,G_{p}\\}$, in any order, with $p\geq 2$. We define

$\displaystyle
h(G)=\odot_{\parallel}(h(G_{1}),\dots,h(G_{p}))=\odot_{\parallel}\Bigg{(}h(G_{1}),\odot_{\parallel}\bigg{(}h(G_{2}),\odot_{\parallel}\Big{(}\dots,\odot_{\parallel}\big{(}h(G_{p-1}),h(G_{p})\big{)}\Big{)}\bigg{)}\Bigg{)}.$

We say that a graph has $\mathrm{NLC}_{+}$ width $k$ if it can be constructed
according to an $\mathrm{NLC}_{+}$ decomposition tree of width $k$. For any
node $x$ of an $\mathrm{NLC}_{+}$ decomposition tree $T$, we also define
$T[x]$ and $G[x]$ in the same way as for NLC-decompositions trees. We now show
that allowing large arity and imposing connectivity does not ruin the good
properties of $\mathrm{NLC}$-decomposition.

######  Lemma 5.4.

For every $k\geq 1$, all $n$-node connected graphs of $\mathrm{NLC}$-width $k$
have $\mathrm{NLC}_{+}$-decomposition trees of width at most $k\cdot 2^{k+1}$,
and depth $\mathcal{O}(\log n)$.

The proof of the lemma is based on the following statement.

######  Claim 1.

Let $G=(V,E)$ be a connected graph of $\mathrm{NLC}$-width $w\geq 1$. Let $T$
be an $\mathrm{NLC}$-decomposition tree of $G$ of width $w$ and depth $d$.
Then $G$ admits an $\mathrm{NLC}_{+}$-decomposition tree $T_{+}$ of width $w$
and depth at most $2d$. Moreover, the color of each vertex of $G$ at the root
of $T_{+}$ is the same as the color of this vertex at the root of $T$.

######  Proof 5.5.

The proof is by induction on $d$. The claim is straightforward for $d=1$ as
$T$ is also an $\mathrm{NLC}_{+}$-decomposition tree in this case. Let $d>1$,
and let us assume by induction hypothesis that the claim holds for all
connected graphs having an NLC-decomposition tree of depth smaller than $d$.
Let $x$ be a node of tree $T$ such that $G[x]$ (corresponding to the
decomposition subtree $T[x]$) is connected, but, for at least one of the
children $z_{1},z_{2}$ of $x$, $G[z_{i}]$ is disconnected. Note that if no
such $x$ exists, then $T$ is an $\mathrm{NLC}_{+}$-decomposition tree, the
connectivity condition being satisfied at each node. We choose $x$ closest to
the root, in the sense that no other node from $x$ to the root has this
property. (Of course, there might be several such nodes $x$, none of them
being ancestor of the other in the tree.) For each $i\in\\{1,2\\}$, let
$D_{i}^{1},D_{i}^{2},\dots,D_{i}^{p_{i}}$ be the connected components of
$G[z_{i}]$. Observe that each $D_{i}^{j}$, $1\leq j\leq p_{i}$ has an
$\mathrm{NLC}$-decomposition tree $T_{i}^{j}$ of depth at most the depth of
$T[z_{i}]$, obtained by trimming from $T[z_{i}]$ all leaves that do not
correspond to vertices of $D_{i}^{j}$. By induction hypothesis, graph
$D_{i}^{j}$ has an $\mathrm{NLC}_{+}$-decomposition tree $T_{+}(i,j)$ of width
$w$ and of depth at most twice the depth of $T[z_{i}]$.

We obtain the tree $T_{+}$ as follows. For node $x$, if $G[z_{i}]$ has a
unique component $D_{i}^{1}$, we replace the subtree $T[z_{1}]$ by
$T_{+}(i,1)$. If $G[z_{i}]$ has several components
$D_{i}^{1},D_{i}^{2},\dots,D_{i}^{p_{i}}$, then we replace $T[z_{i}]$ by a
subtree of root $\parallel$, with $p_{i}$ children, the $j$th child being the
root of $T_{+}(i,j)$. Observe that in this way, the label of $x$ remains
unchanged, and $T_{+}[x]$ is an $\mathrm{NLC}_{+}$-decomposition tree of
$G[x]$. By performing in parallel these operations on all such nodes $x$, we
obtain an $\mathrm{NLC}_{+}$-decomposition tree of $G$. The width of the
decomposition has not changed. Moreover the depth has been increased by a
factor 2 at most. Indeed, for each node $x$, we replaced $T[z_{i}]$ by
subtrees of depth at most twice the original depth, and the node $x$ itself
might have caused the addition of a new layer of children labelled
$\parallel$. Therefore, the depth of $T_{+}[x]$ is at most
$2\cdot\max\\{\mbox{depth}(T[z_{1}]),\mbox{depth}(T[z_{2}])\\}$+2, hence at
most twice the depth of $T[x]$. Altogether, the depth of $T_{+}$ is at most
twice the depth of $T$. This concludes the induction step, and the proof of
Claim 1.

######  Proof 5.6 (Proof of Lemma 5.4.).

Thanks to Lemma 4.1, every $n$-node connected graph $G$ of NLC-width $k$
admits an NLC-decomposition tree of width $k\cdot 2^{k+1}$ and depth $O(\log
n)$. By Claim 1, we obtain an $\mathrm{NLC}_{+}$-decomposition tree of the
same width $k\cdot 2^{k+1}$, and still of logarithmic depth.

Let $T$ be an $\mathrm{NLC}_{+}$ -decomposition. Recall that, for every node
$x$ of $T$, we denote by $h(x)$ the homomorphism class of $G[x]$ w.r.t.
property ${\Pi}$. Moreover, we set

$\textsf{color}(x)=(\textsf{color}^{1}(x),\dots,\textsf{color}^{k^{\prime}}(x))$
(2)

where, for every $j\in\\{1,\dots,k^{\prime}\\}$, $\textsf{color}^{j}(x)$ is
the number of vertices colored $j$ at node $x$ after the recoloring
operations. Finally, we denote by $\textsf{exit}(x)$ the identifier of some
vertex that belongs to $G[x]$, called the exit vertex of $G[x]$. When $x$ is
of type $\parallel$ then $\textsf{exit}(x)$ is an arbitrary vertex in $G[x]$.
When $x$ is of type $\Join$, we have by Definition 5.3 that $G[x]$ is
connected. Let $z^{0}$ and $z^{1}$ be the left and right children of $x$,
respectively. Then, we choose $\textsf{exit}(x)$ as an arbitrary node
belonging to $G[z^{0}]$ that is adjacent to some node in $G[z^{1}]$.

###  5.3 Certificate Assignment

As for cographs, the certificates are divided in several parts, called _main
messages_ and _auxiliary messages_. We add a third part, called _service
messages_. Let us fix some $\mathrm{NLC}_{+}$-decomposition of width $k$ and
depth $\mathcal{O}(\log n)$ of the input graph $G$.

#### Main messages.

These messages are used to check the local correctness of the decomposition
tree. The main message of node $u\in V$ contains the following information.

  * •

The sequence $\textsf{path}(u)=(x_{1}(u),\dots,x_{d}(u))$ as defined in
Section 4 for certifying cographs.

  * •

The sequence
$\textsf{links}(u)=(\ell_{1}(u),\dots,\ell_{d}(u))\in\\{0,1,\bot\\}^{d}$,
representing the sequence of edges that are to be followed to reach $x_{d}(u)$
from $x_{1}(u)$, similarly to Section 4, but taking into account the presence
of nodes $\parallel$ with large arity. More precisely, $\ell_{1}(u)=\bot$, and
for every $i\geq 2$,

    * –

if $x_{i-1}(u)$ is of type $\parallel$ then $\ell_{i}(u)=\bot$;

    * –

if $x_{i-1}(u)$ is of type $\Join$ then $\ell_{i}(u)=0$ whenever $x_{i}(u)$ is
the left children of $x_{i}(u)$, and $\ell_{i}(u)=1$ otherwise.

  * •

The sequence $\textsf{h}(u)=(h_{1}(u),\dots,h_{d}(u))$ defined in Eq. (1).

  * •

The sequence
$\textsf{color}(u)=(\textsf{color}_{1}(u),\dots,\textsf{color}_{d}(u))$, such
that, for each $i\in\\{1,\dots,d\\}$, $\textsf{color}_{i}(u)$ is the sequence
$\textsf{color}(x_{i}(u))=(\textsf{color}^{1}_{i}(u),\dots,\textsf{color}^{k^{\prime}}_{i}(u))$
defined in Eq. (2).

  * •

The sequence
$\textsf{exit}(u)=(\textsf{exit}_{1}(u),\dots,\textsf{exit}_{d}(u))$, where,
for each $i\in\\{1,\dots,d\\}$, $\textsf{exit}_{i}(u)$ is the identifier of
node $\textsf{exit}(x_{i}(u))$.

In the following, for every $i\in[d]$, we denote
$\textsf{main}(u)=(\textsf{main}_{1}(u),\dots,\textsf{main}_{d}(u))$ where,
for each $i\in[d]$,

$\textsf{main}_{i}(u)=\Big{(}x_{i}(u),\;\ell_{i}(u),\;h_{i}(u),\;\textsf{color}_{i}(u),\;\textsf{exit}_{i}(u)\Big{)}.$

#### Auxiliary messages.

These messages are used to certify the connectivity of the subtrees rooted at
nodes $x$ of type $\Join$. Let $z^{0}$ and $z^{1}$ be the children of $x$ in
$T$. An _auxiliary tree associated to $x$_, denoted by $A(x)$, is a spanning
tree of $G[x]$. In the auxiliary messages, we certify the existence of $A(x)$
using the standard certification for trees [46]. That is, we give each node of
the tree the identifier of the root, the identifier of its parent, and its
distance to the root. We also use the auxiliary messages to certify that each
vertex created in $G[z^{0}]$ (respectively $G[z^{1}]$) received the same
information about $z^{0}$. Formally, every vertex $u$ receives the sequence

$\textsf{aux}(u)=(\textsf{aux}_{1}(u),\dots,\textsf{aux}_{d}(u))$

where, for each $i\in\\{1,\dots,d\\}$, $\textsf{aux}_{i}(u)=\bot$ whenever
$x_{i}(u)$ is of type $\parallel$, and, otherwise,

$\textsf{aux}_{i}(u)=(\textsf{root}_{i}(u),\textsf{parent}_{i}(u),\textsf{distance}_{i}(u),\textsf{childrenMain}_{i}(u))$

where

  * •

$\textsf{root}_{i}(u)$ is the identifier of the node
$\textsf{exit}(x_{i}(u))$;

  * •

$\textsf{parent}_{i}(u)$ is the identifier of the parent of $u$ in
$A(x_{i}(u))$, where $\textsf{parent}_{i}=\bot$ if $u=\textsf{root}_{i}(u)$;

  * •

$\textsf{distance}_{i}(u)$ is the distance between $u$ and
$\textsf{exit}(x_{i}(u))$ in $A(x_{i}(u))$;

  * •

$\textsf{childrenMain}^{j}_{i}(u)=(z^{j},h(z^{j}),\textsf{color}(z^{j}),\textsf{exit}(z^{j}))$
for $j\in\\{0,1\\}$.

#### Service messages.

These messages are used to check consistency in the subgraphs induced by the
subtrees rooted at nodes of type $\parallel$. In other words, they are used to
handle the case of nodes in the tree $T$ constructing non-connected subgraphs.
Before explaining these messages, let us define some additional data
structures.

Let $x$ be a node of type $\parallel$, and let $y$ denote the parent of $x$ in
$T$. Again by Lemma 5.4, for each child $z_{i}$, $1\leq i\leq p$, of $x$, the
graph $G[z_{i}]$ corresponds to a connected component of the graph $G[x]$
(which is disconnected by construction). A _service tree associated to_ $x$,
denoted by $S(x)$, is a Steiner tree in $G[y]$ with terminals
$\\{\textsf{exit}(z_{1}),\dots,\textsf{exit}(z_{p})\\}$, and root
$\textsf{exit}(x)$. The service messages are used to certify the existence of
$S(x)$ in a way similar to the auxiliary tree. We also use the service
messages to certify the consistency between $h(z_{1}),\dots,h(z_{p})$ and
$h(x)$. This latter certification is slightly more complicated than for
auxiliary trees because a parallel node may have an arbitrarily large number
of children, and one cannot store the identifiers, the classes and the colors
of all the terminals if one want to keep the certificate size small.

Let $u$ be a vertex in $S(x)$. The service message of $u$ contains the root of
$S(x)$, the parent of $u$, and the depth of $u$ in $S(x)$. Let us denote by
$S(x,u)$ the subtree of $S(x)$ rooted at $u$. Furthermore, let us call
$\textsf{inCharge}_{x}(u)$ the set of the indices of the terminals of $S(x)$
contained in $S(x,u)$. Formally,

$\textsf{inCharge}_{x}(u)=\\{i\in\\{1,\dots,p\\}\mid\textsf{exit}(z_{i})\in
S(x,u)\\}$

Now let us denote by $G[\textsf{inCharge}_{x}(u)]$ the subgraph of $G$ induced
by the disjoint union of all graphs $G[z_{i}]$,
$i\in\textsf{inCharge}_{x}(u)$. The service message of $u$ includes the
homomorphism class $h(G[\textsf{inCharge}_{x}(u)])$. The correctness of this
homomorphism class will be verified using only the homomorphism classes of the
children of $u$ in $S(x)$. Observe that $S(x,\textsf{exit}(x))=S(x)$, and

$h(G[\textsf{inCharge}_{x}(\textsf{exit}(x))]=h(x).$

Observe that node $u$ is necessarily contained in $G[y]$, but not necessarily
in $G[x]$. Therefore, it is possible that $x$ does not appear in the main
message of $u$. Therefore, for each $j\in\\{0,1\\}$, vertex $u$ also receives
the sequence

$\textsf{service}^{j}(u)=(\textsf{service}^{j}_{1}(u),\dots,\textsf{service}^{j}_{d}(u)),$

where, for each $i\in[d]$, the value of $\textsf{service}^{j}_{i}(u)$
represents the part of the certification of the service tree $S(x)$, where $x$
is the left child (respectively the right child) of $x_{i-1}(u)$.
Specifically, if $x$ is not of type $\parallel$, or if $u$ does not
participate in $S(x)$, then $\textsf{service}^{j}_{i}(u)=\bot$. Otherwise,

$\textsf{service}^{j}_{i}(u)=(\textsf{root}^{j}_{i}(u),\textsf{parent}^{j}_{i}(u),\textsf{distance}^{j}_{i}(u),\textsf{class}^{j}_{i}(u),\textsf{colorCharge}^{j}(u))$

where

  * •

$\textsf{root}^{j}_{i}(u)$ is the identifier of the root of $S(x)$;

  * •

$\textsf{parent}^{j}_{i}(u)$ is the identifier of the parent of $u$ in $S(x)$,
with $\textsf{parent}^{j}_{i}(u)=\bot$ if $u=\textsf{root}^{j}_{i}(u)$,;

  * •

$\textsf{distance}^{j}_{i}(u)$ is the distance between $u$ and the root
$\textsf{exit}(x)$ in $S(x)$;

  * •

$\textsf{class}^{j}_{i}(u)$ is the homomorphism class of
$G[\textsf{inCharge}_{x}(u)]$;

  * •

$\textsf{colorCharge}_{i}^{j}(u)=(\textsf{colorCharge}_{i}^{j,1}(u),\dots,\textsf{colorCharge}_{i}^{j,k^{\prime}}(u))$
where $\textsf{colorCharge}_{i}^{j,s}(u)$ is the number of vertices colored
$s$ in $G[\textsf{inCharge}_{x}(u)]$, for every $s\in[k^{\prime}]$.

###  5.4 Verification Scheme

The main role of the verification procedure is to check that the
$\mathrm{NLC}_{+}$-decomposition tree is correct, that is (1) it corresponds
to the graph $G$, and (2) at each node $x$ of the decomposition tree, the
homomorphism class for property $\Pi$ provided by the prover corresponds to
$h(G[x])$.

Each vertex $u\in V$ checks that all its messages in its certificate are
correctly formatted. Then, the verification is split in three parts: (1)
verification of the main messages, (2) verification of the auxiliary messages,
and (3) verification of the service messages.

#### Verification of main messages.

Each vertex $u\in V$ verifies the following conditions:

  1. 1.

$x_{d}(u)$ is of type $\mathsf{newVertex}_{s}$ for some $s\in[k^{\prime}]$;

  2. 2.

$\textsf{exit}_{d}(u)=\mathsf{id}(u)$;

  3. 3.

$\textsf{color}^{j}_{d}(u)=0$ for every $j\in[k^{\prime}]\setminus\\{s\\}$,
and $\textsf{color}^{s}_{d}(u)=1$;

  4. 4.

$h_{d}(u)$ is the homomorphism class for ${\Pi}$ of a graph equal to a single
node labelled $\ell(u)$, colored $s$;

  5. 5.

$x_{1}(u)$ is of type $\Join$, and for each $i\in\\{2,\dots,d(u)\\}$, if
$x_{i}$ is of type $\parallel$ then $x_{i-1}(u)$ is of type $\Join$;

  6. 6.

$h_{1}(u)$ is an _accepting_ homomorphism class for ${\Pi}$, i.e., graphs of
$\mathrm{NLC}_{+}$-width $k^{\prime}$ having this class satisfy $\Pi$.

Let us define $\mathsf{currentcolor}(u,i)$ in the same way that we did in the
verification of cographs. Moreover, for a vertex $v\in V$, let us denote
$i^{*}=\textsf{index}(u,v)$ as the maximum index $i\in[d(u)]$ such that
$\ell_{j}(u)=\ell_{j}(v)$ for every $j\leq i$. Then, $u$ computes
$\textsf{index}(u,v)$ for each of its neighbors $v\in N(v)$, and checks:

  1. 7.

$\textsf{main}_{i}(u)=\textsf{main}_{i}(v)$ for every $i\leq i^{*}$.

  2. 8.

$x_{i^{*}}(u)$ is of type $\Join$, and

     * •

if $\ell_{i^{*}+1}(u)=0$ then $u$ checks that $x_{i^{*}}$ contains the join
operation $\Join_{S}$ with

$(\mathsf{currentcolor}(u,i^{*}),\mathsf{currentcolor}(v,i^{*}))\in S$

     * •

if $\ell_{i^{*}+1}(u)=1$ then $u$ checks that $x_{i^{*}}$ contains the join
operation $\Join_{S}$ with

$(\mathsf{currentcolor}(v,i^{*}),\mathsf{currentcolor}(u,i^{*}))\in S.$

  3. 9.

For each $j\in[k^{\prime}]$, vertex $u$ checks that it has exactly
$\textsf{color}^{j}_{i^{*}+1}(v)$ neighbors $w$ such that
$\textsf{index}(u,w)=i^{*}$, $\ell_{i^{*}+1}(w)\neq\ell_{i^{*}+1}(u)$, and
$\mathsf{currentcolor}(w,i^{*}+1)=j$;

  4. 10.

Vertex $u$ then considers the homomorphism classes $h_{i^{*}}(u)$,
$h_{i^{*}+1}(u)$ and $h_{i^{*}+1}(v)$. (Recall that these encode the
homomorphism classes of relation ${\Pi}$ for graphs $G[x_{i^{*}}(u)]$,
$G[x_{i^{*}+1}(u)]$ and $G[x_{i^{*}+1}(v)]$, respectively.)

     * •

If $\ell_{i*+1}=0$ then $x_{i^{*}+1}(u)$ must be the left child of
$x_{i^{*}}(u)$, and vertex $u$ checks that

$h_{i^{*}}(u)=\odot_{\mathsf{recolor}_{R}}(\odot_{\Join_{S}}(h_{i^{*}+1}(u),h_{i^{*}+1}(v))).$

     * •

If $\ell_{i*+1}=1$ then $x_{i^{*}+1}(u)$ must be the right child of
$x_{i^{*}}(u)$, and vertex $u$ checks that

$h_{i^{*}}(u)=\odot_{\mathsf{recolor}_{R}}(\odot_{\Join_{S}}(h_{i^{*}+1}(v)),h_{i^{*}+1}(u)).$

  5. 11.

For each $j\in[k^{\prime}]$,

$\textsf{color}^{j}_{i^{*}}(u)=\sum_{s\in
R^{-1}(j)}\left(\textsf{color}^{s}_{i^{*}+1}(u)+\textsf{color}^{s}_{i^{*}+1}(v)\right).$

  6. 12.

Finally, for each $i\in[d(u)]$ such that $x_{i}(u)$ is of type $\Join$, if
$\textsf{exit}_{i}(u)=\mathsf{id}(u)$, then $u$ checks that $\ell_{i+1}(u)=0$,
and that there exists $v\in N(u)$ such that $\textsf{index}(u,v)=i$ and
$\ell_{i+1}(v)=1$.

#### Verification of auxiliary messages.

For every $i\in[d(u)]$ vertex $u$ checks that $\textsf{aux}_{i}\neq\bot$ if
and only if $x_{i}(u)$ is of type $\Join$. Let us suppose now that
$\textsf{aux}_{i}\neq\bot$. Then $u$ checks the following conditions

  1. 13.

$\textsf{root}_{i}(u)=\textsf{exit}_{i}(u)$;

  2. 14.

if $\textsf{parent}_{i}(u)=\perp$ then $\textsf{root}_{i}(u)=\mathsf{id}(u)$;

  3. 15.

if $v=\textsf{parent}_{i}(u)\neq\bot$ then $v\in N(u)$,
$\textsf{index}(u,v)\geq i$, $\textsf{aux}_{i}(v)\neq\perp$,
$\textsf{root}_{i}(v)=\textsf{root}_{i}(u)$,
$\textsf{childrenMain}^{0}_{i}(u)=\textsf{childrenMain}^{0}_{i}(v)$,
$\textsf{childrenMain}^{1}_{i}(u)=\textsf{childrenMain}^{1}_{i}(v)$, and

$\textsf{distance}_{i}(v)=\textsf{distance}_{i}(u)-1;$

  4. 16.

if $j=\ell_{i+1}(u)$ then
$\textsf{childrenMain}^{j}_{i}(u)=\textsf{main}_{i+1}(u)$.

#### Verification of service messages.

For every $i\in[d(u)]$ and $j\in\\{0,1\\}$ for which
$\textsf{service}^{j}_{i}(u)\neq\perp$, $u$ checks the following conditions:

  1. 17.

If $\ell_{i}(u)=j$ then $x_{i}(u)$ is of type $\parallel$.

  2. 18.

If $v=\textsf{parent}^{j}_{i}(u)\neq\perp$ then $v\in N(u)$,
$\textsf{index}(u,v)\geq i-1$, $\textsf{service}^{j}_{i}(v)\neq\perp$,
$\textsf{root}^{j}_{i}(v)=\textsf{root}^{j}_{i}(u)$ and
$\textsf{distance}^{j}_{i}(v)=\textsf{distance}_{i}^{j}(u)-1$.

  3. 19.

If $\textsf{parent}^{j}_{i}(u)=\perp$ then
$\textsf{root}^{j}_{i}(u)=\mathsf{id}(u)$.

If $u$ has no neighbors $w\in V$ such that $\textsf{parent}^{j}_{i}(w)=u$,
then $u$ deduces that it is a leaf of the tree $S(x_{i}^{j})$. In that case,
$u$ checks the following conditions:

  1. 20.

$u$ is a terminal, so $\textsf{exit}_{i+1}(u)=\mathsf{id}(u)$;

  2. 21.

$\textsf{class}_{i}^{j}(u)=h_{i+1}(u)$ and
$\textsf{colorCharge}_{i}^{j}(u)=\textsf{color}_{i+1}(u)$.

If $u$ is not a leaf of $S(x_{i}^{j})$, then $u$ computes the set
$\textsf{children}_{i}^{j}(u)$ of nodes $w\in V$ such that
${\textsf{parent}_{i}^{j}(w)=u}$. Then $u$ checks the following conditions:

  1. 22.

For each $s\in[k^{\prime}]$, let $\gamma=\textsf{color}_{i+1}^{s}(u)$ if
$u=\textsf{exit}_{i+1}(u)$ and $\ell_{i}(u)=j$, and let $\gamma=0$ otherwise.
Then $u$ checks that:

$\textsf{colorCharge}^{j,s}(u)=\sum_{w\in\textsf{children}_{i}^{j}(u)}\textsf{colorCharge}^{j,s}(w)+\gamma$

  2. 23.

If $\textsf{children}_{i}^{j}(u)$ contains a single vertex $w$, then $u$
checks that $\textsf{class}_{i}^{j}(u)=\textsf{class}_{i}^{j}(w)$.

  3. 24.

If $\textsf{children}_{i}^{j}(u)$ contains two or more vertices, then $u$
defines an arbitrary order of the vertices in $\textsf{children}_{i}^{j}(u)$,
namely $w_{1},\dots,w_{p}$. Then, $u$ defines a sequence of homomorphism
classes $c_{1},\dots,c_{p}$ where, $c_{1}=\textsf{class}_{i}^{j}(w_{1})$, and
for each $i\in\\{2,\dots,p\\}$:

$c_{i}=\odot_{\parallel}(c_{i-1},\textsf{class}_{i}^{j}(w_{i})).$

where $\odot_{\parallel}$ corresponds to the function
$\odot_{\Join_{\emptyset}}$. Finally checks that
$c_{p}=\textsf{class}_{i}^{j}(u)$.

If $u=\textsf{exit}_{i}(u)$, then $u$ checks the following additional
conditions for each $j\in\\{0,1\\}$:

  1. 25.

$\textsf{parent}_{i}^{j}(u)=\bot$, and $\textsf{distance}_{i}^{j}(u)=0$;

  2. 26.

$\textsf{class}_{i}^{j}(u)=h_{i}(u)$, and
$\textsf{colorCharge}_{i}^{j}(u)=\textsf{color}_{i}(u)$.

###  5.5 Completeness and Soundness

The completeness follows directly from the existence of an
$\mathrm{NLC}_{+}$-decomposition $T$ of $G$ as described in Lemma 5.4 and from
the construction of the main, auxiliary and service messages, based on this
decomposition.

For soundness, assume that the verification protocol accepts at every vertex.
Let us define the set of all main messages as
$\textsf{mainset}=\\{\textsf{main}(u):u\in V\\}$, and let $d^{*}=\max_{u\in
V}d(u)$. For every $M\in\textsf{mainset}$ we denote $d(M)=d(u)$ where $u$ is
such that $\textsf{main}(u)=M$. Now, we define $\textsf{Prefix}(M,i)$ as the
set of vertices $v\in V$ that have the same first $i$ values in their main
messages. Formally,

$\textsf{Prefix}(M,i)=\\{v\in V:M_{j}=\textsf{main}_{j}(v),\textrm{ for every
}1\leq j\leq i\\}.$

By condition 2 in the verification protool,
$\textsf{exit}_{d}(u)=\mathsf{id}(u)$. Thus
$\textsf{main}(u)\neq\textsf{main}(v)$ for every pair of vertices $u\neq v$.
Therefore, $\textsf{Prefix}(\textsf{main}(u),d(u))=\\{u\\}$. Also, by
condition 7 we have that $\textsf{Prefix}(M,1)=V$. Given
$M\in\textsf{mainset}$, and $i\in[d(M)]$, let

$M_{i}=(x_{i}(M),\ell_{i}(M),h_{i}(M),\textsf{color}_{i}(M),\textsf{exit}_{i}(M))$

be the list $\textsf{main}_{i}(v)$ for a vertex $v$ such that
$\textsf{main}(v)=M$.

######  Lemma 5.7.

For every $M\in\textsf{mainset}$, and every $i\in[d(M)]$, there exists a
$\mathrm{NLC}_{+}$-decomposition tree $T[M,i]$ of
$G[M,i]=G[\textsf{Prefix}(M,i)]$ such that, for all
$u\in\textsf{Prefix}(M,i)$, the following holds.

  * •

For every $j$ with $i\leq j\leq d(u)$, $x_{j}(u)$ contains the operations in
the $j$-th node in path from the root of $T[M,i]$ to the node where $u$ is
created;

  * •

$h_{i}(u)=h(G[M,i])$;

  * •

For every $s\in[k^{\prime}]$, $\textsf{color}^{s}_{i}(u)$ is the number of
vertices colored $s$ in the root of $T[M,i])$.

######  Proof 5.8.

The proof is by induction on $i$, in decreasing order for each $M$. Let us fix
$M\in\textsf{mainset}$. The base case is $i=d(M)$, and
$\textsf{Prefix}(M,d(M))$ is a single vertex $u$ satisfying
$\textsf{main}(u)=M$. In this case the lemma is true by conditions 1-4. For
the inductive case, let us suppose that there exists $t>1$ such that the lemma
is true for every $M\in\textsf{mainset}$, and $i\in\\{t,\dots,d(M)\\}$, and
let us show that the lemma holds an arbitrary pair $M\in\textsf{mainset}$ and
$i=t-1$.

– Let us suppose first that $x_{i}(M)$ is of type $\Join$. Consider the set

$\beta_{i}(M)=\\{(\textsf{root}_{i}(u),\textsf{parent}_{i}(u),\textsf{distance}_{i}(u))\mid
u\in\textsf{Prefix}(M,i)\\}.$

From conditions 13-15, we have that $\beta_{i}(M)$ certifies a spanning tree
of $\textsf{Prefix}(M,i)$ rooted at $\textsf{exit}_{i}(M)$. In particular, we
have that $\textsf{Prefix}(M,i)$ induces a connected subgraph of $G$. Let us
call $u^{0}$ the vertex with identifier $\textsf{exit}_{i}(M)$. By condition
12, we have $\ell_{i+1}(u^{0})=0$, and there exists a vertex $u^{1}\in N(u)$
such that $\textsf{index}(u,v)=i$ and $\ell_{i+1}(u^{1})=1$. Let us call
$M^{0}=\textsf{main}(u^{0})$ and $M^{1}=\textsf{main}(v^{1})$. Our candidate
for $T[M,i]$ is the tree defined by a root $x_{i}(M)$ with two children. The
left children induces the subtree $T[M^{0},i+1]$ while the right children
induces the subtree $T[M^{1},{i+1}]$.

Observe first that $\textsf{Prefix}(M,i)$ can be partitioned in
$\textsf{Prefix}(M^{0},i+1)$ and $\textsf{Prefix}(M^{1},i+1)$. Indeed, let $w$
be a vertex in $\textsf{Prefix}(M,i)$, and let $j=\ell_{i+1}(w)$. By condition
16, we have that $\textsf{childrenMain}^{j}_{i}(w)=\textsf{main}_{i+1}(w)$. By
condition 15, and the fact that $\textsf{Prefix}(M,i)$ is connected, we have
that $\textsf{main}_{i+1}(w)=\textsf{main}_{i+1}(w^{\prime})$ for every
$w^{\prime}\in\textsf{Prefix}(M,i)$ for which $\ell_{i+1}(w^{\prime})=j$. In
particular $\textsf{main}_{i+1}(w)=\textsf{main}_{i+1}(u^{j})$, and therefore
$w$ belongs to $\textsf{Prefix}(M^{j},i+1)$.

By the induction hypothesis, for each $j\in\\{0,1\\}$, $T[M^{j},i+1]$ is an
$\mathrm{NLC}_{+}$ decomposition tree of $G[M^{j},i+1]$. Moreover,
$h_{i+1}(M^{j})=h(G[M^{j},i+1])$, and, for each $s\in[k^{\prime}]$, we have
that $\textsf{color}^{s}_{i+1}(M^{j})$ is the number of vertices colored $s$
in the root of $T[M^{j},i+1]$. Let $S$ be the set of join operations defined
in $x_{i}(M)$, and let $u\in\textsf{Prefix}(M^{0},i+1)$ and
$v\in\textsf{Prefix}(M^{1},i+1)$ be such that $\\{u,v\\}\in
E(G[\textsf{Prefix}(M,i)])$. By condition 8, we have that

$(\textsf{currentcolor}(u,i),\textsf{currentcolor}(v,i))\in S.$

Moreover, by condition 9, vertex $u$ has exactly
$\textsf{color}_{i+1}^{s}(M^{1})$ neighbors $v\in\textsf{Prefix}(M^{1},i+1)$
such that $\textsf{currentcolor}(v,i)=s$. This implies that the join
operations defined in $x_{i}(M)$ create exactly the set of edges $\\{u,v\\}\in
E(G[M,i])$ such that $\textsf{index}(u,v)=i$, and no other edges. It follows
that $T[M,i]$ is an $\mathrm{NLC}_{+}$-decomposition tree of $G[M,i]$.
Finally, by condition 10 applied at $u^{0}$, we have that
$h_{i}(M)=h(G[M,i])$, and, by condition 11 applied at $u^{0}$, we have that,
for every $s\in[k^{\prime}]$, $\textsf{color}_{i}^{s}(M)$ is the number of
vertices colored $s$ in the root of $T[M,i]$.

– Let us suppose now that $x_{i}(M)$ is of type $\parallel$, and let us define
the following subset of mainset:

$\textsf{mainPrefix}(M,i)=\\{M^{\prime}\in\textsf{mainset}\mid\textsf{Prefix}(M,i)=\textsf{Prefix}(M^{\prime},i)\\}$

Observe that from the induction hypothesis, we have that, for each
$M^{\prime}\in\textsf{mainPrefix}(M,i)$, there is an
$\mathrm{NLC}_{+}$-decomposition tree $T[M^{\prime},i+1]$ of
$G[M^{\prime},i+1]$, satisfying the conditions of the lemma. Our candidate for
$T[M,i]$ is a tree rooted in $x_{i}(M)$, where the children of $x_{i}(M)$
induce the set of trees

$\\{T[M^{\prime},i+1]:M^{\prime}\in\textsf{mainPrefix}(M,i)\\}.$

Indeed, every vertex $u$ in $\textsf{Prefix}(M,i)$ satisfies that
$x_{i}(u)=x_{i}(M)$. Then, by condition 8, $u$ cannot have a neighbor $v$ such
that $\textsf{index}(u,v)=i$. Therefore $T[M,i]$ does define an
$\mathrm{NLC}_{+}$ decomposition of $G[M,i]$. Let $j=\ell_{i}(M)$, and let us
consider the set

$\alpha_{i}^{j}(M)=\\{(\textsf{root}^{j}_{i}(u),\textsf{parent}^{j}_{i}(u),\textsf{distance}^{j}_{i}(u))\mid
u\in\textsf{Prefix}(M,i-1)\;\text{and}\;\textsf{service}_{i}^{j}(u)\neq\bot\\}.$

Let $u$ be a vertex such that $\textsf{main}(u)\in\textsf{mainPrefix}(M,i)$.
From condition 5, $x_{i+1}(u)$ is of type $\Join$. Hence,
$\textsf{Prefix}(\textsf{main}(u),i+1)$ induces a connected set of vertices in
$G$. Therefore, by conditions 17-20 and 25, $\alpha_{i}^{j}(M)$ certifies a
Steiner tree in $G$ rooted at $\textsf{exit}_{i}(M)$, with set of terminals

$\textsf{terminals}_{i}(M)=\\{u\in V\mid\exists
M^{\prime}\in\textsf{mainPrefix}(M,i),\mathsf{id}(u)=\textsf{exit}_{i+1}(M^{\prime})\\}.$

From conditions 21 and 23-26, $h_{i}(M)$ is the homomorphism class of ${\Pi}$
obtained from the disjoint union function ${\odot}_{\parallel}$ over the set

$\\{h_{i+1}(M^{\prime}):M^{\prime}\in\textsf{mainPrefix}(M,i)\\}.$

By the induction hypothesis, it follows that $h_{i}(M)$ is the homomorphism
class of $G[M^{\prime},i+1]$. From conditions 21, 22, and 26, we have that,
for each $s\in[k^{\prime}]$,

$\textsf{color}^{s}_{i}(M)=\sum_{u\leavevmode\nobreak\ \in\leavevmode\nobreak\
\textsf{terminals}_{i}(M)}\textsf{color}^{s}_{i+1}(u).$

Again, by the induction hypothesis, $\textsf{color}_{i}^{s}(M)$ is the number
of vertices colored $s$ in the root of $T[M,i]$.

Finally, observe that by condition 7, for every $M$ and
$M^{\prime}\in\textsf{mainset}$, we have $M_{1}=M^{\prime}_{1}$. Then,
$\textsf{Prefix}(M,1)=V$. Applying Lemma 5.7 to an arbitrary
$M\in\textsf{mainset}$ and for $i=1$, we deduce that $T[M,1]$ is an
$\mathrm{NLC}_{+}$-decomposition tree of $G$. It follows that $G$ is a graph
of $\mathrm{NLC}_{+}$-width $k^{\prime}$. Moreover, also by Lemma 5.7, we have
$h_{1}(M)=h(G)$. Finally, by condition 6 we conclude that $G$ satisfies
property $\Pi$. ∎

###  5.6 Certificate Size

For the certificate size, let $u$ an arbitrary vertex, let $i\in d(u)$, and
let $j\in\\{0,1\\}$. Observe that each item of $\textsf{main}_{i}(u)$,
$\textsf{aux}_{i}(u)$, and $\textsf{service}^{j}_{i}(u)$ can be encoded with
$\mathcal{O}(\log n)$ bits. By Lemma 5.4, we have that $d(u)=\mathcal{O}(\log
n)$. Therefore, the certificate of $u$ is of size $\mathcal{O}(\log^{2}n)$.

##  6 Certifying Solutions of Optimization Problems

In this section we extend our proof-labelling scheme to optimization problems
expressible by $\mathrm{MSO}_{1}$ predicates over graphs and vertex sets, on
graphs of bounded clique-width. More precisely we consider $\mathrm{MSO}_{1}$
predicates $\Pi(G,X)$, over graphs $G=(V,E)$ and vertex subsets $X\subseteq
V$. An optimization problem for $\Pi$ on graph $G$ consists in finding the
maximum (or minimum) size vertex subset $X$ such that $\Pi(G,X)$ is true. For
example, one can easily describe an $\mathrm{MSO}_{1}$ predicate $\Pi(G,X)$
expressing that "$X$ is an independent set of $G$", or "$X$ is a dominating
set of $G$". Hence problems like minimum dominating set or maximum independent
set are particular cases of optimization problems expressible by
$\mathrm{MSO}_{1}$ predicates over graphs and vertex sets.

######  Theorem 6.1.

Let $k$ be a non-negative integer. For every $\mathrm{MSO}_{1}$ predicate
$\Pi$ on vertex-labeled graphs and vertex-sets, and every $n$-node graph
$G=(V,E)$ with $\mathsf{cw}(G)\leq k$, and every $X\subseteq V$, there exists
a PLS certifying that $X$ is the set of minimum (or maximum) size such that
$(G,X)$ satisfies $\Pi$ among all sets $Y$ such that $(G,Y)$ satisfies $\Pi$,
with $O(\log^{2}n)$-bit certificates.

Theorem 6.1 actually also extends to $\mathrm{MSO}_{1}$ predicates
$\Pi(G,X_{1},X_{2},\dots,X_{q})$ over graphs and a bounded number of vertex
subsets, and the optimization can be performed with respect to some linear
evaluation function over the sizes of $X_{1},\dots,X_{q}$. Such optimization
problems are called $LinEMSOL$ in [16]. However, since most natural
optimization problems are expressed on a single vertex subset, and in order to
keep the notations simpler, we focus here solely on predicates of type
$\Pi(G,X)$.

###  6.1 Proof of Theorem 6.1

Operations $\Join_{S}$ and $\mathsf{recolor}_{R}$ directly extend to pairs of
graphs and vertex subsets: $(G_{1},X_{1})\Join_{S}(G_{2},X_{2})$ corresponds
to pair $(G_{1}\Join_{S}G_{2},X_{1}\cup X_{2})$, and recoloring
$\mathsf{recolor}_{R}(G,X)$ is simply the pair $(\mathsf{recolor}_{R}(G),X)$.

The notion of regularity (Definition 5.1) extends to predicates over graphs
and vertex subsets, moreover such $\mathrm{MSO}_{1}$ predicates are regular on
graphs of bounded NLC-width. (Again, this even holds for predicates with a
bounded number of vertex subsets [16]).

######  Definition 6.2.

Let $\Pi(G,X)$ be a predicate over graphs and vertex sets. Predicate $\Pi$ is
called _NLC-regular_ if, for any value $k$, we can associate a finite set
$\mathcal{C}$ of _homomorphism classes_ and a _homomorphism function_ $h$,
assigning to each graph $G\in\mathrm{NLC}_{k}$ and each vertex subset $X$ of
$G$ a class $h(G,X)\in\mathcal{C}$ such that:

  1. 1.

If $h(G_{1},X_{1})=h(G_{2},X_{2})$ then $\Pi(G_{1},X_{1})=\Pi(G_{2},X_{2})$.

  2. 2.

For each composition operation $\Join_{S}$ of arity 2 there exists a function
$\odot_{\Join_{S}}:\mathcal{C}\times\mathcal{C}\rightarrow\mathcal{C}$ such
that, for any two $\mathrm{NLC}_{k}$ graphs $G_{1}$ and $G_{2}$ with vertex
subsets $X_{1}$, $X_{2}$,

$h((G_{1},X_{1})\Join_{S}(G_{2},X_{2}))=\odot_{\Join_{S}}(h(G_{1},X_{1}),h(G_{2},X_{2})).$

  3. 3.

For each composition operation $\mathsf{recolor}_{R}$ of arity 1 there is a
function $\odot_{\mathsf{recolor}_{R}}:\mathcal{C}\rightarrow\mathcal{C}$ such
that, for any $\mathrm{NLC}_{k}$ graph $G$ and vertex subset $X$,

$h(\mathsf{recolor}_{R}(G,X))=\odot_{\mathsf{recolor}_{R}}(h(G,X)).$

Moreover functions $\odot_{\Join_{S}}$ and $\odot_{\mathsf{recolor}_{R}}$ can
be computed in constant time for any recoloring function $R:[k]\to[k]$ and any
set $S$ of pairs of $[k]\times[k]$. Also, for any graph with a unique vertex
colored $i\in[k]$, its two classes (corresponding to the two possible vertex
subsets, the singleton and the empty set) can be computed in constant time.
Again, by constant time, we mean only depending on $k$ and on the
$\mathrm{MSO}_{1}$ formula describing $\Pi$.

For example, if $\Pi(G,X)$ expresses that $X$ is an independent set of $G$,
then we can take $\mathcal{C}$ as the set of subsets of $[k]$, plus a special
symbol $\bot$, and define $h(G,X)$ as follows: $h(G,X)=\bot$ if $X$ is not an
independent set, otherwise $h(G,X)$ is the subset of $[k]$ such that $i\in
h(G,X)$ if $X$ contains some vertex colored $i$. Again, it is a matter of
exercise to construct the classes for graph with a single vertex, as well as
functions $\odot_{\mathsf{recolor}_{R}}$ and $\odot_{\Join_{S}}$. Indeed, if
$G$ has a unique vertex $x$ coloured $i\in[k]$ then $h(G,\emptyset)=\emptyset$
and $h(G,\\{x\\})=\\{i\\}$. Function $\odot_{\mathsf{recolor}_{R}}$ simply
takes into account the recoloring of vertices. Let $R:[k]\to[k]$ be a
recoloring. Note that $\odot_{\mathsf{recolor}_{R}}(\bot)=\bot$ (this
corresponds to pairs $(G,X)$ where $X$ is not an independent set of $G$). Let
$c$ be a subset of $[k]$, note that
$\odot_{\mathsf{recolor}_{R}}(c)=c^{\prime}$ with
$c^{\prime}=\\{j\in[k]\mid\exists i\in c\text{\leavevmode\nobreak\ such
that\leavevmode\nobreak\ }R(i)=j\\}$. Indeed, if $c=h(G,X)$ for some pair
$(G,X)$, then $c^{\prime}$ corresponds to the colours of vertices of $X$ after
recoloring. Eventually, we describe the binary function
$\odot_{\Join_{S}}:\mathcal{C}\times\mathcal{C}\to\mathcal{C}$. Observe that
$\odot_{\Join_{S}}(c_{1},c_{2})=\bot$ if $c_{1}=\bot$ or $c_{2}=\bot$. Indeed
this corresponds to the case when $c_{1}=h(G_{1},X_{1})$ and
$c_{2}=h(G_{2},X_{2})$, and $X_{1}$ is not an independent set of $G_{1}$, or
$X_{2}$ is not an independent set of $G_{2}$ ; therefore $X=X_{1}\cup X_{2}$
cannot be an intependent set of $G_{1}\Join_{S}G_{2}$. For similar reasons, if
there is some pair $(i,j)\in S$ such that $i\in c_{1}$ and $j\in c_{2}$, then
$\odot_{\Join_{S}}(c_{1},c_{2})=\bot$, because the $\Join_{S}$ operation adds
an edge between $X_{1}$ and $X_{2}$, so $G$ is not an independent set of $G$.
Otherwise, we have $\odot_{\Join_{S}}(c_{1},c_{2})=c_{1}\cup c_{2}$, since the
set of colours of $X$ is the union of the sets of colours of $X_{1}$ and
$X_{2}$. This proves the NLC-regularity of predicate ”$X$ in an independent
set of $G$”.

By [16], all $\mathrm{MSO}_{1}$ predicates are regular:

######  Proposition 6.3.

Any property $\Pi$ over graphs and vertex subsets expressible by an
$\mathrm{MSO}_{1}$ predicate is NLC-regular. Moreover, given the corresponding
$\mathrm{MSO}_{1}$ formula and parameter $k$, one can explicitely compute the
set of homomorphism classes $\mathcal{C}$, as well as functions
$\odot_{\Join_{S}}$ and $\odot_{\mathsf{recolor}_{R}}$ for any
$S\in[k]\times[k]$ and any $R:[k]\to[k]$, and the homomorphism class of the
graph formed by a unique vertex coloured $i$, for any $i\in[k]$.

To unify maximization and minimization problems, assume that we deal with
weighted graphs. In this setting, each vertex $u$ of $G$ is assigned an
integer $weight(u)$ in the interval $[-MAXW,+MAXW]$ for some positive integer
constant $MAXW$. The aim of the optimization is to find a maximum weight
vertex subset $X$ satisfying $\Pi(G,X)$. Natural minimization problems are
turned into maximization problems, using negative weights.

In the certification context, we will be given graph $G$ together with the set
$X$ of _selected vertices_. The selected vertices are encoded by a function
$sel:V\to\\{0,1\\}$. The set $X_{s}$ of selected vertices corresponds to
$X_{s}=\\{u\in V(G)\mid sel(u)=1\\}$ and we aim to certify that $\Pi(G,X_{s})$
is true and $X_{s}$ is of maximum weight among all sets $X$ satisfying
$\Pi(G,X)$. Each node $u$ of the graph knows its status $sel(u)$, so it knows
whether it is selected or not. Let us note that we prefer to separate the
vertex selection function $sel$ and the vertex labeling function $\ell$, for
two reasons: they play different roles (the labelling is part of the input,
while selected vertices must be proved to be an optimal output for the
problem), moreover the two can be combined, in the sense that the optimization
is performed on labeled graphs (e.g., in the red-blue dominating set problem,
the input is a graph with vertices labelled 0 for red and 1 for blue, and the
aim is to find a minimum size set X of red vertices dominating all blue
vertices).

We need to enrich the certificates for decision problems described in the
Section 5. For each class $c\in\mathcal{C}$, let $MaxW(G,c)$ denote the
maximum $weight(X)$ over all vertex subsets $X$ of graph $G$ such that
$h(G,X)=c$. If no such $X$ exists, we set $MaxW(G,c)=-\infty$. Informally, in
each certificate, homomorphism classes over subgraphs of $G$ are replaced by
homomorphism classes over the same subgraphs, with the corresponding subset of
selected vertices. Moreover, whenever we had to consider a partial solution
over a subgraph $G^{\prime}$ of $G$, we also store in the message, besides the
homomorphism class $h(G,X^{\prime})$, the weight of the selected vertices
$X^{\prime}$ of $G^{\prime}$, as well as all values $MaxW(G^{\prime},c)$, over
all possible classes $c\in\mathcal{C}$. The latter will allow to check that
there is no better solution for the problem than our set of selected vertices.

The following proposition is a straightforward application of the definition
of $MaxW(G,c)$. It was also observed, in slightly different terms, in [16] and
it provides the tool to update values $MaxW$, from bottom to top, if we are
given a decomposition tree.

######  Proposition 6.4.

Let $\Pi(G,X)$ be an $\mathrm{MSO}_{1}$ predicate over graphs and vertex
subsets, $k$ be a fixed parameter, and $c\in\mathcal{C}$ a homomorphism class.

  1. 1.

If $G$ is formed by a single vertex $x$ of colour $i$. Then

$MaxW(G,c)=\max\\{weight(X)\mid X\subseteq\\{x\\}\text{\leavevmode\nobreak\
such that\leavevmode\nobreak\ }h(G,X)=c\\}.$

  2. 2.

If $G=G_{1}\Join_{S}G_{2}$, then

$MaxW(G,c)=\max_{c_{1},c_{2}\in\mathcal{C}\times\mathcal{C}}\\{MaxW(G_{1},c_{1})+MaxW(G_{2},c_{2})\\},$

over all pairs of classes
${c_{1},c_{2}\in\mathcal{C}\times\mathcal{C}}\text{\leavevmode\nobreak\ s.
t.\leavevmode\nobreak\ }\odot_{\Join_{S}}(c_{1},c_{2})=c$.

  3. 3.

If $G=R(G^{\prime})$, then

$MaxW(G,c)=\max\\{MaxW(G^{\prime},c^{\prime})\mid{c^{\prime}\in\mathcal{C}}\text{\leavevmode\nobreak\
such that\leavevmode\nobreak\ }\odot_{R}(c^{\prime})=c.\\}$

In all above equations we consider that the maximum of an empty set is
$-\infty$.

We can now formally describe the certificates. We only precise what changes
with respect to messages defined in Section 5.

#### Main messages.

In the decision setting, the main message of each node $u$ contains a sequence
$\textsf{h}(u)=(h_{1}(u),\dots,h_{d}(u))$. Recall that $x_{i}(u)$ denotes the
$i$th node on the path of the $NLC_{+}$ decomposition tree $T$ of $G$, from
the root to the leaf creating $u$, and $h_{i}(u)$ denotes the homomorphism
class of predicate $\Pi$ at node $x_{i}(u)$, i.e., corresponding to the
induced subgraph $G[x_{i}(u)]$ of $G$. In the optimization setting we simply
use as $h_{i}(u)$ the class $h(G[x_{i}(u)],X_{s}[x_{i}(u)])$, where
$X_{s}[x_{i}(u)]$ is the set of selected vertices of $G[x_{i}(u)]$.

We add to the main message of $u$ the sequence
$\textsf{weight}(u)=(\textsf{weight}_{1}(u),\dots,\textsf{weight}_{d}(u))$,
such that, for each $i\in\\{1,\dots,d\\}$, $\textsf{weight}_{i}(u)$ denotes
the total weight of selected vertices at $x_{i}(u)$, that is, the weight of
$X_{s}[x_{i}(u)]$.

We also add the sequence
$\textsf{MaxW}(u)=(\textsf{MaxW}_{1}(u),\dots,\textsf{MaxW}_{d}(u))$, where
$\textsf{MaxW}_{i}(u)$ denotes the list $\\{MaxW(G[x_{i}(u)],c)\mid
c\in\mathcal{C}\\}$ of maximal weights of possible partial solutions at node
$x_{i}$, over all possible classes $c\in\mathcal{C}$.

#### Auxiliary messages.

Recall that at each node $x$ of type $\Join$ of the NLC+ decomposition tree,
we use a spanning tree $A(x)$ of the graph $G[x]$ hanging at $x$ and and
auxiliary messages to check that $G[x]$ is indeed connected, and that the
messages in this subgraph are coherent. Formally each node $u$ of $G$ is
provided an auxiliary message
$\textsf{aux}(u)=(\textsf{aux}_{1}(u),\dots,\textsf{aux}_{d}(u))$, where
$\textsf{aux}_{i}(u)$ is set to $\bot$ if $x_{i}(u)$ is of type $\parallel$,
otherwise it contains the information required for the spanning tree
$A(x_{i}(u))$ and the coherence of messages of $G[x_{i}(u)]$. The difference
for optimization problems consists in enriching the part
$\textsf{childrenMain}^{j}_{i}(u)=(z^{j},h(z^{j}),\textsf{color}(z^{j}),\textsf{exit}(z^{j}))$
for $j\in\\{0,1\\}$, where $z^{0}$ and $z^{1}$ denote the children of
$x_{i}(u)$ in the NLC+ decomposition tree. As for main messages, in the
optimization setting $h(z^{j})$ will denote the homomorphism class for
property $\Pi$ on $G[z^{j}]$ and its selected vertices. Moreover we add to
$\textsf{childrenMain}^{j}_{i}(u)$ the information $\textsf{weight}(z^{j})$
and $\textsf{MaxW}(z^{j})$, for $j\in\\{0,1\\}$, where
$\textsf{weight}(z^{j})$ is the weight of selected vertices of $G[z^{j}]$ and
$\textsf{MaxW}(z^{j})=\\{MaxW(G[z^{j}],c)\mid c\in\mathcal{C}\\}$ is the list
of all optimal solutions, over all homomorphism classes, in graph $G[z^{j}]$.

#### Service messages.

Recall that these messages are created at each node $x$ of type $\parallel$ in
the decomposition tree, and they concern the vertices of some tree $S(x)$,
connecting the graphs corresponding to subtrees of children $z_{i}$ of $x$,
$1\leq i\leq p$ through their exit vertices. Also recall that for each node
$u$ of $S(x)$, we have defined the set of indices
$\textsf{inCharge}_{x}(u)=\\{i\in\\{1,\dots,p\\}\mid\textsf{exit}(z_{i})\in
S(x,u)\\}$, meaning that the service message of $u$ for $x$ concerns the
partial solution $G[\textsf{inCharge}_{x}(u)]$, the subgraph of $G$ induced by
the disjoint union of all graphs $G[z_{i}]$ with
$i\in\textsf{inCharge}_{x}(u)$. By symmetry, let
$X_{s}[\textsf{inCharge}_{x}(u)]$ be the union of labelled vertices
$X_{s}[z_{i}]$, $i\in\textsf{inCharge}_{x}(u)$.

Recall that, for decision problems (see Section 5 for a full description of
service messages), we used value $\textsf{class}^{j}_{i}(u)$ corresponding to
homomorphism of $G[\textsf{inCharge}_{x}(u)]$ (here $j=0$ if $x$ is in the
left child of $x_{i-1}(u)$, and $j=1$ if $x$ is the right child of
$x_{i-1}(u)$). In the optimization version, we use instead the homomorphism
class $h(G[\textsf{inCharge}_{x}(u)],X_{s}[\textsf{inCharge}_{x}(u)])$, and we
add the weight $\textsf{weightService}^{j}_{i}(u)$ of
$X_{s}[\textsf{inCharge}_{x}(u)]$, and the list $\textsf{MaxWService}^{j}_{i}$
of all values $\\{MaxW(G[\textsf{inCharge}_{x}(u)],c)\mid c\in\mathcal{C}\\}$.

We emphasize again that, when we generalized the certification messages from
decision problems to optimization problems, we applied the same process on
every partial solution, on (induced) subgraphs $G^{\prime}$ of $G$: the
homomorphism class $h(G^{\prime})$ was replaced with the corresponding
homomorphism class $h(G^{\prime},X^{\prime}_{s})$ over selected vertices of
$G^{\prime}$, and the messages were enriched with the weight
$weight(X^{\prime}_{s})$ of $X^{\prime}_{s}$ and with the set
$\\{MaxW(G^{\prime},c)\mid c\in\mathcal{C}\\}$ of all maximal partial
solutions of $G^{\prime}$, over all possible homomorphism classes.

Therefore, in the verification scheme, we only need to update all
verifications that were in charge of homomorphism classes $h(G^{\prime})$ for
some subgraph $G^{\prime}$, and to enrich them to verify:

  * •

$h(G^{\prime},X^{\prime}_{s})$, using Definition 6.2 instead of Definition
5.1,

  * •

the weight $weight(X^{\prime}_{s})$ of $X^{\prime}_{s}$, by simply summing
over smaller partial solutions,

  * •

the wholes set $\\{MaxW(G^{\prime},c)\\}$ over all classes $c$ of
$\mathcal{C}$. For the latter, we simply use Proposition 6.4, in the same
manner as we used Definition 5.1, to check that each value
$MaxW(G^{\prime},c)$ is correct.

This occurs in the following places – we refer again to modifications w.r.t.
Section 5.

#### Verification of main messages.

Item 4, on graph $G^{\prime}$ with a single vertex $u$: we must check that
$weight(X^{\prime}_{s})=0$ if $u$ is not selected, otherwise
$weight(X^{\prime}_{s})=weight(u)$. Values $MaxW(G^{\prime},c)$ are computing
using the first item of Proposition 6.4.

Item 6, for the whole graph $G$. Besides checking that $h_{1}(u)=h(G,X_{s})$
is an accepting class for property $\Pi$, we also check that the weight of
$X_{s}$ (i.e., $\textsf{weight}_{1}(u)$) equals the maximum of
$MaxW(G,c)\in\textsf{MaxW}_{1}(u)$ over all _accepting_ classes $c$. This
ensures that the solution $X_{s}$ is indeed optimal.

Item 10, corresponding to an edge between vertices $u$ and $v$ such that
$x_{i^{*}}(u)$, their lowest common ancestor in the NLC+ decomposition tree,
is a binary $\Join$ node. In this case $G[x_{i^{*}}(u)]$ is obtained from
$G[x_{i^{*}+1}(u)]$ and $G[x_{i^{*}+1}(v)]$ by a sequence of operations
$\Join_{S}$ then $\mathsf{recolor}_{R}$. As for decision problems, we verify
using Definition 6.2 that class $h_{i^{*}}(u)$ is coherent with classes
$h_{i^{*}+1}(u)$ and $h_{i^{*}+1}(v)$ after performing $\Join_{S}$ then
$\mathsf{recolor}_{R}$. Then we perform the similar verification for each
value $MaxW(G[x_{i^{*}}(u)],c)\in\textsf{MaxW}_{i^{*}}(u)$ using Proposition
6.4 (items 2 and 3) to check that $\textsf{MaxW}_{i^{*}}(u)$ is indeed
obtained from $\textsf{MaxW}_{i^{*}+1}(u)$ and $\textsf{MaxW}_{i^{*}+1}(v)$ by
a sequence of operations $\Join_{S}$ then $\mathsf{recolor}_{R}$. Also, we
check that
$\textsf{weight}_{i^{*}}(u)=\textsf{weight}_{i^{*}+1}(u)+\textsf{weight}_{i^{*}+1}(v)$.

#### Verification of auxiliary messages.

We do not need any changes, since this is only a coherence check based on the
equality of parts childrenMain of the messages.

#### Verification of service messages.

We need to verify messages $\textsf{class}^{j}_{i}(u)$ corresponding to
homomorphism of $G[\textsf{inCharge}_{x}(u)]$, the weight
$\textsf{weightService}^{j}_{i}(u)$ of $X_{s}[\textsf{inCharge}_{x}(u)]$, and
the list $\textsf{MaxWService}^{j}_{i}(u)$ of all values
$\\{MaxW(G[\textsf{inCharge}_{x}(u)],c)\mid c\in\mathcal{C}\\}$.

Item 21 is performed when $u$ is a leaf of the tree $S(x_{i}^{j})$, in
particular it is the exit vertex of $G[x_{i+1}(u)]$ and
$\textsf{inCharge}_{x}(u)=G[x_{i+1}(u)]$. As in Section 5 we check that
$\textsf{class}_{i}^{j}(u)=h_{i+1}(u)$. We also check that
$\textsf{weightService}^{j}_{i}(u)=\textsf{weight}_{i+1}(u)$ and
$\textsf{MaxWService}^{j}_{i}=\textsf{MaxW}_{i+1}(u)$.

Recall that, for vertex $u$, $\textsf{children}_{i}^{j}(u)$ denotes the set of
nodes $w\in V$ such that ${\textsf{parent}_{i}^{j}(w)=u}$, and this set is
known to $u$. In particular
$\textsf{inCharge}_{x}(u)=\parallel_{w\in\textsf{children}_{i}^{j}(u)}\textsf{inCharge}_{x}(w)$.
In particular
$\textsf{inCharge}_{x}(u)=\cup_{w\in\textsf{children}_{i}^{j}(u)}\textsf{inCharge}_{x}(w)$.

Item 23 This verification occurs when $\textsf{children}_{i}^{j}(u)$ has a
unique node $w$. Besides the verification that
$\textsf{class}_{i}^{j}(u)=\textsf{class}_{i}^{j}(w)$ we also check that
$\textsf{weightService}^{j}_{i}(u)=\textsf{weightService}^{j}_{i}(w)$ and
$\textsf{MaxWService}^{j}_{i}(u)=\textsf{MaxWService}^{j}_{i}(w)$.