# Computing Fault-Containment Times of Self-Stabilizing Algorithms Using Lumped Markov Chains
## 3 System Model  
This paper uses the synchronous model of distributed computing as defined in the standard literature [2; 8; 19]. A distributed system is represented as an undirected graph \(G(V,E)\) where \(V\) is the set of _nodes_ and \(E\subseteq V\times V\) is the set of _edges_. Let \(n=|V|\) and \(\Delta(G)\) denote the maximal degree of \(G\). The topology is assumed to be fixed. If two nodes are connected by an edge, they are called _neighbors_. The set of neighbors of node \(v\) is denoted by \(N(v)\subseteq V\) and \(N[v]=N(v)\cup\{v\}\). Each node stores a set of variables. The values of all variables constitute the _local state_ of a node. Let \(\sigma\) denote the set of possible local states of a node. The _configuration_ of a system is the tuple of all local states of all nodes. \(\Sigma=\sigma^{n}\) denotes the set of global states. A configuration is called _legitimate_ if it conforms with the specification. The set of all legitimate configurations is denoted by \(\mathcal{L}\). Nodes communicate either via locally shared memory or by exchanging messages. In the shared memory model each node executes a protocol consisting of a list of rules of the form _guard_\(\longrightarrow\)_statement_. The guard is a Boolean expression over the variables of the node and its neighbors. The statement consists of a series of commands. A node is called _enabled_ if one of its guards evaluates to true. The execution of a statement is called a _move_. In the message passing model a node performs three actions per round: receiving messages from neighbors, executing code, and sending messages to neighbors. Direct access to the state of neighboring nodes is impossible. Two nodes \(u\) and \(v\) communicate via two link registers: \(u\) writes in its register and \(v\) reads from it and \(v\) writes in its register and \(u\) reads from it. In this model the state of a node also includes the states of its registers. This works assumes the \(\mathcal{CONGEST}\) model of distributed computation [19]. Algorithms in the \(\mathcal{CONGEST}\) model enforce a \(O(\log n)\) limitation on the maximum message size. Hence, with a single message only a constant number of node identifiers in the range \(\{0,\ldots,n\}\) can be transmitted. Execution of the statements is performed in a synchronous style, i.e., all enabled nodes execute their code in every round. An _execution_\(e=\langle c_{0},c_{1},c_{2},\ldots\rangle\), \(c_{i}\in\Sigma\) is a sequence of configurations, where \(c_{0}\) is called the _initial configuration_ and \(c_{i}\) is the configuration after the \(i\)-th round. In other words, if the current configuration is \(c_{i-1}\) and all enabled nodes make a move, then this yields \(c_{i}\). Let \(\mathcal{A}\) be a distributed algorithm and \(\mathcal{L}\subseteq\Sigma\) a set of configurations. \(\mathcal{A}\) is called self-stabilizing with respect to \(\mathcal{L}\) if it satisfies the convergence and closure properties. The first property states that every execution of \(\mathcal{A}\) reaches \(\mathcal{L}\) after a finite number of rounds. The second property states that \(\mathcal{A}(c)\in\mathcal{L}\) for all \(c\in\mathcal{L}\) as long as no fault occurs. The worst case stabilization time \(ST_{\mathcal{A}}(G)\) of \(\mathcal{A}\) for a graph \(G\) is equal to the maximal number of rounds after which \(\mathcal{A}\) reaches a legitimate configuration of \(G\) regardless of the initial configuration under the assumption that no errors occur. Definition 1: A configuration \(c\in\Sigma\) of a self-stabilizing algorithm with respect to \(\mathcal{L}\) is called k-faulty if a configuration \(c^{\prime}\in\Sigma\) satisfying \(\mathcal{L}\) exists such that \(c\) differs from \(c^{\prime}\) in the local states of at most \(k\) nodes. Note that for the message passing model this definition also covers message corruption. This paper analyzes the most common fault situation: 1-faulty configurations. They arise when a single node \(v\) is hit by a memory corruption or a single message sent by \(v\) is corrupted.