Obsidian/Writing/ERLM/goals-and-outcomes/v4.tex

\section{Goals and Outcomes - REVISED}

The goal of this research is to develop a unified framework combining temporal
logic synthesis with continuous-time verification methods to create autonomous
hybrid control systems with complete correctness guarantees. Hybrid control
systems have great potential for autonomous control applications because they
can switch between different control laws based on discrete triggers in the
system's operating range. This approach allows autonomous controllers to use
several tractable control laws optimized for different regions in the state
space, rather than relying on a single controller across the entire operating
range. But, the discrete transitions between control laws in hybrid controllers
present significant challenges in proving stability and liveness properties for
the complete system. While tools from control theory can establish properties
for individual control modes, these guarantees do not generalize when mode
switching is introduced. Conversely, significant advances in formal methods have
enabled automatic synthesis of discrete controllers from temporal logic
specifications—tools like Strix can generate provably correct switching logic
for complex logical requirements. However, these synthesis approaches assume
instantaneous mode transitions and operate purely in discrete state spaces. In
hybrid systems, transitions occur along continuous trajectories governed by
differential equations, creating a fundamental verification gap that neither
purely discrete synthesis nor traditional control theory can address alone.

This research addresses a fundamental challenge in hybrid controller synthesis
and verification by unifying discrete system synthesis with continuous system
analysis. We will leverage formal methods to create controllers that are
correct-by-construction, enabling guarantees about the complete system's
behavior. To demonstrate this approach, we will develop an autonomous controller
for nuclear power plant start-up procedures. Nuclear power represents an
excellent test case because the continuous reactor dynamics are well-studied,
while the discrete mode switching requirements are explicitly defined in
regulatory procedures and operating guidelines. Current nuclear reactor control
\textit{is} already a hybrid system. For example, during reactor startup,
operators must transition from initial cold conditions through controlled
heating phases to predetermined power levels. Each phase employs different
automated controllers: temperature ramp controllers during heatup, reactivity
controllers approaching criticality, and load-following controllers during
operation. The decision of when to switch between these controllers currently
relies on human operators interpreting written procedures. Our approach would
formalize such transition conditions and synthesize the switching logic
automatically.

The capability to create high-assurance hybrid control systems has significant
potential to reduce labor costs in operating critical systems by removing human
operators from control loops. Nuclear power stands to benefit substantially from
increased controller autonomy, as operations and maintenance represent the
largest expense for current reactor designs. While emerging technologies such as
microreactors and small modular reactors will reduce maintenance costs through
factory-manufactured replacement components, they face increased per-megawatt
operating costs if required to maintain traditional staffing levels. However, if
increased autonomy can be safely introduced, these economic challenges can be
addressed while maintaining safety standards.

If this research is successful, we will achieve the following outcomes:

\begin{enumerate}

  \item
    \textbf{Formalize mode switching requirements as logical specifications that
    can be synthesized into discrete controller implementations.} The discrete
    transitions between continuous controller modes are often explicitly defined
    in operating procedures and regulatory requirements for critical systems.
    These natural language requirements will be translated into temporal logic
    specifications, which will then be synthesized into provably correct
    discrete controllers for continuous mode switching.

  \item 
    \textbf{Develop and verify formal characterizations of hybrid mode
    dynamics and safety conditions.} We will establish mathematical frameworks
    distinguishing transitory modes with reachability requirements to target
    states from stabilizing modes with invariant maintenance properties. For
    linear dynamics, classical control theory will establish stability and
    performance within each mode. For nonlinear systems, reachability analysis
    will verify that transitory modes drive the system toward intended
    transitions while maintaining safety constraints, and that stabilizing modes
    preserve their designated operating regions. This unified approach will
    enable provable conditions for safe state space traversal and transition
    timing.

  \item 
    \textbf{Prove that hybrid system implementations achieve safety and
    performance specifications across operational mode sequences.} By
    synthesizing discrete controller transitions from logical specifications
    using correct-by-construction methods and verifying that continuous
    components perform appropriately between discrete transitions, we can
    establish mathematical guarantees that the hybrid system maintains safety
    constraints and meets performance requirements during autonomous operational
    sequences such as reactor startup procedures, where multiple control modes
    must be coordinated to achieve higher-level operational objectives.
  
\end{enumerate}