Obsidian/Writing/ERLM/state-of-the-art/v1.tex

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

We have previously discussed that a set of specifications can be checked as to
whether or not the constitute a realizable system. If a system is realizable,
there are a significant number of tools that can synthesize reactive control
systems from the set of logical specifications. Reactive systems are those that
take an input, and produce a reaction (an output). They depend on the current
system state and input to produce the next state. Competitions such as the
Reactive Synthesis Competition (SYNTCOMP) have existed for over a decade where
different groups try to produce the best reactive synthesis algorithm. These
systems are tested against a series of benchmarks to examine the number,
quality, and resources consumed to produce realizations of reactive systems from
logical specifications.

LIMITATION: while reactive synthesis exists, and we have an extensive amount of
documentation on nuclear power regulation and operating procedures exists, we
have not tried to combine the two together. 

Finally, formal methods has contributed the hybrid automata and differential
dynamic logic to try and solve the hybrid system verification problem. Hybrid
automata are an expansion of finite automata. Hybrid automata define each node
as being a control mode, similar to how finite state automata define each node
as a single state. For hybrid automata, the node represents the \textit{discrete
state}. Meanwhile, the transitions between states indicate the transitions
between continuous modes. These transitions represent the executions of
\(\nu(\cdot)\) that change the discrete state \(q\). Hybrid automata introduce a
way to graphically represent the transitions between continuous dynamic modes.

Differential dynamic logic (dL), on the other hand, is an expansion of linear
temporal logic to include support for real numbers and differential equation
solving. dL introduces two new operators focused on including dynamic behaviors.
The first is the box modality \([\alpha]\phi\), which states that for all
possible executions of the hybrid system \(\alpha\), \(\phi\) holds. The second
is the diamond modality \(\langle \alpha \rangle \phi\), which states that for
the hybrid system \(\alpha\), there is a trajectory where \(\phi\) holds. With
these two additional modalities, hybrid systems can be reasoned about directly
while including the continuous dynamics. That does not mean that working with
dL is easy however, as the effort to perform verification is encumbered by the
knowledge requirement of differential equations, logical specifications, and
then finally, sequent calculus to actually try and prove things written in dL.
dL is expressive enough to capture any hybrid system behavior, but the effort to
actually prove requirement adherence is challenging, even with automated proof
assistant tools.

In the next section, we will discuss how this research will address these
limitations and provide a path forward for building high assurance hybrid
control systems.