\section{Research Approach}
\iffalse

  HACS: hybrid autonomous control system
  HAHACS: High-Assurance Hybrid AUtonomous Control System


The research approach here needs to clearly outline the solution the the problem
and identify the actions taken that will advance knowledge and solve the
problem.

First, what is the problem? 

\textit{ 

  Inhibition to adopt hybrid autonomous control in critical infrastructure is
  rooted in safety concerns of system stability. Without a human in the loop
  with general intelligence, HACS have not been trusted where failure modes can
  be unique and novel.

}

So, what's the solution?

\textit{

  This research approach develops a methodology to build HACS that are provably
  safe. This methodology builds on existing technologies, and unifies different
  research thrusts to build a complete hybrid control system. To do this, the
  problem of a HAHCS is broken into three distinct pieces:

  \begin{enumerate}

    \item System specification: properties of the HAHaCS such as transition
      between control modes and system invariants are specified using a formal
      methods tool. 
        - This provides exact behavior
        - allows realizabillity checking of controller specs. Can a controller
        actually be built from these specs?
        - ?
        - ?

    \item Discrete Behavior Synthesis: The discrete component of the controller
      is synthesized directly from system specifications using reactive
      synthesis.
        - This ELIMINATES wholesale the possibility of introducing logical bugs
        in the creation of the strategic part of the HAHCS. Critical decisions
        that are normally made by a human are automated directly from the
        formal specifications.
        - This does two critical things:
          - It makes the creation of the controller tractable. The reasons the
          controller changes between modes acn be traced back to the
          specification (and thus any requirements), which is a trace for
          liability and justification of system behavior
          - Discrete control decisions made by humans are reliant on the human
          operator operating correctly. Humans are intrinsically probabalistic
          creatures who cannot eliminate human error. By defining the behavior
          of this system using temporal logics and synthesizing the controller
          using deterministic algorithims, we are assured that strategic
          decisions will always be made as according to operating procedures.

    \item Continuous Behavior Synthesis and Verification: The continuous
      components of the controller are built using existing dynamics and control
      theory but then verified using reachability and barrier certificats.
        - It's very challenging (nigh impossible) to say for certain how to
        build any continuous control mode. That is honestly going to be have to
        left to the specific control system and its objectives. It's not really
        the point of this PhD to say how to do that. For that reason, I'm going
        to assume that controllers between modes are generally possible to
        build. That is to say that there exists a controller that can transition
        between modes, but it is a human hunt to find it.
        - To check if a candidate controller does transition between discrete
        modes, we do two things:
          - Check invariants using reachability. Specifications will require
          that control modes transiiton from one mode to the next, where
          appropriate. When this is the case, these invariants are extracted to
          be checked using reachability. The control mode is given the possible
          entry conditions of the 'entry' mode, and the possible 'exit' states
          are analyzed. A cont. controller passes this reachability test if
          there is no reachable state that is not at the exit condition of the
          state transition. 

          --- This needs flushed out more. I think this can really be clarified
          using entry and exit conditions of Mealy machines. The continuous
          system IS the transition, and the reachabililty test is saying whether
          or not the physical system actually satisfies the entry and exit
          conditions. 

          - Then, for systems that need to STAY within one mode, we will use
          barrier certificates. These can let us define a continuous state
          boundary, and define for a discrete controller state, the total
          controller will NOT leave the continuous boundary.

        - One thing that must be considered is the idea that this analysis is
        predicated on the physical system being correct to the model. If this
        isn't true, we must define continuous modes that catch failure states.
        If transition invariants are violated, we must shut down the system, and
        build safety oriented control modes that we can be sure with a much
        broader set of entry conditions will safely shut down the plant.

      -- Q for dan: is it critical to really have software to namedrop or is it
      better to stay amorphous on the technology? Iirc Manyu did a little bit of
      both.

  \end{enumerate}


  What's the intellectual merit?

  \textit{

    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
    control systems, by allowing a close connection and tracability between
    requirements from regulations to system specifications.

  }

}

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