We present a self-stabilizing algorithm for the unison problem which is efficient in time, workload, and space in a weak model. Precisely, our algorithm is defined in the atomic-state model and works in anonymous asynchronous connected networks in which even local ports are unlabeled. It makes no assumption on the daemon and thus stabilizes under the weakest one: the distributed unfair daemon. In an n-node network of diameter D and assuming the knowledge B ≥ 2D+2, our algorithm only requires Θ(log(B)) bits per node and is fully polynomial as it stabilizes in at most 2D+2 rounds and O(min(n²B, n³)) moves. In particular, it is the first self-stabilizing unison for arbitrary asynchronous anonymous networks achieving an asymptotically optimal stabilization time in rounds using a bounded memory at each node. Furthermore, we show that our solution can be used to efficiently simulate synchronous self-stabilizing algorithms in asynchronous environments. For example, this simulation allows us to design a new state-of-the-art algorithm solving both the leader election and the BFS (Breadth-First Search) spanning tree construction in any identified connected network which, to the best of our knowledge, beats all existing solutions in the literature.

Distributed systems are ubiquitous, and their distributed nature make them particularly vulnerable to faults. Being able to automatically recover from these faults is of utmost importance, and self-stabilization is a general and lightweight approach to tackle this problem. However, fully asynchronous self-stabilizing algorithms (FASS) are notoriously difficult to design and prove. It thus makes sense to create and prove a transformer that turns synchronous algorithms into FASSes.

A proof-labeling scheme (PLS) for a boolean predicate Π on labeled graphs is a mechanism used for certifying the legality with respect to Π 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 MSO₂ property Π on labeled graphs, there exists a PLS for Π 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² 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 MSO₁ property Π on labeled graphs, there exists a PLS for Π with O(log² 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₄-free graphs (a.k.a., cographs) can be done using a PLS with O(log² n)-bit certificates, merely because each of these two classes can be specified in MSO₁. In fact, we show that certifying P₄-free graphs can be done with certificates on O(log n) bits only. This is in contrast to the class of C₄-free graphs (which does not have bounded clique-width) which requires Ω̃(√n)-bit certificates.