Stabilizing Nodes from an Anchor


I got this problem from Rustan Leino, who got it from Jay Misra, who had received it from Edsger Dijkstra. This particular description of the problem borrows from a description given by Michael Jackson.

I solved it and wrote up my solution.


In a finite, undirected, connected graph, an integer variable $v(n)$ is associated with each node $n$. One node is distinguished as the anchor. An operation $\mathsf{OP}(n)$ is defined on nodes, as follows.

$\mathsf{OP}(n)$: If node $n$ is the anchor, then do nothing; otherwise, set $v(n)$ to the value $1 + \mbox{min}\{v(m)\},$ where $m$ ranges over all neighbors of $n$ that are distinct from $n.$

An infinite sequence of operations $\langle \mathsf{OP}(n), \mathsf{OP}(m), \ldots \rangle$ is executed, the node arguments $n$, $m$, ... for the operations being chosen arbitrarily and not necessarily fairly. Show that eventually all $v(n)$ stabilize. That is, that after some finite prefix of the infinite sequence of operations, no further operation changes $v(n)$ for any node $n.$

Solution     Reveal