676 lines
38 KiB
TeX
676 lines
38 KiB
TeX
\section{Research Approach}
|
|
|
|
To build a high-assurance hybrid autonomous control system (HAHACS), we must
|
|
first establish a mathematical description of the system. This work draws on
|
|
automata theory\footnote{\textit{Automata theory} is the study of abstract
|
|
machines and the problems they can solve. An \textit{automaton} (plural:
|
|
\textit{automata}) is a mathematical model of a machine that follows a set
|
|
of rules to move between different states. Think of a vending machine: it
|
|
starts in ``waiting,'' moves to ``item selected'' when you push a button,
|
|
then to ``dispensing'' when you pay. Each state has clear rules for what
|
|
happens next. That is an automaton.}, temporal logic, and control theory. A
|
|
hybrid system is a dynamical system that has both continuous and discrete
|
|
states. The specific
|
|
type of system discussed in this proposal is a continuous autonomous hybrid
|
|
system. This means that the system does not have external input and that
|
|
continuous states do not change instantaneously when discrete states change.
|
|
For our systems of interest, the continuous states are physical quantities
|
|
that are always Lipschitz continuous.\footnote{\textit{Lipschitz continuous}
|
|
means the physical quantities (temperature, pressure, etc.) change smoothly
|
|
without sudden jumps. In practical terms: the reactor temperature cannot
|
|
teleport from 200\textdegree{}C to 500\textdegree{}C instantly---it must
|
|
pass through every value in between. This is a reasonable physical
|
|
assumption that makes the math tractable.} This nomenclature is borrowed from the
|
|
Handbook on Hybrid Systems Control \cite{lunze_handbook_2009}, but is
|
|
redefined here for convenience:
|
|
%
|
|
\begin{equation}
|
|
H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \delta,
|
|
\mathcal{R}, Inv)
|
|
\end{equation}
|
|
%
|
|
where:
|
|
%
|
|
\begin{itemize}
|
|
\item $\mathcal{Q}$: the set of discrete states (modes) of the system
|
|
\item $\mathcal{X} \subseteq \mathbb{R}^n$: the continuous state space
|
|
\item $\mathbf{f}: \mathcal{Q} \times \mathcal{X} \rightarrow
|
|
\mathbb{R}^n$: vector fields defining the continuous dynamics for each
|
|
discrete mode $q_i$
|
|
\item $Init \subseteq \mathcal{Q} \times \mathcal{X}$: the set of initial
|
|
states
|
|
\item $\mathcal{G}$: guard conditions that define when discrete state
|
|
transitions may occur
|
|
\item $\delta: \mathcal{Q} \times \mathcal{G} \rightarrow \mathcal{Q}$:
|
|
the discrete state transition function
|
|
\item $\mathcal{R}$: reset maps that define any instantaneous changes to
|
|
continuous state upon discrete transitions
|
|
\item $Inv$: safety invariants on the continuous dynamics
|
|
\end{itemize}
|
|
|
|
HAHACS bridges the gap between discrete and continuous verification by composing
|
|
formal methods from computer science with control-theoretic verification,
|
|
formalizing reactor operations using the framework of hybrid
|
|
automata\footnote{A \textit{hybrid automaton} is an automaton (state
|
|
machine) where each state also has continuous physics running inside it.
|
|
Imagine a thermostat: it has two states (``heating on'' and ``heating
|
|
off''), and in each state, the room temperature follows different physical
|
|
laws. The thermostat switches states based on temperature thresholds. A
|
|
nuclear reactor works the same way, just with many more states and much more
|
|
complex physics.}~\cite{alur_hybrid_1993}. The challenge of hybrid system verification
|
|
lies in the interaction between discrete and continuous dynamics. Discrete
|
|
transitions change the active continuous vector field, creating discontinuities
|
|
in the system's behavior. Traditional verification techniques designed for
|
|
purely discrete or purely continuous systems cannot handle this interaction
|
|
directly. Our methodology addresses this challenge through decomposition. We
|
|
verify discrete switching logic and continuous mode behavior separately, then
|
|
compose these guarantees to reason about the complete hybrid system. This
|
|
compositional strategy follows the assume-guarantee
|
|
paradigm\footnote{The \textit{assume-guarantee} approach is like checking a
|
|
relay race one runner at a time. If Runner~1 guarantees she will reach the
|
|
handoff zone at the right speed, and Runner~2 assumes he will receive the
|
|
baton in that zone and guarantees he will reach the next one, you can prove
|
|
the whole race works without simulating every possible scenario at once.
|
|
Each piece makes promises and relies on promises from adjacent pieces.} for
|
|
hybrid systems, where guarantees about individual modes compose into
|
|
guarantees about the overall
|
|
system~\cite{lunze_handbook_2009, alur_hybrid_1993}. This two-layer
|
|
approach mirrors the structure of reactor operations themselves: discrete
|
|
supervisory logic determines which control mode is active, while continuous
|
|
controllers govern plant behavior within each mode.
|
|
|
|
The creation of a HAHACS amounts to the construction of such a tuple
|
|
together with proof artifacts demonstrating that the intended behavior of the
|
|
control system is satisfied by its actual
|
|
implementation. In concrete terms, this means producing a
|
|
discrete automaton whose transitions are provably correct, continuous
|
|
controllers whose behavior is verified against transition requirements, and
|
|
formal evidence linking the two. This approach is tractable now because the
|
|
infrastructure for each component has matured. The novelty is not in the
|
|
individual pieces, but in the architecture that connects
|
|
them. By defining entry, exit, and safety conditions at the
|
|
discrete level first, we transform the intractable problem of global hybrid
|
|
verification into a collection of local verification problems with clear
|
|
interfaces. Verification is performed per mode rather than on the full
|
|
hybrid system, keeping the analysis tractable even for complex reactor
|
|
operations. Figure~\ref{fig:hybrid_automaton} illustrates this
|
|
structure for a simplified reactor startup sequence, showing discrete modes
|
|
connected by guard-triggered transitions with continuous dynamics governing
|
|
behavior within each mode.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\begin{tikzpicture}[
|
|
state/.style={
|
|
circle, draw=black, thick, minimum size=2.2cm,
|
|
fill=blue!10, align=center, font=\small
|
|
},
|
|
trans/.style={
|
|
->, thick, >=stealth
|
|
},
|
|
guard/.style={
|
|
font=\scriptsize, align=center, fill=white, inner sep=2pt
|
|
},
|
|
dynamics/.style={
|
|
font=\scriptsize\itshape, text=blue!70!black
|
|
}
|
|
]
|
|
% States
|
|
\node[state] (q0) at (0,0) {$q_0$\\Cold\\Shutdown};
|
|
\node[state] (q1) at (5,0) {$q_1$\\Heatup};
|
|
\node[state] (q2) at (10,0) {$q_2$\\Power\\Operation};
|
|
\node[state, fill=red!15] (q3) at (5,-3.5) {$q_3$\\SCRAM};
|
|
|
|
% Normal transitions
|
|
\draw[trans] (q0) -- node[guard, above]
|
|
{$T_{avg} > T_{min}$} (q1);
|
|
\draw[trans] (q1) -- node[guard, above]
|
|
{$T_{avg} \in [T_{op} \pm \delta]$\\$P > P_{crit}$} (q2);
|
|
|
|
% Fault transitions
|
|
\draw[trans, red!70!black] (q1) -- node[guard, left,
|
|
text=red!70!black] {$\neg Inv_1$} (q3);
|
|
\draw[trans, red!70!black] (q2) to[bend left=20] node[guard,
|
|
right, text=red!70!black] {$\neg Inv_2$} (q3);
|
|
|
|
% Recovery transition
|
|
\draw[trans, dashed] (q3) to[bend left=30] node[guard, below]
|
|
{Manual reset} (q0);
|
|
|
|
% Self-loops indicating staying in mode
|
|
\draw[trans] (q2) to[loop right] node[guard, right] {$Inv_2$}
|
|
(q2);
|
|
|
|
% Dynamics labels below states
|
|
\node[dynamics] at (0,-1.4) {$\dot{x} = f_0(x)$};
|
|
\node[dynamics] at (6,-1.2) {$\dot{x} = f_1(x)$};
|
|
\node[dynamics] at (10,-1.4) {$\dot{x} = f_2(x)$};
|
|
\node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$};
|
|
|
|
\end{tikzpicture}
|
|
\caption{Simplified hybrid automaton for reactor startup. Each discrete
|
|
state $q_i$ has associated continuous dynamics $f_i$. Guard conditions
|
|
on transitions (e.g., $T_{avg} > T_{min}$) are predicates over
|
|
continuous state. Invariant violations ($\neg Inv_i$) trigger
|
|
transitions to the SCRAM state. The operational level manages discrete
|
|
transitions; the tactical level executes continuous control within each
|
|
mode.}
|
|
\label{fig:hybrid_automaton}
|
|
\end{figure}
|
|
|
|
\subsection{System Requirements, Specifications, and Discrete Controllers}
|
|
|
|
Human control of nuclear power can be divided into three different scopes:
|
|
strategic, operational, and tactical.\footnote{This was inspired by an article
|
|
about battlefield organizational science~\cite{harvey_levels_2021}.} Strategic
|
|
control is 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 scheduled maintenance and downtime. The time
|
|
scale at this level is long, often spanning months or years. The lowest level of
|
|
control is the tactical level. This is the individual control of pumps,
|
|
turbines, and chemistry. Tactical control has already been somewhat automated in
|
|
nuclear power plants today, and is generally considered ``automatic control''
|
|
when autonomous. These controls are almost always continuous systems with a
|
|
direct impact on the physical state of the plant. Tactical control objectives
|
|
include, but are not limited to, maintaining pressurizer level, maintaining core
|
|
temperature, or adjusting reactivity with a chemical shim.
|
|
|
|
The level of control linking these two extremes 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 bridges high-level and low-level goals. A strategic goal may be to
|
|
perform refueling at a certain time, while the tactical level of the plant is
|
|
currently focused on maintaining a certain core temperature. The operational
|
|
level issues the shutdown procedure, using several smaller tactical goals along
|
|
the way to achieve this strategic objective. This hierarchical division of
|
|
control scope and objectives is illustrated graphically in
|
|
figure~\ref{fig:strat_op_tact}.
|
|
|
|
\begin{figure}
|
|
\centering
|
|
\begin{tikzpicture}[scale=0.8]
|
|
% Pyramid layers
|
|
\fill[blue!30!white] (0,4) -- (2,4) -- (1,5.) -- cycle;
|
|
\fill[blue!20!white] (-1.5,2.5) -- (3.5,2.5) -- (2,4) -- (0,4)
|
|
-- cycle;
|
|
\fill[blue!10!white] (-3,1) -- (5,1) -- (3.5,2.5) -- (-1.5,2.5)
|
|
-- cycle;
|
|
|
|
% Labels inside pyramid
|
|
\node[font=\small\bfseries] at (1,4.5) {Strategic};
|
|
\node[font=\small\bfseries] at (1,3.1) {Operational};
|
|
\node[font=\small\bfseries] at (1,1.6) {Tactical};
|
|
|
|
% Descriptions to the right
|
|
\node[anchor=west, font=\small, text width=8cm] at (5.5,4.6)
|
|
{\textit{Long-term planning:} maintenance scheduling, capacity
|
|
planning, economic dispatch};
|
|
\node[anchor=west, font=\small, text width=8cm] at (5.5,3.1)
|
|
{\textit{Discrete decisions:} startup/shutdown sequences, power
|
|
level changes, mode transitions};
|
|
\node[anchor=west, font=\small, text width=8cm] at (5.5,1.6)
|
|
{\textit{Continuous control:} temperature regulation, pressure
|
|
control, load following};
|
|
|
|
% Bracket showing HAHACS scope (simple line with text)
|
|
\draw[thick] (5.0,1.0) -- (-3.5,1) -- (-3.5,4) -- (2.0,4) --
|
|
cycle;
|
|
\node[font=\small, align=center, rotate=90] at (-4.2,2.5)
|
|
{HAHACS scope};
|
|
\end{tikzpicture}
|
|
\caption{Control scope hierarchy in nuclear power operations.
|
|
Strategic control (long-term planning) remains with human management.
|
|
HAHACS addresses the operational level (discrete mode switching) and
|
|
tactical level (continuous control within modes), which together form
|
|
a hybrid control system.}
|
|
\label{fig:strat_op_tact}
|
|
\end{figure}
|
|
|
|
This operational control level is the main reason for the requirement of human
|
|
operators in nuclear control today. The hybrid nature of this control system
|
|
makes it difficult to prove what the behavior of the combined hybrid system will
|
|
do across the entire state-space, so human operators have been used as a
|
|
stop-gap for safety. Humans have been used for this layer because their general
|
|
intelligence has been relied upon as a safe way to manage the hybrid nature of
|
|
this system---if a failure occured, it has been assumed a human operator can
|
|
figure out a solution to maintain plant performance and safety without
|
|
exhaustive knowledge of plant behavior. However, human factors research has
|
|
sought to minimize the need for general human reasoning by creating extremely
|
|
prescriptive operating manuals with strict procedures dictating what control to
|
|
implement at a given time. These operating manuals have minimized the role of
|
|
human operators today, are the key to the automating the operational control
|
|
scope.
|
|
|
|
The method of constructing a HAHACS in this proposal leverages two key
|
|
observations about current practice. First, the operational scope control is
|
|
effectively discrete control. Second, the rules for implementing this control
|
|
are described in operating procedures prior to their implementation. Instead of
|
|
implementing these procudures with a human controller, we rigorize the
|
|
instructions as a set of formal requirements. The behavior of any control system
|
|
originates in requirements: statements about what the system must do, must not
|
|
do, and under what conditions. For nuclear systems, these requirements derive
|
|
from multiple sources including regulatory mandates, design basis analyses, and
|
|
aforementioned operating procedures. The challenge is formalizing
|
|
these requirements with sufficient precision that they can serve as
|
|
the foundation for autonomous
|
|
control system synthesis and verification. We can build these requirements using
|
|
temporal logic.
|
|
|
|
Temporal logic is a powerful set of semantics for building systems with
|
|
complex but deterministic behavior. Temporal logic extends classical
|
|
propositional logic with operators that express properties over time. Using
|
|
temporal logic, we can make statements relating discrete control modes to one
|
|
another and define all the requirements of a HAHACS. The guard conditions
|
|
$\mathcal{G}$ are defined by determining boundary conditions between discrete
|
|
states and specifying their behavior, while continuous mode invariants can
|
|
also be expressed as temporal logic statements. These specifications form the
|
|
basis of any proofs about a HAHACS and constitute the fundamental truth
|
|
statements about what the behavior of the system is designed to be.
|
|
|
|
Discrete mode transitions include predicates that are Boolean functions over the
|
|
continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
|
|
\text{false}\}$. These predicates formalize conditions like ``coolant
|
|
temperature exceeds 315\textdegree{}C'' or ``pressurizer level is between 30\%
|
|
and 60\%.'' Critically, we do not impose this discrete abstraction artificially.
|
|
Operating procedures for nuclear systems already define go/no-go conditions as
|
|
discrete predicates, but do so in natural language. These thresholds come from
|
|
design basis safety analysis and have been validated over decades of operational
|
|
experience. Our methodology assumes this domain knowledge exists and provides a
|
|
framework to formalize it. This is why the approach is feasible for nuclear
|
|
applications specifically: the work of defining safe operating boundaries has
|
|
already been done by generations of nuclear engineers. The work of translating
|
|
these requirements from interpretable natural language to a formal
|
|
requirement is what remains to be done.
|
|
|
|
Linear temporal logic (LTL) is particularly well-suited for specifying reactive
|
|
systems. LTL formulas are built from atomic propositions (our discrete
|
|
predicates) using Boolean connectives and temporal operators. These operators
|
|
allow us to express safety properties (``the reactor never enters an unsafe
|
|
configuration''), liveness properties (``the system eventually reaches operating
|
|
temperature''), and response properties (``if coolant pressure drops, the system
|
|
initiates shutdown within bounded time''). We note that FRET's realizability
|
|
checking currently supports safety and bounded response properties but not
|
|
general liveness properties~\cite{katis_realizability_2022}. Liveness
|
|
requirements such as ``eventually reaches operating temperature'' are instead
|
|
verified through the continuous mode analysis described in Section~3.2, where
|
|
reachability analysis can confirm that target states are attained within bounded
|
|
time.
|
|
|
|
To build these temporal logic statements, an intermediary tool called
|
|
FRET\footnote{FRET is software developed by NASA that lets engineers write
|
|
safety requirements in structured English sentences, which the tool then
|
|
automatically translates into precise mathematical logic. Instead of
|
|
requiring engineers to learn abstract math notation, FRET meets them
|
|
halfway---you write something close to plain English, and it produces the
|
|
formal logic a computer needs.} is planned to be used. FRET stands for
|
|
Formal Requirements Elicitation Tool, and was developed by NASA to build
|
|
high-assurance timed systems. FRET is an intermediate language between
|
|
temporal logic and natural language that allows for rigid definitions of
|
|
temporal behavior while using a syntax accessible to engineers without formal
|
|
methods expertise\cite{katis_realizability_2022}. This
|
|
benefit is crucial for the feasibility of this methodology in industry. By
|
|
reducing the expert knowledge required to use these tools, their adoption with
|
|
the current workforce becomes easier.
|
|
|
|
A key feature of FRET is the ability to start with logically imprecise
|
|
statements and consecutively refine them into well-posed
|
|
specifications\cite{katis_realizability_2022, pressburger_using_2023}. We
|
|
can use this to our advantage by directly importing operating procedures and
|
|
design requirements into FRET in natural language, then iteratively refining
|
|
them into specifications for a HAHACS. This has two distinct benefits.
|
|
First, it allows us to draw a direct link from design documentation to
|
|
digital system implementation. Second, it clearly demonstrates where natural
|
|
language documents are insufficient. These procedures may still be used by
|
|
human operators, so any room for interpretation is a weakness that must be
|
|
addressed.
|
|
|
|
\dasinline{Maybe add more details about FRET case studies here. This would be
|
|
Pressburger and Katis.}
|
|
|
|
Once system requirements are defined as temporal logic specifications, we use
|
|
them to build the discrete control system. To do this, reactive
|
|
synthesis\footnote{\textit{Reactive synthesis} is perhaps the most
|
|
remarkable part of this work. Instead of a human programmer writing the
|
|
control software and hoping it is correct, the computer \textit{automatically
|
|
generates} a correct controller from the requirements. You tell it what the
|
|
system must do (the temporal logic specs), and it builds a controller that is
|
|
\textit{mathematically guaranteed} to do exactly that. If no such controller
|
|
can exist, it tells you that too.} tools are employed. Reactive synthesis is
|
|
a field in computer science that deals with the automated creation of
|
|
reactive programs from temporal logic specifications.
|
|
A reactive program is one that, for a given state, takes an input and produces
|
|
an output~\cite{jacobs_reactive_2024}. Our systems fit exactly this mold: the
|
|
current discrete state and status of guard conditions are the input, while the
|
|
output is the next discrete state.
|
|
|
|
Reactive synthesis solves the following problem: given an LTL formula $\varphi$
|
|
that specifies desired system behavior, automatically construct a finite-state
|
|
machine (strategy) that produces outputs in response to environment inputs such
|
|
that all resulting execution traces satisfy $\varphi$. If such a strategy
|
|
exists, the specification is called \emph{realizable}. The synthesis algorithm
|
|
either produces a correct-by-construction controller or reports that no such
|
|
controller can exist. This realizability check is itself valuable: an
|
|
unrealizable specification indicates conflicting or impossible requirements in
|
|
the original procedures. The current implementation and one of the main uses of
|
|
FRET today is for exactly this purpose---multiple case studies have used FRET
|
|
for the refinement of unrealizable specifications into realizable systems
|
|
\cite{katis_realizability_2022, pressburger_using_2023}.
|
|
|
|
The main advantage of reactive synthesis is that at no point in the production
|
|
of the discrete automaton is human engineering of the implementation required.
|
|
The resultant automaton is correct to the specification by construction. This
|
|
method of construction eliminates the possibility of human error at the
|
|
implementation stage entirely. The effort shifts entirely to specifying correct
|
|
behavior rather than implementing it. This has two critical implications. First,
|
|
every mode transition can be traced back through the specification to its
|
|
originating requirement, providing a clear liability and justification chain.
|
|
Second, by defining system behavior in temporal logic and synthesizing the
|
|
controller using deterministic algorithms, discrete control decisions become
|
|
provably consistent with operating procedures.
|
|
|
|
The output of reactive synthesis is a finite-state
|
|
machine\footnote{A \textit{finite-state machine} is a model of computation
|
|
with a fixed number of states and clear rules for transitioning between
|
|
them. A traffic light is a simple example: it cycles through green, yellow,
|
|
and red based on timing rules. The reactor controller is a much more complex
|
|
version of the same idea, with hundreds of states and transition rules based
|
|
on physical measurements.} that can be directly translated to executable
|
|
code. Tools such as Strix\footnote{Strix is a state-of-the-art software
|
|
tool that performs reactive synthesis. It won multiple international
|
|
competitions for automatically generating correct controllers from logical
|
|
specifications.} accept full LTL specifications and produce Mealy machines
|
|
via parity game
|
|
solving~\cite{luttenberger_practical_2020, meyer_strix_2018}. For specifications
|
|
within the GR(1) fragment---which captures the reactive input-output structure
|
|
typical of supervisory control---synthesis is efficient and scales to
|
|
specifications with thousands of states. Nuclear operating procedures are
|
|
well-suited to this fragment: environment inputs correspond to plant state
|
|
measurements and guard conditions, while outputs are mode transition commands.
|
|
The synthesized automaton provides a correct-by-construction implementation that
|
|
can be compiled to run on industrial control hardware without manual translation
|
|
of the control logic.
|
|
|
|
\subsection{Continuous Control Modes}
|
|
|
|
The synthesis of the discrete operational controller is only half of an
|
|
autonomous controller. These control systems are hybrid, with both discrete and
|
|
continuous components. This section describes the continuous control modes that
|
|
execute within each discrete state, and how we verify that they satisfy the
|
|
requirements imposed by the discrete layer. It is important to clarify the scope
|
|
of this methodology with respect to continuous controller design. This work will
|
|
verify continuous controllers; it does not synthesize them. The distinction
|
|
parallels model checking in software verification: model checking does not tell
|
|
engineers how to write correct software, but it verifies whether a given
|
|
implementation satisfies its specification. Similarly, we assume that continuous
|
|
controllers can be designed using standard control theory techniques, and to
|
|
that end, are not prohibitive to create. Our contribution is a verification
|
|
framework that confirms candidate controllers compose correctly with the
|
|
discrete layer to produce a safe hybrid system.
|
|
|
|
The operational control scope defines go/no-go decisions that determine what
|
|
kind of continuous control to implement. The entry or exit conditions of a
|
|
discrete state are themselves the guard conditions $\mathcal{G}$ that define the
|
|
boundaries for each continuous controller's allowed state-space region. These
|
|
continuous controllers all share a common state space, but each individual
|
|
continuous control mode operates within its own partition defined by the
|
|
discrete state $q_i$ and the associated guard conditions. This partitioning of
|
|
the continuous state space among several distinct vector fields has
|
|
traditionally been a difficult problem for validation and verification. The
|
|
discontinuity of the vector fields at discrete state interfaces makes
|
|
reachability analysis computationally expensive, and analytic solutions often
|
|
become intractable \cite{kapuria_using_2025, lang_formal_2021}.
|
|
|
|
We circumvent these issues by designing our hybrid system from the bottom up
|
|
with verification in mind. Each continuous control mode has an input set and
|
|
output set clearly defined by our discrete transitions \textit{a priori}.
|
|
Consider that we define the continuous state space as $\mathcal{X}$. Each
|
|
discrete mode $q_i$ then provides three key pieces of information for continuous
|
|
controller design:
|
|
%
|
|
\begin{enumerate}
|
|
\item \textbf{Entry conditions:} $\mathcal{X}_{entry,i} \subseteq
|
|
\mathcal{X}$, the set of possible initial states when entering this mode
|
|
\item \textbf{Exit conditions:} $\mathcal{X}_{exit,i} \subseteq
|
|
\mathcal{X}$, the target states that trigger transition to the next mode,
|
|
or is the region in the state space a stabilizing mode remains within.
|
|
\item \textbf{Safety invariants:} $\mathcal{X}_{safe,i} \subseteq
|
|
\mathcal{X}$, the envelope of safe states during operation in this mode.
|
|
These are derived from invariants \(Inv\).
|
|
\end{enumerate}
|
|
%
|
|
These sets come directly from the discrete controller synthesis and define
|
|
precise objectives for continuous control.\dasnote{This SOUNDS like
|
|
assume-guarantee stuff. Maybe make that connection formal and cite it?} The
|
|
continuous controller for mode $q_i$ must drive the system from any state in
|
|
$\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while remaining
|
|
within $\mathcal{X}_{safe,i}$. We classify continuous controllers into three
|
|
types based on their objectives: transitory, stabilizing, and
|
|
expulsory.\footnote{These three mode types are one of Dane's key
|
|
contributions. \textit{Transitory} modes move the reactor from one operating
|
|
condition to another (like heating up from cold to operating temperature).
|
|
\textit{Stabilizing} modes hold the reactor steady at a target condition
|
|
(like maintaining a constant power level). \textit{Expulsory} modes are
|
|
emergency responses that drive the reactor to safety (like an emergency
|
|
shutdown). By classifying modes this way, each type can be verified using
|
|
the mathematical tools best suited to it, rather than trying to verify
|
|
everything with one approach.} Each type has distinct verification
|
|
requirements that determine which formal methods tools are appropriate.
|
|
|
|
\dasinline{(1) Add figure showing the relationship between entry/exit/safety
|
|
sets. (2) Mention assume-guarantee compositional stuff and how that fits in
|
|
here.}
|
|
|
|
\subsubsection{Transitory Modes}
|
|
|
|
Transitory modes are continuous controllers designed to move the plant from one
|
|
discrete operating condition to another. Their purpose is to execute
|
|
transitions: starting from entry conditions, reach exit conditions, and maintain
|
|
safety invariants throughout. Examples include but are not limited to power
|
|
ramp-up sequences, cooldown procedures, and load-following maneuvers.
|
|
|
|
The control objective for a transitory mode can be stated formally. Given
|
|
entry conditions $\mathcal{X}_{entry}$, exit conditions
|
|
$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and
|
|
closed-loop dynamics $\dot{x} = f(x)$, the controller must satisfy:
|
|
%
|
|
\[
|
|
\forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in
|
|
\mathcal{X}_{exit} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
|
|
\]
|
|
%
|
|
That is, from any valid entry state, the trajectory must eventually reach the
|
|
exit condition without ever leaving the safe region.
|
|
|
|
Verification of transitory modes will use reachability analysis. Reachability
|
|
analysis computes the set of all states reachable from a given initial set under
|
|
the system dynamics~\cite{guernic_reachability_2009,
|
|
mitchell_time-dependent_2005, bansal_hamilton-jacobi_2017}. For a transitory
|
|
mode to be valid, the reachable set from $\mathcal{X}_{entry}$ must satisfy two
|
|
conditions:
|
|
%
|
|
\begin{enumerate}
|
|
\item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the
|
|
mode achieves its objective)
|
|
\item The reachable set never leaves $\mathcal{X}_{safe}$ (safety is
|
|
maintained throughout the transition)
|
|
\end{enumerate}
|
|
%
|
|
Formally, if $\text{Reach}(\mathcal{X}_{entry}, f, [0,T])$ denotes the states
|
|
reachable within time horizon $T$:
|
|
%
|
|
\[
|
|
\text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \subseteq \mathcal{X}_{safe}
|
|
\land \text{Reach}(\mathcal{X}_{entry}, f_i, [0,T]) \cap
|
|
\mathcal{X}_{exit} \neq \emptyset
|
|
\]
|
|
%
|
|
Because the discrete controller defines clear boundaries in
|
|
continuous state space, the verification problem for each transitory mode is
|
|
well-posed. We know the possible initial conditions, we know the target
|
|
conditions, and we know the safety envelope. The verification task is to
|
|
confirm that the candidate continuous controller achieves the objective from
|
|
all possible starting points.
|
|
|
|
Several tools exist for computing reachable sets of hybrid systems, including
|
|
CORA~\cite{althoff_introduction_nodate}, Flow*~\cite{chen_flow_2013,
|
|
chen_taylor_2012}, SpaceEx~\cite{frehse_spaceex_2011}, and
|
|
JuliaReach~\cite{bogomolov_reachability_2020}. The choice of
|
|
tool depends on the structure of the continuous dynamics. Linear systems admit
|
|
efficient polyhedral or ellipsoidal reachability computations. Nonlinear systems
|
|
require more conservative over-approximations using techniques such as Taylor
|
|
models or polynomial zonotopes. For this work, we will select tools appropriate
|
|
to the fidelity of the reactor models available.
|
|
|
|
\subsubsection{Stabilizing Modes}
|
|
|
|
Stabilizing modes are continuous controllers with an objective of maintaining
|
|
a particular discrete state indefinitely. Rather than driving the system
|
|
toward an exit state, they keep the system within a safe
|
|
operating region. Examples include steady-state power operation, hot standby,
|
|
and load-following at constant power level. Reachability analysis for
|
|
stabilizing modes may not be a suitable approach to validation. Instead, we
|
|
plan to use barrier certificates.\footnote{A \textit{barrier certificate} is
|
|
a mathematical proof that a system can never leave a safe region. Imagine
|
|
drawing a fence around the acceptable operating conditions on a map. A
|
|
barrier certificate proves that no matter what happens inside the fence, the
|
|
system's physics will never push it through to the other side. If you can
|
|
find such a certificate, you have proven safety without simulating every
|
|
possible scenario.} Barrier certificates analyze the dynamics of the system
|
|
to determine whether flux across a given boundary
|
|
exists~\cite{prajna_safety_2004}. In other words, they
|
|
evaluate whether any trajectory leaves a given boundary. This definition is
|
|
exactly what defines the validity of a stabilizing continuous control mode.
|
|
|
|
A barrier certificate (or control barrier function) is a scalar function $B:
|
|
\mathcal{X} \rightarrow \mathbb{R}$ that certifies forward invariance of a safe
|
|
set. The idea is analogous to Lyapunov functions for
|
|
stability~\cite{branicky_multiple_1998}: rather than computing trajectories
|
|
explicitly, we find a certificate function whose properties guarantee the
|
|
desired behavior. For a safe set $\mathcal{C} = \{x : B(x) \geq 0\}$ and
|
|
dynamics $\dot{x} = f(x,u)$, the\dasinline{Should clarify that the safe set C is
|
|
not the entire continuous region. It's just the boundary of the region.} barrier
|
|
certificate condition requires:
|
|
%
|
|
\[
|
|
\forall x \in \partial\mathcal{C}: \dot{B}(x) = \nabla B(x) \cdot f(x,u(x))
|
|
\geq 0
|
|
\]
|
|
%
|
|
This condition states that on the boundary of the safe set (where $B(x) =
|
|
0$), the time derivative of $B$ is non-negative. Geometrically, this means
|
|
the vector field points inward or tangent to the boundary, never outward. If
|
|
this condition holds, no trajectory starting inside $\mathcal{C}$ can ever
|
|
leave.
|
|
|
|
Because the design of the discrete controller defines careful boundaries in
|
|
continuous state space, the barrier \(\mathcal{C}\) is known prior to designing
|
|
the continuous controller. This eliminates the search for an appropriate barrier
|
|
and minimizes complication in validating stabilizing continuous control modes.
|
|
The discrete specifications tell us what region must be invariant; the barrier
|
|
certificate confirms that the candidate controller achieves this invariance.
|
|
|
|
The key advantage is that the verification is independent of how the controller
|
|
was designed. Standard control techniques can be used to build continuous
|
|
controllers, and barrier certificates provide a separate check that the result
|
|
satisfies the required invariants. This also allows for the checking of control
|
|
modes with different models than they are designed for. For example, a lower
|
|
fidelity model can be used for controller design, but a higher fidelity model
|
|
can be used for the actual validation of that stabilizing
|
|
controller.\splitnote{SOS methods proven effective: Papachristodoulou 2021
|
|
(SOSTOOLS v4, pp.1-2) solves barrier certificate optimization via SOS
|
|
constraints---tool integrates with MATLAB. Borrmann 2015 (pp.4-8) demonstrates
|
|
control barrier certificates for multi-agent systems, showing how discrete
|
|
boundaries (mode guards) can inform barrier design. Your claim that discrete
|
|
specs eliminate barrier search is novel and well-supported by these
|
|
foundations.}\splitnote{Hauswirth 2024 (pp.1-3) shows optimization-based robust
|
|
feedback controllers can serve as alternative verification method---suggests
|
|
barrier certificates + reachability provide complementary guarantees for your
|
|
stabilizing modes.}
|
|
|
|
\subsubsection{Expulsory Modes}
|
|
|
|
Expulsory modes are continuous controllers responsible for ensuring safety
|
|
when failures occur. They are designed for robustness rather than optimality.
|
|
The control objective is to drive the plant to a safe shutdown state from
|
|
potentially anywhere in the state space, under degraded or uncertain
|
|
dynamics. Examples include emergency core cooling, reactor SCRAM sequences,
|
|
and controlled depressurization procedures.
|
|
|
|
We can detect that physical failures exist because our physical controllers have
|
|
been previously proven correct by reachability and barrier certificates. We know
|
|
our controller cannot be incorrect for the nominal plant model, so if an
|
|
invariant is violated, we know the plant dynamics have changed. The mathematical
|
|
formulation for expulsory mode verification differs from transitory modes in two
|
|
key ways. First, the entry conditions may be the entire state space (or a large,
|
|
conservatively bounded region) rather than a well-defined entry set. The failure
|
|
may occur at any point during operation. Second, the dynamics include parametric
|
|
uncertainty representing failure modes:
|
|
%
|
|
\[
|
|
\dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure}
|
|
\]
|
|
%
|
|
where $\Theta_{failure}$ captures the range of possible degraded plant
|
|
behaviors identified through failure mode and effects analysis (FMEA) or
|
|
traditional safety analysis.
|
|
|
|
We verify expulsory modes using reachability analysis with parametric
|
|
uncertainty. While tools such as SpaceEx handle nondeterministic
|
|
inputs~\cite{frehse_spaceex_2011}, parametric plant uncertainty requires
|
|
conservative over-approximation of reachable sets across the full parameter
|
|
range. The verification condition requires that for all parameter values within
|
|
the uncertainty set, trajectories from the expanded entry region reach the safe
|
|
shutdown state:
|
|
%
|
|
\[
|
|
\forall \theta \in \Theta_{failure}:
|
|
\text{Reach}(\mathcal{X}_{current}, f_\theta, [0,T]) \subseteq
|
|
\mathcal{X}_{shutdown}
|
|
\]
|
|
%
|
|
This is more conservative than nominal reachability, accounting for the fact
|
|
that we cannot know exactly which failure mode is active.
|
|
|
|
Traditional safety analysis techniques inform the construction of
|
|
$\Theta_{failure}$. Probabilistic risk assessment, FMEA, and design basis
|
|
accident analysis identify credible failure scenarios and their effects on
|
|
plant dynamics. The expulsory mode must handle the worst-case dynamics within
|
|
this envelope. This is where conservative controller design is appropriate as
|
|
safety margins will matter more than performance during emergency
|
|
shutdown.\splitnote{Parametric uncertainty approach validated: Kapuria 2025
|
|
(pp.82-120, Sections 5) verifies SmAHTR resiliency against UCAs with
|
|
uncertain dynamics (e.g., PHX secondary flow shutdown, resonating turbine
|
|
flow). Uses reachability + Z3 SMT solver (pp.23-24, Section 2.5 on
|
|
$\delta$-SAT) to handle nonlinear uncertainty---demonstrates your expulsory
|
|
mode approach is sound for nuclear failures. Shows safety can be proven even
|
|
when controller deviates from nominal (pp.85-107, UCA 1
|
|
analysis).}
|
|
|
|
\subsection{Industrial Implementation}
|
|
|
|
The methodology described above must be validated on realistic systems using
|
|
industrial-grade hardware to demonstrate practical feasibility. This research
|
|
will leverage the University of Pittsburgh Cyber Energy Center's partnership
|
|
with Emerson to implement and test the HAHACS methodology on production
|
|
control equipment. Emerson's Ovation distributed control system is widely
|
|
deployed in power generation facilities, including nuclear plants. The
|
|
Ovation platform provides a realistic target for demonstrating that formally
|
|
synthesized controllers can execute on industrial hardware meeting timing and
|
|
reliability requirements. The discrete automaton produced by reactive
|
|
synthesis will be compiled to run on Ovation controllers, with verification
|
|
that the implemented behavior matches the synthesized specification exactly.
|
|
|
|
For the continuous dynamics, we will use a small modular reactor simulation. The
|
|
SmAHTR (Small modular Advanced High Temperature Reactor) model provides a
|
|
relevant testbed for startup and shutdown procedures. The ARCADE (Advanced
|
|
Reactor Control Architecture Development Environment) interface will establish
|
|
communication between the Emerson Ovation hardware and the reactor simulation,
|
|
enabling hardware-in-the-loop testing of the complete hybrid controller.
|
|
|
|
The Emerson collaboration strengthens this work in two ways. Access to
|
|
system experts at Emerson ensures that implementation details of the Ovation
|
|
platform are handled correctly. Direct industry collaboration also provides an
|
|
immediate pathway for technology transfer and alignment with practical
|
|
deployment requirements.
|