diff --git a/Writing/THESIS_PROPOSAL/3-research-approach/v2.tex b/Writing/THESIS_PROPOSAL/3-research-approach/v2.tex
index efac6a109..dc1d06d53 100644
--- a/Writing/THESIS_PROPOSAL/3-research-approach/v2.tex
+++ b/Writing/THESIS_PROPOSAL/3-research-approach/v2.tex
@@ -111,8 +111,8 @@ So, what's the solution?
 
     There is no outstanding way to build HAHACS. This methodology provides a
     basis for systems engineers to think about the components of a HAHACS as
-    interlocking pieces whos verification interlinks into a broader system. This
-    will also motivate the adoption of temporal logic to define autonomous
+    interlocking pieces whos verification interlinks into a broader system.
+    This will also motivate the adoption of temporal logic to define autonomous
     control systems, by allowing a close connection and tracability between
     requirements from regulations to system specifications.
 
@@ -120,6 +120,107 @@ So, what's the solution?
 
 }
 
+Some thoughts on invariants, and how they fit here: There are several types of
+safety invariants that HAHACS might have. 
+
+1. Conditions that initiate a switch between control modes (reactiive synthesis
+relevant) 
+
+2. Invariants about the stability of discrete states (barrier certificates) 
+
+3. Invariants ensuring the transition between discrete states (reachability) 
+
+4. Invariants about the timeliness of discrete transitions (??? Reachability?)
+
+How do we reason about all of these invariants. Well, fundamentally they can
+all be reasoned about with temporal logic statements. Using next and eventually
+operators, we can get to the fundamental behavior of all of these modes. What's
+challenging is the fact that we ensure that all of these specifications are
+validated differs between the type of invariant. This is really the beauty of
+this approach, and the intellectual merit. This proposal provides a way for
+hybrid control systems to be verified for autonomous control systems by
+diversifying the way that the invariants are checked. 
+
+Reactive synthesis helps us build discrete controllers using specifications
+that have conditons that don't depend on time. These invariants generally are
+strategic decisions, such as changing between operating modes, initiating power
+level changes, or perhaps doing a refueling or shutdown routine. These
+specifications are able to be nearly directly drawn from operating procedures,
+and should be closely tied to instructions that would be used for human
+operators. They have checkpoints for the continuous system in between different
+control implements. An example is, raise power at a certain rate while ensure
+temperature remains between certain bounds. These conditions are physical
+states, but they are a binary result. The condition is really binary, desipite
+perhaps having units of celsius or %power. When we build discrete controllers
+from these specifications, we get the validation of the controller of these
+specs for free by nature of reactive synthesis tools. We get direct
+traceability from the operating procedure to the discrete controller
+implementation with minimal human effort.
+
+That being said, there are no free lunches here. Ultimately, we're controlling
+physical systems, and while we can automate the controller building between
+stratgic objectives, it is not trivial to do so for the controller of the
+physical process. These controllers are going to have to be built manually,
+with the continuous dynamics of the system in mind. Helpfully, if
+specifications are complete first, one can obtain discrete controller before
+building physical controllers. The result of this is a simplification of
+controller design, becuase the operational goals of each continuous controller
+is clearly outlined by the invariants that define the goal of each discrete
+mode. While for reactive synthesis purposes conditions such as a certain
+temperature being reached or power level attained are binary variables, the
+continuous physical meaning becomes important in the design and analysis of the
+physical controllers. The continuous value of these conditions becomes the goal
+of the continuous controller design, while also providing a basis to check
+controller performance.
+
+To check continuous controllers are valid, we can split continuous controller
+objectives into two types. First, we have continuous controllers that are
+designed to move the plant between two different discrete modes. These will be
+called 'transitory' controllers, because their entire purpose is to transition
+the plant betweeen between discrete control modes. Because of the specification
+of the hybrid control system a priori, we will have defined what the invariants
+of these transitions are in continuous state space. Then, once a continuosu
+controller design is developed, it can be validated using reachability
+analysis. The input set for the analysis is the possible states that enter this
+transitory mode, while the reachable states must be entirely contained within
+the exit invariant for the controller to pass. At the time of writing this
+proposal, it is not clear what the most efficient way to obetain this
+continuous controller is, but is generally beyond the scope of this work. It is
+assumed that they generally won't be so difficult to find for most systems, as
+the refinement of the discrete controller should simplify the control
+objectives of the physical controllers significantly.
+
+The second type of continuous controller that may be utilized in a HAHAHCS is a
+controller that tries to maintaine a continuous steady state, such that no
+discrete transitions are triggered. Reachability on these systems may not prove
+a prudent approach to validating this behavior for a candidate continuous
+controller, and instead, barrier certificates must be used. Barrier
+certificates analyze the dynamics of the system to say whether or not flux
+across a given boudnary exists. That is to say that they evaluate whether or
+not there is a trajectory or not that leaves a given boundary. This definition
+is exactly what defines the validity of a stabilizing continuous control mode.
+Once again, because the design of the discrete controller defines careful
+boundaries in continuous state space, the barrier is known a priori of which we
+must satisfy this condition. This will eliminate the search for such a barrier,
+and minimze complicatoin in validating stabilizing continuous control modes.
+
+Finally, consideration must be paid for when errors occur. The validation of
+these continuous control modes hinges upon having an assumption ofcorrect
+model, which in the case of a mechanical failure will almsot certainly be
+invalidated. Special continuous controllers for these conditions must be
+created, called 'explusory' control modes. These controllers will be
+responsible for ensuring safety in case of failure, and will be designed with
+reachability, but in this case, additional allocation for the allowing of
+physical parameters will be allowed in the analysis. Traditional safety
+analysis will also be used to identify potential failure modes, and the
+modelling of their worst case dynamics. The HAHCS will be able to idenfity why
+such a fault occors because an discrte boundary condition will be violated by
+the continuous physical controller. That is to say, since we will have
+validated the continuous control modes using reachability and barrier
+certificates a priori, we will know with certainty that the only room for
+dynamics to change is a shift in the plant dynamics, not that of the proven
+controller.
+
 \fi