  Topological self-stabilization describes the ability of a distributed system
to let the nodes themselves establish a meaningful overlay network. Independent
from the initial network topology, the system converges to the desired topology
via forwarding, inserting, and deleting links to neighboring nodes.
Name-passing process calculi, like the pi-calculus, are a well-known and widely
used method to model concurrent and distributed algorithms. The pi-calculus is
designed to naturally express processes with a changing link infrastructure, as
the communication between processes may carry information that can be used for
a change in the linkage between the processes. We redesign a simple local
linearization algorithm with asynchronous message-passing that was originally
designed for a shared memory model. We use an extended localized pi-calculus, a
variant of the pi-calculus, to model the algorithm. Subsequently, we formally
prove the self-stabilizing properties closure, weak convergence for every
arbitrary initial configuration, and strong convergence for two special cases.
In our proofs we utilize rather an assertional reasoning than an action-based
style. Furthermore, we describe the challenges in proving (strong) convergence
in the general case. Additionally, we give strong arguments for strong
convergence, supported by further proven lemmata, and discuss different
approaches for a formal proof.
