# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 3 Addition of Stabilization
### Soundness, Completeness and Complexity Results
: We need to show that the constraints of the problem definition are satisfied. At the beginning of the algorithm \(\delta^{\prime}_{p}=\delta_{p}|S\) and all other transitions added to \(\delta^{\prime}_{p}\) in the rest of the algorithm starts outside \(S\). Thus, \(p^{\prime}|S=p|S\) that satisfies the first constraint. The second constraint is satisfied based on Lemma 1 and the fact that \(R\) includes all states. The third constraint is satisfied, as we do not add any transitions in \(\delta_{r}\) to the program. **Completeness**: Next, we focus on showing that Algorithm 1 is complete, that is, if there is a solution that satisfies the problem statement for adding stabilization, Algorithm 1 finds one. The proof of completeness is based on the analysis of states that are not in \(R\) upon termination. Any state that is not in \(R\) at the end of Algorithm 1, either does not have any environment transition, or it has an environment transition that goes to \(\
eg(R\cup R_{p})\). Thus, we note the following observation:  
**Observation 1**. : _For any \(s_{0}\) such that \(s_{0}\
otin R\) and \(\exists s_{1}::(s_{0},s_{1})\in\delta_{e}\), we have \(\exists s_{2}:s_{2}\in\
eg(R\cup R_{p}):(s_{0},s_{2})\in\delta_{e}\)._  
Also, if a state is in \(R_{p}\) but it is not in \(R\), it has an environment transition to \(\
eg(R\cup R_{p})\). **Observation 2**. : _For any \(s_{0}\in\
eg R\cap R_{p}\), \(\exists s_{1}:s_{1}\in\
eg(R\cup R_{p}):(s_{0},s_{1})\in\delta_{e}\)._  
Now, for the rest of our discussion in this section, we assume that Algorithm 1 has returned failure. The following lemma focuses on the situation where a given revision \(p^{\prime\prime}\) reaches a state marked as \(\
eg(R\cup R_{p})\) by Algorithm 1. **Lemma 2**. : _Let \(\delta^{\prime\prime}_{p}\) be any program such that \(\delta^{\prime\prime}_{p}\cap\delta_{r}=\emptyset\). Let \(s_{j}\) be any state in \(\
eg(R\cup R_{p})\) at the end of Algorithm 1. Then, for every \(p^{\prime\prime}\|_{k}\delta_{e}\) prefix \(\alpha=\langle...,s_{j-1},s_{j}\rangle\), there exists suffix \(\beta=\langle s_{j+1},s_{j+2},\ldots\rangle\), such that \(\alpha\beta\) is a \(p^{\prime\prime}[]_{k}\delta_{e}\) computation and one of two conditions below is correct:_  
1. \(s_{j+1}\in\
eg(R\cup R_{p})\)
2. \(s_{j+1}\in(R_{p}-R)\wedge s_{j+2}\in\
eg(R\cup R_{p})\)Proof. : There are two cases for \(s_{j}\):  
**Case 1** If \(s_{j}\) is environment-enabled in prefix \(\alpha=\langle...,s_{j-1},s_{j}\rangle\)  
According to the Observation 1, since \(s_{j}\in\
eg(R\cup R_{p})\), there exists \(s^{\prime\prime}\in\
eg(R\cup R_{p})\) such that \((s_{j},s^{\prime\prime})\in\delta_{e}\). We set \(s_{j+1}=s^{\prime\prime}\). **Case 2** If \(s_{j}\) is not environment-enabled in \(\alpha=\langle...,s_{j-1},s_{j}\rangle\)  
In this case \((s_{j},s_{j+1})\in\delta_{p}\) and as \(s_{j}\in\
eg(R\cup R_{p})\), \(s_{j+1}\in\
eg R\) (otherwise, \(s_{j}\) would be included in \(R_{p}\), as we can reach state \(s_{j+1}\in R\) with a transition which is not in \(\delta_{r}\)). There are two sub-cases for this case:  
**Case 2.1**\(s_{j+1}\in\
eg R_{p}\)  
In this case \(s_{j+1}\in\
eg(R\cup R_{p})\). **Case 2.2**\(s_{j+1}\in R_{p}\)  
As \(s_{j+1}\in\
eg R\cap R_{p}\), according to Observation 2, we have \(\exists s_{2}:s_{2}\in\
eg(R\cup R_{p}):(s_{j+1},s_{2})\in\delta_{e}\). As \((s_{j},s_{j+1})\in\delta_{p}\), even with fairness \((s_{j+1},s_{2})\) can occur. Therefore we set \(s_{j+2}=s_{2}\), that is, \(s_{j+2}\in\
eg(R\cup R_{p})\). From this lemma, we conclude that for any given program \(p^{\prime\prime}\), if a computation ever reaches a state in \(\
eg(R\cup R_{p})\), there is a computation from that state that never reaches \(R\). Specifically, we have the following corollary:  
**Corollary 1**. : _Let \(\delta_{p}^{\prime\prime}\) be any program such that \(\delta_{p}^{\prime\prime}\cap\delta_{r}=\emptyset\). Let \(s_{j}\) be any state in \(\
eg(R\cup R_{p})\) at the end of Algorithm 1.