\section{State of the art and limits of current practice}

This research will improve our ability to build high assurance autonomous hybrid
control systems by connecting tools from different areas of the scientific
literature. We will combine control and dynamics theory of hybrid systems with
the discrete systems analysis found in the computer science space. These two
fields are disparate, but both approach the problem of high assurance hybrid
systems. First, we will discuss the control theory side. Hybrid systems from a
differential equation perspective will be considered, and comparisons to the
current state of the art of nuclear power control will be discussed. Then, we
will discuss approaches for discrete and hybrid systems from the logical and
computer science perspective. These gap between these two fields is the crux of
the intellectual merit of this research.

\subsection{Control Theory and Hybrid Systems}

Hybrid systems have two components to their behavior. They have continuous
dynamics called 'flow', and have discrete dynamics called 'jumps'. Hybrid
systems can often be described as a set of differential and difference
equations. An hybrid system can be defined as follows:

\begin{align}
  \dot{x}(t) &= f(x(t), q(t), u(t)) \\
  q(k+1) &= \nu(x(k), q(k), u(k))
  \label{eq:hybrid-sys}
\end{align}

In this description there are two functions: \(f(\cdot)\) and
\(\nu(\cdot)\). \(f(\cdot)\) defines the continuous dynamics, while
\(\nu(\cdot)\) defines the discrete dynamics. These functions take three
inputs: the continuous states \(x\), the discrete state \(q\), and an optional
control input \(u\). \(f_i(\cdot)\) here is a nonlinear function, where \(q\)
changes the mode of the continuous dynamics, but is otherwise dependent on the
current continuous states and control input. \(\nu_i(\cdot)\) can be much more
generally created. The only restriction on \(\nu_i(\cdot)\) is that it must
not create an infinite number of jumps in a finite amount of time.
\(\nu_i(\cdot)\) can depend a control input \(u\), or can be
\textit{autonomous}, where the discrete mode is defined by the system states
\(x\) and \(q\). While an autonomous system may not have a control input, that
does not mean the system is not controlled, as the continuous dynamics
\(f_i(\cdot)\) can be constructed such that the system is controlled by the
continuous and discrete states \(x\) and \(q\).
 
The hybrid systems we are most interested in here are \textit{continuous} autonomous
hybrid systems. These systems are hybrid systems whose continuous states \(x\)
do not change during a jump, and do not rely on an external control input. This
research is primarily aimed at control of physical systems whose continuous
states \(x\) are physically required to be continuous across jumps. For example,
a nuclear reactor control rod system may jump from a warm-up ramp control mode to a load
following controller, but the continuous states of the reactor such as
temperature and rod position can not instantaneously change.

Continuous hybrid systems are often constructed by piecing together control
systems for different regions in the state space. This way of building a hybrid
control system is intuitive--controllers are built for local regions with local
objectives. The problem arises when analysis of these local controllers is
generalized to the entire, global, hybrid system. Even in the most simple case
of linear time invariant controller modes, global guarantees of stability can
not be made using linear control theory. Instead, approaches using stitched
networks of Lyapunov functions have been introduced. %CITE CITE CITE%
These Lyapunov functions are difficult to find, but can for some linear switched
hybrid systems provide a way to verification.

Another way of verifying stability of hybrid control systems includes performing
reachability analysis. Reachability is a formal methods tool that uses
abstractifications of a system to determine output ranges of dynamic systems for
a given input. Reachability is not limited to linear systems, and can be
performed on nonlinear systems as well. Reachability for hybrid systems suffers
from two main deficiencies. First, the analysis can take a very long time to
compute. Second, reachability uses approximations. Hybrid systems that have
trajectories of significantly long times can cause problems when using
reachability because either the computation time makes the analysis infeasible,
or the compounding approximation errors makes the analysis meaningless.

\subsection{Formal Methods and Reactive Synthesis}

Hybrid systems often are realized as cyber-physical systems. Cyber-physical
systems have a computational component responsible for control of a physical
process based on live sensors and actuators. Verification of these systems has
drawn two different communities together. We have previously discussed the
engineering perspective coming from the physical control theory background, but
in this section we discuss work coming from the cyber oriented persuasion.

Many cyber systems lend themselves to a finite number of possible states. For
these systems, a map of the possible states and the transition between them can
be drawn and analyzed. This is called a \textit{finite state machine}. Finite
state machines can be easily verified, as all possible states can be
exhaustively checked to meet requirements in a process called model checking.
Model checking has been used extensively in high-assurance digital systems and
to ensure software correctness for critical systems.

In order to check correctness, requirements for these automata must be defined.
Typically this is done using a formal language such as temporal logic. Temporal
logic allows system behaviors to be defined with temporal relations and includes
four operators: next (X), eventually (F), globally (G), and until (U). With
these operators, controller specifications can be created. In a nuclear context,
one might use temporal logic to define safety behaviors of a reactor core
control system. Let's consider an example:

Suppose we are trying to write safety requirements about SCRAM behavior. In
plain English, one might say "If a high temperature alarm is triggered, the
control rods will immediately be inserted and unable to be withdrawn unless
reset by an operator." In a linear temporal logic specification, this would be
written as follows:

\begin{equation}
\mathcal{G}(HighTemp \rightarrow \mathcal{X}(RodsInserted \land (\neg
RodsWithdrawn \text{ } \mathcal{U} \text{ } OperatorReset)))
\end{equation}

A significant body of work has been done around the translation of English
requirements into temporal logic specifications. The Formal Requirements
Elicitation Tool (FRET) developed by the NASA Ames Research Center to help
bridge the gap between natural language and mathematical specification. Using
FRET, one is able to take a bulk number of near-English requirements in a
language called FRETish, and translate them automatically into linear temporal
logic specifications. From this point, it can be examined whether or not
the set of requirements define a realizable system, or if there exists conflicts
between different specifications.