Thesis/3-research-approach/v2.tex

\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

%%%%%%%%%% TABLESETTING

% what is a hybrid system really for this proposal
% Define: A hybrid system with continuous state space X ⊆ ℝⁿ and discrete modes Q = {q₁, q₂, ..., qₘ}
% Each discrete mode qᵢ has an associated continuous state region Xᵢ ⊆ X
% The discrete controller manages transitions between modes based on continuous state thresholds

% what are requirements, anyways?

% why do we care about defining the whole hybrid system into requirements?

% How do different requirements line up into different parts of the system?
% (operational vs strategic requirements and their relevance to different parts
% of our system)

Autonomous control systems are fundamentally different from automatic control
systems. The difference between these systems is the level at which
they operate. Automatic control systems are purely operational systems, 

To build a high-assurance hybrid autonomous control system (HAHACS), a
mathematical description of the system must be established. This work will make
use of automata theory while including logical statements and control theory.
The nomenclature and lexicon between these fields is far from homogenous, and
the reviewer of this proposal is not expected to be an expert in all fields
simultaneously. To present the research ideas as clearly as possible in this
section, the following syntax is explained.

A hybrid system is a dynamical system that has both continuous and discrete
states. The specific type of system discussed in this proposal are continuous
autonomous hybrid  systems. This means that these systems a) do not have
external input \footnote{This is not strictly true in our case because we allow
strategic inputs. For example, a remote powerplant may receive a start-up or
shutdown command from a different location, but only this binary high level
input is a strategic input.} and b) continuous states do not change
instantaneously when discrete states change. For our systems of interest, the
continuous states are physical, and are always Lipschitz continuous. This
nomenclature is heavily borrowed from \cite{HANDBOOK ON HYBRID SYSTEMS CONTROL},
but is redefined here for convenience:

\begin{equation}
  H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \mathcal{R}, Inv)
\end{equation}

where:

\begin{itemize}
  \item \( \mathcal{Q}\): is the discrete states of the system
  \item \( \mathcal{X}\): is the continuous states of the system
  \item \(\mathbf{f}: \mathcal{Q} \times \mathbb{R} \rightarrow \mathbb{R} \), where
    \(\mathbf{f}_i\) is a
    vector field that defines the continuous dynamics for each \(q_i\)
  \item \(Init\): the initial states of \(q\) and \(x\)
  \item \( G\): guard
    conditions that define when discrete state transitions occur
  \item \(\delta: \mathcal{Q} \times G \rightarrow \mathcal{Q}\), are the
    discrete state transition functions
  \item \mathcal{R}: Reset maps that define state 'jumps'
  \item \(Inv\): Safety invariants on the continuous dynamics
\end{itemize}

The creation of a HAHACS essentially boils down to the creation of such a tuple
where there are proof artifacts that the intended behavior of the control system
are satisfied by the actual implementation of the control systems. But to create
such a HAHACS, we must first completely describe its behavior.

%% Brief discussion on what each part of this tuple means for us

\subsection{System Requirement and Specifications}

Temporal logic is a powerful set of semantics to build systems that can have
complex but deterministic behavior. 


%%%%%%%%%%% Building discrete controllers

% Buildout of requirements from written procedures (this is easy for critical
% systems - we already have the requirements)

% What happens to the invariants that specify a continuous space? Save em for
% later. Here they become binary for our purposes
% KEY POINT: We don't IMPOSE discrete abstraction - we FORMALIZE existing practice
% Operating procedures (esp. nuclear) already define go/no-go conditions as discrete predicates
% e.g., "WHEN coolant temp >315°C AND pressurizer level 30-60% THEN MAY initiate load following"
% These thresholds come from design-basis safety analysis, validated over decades
% Our methodology assumes this domain knowledge exists and provides formalization framework
% The discrete predicates p₁, p₂, ... are Boolean functions over continuous state: pᵢ: X → {true, false}
% Q: How do we rigorously set thresholds for continuous→discrete abstraction?
% Q: How do we handle hysteresis to prevent mode chattering near boundaries?
% Q: How do we account for sensor noise and measurement uncertainty?
% Q: How do we handle numerical precision issues when creating discrete automata? (relates to task 36)

% Discrete controller implementation can be realized with reactive synthesis. 
% LTL specs to automata

% talk a bit about tools here like FRET. Talk about previous attempts.

