# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 2 Preliminaries
### Faults and Fault-Tolerance  
Like environment transitions, we define a class of faults for a program as a set of transitions that may change the state of the program:  
**Definition 12** (Fault). : _A class of faults \(f\) for \(p(=\langle S_{p},\delta_{p}\rangle)\) is a subset of \(S_{p}\times S_{p}\)._  
Now, we extend Definition 6 to one that captures the computation of a program in presence of fault transitions:  
**Definition 13** (\(p[]_{k}\delta_{e}[]\)_computation). : _Let \(p\) be a program with state space \(S_{p}\) and transitions \(\delta_{p}\). Let \(\delta_{e}\) be an environment for program \(p\), \(k\) be an integer greater than \(1\) and \(f\) be the set of faults for program \(p\). We say that a sequence \(\sigma=\langle s_{0},s_{1},s_{2},...\rangle\) is a \(p[]_{k}\delta_{e}[]\) computation iff_  
* \(\forall i:i\geq 0:s_{i}\in S_{p}\)_, and_
* \(\forall i:i\geq 0:(s_{i},s_{i+1})\in\delta_{p}\cup\delta_{e}\cup f\)_, and_
* \(\forall i:i\geq 0:(s_{i},s_{i+1})\in\delta_{e}\Rightarrow\)__\(\forall l:i<l<i+k:(\exists\delta_{l}^{\prime}::(s_{l},s_{l}^{\prime})\in \delta_{p}\Rightarrow(s_{l},s_{l+1})\in(\delta_{p}\cup f))\)_, and_
* \(\exists n:n\geq 0:(\forall j:j>n:(s_{j-1},s_{j})\in(\delta_{p}\cup\delta_{e}))\)_._  
Note that in the above definition, we require that fault transitions finally stop occurring. This captures the transient nature of faults. On the other hand, environment transitions keep occurring forever. Fault transitions can perturb the program by arbitrarily changing its state. The definition of fault-span captures the boundary up to which the program could be perturbed by faults. Thus,  
**Definition 14** (Fault-span). : _The state predicate \(T\) is a \(k\)-\(f\)-span of \(p\) from \(S\) in environment \(\delta_{e}\) iff_  
* \(S\Rightarrow T\)_, and__for every \(p[]_{k}\delta_{e}[]f\) computation \(\langle s_{0},s_{1},s_{2},\ldots\rangle\), where \(s_{0}\in S\), \(\forall i:s_{i}\in T\)._  
Next, we define the notion of fault-tolerance. We consider two different types of fault-tolerance namely failsafe and masking fault-tolerance. A failsafe fault-tolerance ensures that the safety property of the desired specification (cf. Definition 9) is not violated even if faults occur. In other words, we have  
**Definition 15** (Failsafe fault-tolerance). : _Program \(p\) is failsafe \(k\)-\(f\)-tolerant to specification spec (=\(\langle Sf,Lv\rangle\)) from \(S\) in environment \(\delta_{e}\) iff the following two conditions hold:_  
* \(p\) _k-satisfies spec from_ \(S\) _in environment_ \(\delta_{e}\) _and_
* _any prefix of any_ \(p[]_{k}\delta_{e}[]f\) _computation that starts from_ \(S\) _satisfies_ \(Sf\)_._  
Masking fault-tolerance is stronger than failsafe fault-tolerance, as in addition to satisfying the safety property, masking fault-tolerance requires recovery to the invariant. Specifically,  
**Definition 16** (Masking fault-tolerance). : \(p\) _is masking \(k\)-\(f\)-tolerant to specification spec from \(S\) in environment \(\delta_{e}\) iff the following two conditions hold:_  
* \(p\) _is failsafe_ \(k\)_-\(f\)-tolerant to spec (=_\(\langle Sf,Lv\rangle\)_) from_ \(S\) _in environment_ \(\delta_{e}\) _and_
* _there exists_ \(T\) _such that (1)_ \(T\) _is an_ \(k\)_-_\(f\)_-span of_ \(p\) _from_ \(S\) _in environment_ \(\delta_{e}\) _and (2) for every_ \(p[]_{k}\delta_{e}[]f\) _computation_ \(\sigma(=\langle s_{0},s_{1},s_{2},\ldots\rangle)\) _that starts from a state in_ \(S\)_, for any_ \(i\) _such that_ \(s_{i}\in T\)_, then there exists_ \(j\geq i\) _such that_ \(s_{j}\in S\)_._  
The second constraint in Definition 16 simply means that in any computation that starts at \(T\) must go to \(S\). We also define the notion of stabilizing programs. We extend the definition from References [7] and [8] for a program in the presence of environment actions. **Definition 17** (Stabilization).