# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 2 Preliminaries
### Program Design Model  
We define a program in terms of its states and transitions. Intuitively, the state space of a program represents the set of all possible states that a program can be in. On the other hand, transitions specify how the program moves from one state to another. **Definition 1** (Program). : _A program \(p\) is a tuple \(\langle S_{p},\delta_{p}\rangle\) where \(S_{p}\) is the state space of program \(p\) and \(\delta_{p}\subseteq S_{p}\times S_{p}\)._  
In addition to program transitions, the state of a program may change due to the environment where the program is running. Instead of modeling the environment in terms of concepts such as variables that are written by program and variables that are written by the environment, we use a more general approach which models it as a set of transitions that is a subset of \(S_{p}\times S_{p}\). **Definition 2** (Environment). : _An environment \(\delta_{e}\) for program \(p\), is defined as a subset of \(S_{p}\times S_{p}\)._  
Our algorithms assume that from any state in the state space of a program \(p\) in an environment \(\delta_{e}\), there is at least one transition in \(\delta_{p}\cup\delta_{e}\). If there is no transition from state \(s_{0}\) in \(\delta_{p}\cup\delta_{e}\) of the given program, we add the self-loop transition \((s_{0},s_{0})\) to \(\delta_{p}\). We note that this assumption is not restrictive. Instead, it is made to simplify subsequent definitions, since we do not need to concern with _terminating computations_ separately. We refer to a subset of states of a program by a state predicate. Thus, we have  
**Definition 3** (State Predicate). : _A state predicate of \(p\) is any subset of \(S_{p}\)._  
Note that we can represent a state predicate by either a subset of states or a predicate. Thus, there is a correspondence between a state predicate and subset of states where the state predicate is true. For example, state predicate \(True\) is a subset that includes all states of a program and \(False\) is an empty set. Similarly, the negation of a state predicate is the set of states where the given state predicate is false. We say a state predicate is closed in a set of transitions if no transition in the set leaves the state predicate. **Definition 4** (Closure). : _A state predicate \(S\) is closed in a set of transitions \(\delta\) iff \((\forall(s_{0},s_{1}):(s_{0},s_{1})\in\delta:(s_{0}\in S\Rightarrow s_{1}\in S ))\). (We use \(Qx:D(x):P(x)\) to specify a formula where \(Qx\) is a quantifier that is instantiated to be \(\forall x\) or \(\exists x\), \(D(x)\) is a domain where \(x\) can come from and \(P(x)\) is predicate over \(x\). When there is no restriction on the domain, we use \(Q::P\). For example, '\(\exists x:x\) is odd: \(x\) is prime' states that there exists an \(x\) in \(\{1,3,5,\cdots\}\) that is a prime. )_  
**Definition 5** (Projection). : _The projection of a set of transition \(\delta\) on state predicate \(S\), denoted as \(\delta|S\), is set \(\{(s_{0},s_{1}):(s_{0},s_{1})\in\delta\wedge s_{0},s_{1}\in S\}\rangle\). In other words, \(\delta|S\) consists of transitions of \(\delta\) that start at \(S\) and end in \(S\)._  
A computation of a program in an environment is a sequence of states that starts in an initial state and in each state executes either a program transition or an environment transition. Moreover, after an environment transition executes, the program is given a chance to execute in the next \(k-1\) steps. However, whenever in a state no program transition is available, an environment transition can execute. **Definition 6** (\(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\) and \(k\) be an integer greater than 1.