# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 3 Addition of Stabilization
### Soundness, Completeness and Complexity Results  
In this Section, we show that Algorithm 1 is sound and complete and its time complexity is polynomial in the size of the state space. **Soundness**: First, we show that Algorithm 1 is sound, that is, if it finds a solution, the solution satisfies the problem statement for adding stabilization provided in Section 3.1. Based on the notion of fairness for program transitions, we introduce the notion of whether an environment transition can execute in a given computation prefix. An environment transition can execute in a computation prefix if an environment transition exists in the last state of the prefix and either (1) there are no program transitions starting from the last state of the prefix or (2) the last \(k-1\) transitions of the prefix are program transitions. **Definition 18** (Environment-enabled). : _In any prefix of any \(p[]_{k}\delta_{e}\) computation \(\sigma=\langle s_{0},s_{1},\ldots,s_{i}\rangle\), \(s_{i}\) is an environment-enabled state iff \((\exists s::(s_{i},s)\in\delta_{e})\wedge\)\(\Big{(}\big{(}\
exists(s_{i},s^{\prime})::(s_{i},s^{\prime})\in\delta_{p} \big{)}\vee\)\(\big{(}\
exists j:j>i-k:(s_{j},s_{j+1})\in\delta_{e}\big{)}\Big{)}\)._  
The following lemma focuses on the recovery to \(S\) from states in \(R\):  
**Lemma 1**. : _Any \(p^{\prime}[]_{k}\delta_{e}\) computation that starts from a state in \(R\), contains a state in \(S\)._  
Proof. : We prove this by induction. **Base case**: \(R=S\). The statement is satisfied trivially. **Induction hypothesis**: Theorem holds for the current set of \(R\). **Induction step**: We show when we add a state to \(R\), the theorem still hold for \(R\). A state \(s_{0}\) is added to \(R\) in two cases:  
Figure 3: Illustration of how \(R\) expands in Algorithm 1. **Case 1** (\(\
exists_{2}:s_{2}\in\
eg(R\cup R_{p}):(s_{0},s_{2})\in\delta_{e}\)) \(\land\) (\(\exists s_{1}:s_{1}\in(R\cup R_{p}):(s_{0},s_{1})\in\delta_{e}\))  
Since there is no \(s_{2}\) in \(\
eg(R\cup R_{p})\) such that \((s_{0},s_{2})\in\delta_{e}\), for every \((s_{0},s_{1})\in\delta_{e}\), \(s_{1}\) is in \(R\cup R_{p}\). In addition, we know that there is at least one \(s_{1}\) in \(R\cup R_{p}\) such that \((s_{0},s_{1})\in\delta_{e}\). By the construction of \(R_{p}\), we know that if \(s_{1}\) is in \(R_{p}\), there is a program transition from \(s_{1}\) to a state in \(R\). Since \((s_{0},s_{1})\in\delta_{e}\) and because of the fairness assumption, the program can occur and reach \(R\). Thus, every computation starting from \(s_{0}\) has a state in \(R\). Since we do not change the set of transitions of states in \(R\) of the previous iteration, the set of computations starting from any state in \(R\) is unchanged. Thus, based on the induction hypothesis, every computation starting from \(s_{0}\) has a state in \(S\). **Case 2**\(\
exists_{2}:s_{2}\in\
eg(R\cup R_{p}):(s_{0},s_{2})\in\delta_{e}\wedge s_{0} \in R_{p}\)  
Since there is no \(s_{2}\) in \(\
eg(R\cup R_{p})\) such that \((s_{0},s_{2})\in\delta_{e}\), for every \((s_{0},s_{1})\in\delta_{e}\), \(s_{1}\) is either in \(R\) or \(R_{p}\). In addition, we know that there is at least one state \(s_{3}\) in \(R\) such that \((s_{0},s_{3})\in\delta_{p}\). In any \(p^{\prime}\|_{k}\delta_{e}\) computation starting from \(s_{0}\) if \((s_{0},s_{1})\in\delta^{\prime}_{p}\) then \(s_{1}\in R\). If \((s_{0},s_{1})\in\delta_{e}\) then \(s_{1}\in R\cup R_{p}\). By construction of \(R_{p}\), we know that if \(s_{1}\) is in \(R_{p}\), there is a program transition from \(s_{1}\) to a state in \(R\). Since \((s_{0},s_{1})\in\delta_{e}\) and because of the fairness assumption, program can reach \(R\). Thus, every computation starting from \(s_{0}\) has a state in \(R\). Since we do not change the set of transitions of states in \(R\) of the previous iteration, the set of computations starting from any state in \(R\) is unchanged. Thus, based on the induction hypothesis, every computation starting from \(s_{0}\) has a state in \(S\). **Theorem 1**. : _Algorithm 1 is sound._  
Proof.