\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.

  }

}

\fi