Human control of nuclear power can be divided into three different scopes:
strategic, operational, and tactical. Strategic control is the high-level and
long term decision making for the plant. This level has objectives that are
complex and economic in scale, such as managing labor needs and supply chains to
optimize sheduled maintenence and downtime. The time scale on this level of
control is long, often over months or years. The lowest level of control is the
tactical level. This is the individual control of pumps, turbines, and
chemistry of the plant. This level of control has already been somewhat
automated today in nuclear power, and is generally considered 'automatic
control' when autonomous. These controls are almost always continuous systems,
and have a direct impact on the physical state of the plant. Tactical control
objectives are things like maintaining a pressurizer level, maintaining a
certain core temperature, or adjusting reactivity with a chemical shim. The level of
control linking these two levels, then, is the operational control scope.
Operational control is the primary responsibility of human operators today.
Operational control takes the current strategic objective, and implements
tactical control objectives to drive the plant towards strategic goals. In this
way, it is the bridge between high and low level goals. A strategic goal may be
to perform refueling at a certain time, while the tactical level of the plant
currently is focused on mainting a certain core temperature. The operational
level is what issues the shutdown procedure of the plant, using several smaller
tactical goals along the way to achieve this objective. Thus, the combination of
the operational and tactical level of the plant fundamentally forms a hybrid
controller. The tactical level is the continuous evolution of the plant
according to the control input and control law, while the operational level is a
discrete state evolution which determines the tactical control law to reach
different operational states.

This operational control level is the main reason for the requirement of human
opeartors in nuclear control today. The hybrid nature of this control system
makes it difficult to prove that a controller will perform according to the
strategic requirements, as the infrastructure to build hybrid systems today
dooes not exist. Humans have been used for this layer because the general
intelleigence of humans has be relied upon as a safe way to manage the hybrid
nature of this system. But, these operators are using prescriptive operating
manuals to perform their control with strict procedures on what control to
implement at a given time. These procedures are the key to the operational
control scope.

The method of constructing a HAHACS in this proposal leverages two key points of
the way this control scope is done today: first, the operational scope control
is effectively discrete control. Second, the rules of implementing this control
are described a priori to their implementation in operating procedures. We can
make great use of these facts by formalizing the rules for transitioning between
discrete states. To do this, we will use temporal logic to formalize discrete
switching behavior. 

Temporal logic is a rich syntax that allows for the definition of logical
calculations including time related bounds. For this reason, we can make
statements relating discrete control modes to one another. Using temporal logic,
we can effectively describe all of the requirements of a HAHACS. The guard
conditions \(G\) are easily defined by determining boundary conditions between
discrete states and defining their behavior, while continuous mode invariants
can be defined using temporal logic statements as well. These form the basis of
any proofs about a HAHACS, and are the fundamental 'truth' statements about what
the behavior of the system is designed to be.

To build these temporal logic statements, an intermediary tool called FRET is
planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
was designed by NASA to build high assurance timed systems. FRET is an
intermediarly language between temporal logic and natural language that allows
for rigid definitions of temporal behvarior while using a logic-novice friendly
syntax. This benefit is crucial for the feasibility of this methodology for
industry, as minimizing the barrier to formal methods is a critical component of
their scucess. By reducing the expert knowledge required to use these tools,
their adoption with current workforce becomes easier. 

A key feature of FRET is the ability to start with logically imprecise
statements and consecutively refine them into a well-posited specification. We
can use this to our advantage by directly dumping in operating procedures and
design requirements into FRET in natural language, and iteratively refining them
into the specifications for a HAHACS. This has two distinct but important
benefits. First, it allows us to draw a direct link from the design
documentation to the digital system implementation. Second, it clearly
demonstrates where the natural language documents are insufficient. These
procedures may still be used by human operators, so any wiggle room for
interpretation is a weakness that must be addressed.

%Talk about how we go from temp logic to reactive synth. Metnion fret can
%export, or naturlly support reactive synth solver ltlsynt, a sota react synth
%solver

% talk about what the benefits of reactive synth are. Proof chain, machine
% checkable, blah blah blah

%%%%%%%%%%%% Building continuous controllers

% The whole point of a hybrid system is that there are continuous components
% underneath the digital system. We built the discrete like the physical doesn't
% exist, but it really does. So how do we capture the physical system too?

% SCOPE FRAMING: This methodology VERIFIES continuous controllers, not SYNTHESIZES them
% Compare to model checking: doesn't tell you HOW to design software, verifies if it satisfies specs
% We assume controllers can be designed using standard control theory techniques
% Our contribution: verification that candidate controllers compose correctly with discrete layer

