# Automatic Addition of Fault-Tolerance in Presence of Unchangeable Environment Actions +
## 1 Introduction  
Model repair is the problem of revising an existing model/program so that it satisfies new properties while preserving existing properties. It is desirable in several contexts such as when an existing program needs to be deployed in a new setting or to repair bugs. Model repair for fault-tolerance enables one to separate the fault-tolerance and functionality so that the designer can focus on the functionality of the program and utilize automated techniques for adding fault-tolerance. It can also be used to add fault-tolerance against a newly discovered fault. This paper focuses on performing such repair when some actions cannot be removed from the model. We refer to such transitions as unchangeable environment actions. There are several possible reasons for actions being unchangeable. Examples include scenarios where the system consists of several components -some of which are developed in-house and can be repaired and some of which are third-party and cannot be changed. They are also useful in systems such as Cyber-Physical Systems (CPS) where modifying physical components may be very expensive or even impossible. The environment actions differ from fault actions considered in existing work such as [1]. Fault actions are assumed to be temporary in nature and all the previously proposed algorithms to add fault-tolerance in [1] work only with this important assumption that faults finally stop occurring. Unlike fault actions, environment actions can keep occurring. Environment actions also differ from adversary actions considered in [2] or in the context of security intrusions. In particular, the adversaryintends to cause harm to the system. By contrast, environment actions can be collaborative as well. In other words, environment actions are simultaneously collaborative and disruptive. The goal of this work is to identify whether it is possible for the program to be repaired so that it can utilize the assistance provided by the environment while overcoming its disruption. To give an intuition of the role of the environment and the difference between program, environment and fault actions, we present the following examples. **Intuitive examples to illustrate the role of the environment. ** The first intuitive example is motivated by a simple pressure cooker (see Figure 1). The environment (heat source) causes the pressure to increase. In the subsequent discussion, we analyze this pressure cooker when the heat source is always on. There are two mechanisms to decrease the pressure, a vent and an overpressure valve. For the sake of presentation, assume that pressure below 4 is normal. If the pressure increases to 4 or 5, the vent mechanism reduces the pressure by 1 in each step. However, the vent may fail (e.g., if something gets stuck in the vent pipe) and its pressure reduction mechanism becomes disabled. If the pressure reaches 6, the overpressure valve mechanism causes the valve to open resulting in an immediate drop in pressure to be less than 4. We denote the state where the pressure is \(x\) by \(s_{x}\) when the vent is working and by \(fs_{x}\) when the vent has failed. Our goal in the subsequent discussion is to model the pressure cooker as a program and identify an approach for the role of the environment and its interaction with the program so that we can conclude this requirement: _starting_ from _any_ state identified above, the system reaches a state where the pressure is less than 4. Next, we argue that how the role of the environment differs from the role of fault and program actions. In turn, this prevents us from using existing approaches such as Reference [1]. Specifically,  
* Treating the environment as a fault does not work. Faults are assumed to be exceptional events in the system that are expected to stop after some time. By contrast, heat is an essential part of the system that is needed for the system to work.