\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(\codt)\) can be much more
generally created. The only restriction on \(\nu_i(\codt)\) is that it must
not create an infinite number of jumps in a finite amount of time.
\(\nu_i(\codt)\) 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}