% What are the main different kinds of continuous modes we may see?
% Mathematical structure: Each discrete mode qᵢ provides three key pieces of information:
% 1. Entry conditions: X_entry,i ⊆ X (initial state set)
% 2. Exit conditions: X_exit,i ⊆ X (target state set)
% 3. Invariants: X_safe,i ⊆ X (safety envelope during operation)
% These come from the discrete controller synthesis and define objectives for continuous control
% Q: Who designs the continuous controllers and how? This methodology verifies
% them, but doesn't synthesize them. Is this a scope problem?

%%%%%% Transitory modes

% entry and exit conditions
% the goal is getting from one physical state to another
% MATHEMATICAL FORMULATION:
% Control objective: reach(X_entry,i) → reach(X_exit,i) while maintaining x(t) ∈ X_safe,i
% Standard control techniques (LQR, MPC, trajectory optimization) applied with these constraints
%
% VERIFICATION: Reachability analysis confirms ALL trajectories starting in X_entry,i
% reach X_exit,i without violating X_safe,i
% Formally: Reach(X_entry,i, f(x,u), T) ⊆ X_exit,i ∪ X_safe,i
% where f(x,u) is the closed-loop continuous dynamics
%
% we have the physical requirements from earlier specifications. Here we use
% them in a reachability analysis. This time, we use the actual physical values
% instead of the binary yes/no we used for discrete
% Q: How do we verify timing constraints? If a transitory controller eventually
% reaches the exit condition but takes too long, that violates safety. Timed
% automata? Timed reachability?
% Q: Should formalize the Mealy machine perspective - continuous system IS the
% transition, and entry/exit conditions are the discrete states. This could be
% a unifying conceptual framework.

%%%%%% stabilizing modes

% these are control modes with an objective of KEEPING a certain discrete state
% stable
%
% MATHEMATICAL FORMULATION:
% Control objective: remain(X_target,i) where X_target,i ⊂ X_safe,i
% Standard feedback control (PID, state feedback, LQG) applied to maintain equilibrium
%
% VERIFICATION: Barrier certificates prove closed-loop dynamics cannot escape X_safe,i
% Formally: Find B(x) s.t. ∇B(x)·f(x,u) ≤ 0 for all x ∈ ∂X_safe,i
% This proves no trajectory can cross the boundary (no flux out of safety region)
%
% we also have the physical requirements for this. These can be used for barrier
% certificates. We can prove that our model won't leave a given area without
% some disturbance. 

%%%%%% expulsory modes
% I've made an implicit assumption when talking about transitory and stabilizing
% modes. That our model is correct. This might not be true

% In the case of a failure, our model will almost certainly be incorrect. For
% this, we have to build safe shutdown modes too, since a human won't be in the
% loop to shut things down.
%
% MATHEMATICAL FORMULATION:
% Control objective: reach(X_current) → reach(X_safe_shutdown) under parameter uncertainty
% where X_current may be anywhere in X (worst-case entry conditions)
% Dynamics have parametric uncertainty: f(x,u,θ) where θ ∈ Θ_failure
%
% VERIFICATION: Parametric reachability analysis with robustness margins
% Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure
% Conservative bounds on Θ_failure come from FMEA/traditional safety analysis

% WE can detect physical failures exist because our physical controllers have
% previously been proven as correct by reachability and barrier certificates. We
% KNOW our controller cannot be incorrect for the plant, so if an invariant is
% violated, we KNOW it's the plant that has changed.
% Q: What about sensor failures (wrong readings vs actual plant failure)?
% Q: What about unmodeled disturbances that aren't failures?
% Q: What if model uncertainty was too optimistic to begin with?
% Need to be more precise about what "model failure" means and detect-ability. 

% We do this using continuous modes that shutdown the system, and using
% reachability analysis with parametric uncertainty, we can prove for a range of
% error conditions we can maintain safe shutdown.
% Q: How much parametric uncertainty is enough? How do we determine bounds for
% worst-case failure dynamics? Need methodology for this.

%%%%%%%%%%%% Implementation with industrial partnerships
%%%%%%% Emerson
%talk about this
% ovation system
% scenic? Is that what they call it?
% ripe partnership with Westinghouse
% Likely build a model with a ccng plant. They already have sophisticated models
% of them
% build controller with simplified model, then test with high fidelity digital
% twin




%
%%%%%%%%%%