danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

feedback from earlier now integrated. Clear of almost all notes.

Browse Source
This commit is contained in:
Dane Sabo 2026-03-16 17:15:35 -04:00
parent 6901dc8276
commit af2ce44fd6
9 changed files with 384 additions and 732 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

124
1-goals-and-outcomes/goals.tex
View File

@ -1,76 +1,53 @@
\section{Goals and Outcomes} \section{Goals and Outcomes}
\dasinline{Research statement is very similar to GO
because that's what I had when I prepared it.
If it's going to be an executive summary, it
should talk more about the other sections rather
than just being a slightly different GO section.}
% GOAL PARAGRAPH % GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous The goal of this research is to develop a methodology for creating autonomous
hybrid control systems with mathematical guarantees of safe and correct hybrid control systems with mathematical guarantees of safe and correct
behavior.\splitnote{Clear thesis statement. Gets right to it.} behavior.
% INTRODUCTORY PARAGRAPH Hook % INTRODUCTORY PARAGRAPH Hook
Nuclear power plants require the highest levels of control system reliability, Nuclear power plants require the highest levels of control system reliability,
where failures can result in significant economic losses, service where failures can result in significant economic losses, service interruptions,
interruptions, or radiological or radiological release.
release.\splitnote{Stakes established immediately — good hook.}
% Known information % Known information
Currently, nuclear plant operations rely on extensively trained human Currently, nuclear plant operations rely on extensively trained human operators
operators who follow detailed written procedures and strict regulatory who follow detailed written procedures and strict regulatory requirements to
requirements to manage reactor control. These operators make critical manage reactor control. These operators make critical decisions about when to
decisions about when to switch between different control modes based on their switch between different control modes based on their interpretation of plant
interpretation of plant conditions and procedural guidance. conditions and procedural guidance.
% Gap % Gap
\oldt{This reliance on human operators prevents autonomous control This reliance on human operators prevents autonomous control and creates a
capabilities and creates a fundamental economic challenge for next-generation fundamental economic barrier for next-generation reactor designs. Small modular
reactor designs.} \newt{This reliance on human operators prevents autonomous reactors face per-megawatt staffing costs far exceeding those of conventional
control and creates a fundamental economic barrier for next-generation plants, threatening their economic viability.
reactor designs.} Small modular reactors face per-megawatt staffing costs
far exceeding those of conventional plants, threatening their economic
viability.
% Critical Need % Critical Need
\oldt{What is needed is a method to create autonomous control systems that What is needed is a method to create autonomous control systems that safely
safely manage complex operational sequences with the same assurance as manage complex operational sequences with the same assurance as human-operated
human-operated systems, but without constant human supervision.} systems, but without constant human supervision.
\newt{Autonomous control systems must safely manage complex operational
sequences with the same assurance as human-operated systems, but without
constant human supervision.}
% APPROACH PARAGRAPH Solution % APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods with control theory to To address this need, we will combine formal methods with control theory to
build hybrid control systems that are correct by construction. build hybrid control systems that are correct by construction.
% Rationale % Rationale
Hybrid systems use discrete logic to switch between continuous control modes, Hybrid systems use discrete logic to switch between continuous control modes,
mirroring how operators change control strategies. Existing formal methods mirroring how operators change control strategies. Existing formal methods can
can generate provably correct switching logic from written requirements, but generate provably correct switching logic from written requirements, but they
they cannot handle the continuous dynamics that occur during transitions cannot handle the continuous dynamics that occur during transitions between
between modes. Meanwhile, traditional control theory can verify continuous modes. Meanwhile, traditional control theory can verify continuous behavior but
behavior but lacks tools for proving correctness of discrete switching lacks tools for proving correctness of discrete switching decisions.
decisions.\splitnote{Excellent setup of the gap — shows why neither approach
alone is sufficient.}
% Hypothesis % Hypothesis
By synthesizing discrete mode transitions directly from written operating By synthesizing discrete mode transitions directly from written operating
procedures and verifying continuous behavior between transitions, we can procedures and verifying continuous behavior between transitions, we can create
create hybrid control systems with end-to-end correctness guarantees. If hybrid control systems with end-to-end correctness guarantees. If existing
existing procedures can be formalized into logical specifications and procedures can be formalized into logical specifications and continuous dynamics
continuous dynamics verified against transition requirements, then autonomous verified against transition requirements, then autonomous controllers can be
controllers can be built that are provably free from design built that are provably free from design defects.
defects.\splitnote{Hypothesis is clear and testable.}
% Pay-off % Pay-off
\oldt{This approach will enable autonomous control in nuclear power plants This approach will enable autonomous control in nuclear power plants while
while maintaining the high safety standards required by the industry. maintaining the high safety standards required by the industry. The University
of Pittsburgh Cyber Energy Center's partnership with Emerson provides access to
% Qualifications industry-standard control hardware, ensuring that developed solutions align with
This work is conducted within the University of Pittsburgh Cyber Energy practical implementation requirements from the outset.
Center, which provides access to industry collaboration and Emerson control
hardware, ensuring that developed solutions align with practical
implementation requirements.} \newt{This approach will enable autonomous
control in nuclear power plants while maintaining the high safety standards
required by the industry. The University of Pittsburgh Cyber Energy Center's
partnership with Emerson provides access to industry-standard control
hardware, ensuring that developed solutions align with practical
implementation requirements from the outset.}
% OUTCOMES PARAGRAPHS % OUTCOMES PARAGRAPHS
If this research is successful, we will be able to do the following: If this research is successful, we will be able to do the following:
@ -81,18 +58,14 @@ If this research is successful, we will be able to do the following:
\item \textbf{Translate written procedures into verified control logic.} \item \textbf{Translate written procedures into verified control logic.}
% Strategy % Strategy
We will develop a methodology for converting existing written operating We will develop a methodology for converting existing written operating
procedures into formal specifications that can be automatically procedures into formal specifications that can be automatically synthesized
synthesized into discrete control logic. This process will use structured into discrete control logic. This process will use structured intermediate
intermediate representations to bridge natural language procedures and representations to bridge natural language procedures and mathematical
mathematical logic. logic.
% Outcome % Outcome
\oldt{Control system engineers will generate verified mode-switching Control system engineers will generate verified mode-switching controllers
controllers directly from regulatory procedures without formal methods directly from regulatory procedures, lowering the barrier to high-assurance
expertise, lowering the barrier to high-assurance control systems.} control systems.
\newt{This will lower the barrier to high-assurance control systems by
generating verified mode-switching controllers directly from regulatory
procedures.}\dasinline{Same comment as in executive summary. Might not be
true and is not the point.}
% OUTCOME 2 Title % OUTCOME 2 Title
\item \textbf{Verify continuous control behavior across mode transitions.} \item \textbf{Verify continuous control behavior across mode transitions.}
@ -116,8 +89,7 @@ If this research is successful, we will be able to do the following:
reactor simulation using industry-standard control hardware. This reactor simulation using industry-standard control hardware. This
demonstration will prove correctness across multiple coordinated control demonstration will prove correctness across multiple coordinated control
modes from cold shutdown through criticality to power modes from cold shutdown through criticality to power
operation.\splitnote{``cold shutdown through criticality to power operation.
operation'' — concrete and impressive scope.}
% Outcome % Outcome
We will demonstrate that autonomous hybrid control can be realized in the We will demonstrate that autonomous hybrid control can be realized in the
nuclear industry with current equipment, establishing a path toward nuclear industry with current equipment, establishing a path toward
@ -127,21 +99,11 @@ If this research is successful, we will be able to do the following:
% IMPACT PARAGRAPH Innovation % IMPACT PARAGRAPH Innovation
The innovation in this work is unifying discrete synthesis with continuous The innovation in this work is unifying discrete synthesis with continuous
verification to enable end-to-end correctness guarantees for hybrid verification to enable end-to-end correctness guarantees for hybrid systems.
systems.\splitnote{Clear ``what's new'' statement.}
% Outcome Impact % Outcome Impact
If successful, control engineers will create autonomous controllers from If successful, control engineers will create autonomous controllers from
existing procedures with mathematical proof of correct behavior. existing procedures with mathematical proof of correct behavior. High-assurance
High-assurance autonomous control will become practical for safety-critical autonomous control will become practical for safety-critical applications.
applications.
% Impact/Pay-off % Impact/Pay-off
\oldt{This capability is essential for the economic viability of This research will provide the tools to achieve that autonomy while maintaining
next-generation nuclear power. Small modular reactors offer a promising the exceptional safety record the nuclear industry requires.
solution to growing energy demands, but their success depends on reducing
per-megawatt operating costs through increased autonomy. This research will
provide the tools to achieve that autonomy while maintaining the exceptional
safety record the nuclear industry requires.} \newt{This research will
provide the tools to achieve that autonomy while maintaining the exceptional
safety record the nuclear industry
requires.}\dasinline{This paragraph is literally the same as the rest of the
GO. Does not belong here and feels very redundant.}

97
1-goals-and-outcomes/research-statement.tex
View File

@ -1,78 +1,56 @@
\dasnote{Research statement is very similar to GO because that's what I had
when I prepared it. If it's going to be an executive summary, it should talk
more about the other sections rather than just being a slightly different GO
section.}
% GOAL PARAGRAPH % GOAL PARAGRAPH
The goal of this research is to develop a methodology for creating autonomous The goal of this research is to develop a methodology for creating autonomous
\oldt{control systems with event-driven control laws that have guarantees of hybrid control systems with mathematical guarantees of safe and correct
safe and correct behavior.} \newt{hybrid control systems with mathematical behavior.
guarantees of safe and correct behavior.}\splitnote{Strong, direct opening.
Sets scope immediately.}
\dasinline{Title needs updated to High Assurance Hybrid
Control Systems. Maybe removal of `formal'?}
% INTRODUCTORY PARAGRAPH Hook % INTRODUCTORY PARAGRAPH Hook
Nuclear power relies on extensively trained operators who follow detailed Nuclear power relies on extensively trained operators who follow detailed
written procedures to manage reactor control. Based on these procedures and written procedures to manage reactor control. Based on these procedures and
\oldt{operators'} \newt{their} interpretation of plant conditions, their interpretation of plant conditions, they make critical decisions about
\oldt{operators} \newt{they} make critical decisions about when to switch when to switch between control objectives.
between control objectives.
% Gap % Gap
\oldt{But, reliance} \newt{This reliance} on human operators has created an This reliance on human operators has created an economic challenge for
economic challenge for next-generation nuclear power plants. Small modular next-generation nuclear power plants. Small modular reactors face significantly
reactors face significantly higher per-megawatt staffing costs than higher per-megawatt staffing costs than conventional plants. Autonomous control
conventional plants.\dasinline{Obvious but source required.} Autonomous systems are needed that can safely manage complex operational sequences with the
control systems \oldt{are needed that can} \newt{must} safely manage complex same assurance as human-operated systems, but without constant supervision.
operational sequences with the same assurance as human-operated systems, but
without constant supervision.
% APPROACH PARAGRAPH Solution % APPROACH PARAGRAPH Solution
To address this need, we will combine formal methods from computer science To address this need, we will combine formal methods from computer science
with control theory \oldt{to build hybrid control systems that are correct by with control theory to build hybrid control systems that are correct by
construction.} \newt{to build hybrid control systems that are correct by
construction, leveraging the extensive domain knowledge already embedded in construction, leveraging the extensive domain knowledge already embedded in
existing operating procedures and safety analyses.} existing operating procedures and safety analyses.
% Rationale % Rationale
Hybrid systems use discrete logic to switch between continuous control modes, Hybrid systems use discrete logic to switch between continuous control modes,
similar to how operators change control strategies. Existing formal methods similar to how operators change control strategies. Existing formal methods
generate provably correct switching logic but cannot handle continuous generate provably correct switching logic but cannot handle continuous
dynamics during transitions, while traditional control theory verifies dynamics during transitions, while traditional control theory verifies
continuous behavior but lacks tools for proving discrete switching continuous behavior but lacks tools for proving discrete switching
correctness.\splitnote{Nice parallel structure showing the gap.} correctness.
% Hypothesis and Technical Approach % Hypothesis and Technical Approach
We will bridge this gap through a three-stage methodology. First, we will We will bridge this gap through a three-stage methodology. First, we will
translate written operating procedures into temporal logic specifications translate written operating procedures into temporal logic specifications using
using NASA's Formal Requirements Elicitation Tool (FRET). \oldt{which NASA's Formal Requirements Elicitation Tool (FRET). FRET structures requirements
structures requirements into scope, condition, component, timing, and into scope, condition, component, timing, and response elements. This approach
response elements. This structured approach enables realizability checking to enables realizability checking that identifies conflicts and ambiguities in
identify conflicts and ambiguities in procedures before implementation.} procedures before implementation. Second, we will synthesize discrete mode
\newt{FRET structures requirements into scope, condition, component, timing, switching logic using reactive synthesis to produce deterministic automata that
and response elements, enabling realizability checking that identifies are correct by construction. Third, we will develop continuous controllers for
conflicts and ambiguities in procedures before implementation.} each discrete mode using standard control theory and reachability analysis. We
\dasinline{Had to read this twice.} will classify continuous modes based on their transition objectives and verify
Second, we will synthesize discrete mode switching logic using reactive safe mode transitions using barrier certificates and reachability analysis.
synthesis \oldt{to generate deterministic automata that are provably correct
by construction.} \newt{to produce deterministic automata that are correct by
construction.}\dasinline{Also had to read this twice. A lot of
jargon. Check topic stress.}
Third, we will develop continuous controllers for each discrete mode using
standard control theory and reachability analysis. We will classify
continuous modes based on their transition objectives \oldt{, and then employ
assume-guarantee contracts and barrier certificates to prove that mode
transitions occur safely and as defined by the deterministic automata.}
\newt{and verify safe mode transitions using barrier certificates and
reachability analysis.}\dasinline{I don't think I ever mention this phrase
again specifically. Might be a dogwhistle to other work unintentionally. Must
be careful.}
This compositional approach enables local verification of continuous modes This compositional approach enables local verification of continuous modes
without requiring global trajectory analysis across the entire hybrid system. without requiring global trajectory analysis across the entire hybrid system.
\oldt{We will demonstrate this on an Emerson Ovation control system.} We will validate this methodology through hardware-in-the-loop testing
\newt{We will validate this methodology through hardware-in-the-loop testing
on an Emerson Ovation distributed control system, made possible through the on an Emerson Ovation distributed control system, made possible through the
University of Pittsburgh Cyber Energy Center's industry partnership.} University of Pittsburgh Cyber Energy Center's industry partnership.
\dasinline{Where did this come from? Needs context.}
% Pay-off % Pay-off
This approach \oldt{will demonstrate autonomous control can be used for} This approach enables autonomous management of complex nuclear power operations
\newt{enables autonomous management of} complex nuclear power operations
while maintaining safety guarantees. while maintaining safety guarantees.
% OUTCOMES PARAGRAPHS % OUTCOMES PARAGRAPHS
@ -85,12 +63,8 @@ If this research is successful, we will be able to do the following:
into formal specifications. These specifications will be synthesized into into formal specifications. These specifications will be synthesized into
discrete control logic using reactive synthesis tools. discrete control logic using reactive synthesis tools.
% Outcome % Outcome
\oldt{Control engineers will be able to generate mode-switching Control engineers will be able to generate mode-switching
controllers from regulatory procedures with little formal methods controllers from regulatory procedures, reducing barriers to high-assurance control systems.
expertise, reducing barriers to high-assurance control systems.}
\newt{This will reduce barriers to high-assurance control systems by
generating verified mode-switching controllers directly from regulatory
procedures.}\dasinline{This may not be true, and perhaps does not belong.}
% OUTCOME 2 Title % OUTCOME 2 Title
\item \textit{Verify continuous control behavior across mode transitions.} \item \textit{Verify continuous control behavior across mode transitions.}
@ -109,13 +83,8 @@ If this research is successful, we will be able to do the following:
We will implement this methodology on a small modular reactor simulation We will implement this methodology on a small modular reactor simulation
using industry-standard control hardware. using industry-standard control hardware.
% Outcome % Outcome
\oldt{Control engineers will be able to achieve autonomy without Without retraining costs or new equipment, control engineers
retraining costs or developing new equipment by implementing
high-assurance autonomous controls on industrial platforms they already
use.} \newt{Without retraining costs or new equipment, control engineers
will be able to implement high-assurance autonomous controls on industrial will be able to implement high-assurance autonomous controls on industrial
platforms they already use.}\dasinline{Flip the clauses. Put retraining hardware they already use.
and new equipment before the comma, end with building HAHACs with control
hardware they already use. That's the more important part.}
\end{enumerate} \end{enumerate}

287
2-state-of-the-art/state-of-art.tex
View File

@ -1,66 +1,33 @@
\section{State of the Art and Limits of Current Practice} \section{State of the Art and Limits of Current Practice}
The principal aim of this research is to create autonomous reactor control The principal aim of this research is to create autonomous reactor control
systems that are tractably safe. \oldt{To understand what is being automated, systems that are tractably safe. Understanding what is being automated requires
we must first understand how nuclear reactors are operated today. This section understanding how nuclear reactors are operated today. This section examines
examines reactor operators and the operating procedures we aim to leverage, reactor operating procedures, investigates limitations of human-based operation,
then investigates limitations of human-based operation, and concludes with and reviews current formal methods approaches to reactor control systems.
current formal methods approaches to reactor control systems.}
\newt{Understanding what is being automated requires understanding how
nuclear reactors are operated today. This section examines reactor operating
procedures, investigates limitations of human-based operation, and reviews
current formal methods approaches to reactor control
systems.}\dasinline{Don't like ``we'' here. Sounds like ``we're going on an
adventure!'' and feels jocular. Maybe: ``To motivate this proposal, the
state of the art of nuclear reactor control, blah, and blah, are discussed
in this section.''}
\subsection{Current Reactor Procedures and Operation} \subsection{Current Reactor Procedures and Operation}
\oldt{Nuclear plant procedures exist in a hierarchy: normal operating Nuclear plant operations are governed by a hierarchy of written procedures,
procedures for routine operations, abnormal operating procedures for ranging from normal operating procedures for routine operations to Emergency
off-normal conditions, Emergency Operating Procedures (EOPs) for Operating Procedures (EOPs) for design-basis accidents and Severe Accident
design-basis accidents, Severe Accident Management Guidelines (SAMGs) for Management Guidelines (SAMGs) for beyond-design-basis events. These procedures
beyond-design-basis events, and Extensive Damage Mitigation Guidelines exist because reactor operation requires deterministic responses to a wide range
(EDMGs) for catastrophic damage scenarios.} \newt{Nuclear plant operations of plant conditions, from routine power changes to catastrophic failures. These
are governed by a hierarchy of written procedures, ranging from normal procedures must comply with 10 CFR 50.34(b)(6)(ii) and are developed using
operating procedures for routine operations to Emergency Operating guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}. Procedures undergo
Procedures (EOPs) for design-basis accidents and Severe Accident Management technical evaluation, simulator validation testing, and biennial review as part
Guidelines (SAMGs) for beyond-design-basis events. These procedures exist of operator requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this
because reactor operation requires deterministic responses to a wide range rigor, procedures fundamentally lack exhaustive verification of key safety
of plant conditions, from routine power changes to catastrophic properties.
failures.}\dasinline{This sentence is MASSIVE. Why is there 6 lines
describing different types of procedures? WHO CARES? Need a sentence after
saying why we have these procedures.} These procedures must comply with 10
CFR 50.34(b)(6)(ii) and are developed using guidance from
NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their development relies
fundamentally on expert judgment and simulator validation rather than formal
verification.
Procedures undergo technical evaluation, simulator validation testing, and
biennial review as part of operator requalification under 10 CFR
55.59~\cite{10CFR55.59}. Despite this rigor, procedures fundamentally lack
\oldt{formal verification of key safety properties.} \newt{exhaustive
verification of key safety properties.}\dasinline{Does the audience know
what formal verification is at this point? Probably, but should say
differently. Maybe `exhaustive' or `definitive'.} No mathematical proof
exists that procedures cover all possible plant states, that required actions
can be completed within available timeframes, or that transitions between
procedure sets maintain safety invariants.
\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of \textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
correctness and completeness.} \oldt{Current procedure development relies on correctness and completeness.} No mathematical proof exists that procedures
expert judgment and simulator validation. No mathematical proof exists that cover all possible plant states, that required actions can be completed within
procedures cover all possible plant states, that required actions can be available timeframes, or that transitions between procedure sets maintain safety
completed within available timeframes, or that transitions between procedure invariants. Paper-based procedures cannot ensure correct application, and even
sets maintain safety invariants. Paper-based procedures cannot ensure correct computer-based procedure systems lack the formal guarantees that automated
application, and even computer-based procedure systems lack the formal reasoning could provide.
guarantees that automated reasoning could provide.} \newt{Paper-based
procedures cannot ensure correct application, and even computer-based
procedure systems lack the guarantees that automated reasoning could
provide.}\splitpolish{This repeats the ``No mathematical proof exists...''
sentence almost verbatim from the paragraph above. Either cut it from the
paragraph or from the LIMITATION box.}
Nuclear plants operate with multiple control modes: automatic control, where Nuclear plants operate with multiple control modes: automatic control, where
the reactor control system maintains target parameters through continuous the reactor control system maintains target parameters through continuous
@ -74,71 +41,38 @@ safety signals with millisecond response times, and engineered safety
features actuate automatically on accident signals without operator action features actuate automatically on accident signals without operator action
required. required.
\oldt{The division between automated and human-controlled functions reveals This division between automated and human-controlled
the fundamental challenge of hybrid control. Highly automated systems handle
reactor protection---automatic trips on safety parameters, emergency core
cooling actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
operators, however, retain control of strategic decision-making: power level
changes, startup/shutdown sequences, mode transitions, and procedure
implementation.} \newt{This division between automated and human-controlled
functions is itself the hybrid control problem. Automated systems handle functions is itself the hybrid control problem. Automated systems handle
reactor protection: trips on safety parameters, emergency core cooling reactor protection: trips on safety parameters, emergency core cooling
actuation, containment isolation, and basic process actuation, containment isolation, and basic process
control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
operators retain control of everything else: power level changes, operators retain control of everything else: power level changes,
startup/shutdown sequences, mode transitions, and procedure startup/shutdown sequences, mode transitions, and procedure
implementation.}\dasinline{After reading the next sentence, ``key safety'' implementation.
can honestly just be a semicolon.}\dasinline{Not sure what the challenge
actually is as this paragraph is written. What's the
point?}\splitnote{This is the key insight — the hybrid nature is already
there, just not formally verified.}
\subsection{Human Factors in Nuclear Accidents} The persistent role of human error in nuclear safety incidents---despite decades
of improvements in training and procedures---provides the most compelling
\oldt{Current-generation nuclear power plants employ over 3,600 active motivation for formal automated control with mathematical safety guarantees.
NRC-licensed reactor operators in the United Operators hold legal authority under 10 CFR Part 55 to make critical
States~\cite{operator_statistics}. These operators divide into Reactor decisions~\cite{10CFR55}, including departing from normal regulations during
Operators (ROs), who manipulate reactor controls, and Senior Reactor emergencies. This authority itself introduces risk. The Three Mile Island (TMI)
Operators (SROs), who direct plant operations and serve as shift accident demonstrated how a combination of personnel error, design deficiencies,
supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs and and component failures led to partial meltdown when operators misread confusing
one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor and contradictory readings and shut off the emergency water
operator requires several years of training.} \newt{Nuclear plant staffing system~\cite{Kemeny1979}. The President's Commission on TMI identified a
requires at least two Reactor Operators (ROs) and one Senior Reactor fundamental ambiguity: placing responsibility for safe power plant operations on
Operator (SRO) per unit~\cite{10CFR50.54}, with operators requiring several the licensee without formal verification that operators can fulfill this
years of training and NRC licensing under 10 CFR Part responsibility does not guarantee safety. This tension between operational
55~\cite{10CFR55}.}\dasinline{Why is this here? Should this be in broader flexibility and safety assurance remains unresolved: the person responsible for
impacts about running out of ROs? As it is here I have no idea why this is reactor safety is often the root cause of failures.\splitnote{``the person
here.} responsible for reactor safety is often the root cause of failures'' —
devastating summary. Very effective.}
The persistent role of human error in nuclear safety incidents---despite
decades of improvements in training and procedures---provides the most
compelling motivation for formal automated control with mathematical safety
guarantees.\splitnote{Strong thesis for this subsection.} Operators hold
legal authority under 10 CFR Part 55 to make critical
decisions~\cite{10CFR55},\dasinline{Cite.} including departing from normal
regulations during emergencies. \oldt{The Three Mile Island (TMI) accident}
\newt{This authority itself introduces risk. The Three Mile Island (TMI)
accident}\dasinline{Needs a connector here. Like ``But this can in and of
itself prime plants for an accident.'' Then continue.} demonstrated how a
combination of personnel error, design deficiencies, and component failures
led to partial meltdown when operators misread confusing and contradictory
readings and shut off the emergency water system~\cite{Kemeny1979}. The
President's Commission on TMI identified a fundamental ambiguity: placing
responsibility for safe power plant operations on the licensee without
formal verification that operators can fulfill this responsibility does not
guarantee safety. This tension between operational flexibility and safety
assurance remains unresolved: the person responsible for reactor safety is
often the root cause of failures.\splitnote{``the person responsible for
reactor safety is often the root cause of failures'' — devastating summary.
Very effective.}
Multiple independent analyses converge on a striking statistic: 70--80\% of Multiple independent analyses converge on a striking statistic: 70--80\% of
nuclear power plant events are attributed to human error, versus nuclear power plant events are attributed to human error, versus
approximately 20\% to equipment failures~\cite{WNA2020}. More significantly, approximately 20\% to equipment failures~\cite{WNA2020}. More significantly,
the root cause of all severe accidents at nuclear power plants---Three Mile the root cause of all severe accidents at nuclear power plants---Three Mile
Island, Chernobyl, and Fukushima Daiichi---has been identified as poor Island, Chernobyl, and Fukushima Daiichi---has been identified as primarily human
safety management and safety culture: primarily human
factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at
Chinese nuclear power plants from Chinese nuclear power plants from
2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved 2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
@ -159,29 +93,20 @@ drives it home.}
\subsubsection{HARDENS} \subsubsection{HARDENS}
The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS) The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
project represents the most advanced application of formal methods to project represents the most advanced application of formal methods to nuclear
nuclear reactor control systems to date~\cite{Kiniry2024}. reactor control systems to date~\cite{Kiniry2024}. HARDENS aimed to address a
fundamental dilemma: existing U.S. nuclear control rooms rely on analog
technologies from the 1950s--60s. This technology is obsolete compared to modern
control systems and incurs significant risk and cost. A U.S. Nuclear Regulatory
Commission report demonstrated that model-based systems engineering and formal
methods could design, verify, and implement a complex protection system meeting
regulatory criteria. The project delivered a Reactor Trip System (RTS)
implementation with traceability from regulatory requirements to verified
software through formal architecture specifications.
HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear HARDENS employed formal methods tools at
control rooms rely on analog technologies from the
1950s--60s.\dasinline{Source?} This technology is obsolete compared to
modern control systems and incurs significant risk and cost. The NRC
contracted Galois, a formal methods firm, to demonstrate that Model-Based
Systems Engineering and formal methods could design, verify, and implement a
complex protection system meeting regulatory criteria at a fraction of
typical cost. The project delivered a Reactor Trip System (RTS)
implementation with full traceability from \oldt{NRC Request for Proposals
and IEEE standards through formal architecture specifications to verified
software.} \newt{regulatory requirements through formal architecture
specifications to verified software.}\dasinline{Wordsmith this to remove the
RFP and IEEE standards language. Should just say requirements.}
\oldt{HARDENS employed formal methods tools and techniques across the
verification hierarchy.} \newt{HARDENS employed formal methods tools at
every level of system development, from high-level requirements through every level of system development, from high-level requirements through
executable models to generated code.}\dasinline{Zero discussion about what executable models to generated code. High-level specifications used
the verification hierarchy is. What is a specification or a requirement to
someone who hasn't heard of one before?} High-level specifications used
Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to
capture stakeholder requirements, domain engineering, certification capture stakeholder requirements, domain engineering, certification
requirements, and safety requirements. Requirements were analyzed for requirements, and safety requirements. Requirements were analyzed for
@ -192,29 +117,16 @@ models of sensors, actuators, and compute infrastructure. Automatic code
synthesis generated verifiable C implementations and SystemVerilog hardware synthesis generated verifiable C implementations and SystemVerilog hardware
implementations directly from Cryptol models---eliminating the traditional implementations directly from Cryptol models---eliminating the traditional
gap between specification and implementation where errors commonly gap between specification and implementation where errors commonly
arise.\splitnote{Good technical depth on HARDENS toolchain.} arise.
\oldt{Despite its accomplishments, HARDENS has a fundamental limitation Despite these accomplishments, HARDENS addressed only discrete digital
directly relevant to hybrid control synthesis: the project addressed only
discrete digital control logic without modeling or verifying continuous
reactor dynamics. The Reactor Trip System specification and verification
covered discrete state transitions (trip/no-trip decisions), digital sensor
input processing through discrete logic, and discrete actuation outputs
(reactor trip commands). The project did not address continuous dynamics of
nuclear reactor physics. Real reactor safety depends on the interaction
between continuous processes---temperature, pressure, neutron flux---evolving
in response to discrete control decisions. HARDENS verified the discrete
controller in isolation but not the closed-loop hybrid system behavior.}
\newt{Despite these accomplishments, HARDENS addressed only discrete digital
control logic. The Reactor Trip System verification covered discrete state control logic. The Reactor Trip System verification covered discrete state
transitions, digital sensor processing, and discrete actuation outputs. It transitions, digital sensor processing, and discrete actuation outputs. It
did not model or verify continuous reactor dynamics. Real reactor safety did not model or verify continuous reactor dynamics. Real reactor safety
depends on the interaction between continuous processes---temperature, depends on the interaction between continuous processes---temperature,
pressure, neutron flux---evolving in response to discrete control decisions. pressure, neutron flux---evolving in response to discrete control decisions.
HARDENS verified the discrete controller in isolation but not the HARDENS verified the discrete controller in isolation but not a
closed-loop hybrid system behavior.}\dasinline{Edit these to more clearly closed-loop hybrid system behavior.
separate the context from the limit. The limitation should be in the
limitation.}\splitnote{Clear articulation of the gap your work fills.}
\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic \textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic
without continuous dynamics or hybrid system verification.} Verifying without continuous dynamics or hybrid system verification.} Verifying
@ -223,66 +135,49 @@ system exhibits desired continuous behavior such as stability, convergence to
setpoints, or maintained safety margins. setpoints, or maintained safety margins.
HARDENS produced a demonstrator system at Technology Readiness Level 2--3 HARDENS produced a demonstrator system at Technology Readiness Level 2--3
(analytical proof of concept with laboratory breadboard validation) rather (analytical proof of concept with laboratory breadboard validation) rather than
than a deployment-ready system validated through extended operational a deployment-ready system validated through extended operational testing. The
testing. The NRC Final Report explicitly notes~\cite{Kiniry2024} that all NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
material is considered in development, not a finalized product, and that considered in development, not a finalized product, and that ``The demonstration
``The demonstration of its technical soundness was to be at a level of its technical soundness was to be at a level consistent with satisfaction of
consistent with satisfaction of the current regulatory criteria, although the current regulatory criteria, although with no explicit demonstration of how
with no explicit demonstration of how regulatory requirements are regulatory requirements are met.'' The project did not include deployment in
met.''\dasinline{Check this quote. Absolutely damning for HARDENS if true %DAS 3/16/26. I double checked this quote. It's on page 4 of the HARDENS report
and hilarious Galois said this.} The project did not include deployment in actual nuclear facilities, testing with real reactor systems under operational
actual nuclear facilities, testing with real reactor systems under conditions, side-by-side validation with operational analog RTS systems,
operational conditions, side-by-side validation with operational analog RTS systematic failure mode testing, NRC licensing review, or human factors
systems, systematic failure mode testing, NRC licensing review, or human validation with licensed operators in realistic control room scenarios.
factors validation with licensed operators in realistic control room
scenarios.
\textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental \textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
validation.} \oldt{While formal verification provides mathematical validation.} While formal verification provides mathematical correctness
correctness guarantees for the implemented discrete logic, the gap between guarantees for the implemented discrete logic, the gap between formal
formal verification and actual system deployment involves myriad practical verification and actual system deployment involves myriad practical
considerations: integration with legacy systems, long-term reliability under considerations: integration with legacy systems, human-system interaction in
harsh environments, human-system interaction in realistic operational realistic operational contexts, and regulatory acceptance of formal methods as
contexts, and regulatory acceptance of formal methods as primary assurance primary assurance evidence remain as significant challenges.
evidence.} \newt{The gap between formal verification and actual system
deployment remains wide: integration with legacy systems, long-term
reliability under harsh environments, human-system interaction, and
regulatory acceptance of formal methods as primary assurance
evidence.}\dasinline{Same as before. Separate limit from context better.}
\subsubsection{Sequent Calculus and Differential Dynamic Logic} \subsubsection{Sequent Calculus and Differential Dynamic Logic}
\oldt{There has been additional work to do verification of hybrid systems by A separate line of work
extending the temporal logics directly.} \newt{A separate line of work
extends temporal logics to verify hybrid systems extends temporal logics to verify hybrid systems
directly.}\dasinline{Need to introduce temporal logic and FRET here first.} directly. The result has been the field of differential dynamic logic (dL). dL
The result has been the field of differential dynamic logic (dL). dL
introduces two additional operators into temporal logic: the box operator and introduces two additional operators into temporal logic: the box operator and
the diamond operator. The box operator \([\alpha]\phi\) states that for some the diamond operator. The box operator \([\alpha]\phi\) states that for some
region \(\phi\), the hybrid system \(\alpha\) always remains within that region \(\phi\), the hybrid system \(\alpha\) always remains within that
region. In this way, it is a safety \oldt{ivariant} \newt{invariant} being region. In this way, it is a safety invariant being
enforced for the system.\splitfix{Typo: ``ivariant'' should be enforced for the system. The second operator, the diamond operator
``invariant''} The second operator, the diamond operator
\(<\alpha>\phi\) says that for the region \(\phi\), there is at least one \(<\alpha>\phi\) says that for the region \(\phi\), there is at least one
trajectory of \(\alpha\) that enters that region. This is a declaration of a trajectory of \(\alpha\) that enters that region. This is a declaration of a
liveness property. liveness property.
%source: https://symbolaris.com/logic/dL.html
While dL allows for the specification of these liveness and safety While dL allows for the specification of these liveness and safety properties,
properties, actually proving them for a given hybrid system is quite actually proving them for a given hybrid system is quite difficult. Automated
difficult. Automated proof assistants such as KeYmaera X exist to help proof assistants such as KeYmaera X exist to help develop proofs of systems
develop proofs of systems using dL, but so far have been insufficient for using dL, but so far have been insufficient for reasonably complex hybrid
reasonably complex hybrid systems. The main issue behind creating system systems. The main issue behind creating system proofs using dL is
proofs using dL is state space explosion and non-terminating solutions. non-terminating solutions. Approaches have been made to alleviate these issues
%Source: that one satellite tracking paper that has the problem with the for nuclear power contexts using contract and decomposition based methods, but
%gyroscopes overloding and needing to dump speed all the time do not yet constitute a complete design methodology \cite{kapuria_using_2025}.
Approaches have been made to alleviate these issues for nuclear power
contexts using contract and decomposition based methods, \oldt{but are far
from a complete methodology to design systems with.} \newt{but do not yet
constitute a complete design methodology.}\splitpolish{``but are far from a
complete methodology to design systems with'' — awkward ending preposition.}
%source: Manyu's thesis.
Instead, these approaches have been used on systems that have been designed a Instead, these approaches have been used on systems that have been designed a
priori, and require expert knowledge to create the system proofs. priori, and require expert knowledge to create the system proofs.
@ -296,8 +191,4 @@ post-hoc analysis of existing systems, not for the constructive design of
autonomous controllers.} Current dL-based approaches verify systems that autonomous controllers.} Current dL-based approaches verify systems that
have already been designed, requiring expert knowledge to construct proofs. have already been designed, requiring expert knowledge to construct proofs.
They have not been applied to the synthesis of new controllers from They have not been applied to the synthesis of new controllers from
operational requirements.\splitinline{Your comment here is spot-on. You operational requirements.
should add a LIMITATION box: \textit{Differential dynamic logic has been
used for post-hoc analysis of existing systems, not for the constructive
design of autonomous controllers.} This is exactly the gap you're filling —
you're doing synthesis, not just verification.}

BIN
20260314_reading.pdf Normal file
View File

Binary file not shown.

483
3-research-approach/approach.tex
View File

@ -1,54 +1,5 @@
\section{Research Approach} \section{Research Approach}
% ============================================================================
% STRUCTURE (maps to Thesis.RA tasks):
% 1. Introduction + Hybrid Systems Definition (Task 34)
% 2. System Requirements and Specifications (Task 35)
% 3. Discrete Controller Synthesis (Task 36)
% 4. Continuous Controllers Overview (Task 37)
% 4.1 Transitory Modes (Task 38)
% 4.2 Stabilizing Modes (Task 39)
% 4.3 Expulsory Modes (Task 40)
% 5. Industrial Implementation (Task 41)
% ============================================================================
% ----------------------------------------------------------------------------
% 1. INTRODUCTION AND HYBRID SYSTEMS DEFINITION
% ----------------------------------------------------------------------------
\oldt{Previous approaches to autonomous control have verified discrete
switching logic or continuous control behavior, but not both simultaneously.
Validation of continuous controllers today consists of extensive simulation
trials. Discrete switching logic for routine operation has been driven by
human operators, whose evaluation includes simulated control room testing and
human factors research. Neither method, despite being extremely resource
intensive, provides rigorous guarantees of control system behavior. HAHACS
bridges this gap by composing formal methods from computer science with
control-theoretic verification, formalizing reactor operations using the
framework of hybrid automata.} \newt{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.}\dasinline{Honestly just get rid of this whole
paragraph.}
The challenge of hybrid system verification lies in the interaction between
discrete and continuous dynamics. Discrete transitions change the
\oldt{governing} \newt{active}\dasinline{Governing what? People? Whos in
Whoville?} 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.\splitpolish{Missing space before ``Our}\dasinline{This whole
paragraph should just be after the definition of the tuple. First sentence
can stay, but all this explanation should move.} 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.\splitsuggest{Compositional verification
claim needs citation. See assume-guarantee literature (Henzinger, Alur).
None of the NEEDS\_REVIEWED papers directly prove this composition is sound
for your specific approach.} 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.
To build a high-assurance hybrid autonomous control system (HAHACS), we must To build a high-assurance hybrid autonomous control system (HAHACS), we must
first establish a mathematical description of the system. This work draws on first establish a mathematical description of the system. This work draws on
automata theory, temporal logic, and control theory. A hybrid system is a automata theory, temporal logic, and control theory. A hybrid system is a
@ -58,7 +9,7 @@ system. This means that the system does not have external input and that
continuous states do not change instantaneously when discrete states change. continuous states do not change instantaneously when discrete states change.
For our systems of interest, the continuous states are physical quantities For our systems of interest, the continuous states are physical quantities
that are always Lipschitz continuous. This nomenclature is borrowed from the that are always Lipschitz continuous. This nomenclature is borrowed from the
Handbook on Hybrid Systems Control \cite{HANDBOOK ON HYBRID SYSTEMS}, but is Handbook on Hybrid Systems Control \cite{lunz_handbook_2009}, but is
redefined here for convenience: redefined here for convenience:
\begin{equation} \begin{equation}
@ -85,18 +36,33 @@ where:
\item $Inv$: safety invariants on the continuous dynamics \item $Inv$: safety invariants on the continuous dynamics
\end{itemize} \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. 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.\splitsuggest{Compositional verification claim
needs citation. See assume-guarantee literature (Henzinger, Alur). None of the
NEEDS\_REVIEWED papers directly prove tHANDBOOK ON HYBRID SYSTEMShis composition is sound for your
specific approach.} 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 The creation of a HAHACS amounts to the construction of such a tuple
together with proof artifacts demonstrating that the intended behavior of the together with proof artifacts demonstrating that the intended behavior of the
control system is satisfied by its actual control system is satisfied by its actual
implementation.\oldt{}\newt{ In concrete terms, this means producing a implementation. In concrete terms, this means producing a
discrete automaton whose transitions are provably correct, continuous discrete automaton whose transitions are provably correct, continuous
controllers whose behavior is verified against transition requirements, and controllers whose behavior is verified against transition requirements, and
formal evidence linking the two.}\dasinline{Add a sentence explaining what formal evidence linking the two. This approach is tractable now because the
this actually means.} This approach is tractable now because the
infrastructure for each component has matured. The novelty is not in the infrastructure for each component has matured. The novelty is not in the
individual pieces, but in the architecture that connects individual pieces, but in the architecture that connects
them.\splitnote{This is your key insight --- the novelty is compositional, them. By defining entry, exit, and safety conditions at the
not component-level.} By defining entry, exit, and safety conditions at the
discrete level first, we transform the intractable problem of global hybrid discrete level first, we transform the intractable problem of global hybrid
verification into a collection of local verification problems with clear verification into a collection of local verification problems with clear
interfaces. Verification is performed per mode rather than on the full interfaces. Verification is performed per mode rather than on the full
@ -153,8 +119,6 @@ operations.
\node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$}; \node[dynamics] at (5,-4.9) {$\dot{x} = f_3(x)$};
\end{tikzpicture} \end{tikzpicture}
\dasinline{Figure dynamics show control inputs u, but these systems are
autonomous. What's up with that?}
\caption{Simplified hybrid automaton for reactor startup. Each discrete \caption{Simplified hybrid automaton for reactor startup. Each discrete
state $q_i$ has associated continuous dynamics $f_i$. Guard conditions state $q_i$ has associated continuous dynamics $f_i$. Guard conditions
on transitions (e.g., $T_{avg} > T_{min}$) are predicates over on transitions (e.g., $T_{avg} > T_{min}$) are predicates over
@ -164,15 +128,8 @@ autonomous. What's up with that?}
mode.} mode.}
\label{fig:hybrid_automaton} \label{fig:hybrid_automaton}
\end{figure} \end{figure}
\dasnote{There's no reference of this figure in the prose. Perhaps some
%%% NOTES (Section 1): explanation could be done in a paragraph to explain the thought process.}
% - May want to clarify the "no external input" claim with a footnote about
% strategic inputs (e.g., remote start/stop commands)
% - The reset map R is often identity for physical systems; clarify if needed
% ----------------------------------------------------------------------------
% 2. SYSTEM REQUIREMENTS AND SPECIFICATIONS
% ----------------------------------------------------------------------------
\subsection{System Requirements, Specifications, and Discrete Controllers} \subsection{System Requirements, Specifications, and Discrete Controllers}
Human control of nuclear power can be divided into three different scopes: Human control of nuclear power can be divided into three different scopes:
@ -186,28 +143,20 @@ chemistry. Tactical control has already been somewhat automated in nuclear
power plants today, and is generally considered ``automatic control'' when power plants today, and is generally considered ``automatic control'' when
autonomous. These controls are almost always continuous systems with a direct autonomous. These controls are almost always continuous systems with a direct
impact on the physical state of the impact on the physical state of the
plant.\dasinline{This should be written to be clear this isn't an exhaustive plant. Tactical control objectives include, but are not limited
list.} Tactical control objectives include\oldt{}\newt{, but are not limited to, maintaining pressurizer level, maintaining core temperature, or
to,} maintaining pressurizer level, maintaining core temperature, or
adjusting reactivity with a chemical shim. adjusting reactivity with a chemical shim.
The level of control \oldt{linking} \newt{linking The level of control linking these two extremes is the operational control
these two extremes of}\dasinline{Linking of these two extremes. Don't even
say control here.} \oldt{these two extremes is the} operational control
scope. Operational control is the primary responsibility of human operators scope. Operational control is the primary responsibility of human operators
today. Operational control takes the current strategic objective and today. Operational control takes the current strategic objective and implements
implements tactical control objectives to drive the plant towards strategic tactical control objectives to drive the plant towards strategic goals. In this
goals. In this way, it bridges high-level and low-level goals. A strategic way, it bridges high-level and low-level goals. A strategic goal may be to
goal may be to perform refueling at a certain time, while the tactical level perform refueling at a certain time, while the tactical level of the plant is
of the plant is currently focused on maintaining a certain core temperature. currently focused on maintaining a certain core temperature. The operational
The operational level issues the shutdown procedure, using several smaller level issues the shutdown procedure, using several smaller tactical goals along
tactical goals along the way to achieve this \oldt{objective.} the way to achieve this strategic
\newt{strategic objective.}\dasinline{This STRATEGIC objective.} Thus, the objective.
combination of the operational and tactical levels fundamentally forms a
hybrid controller. The tactical level is the continuous evolution of the
plant according to the control input and control law, while the operational
level is a discrete state evolution that determines which tactical control
law to apply.
%Say something about autonomous control systems near here? %Say something about autonomous control systems near here?
@ -253,43 +202,34 @@ law to apply.
\end{figure} \end{figure}
\oldt{This operational control level is the main reason for the requirement This operational control level is the main reason for the requirement of human
of human operators in nuclear control today. The hybrid nature of this operators in nuclear control today. The hybrid nature of this control system
control system makes it difficult to prove that a controller will perform makes it difficult to prove what the behavior of the combined hybrid system will
according to strategic requirements, as unified infrastructure for building do across the entire state-space, so human operators have been used as a
and verifying hybrid systems does not currently exist. Humans have been used stop-gap for safety. Humans have been used for this layer because their general
for this layer because their general intelligence has been relied upon as a intelligence has been relied upon as a safe way to manage the hybrid nature of
safe way to manage the hybrid nature of this system.} \newt{The hybrid this system---if a failure occured, it has been assumed a human operator can
nature of this control problem is the reason human operators remain figure out a solution to maintain plant performance and safety without
essential. Because unified infrastructure for building and verifying hybrid exhaustive knowledge of plant behavior. However, human factors research has
systems does not currently exist, the operational layer has relied on human sought to minimize the need for general human reasoning by creating extremely
general intelligence to manage the interaction between discrete decisions and prescriptive operating manuals with strict procedures dictating what control to
continuous dynamics.}\dasinline{This operational control level is the main implement at a given time. These operating manuals have minimized the role of
reason\ldots Add a sentence why. Because the hybrid dynamics have previously human operators today, are the key to the automating the operational control
been `unknowable', it's been assumed that a human operator could figure it scope.
out on the fly. Or similar.} \oldt{But these operators use prescriptive
operating manuals to perform their control with strict procedures on what
control to implement at a given time.} \newt{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.}\dasinline{Say but human factors
has been seeking to eliminate the need for general human behavior by creating
extremely prescriptive operating manuals. This is our leverage.} These
procedures are the key to the operational control scope.
The method of constructing a HAHACS in this proposal leverages two key The method of constructing a HAHACS in this proposal leverages two key
observations about current practice. First, the operational scope control is observations about current practice. First, the operational scope control is
effectively discrete control. Second, the rules for implementing this effectively discrete control. Second, the rules for implementing this control
control are described prior to their implementation in operating procedures. are described in operating procedures prior to their implementation. Instead of
Before constructing a HAHACS, we must completely describe its intended implementing these procudures with a human controller, we rigorize the
behavior. The behavior of any control system originates in requirements: instructions as a set of formal requirements. The behavior of any control system
statements about what the system must do, must not do, and under what originates in requirements: statements about what the system must do, must not
conditions. For nuclear systems, these requirements derive from multiple do, and under what conditions. For nuclear systems, these requirements derive
sources including regulatory mandates, design basis analyses, and operating from multiple sources including regulatory mandates, design basis analyses, and
procedures. The challenge is formalizing these requirements with sufficient aforementioned operating procedures. The challenge is formalizing these requirements with
precision that they can serve as the foundation for autonomous control system sufficient precision that they can serve as the foundation for autonomous
synthesis and verification. We can build these requirements using temporal control system synthesis and verification. We can build these requirements using
logic.\dasinline{We definitely need some temporal logic juice in the SOTA.} temporal logic.
Temporal logic is a powerful set of semantics for building systems with Temporal logic is a powerful set of semantics for building systems with
complex but deterministic behavior. Temporal logic extends classical complex but deterministic behavior. Temporal logic extends classical
@ -302,27 +242,26 @@ also be expressed as temporal logic statements. These specifications form the
basis of any proofs about a HAHACS and constitute the fundamental truth basis of any proofs about a HAHACS and constitute the fundamental truth
statements about what the behavior of the system is designed to be. statements about what the behavior of the system is designed to be.
Discrete mode transitions include predicates that are Boolean functions over Discrete mode transitions include predicates that are Boolean functions over the
the continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true}, continuous state space: $p_i: \mathcal{X} \rightarrow \{\text{true},
\text{false}\}$. These predicates formalize conditions like ``coolant \text{false}\}$. These predicates formalize conditions like ``coolant
temperature exceeds 315\textdegree{}C'' or ``pressurizer level is between temperature exceeds 315\textdegree{}C'' or ``pressurizer level is between 30\%
30\% and 60\%.'' Critically, we do not impose this discrete abstraction and 60\%.'' Critically, we do not impose this discrete abstraction artificially.
artificially. Operating procedures for nuclear systems already define Operating procedures for nuclear systems already define go/no-go conditions as
go/no-go conditions as discrete predicates. These thresholds come from discrete predicates, but do so in natural language. These thresholds come from
design basis safety analysis and have been validated over decades of design basis safety analysis and have been validated over decades of operational
operational experience. Our methodology assumes this domain knowledge exists experience. Our methodology assumes this domain knowledge exists and provides a
and provides a framework to formalize it. This is why the approach is framework to formalize it. This is why the approach is feasible for nuclear
feasible for nuclear applications specifically: the hard work of defining applications specifically: the work of defining safe operating boundaries has
safe operating boundaries has already been done by generations of nuclear already been done by generations of nuclear engineers. The work of translating
engineers. these requirements from interpretable natural language to a formal requirement is
what remains to be done.
Linear temporal logic (LTL) is particularly well-suited Linear temporal logic (LTL) is particularly well-suited for specifying reactive
for\dasinline{Some of this could be in SOTA vs here. Examples in nuclear
space should be in RA, but the general idea of temporal logic and where it
came from in the context of computers could be in SOTA.} specifying reactive
systems. LTL formulas are built from atomic propositions (our discrete systems. LTL formulas are built from atomic propositions (our discrete
predicates) using Boolean connectives and temporal operators. The key predicates) using Boolean connectives and temporal operators. The key temporal
temporal operators are: operators are:
\begin{itemize} \begin{itemize}
\item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state \item $\mathbf{X}\phi$ (next): $\phi$ holds in the next state
\item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states \item $\mathbf{G}\phi$ (globally): $\phi$ holds in all future states
@ -330,6 +269,7 @@ temporal operators are:
\item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes \item $\phi \mathbf{U} \psi$ (until): $\phi$ holds until $\psi$ becomes
true true
\end{itemize} \end{itemize}
These operators allow us to express safety properties (``the reactor never These operators allow us to express safety properties (``the reactor never
enters an unsafe configuration''), liveness properties (``the system enters an unsafe configuration''), liveness properties (``the system
eventually reaches operating temperature''), and response properties (``if eventually reaches operating temperature''), and response properties (``if
@ -339,19 +279,19 @@ time'').%
checking does NOT support liveness properties. Your ``eventually reaches checking does NOT support liveness properties. Your ``eventually reaches
operating temperature'' example may need alternative verification approach.} operating temperature'' example may need alternative verification approach.}
To build these temporal logic statements, an intermediary tool called FRET is To build these temporal logic statements, an intermediary tool called FRET is
planned to be used. FRET stands for Formal Requirements Elicitation Tool, planned to be used. FRET stands for Formal Requirements Elicitation Tool, and
and was developed by NASA to build high-assurance timed systems. FRET is an was developed by NASA to build high-assurance timed systems. FRET is an
intermediate language between temporal logic and natural language that allows intermediate language between temporal logic and natural language that allows
for rigid definitions of temporal behavior while using a syntax accessible to for rigid definitions of temporal behavior while using a syntax accessible to
engineers without formal methods expertise. This benefit is crucial for the engineers without formal methods expertise\cite{katis_realizability_2022}. This
feasibility of this methodology in industry. By reducing the expert knowledge benefit is crucial for the feasibility of this methodology in industry. By
required to use these tools, their adoption with the current workforce reducing the expert knowledge required to use these tools, their adoption with
becomes easier. the current workforce becomes easier.
A key feature of FRET is the ability to start with logically imprecise A key feature of FRET is the ability to start with logically imprecise
statements and consecutively refine them into well-posed specifications. We statements and consecutively refine them into well-posed
specifications\cite{katis_realizibility_2022, pressburger_using_2023}. We
can use this to our advantage by directly importing operating procedures and can use this to our advantage by directly importing operating procedures and
design requirements into FRET in natural language, then iteratively refining design requirements into FRET in natural language, then iteratively refining
them into specifications for a HAHACS. This has two distinct benefits. them into specifications for a HAHACS. This has two distinct benefits.
@ -359,82 +299,44 @@ First, it allows us to draw a direct link from design documentation to
digital system implementation. Second, it clearly demonstrates where natural digital system implementation. Second, it clearly demonstrates where natural
language documents are insufficient. These procedures may still be used by language documents are insufficient. These procedures may still be used by
human operators, so any room for interpretation is a weakness that must be human operators, so any room for interpretation is a weakness that must be
addressed.\splitnote{FRET has been validated: Katis 2022 (pp.1-2, Section addressed.
0.3) demonstrates FRET's FRETish template system with 160 distinct patterns;
Pressburger 2023 (pp.17, Section 1) shows successful application to
Lift+Cruise case study with 53 requirements formalized and iteratively
refined---strong evidence your approach is feasible.}
(Some examples of where FRET has been used and why it will be successful \dasinline{Maybe add more details about FRET case studies here. This would be
here) Pressburger and Katis.}
%%% NOTES (Section 2):
% - Add concrete FRET example showing requirement $\rightarrow$ FRETish
% $\rightarrow$ LTL
% - Discuss hysteresis and how to prevent mode chattering near boundaries
% - Address sensor noise and measurement uncertainty in threshold definitions
% - Consider numerical precision issues when creating discrete automata
% ----------------------------------------------------------------------------
% 3. DISCRETE CONTROLLER SYNTHESIS
% ----------------------------------------------------------------------------
Once system requirements are defined as temporal logic specifications, we use Once system requirements are defined as temporal logic specifications, we use
them to build the discrete control system. To do this, reactive synthesis them to build the discrete control system. To do this, reactive synthesis
tools are employed. Reactive synthesis is a field in computer science that tools are employed. Reactive synthesis is a field in computer science that
deals with the automated creation of reactive programs from temporal logic deals with the automated creation of reactive programs from temporal logic
specifications. A reactive program is one that, for a given state, takes an specifications. A reactive program is one that, for a given state, takes an
input and produces an output. Our systems fit exactly this mold: the current 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 discrete state and status of guard conditions are the input, while the
output is the next discrete state. output is the next discrete state.
Reactive synthesis solves the following problem: given an LTL formula Reactive synthesis solves the following problem: given an LTL formula $\varphi$
$\varphi$ that specifies desired system behavior, automatically construct a that specifies desired system behavior, automatically construct a finite-state
finite-state machine (strategy) that produces outputs in response to machine (strategy) that produces outputs in response to environment inputs such
environment inputs such that all resulting execution traces satisfy that all resulting execution traces satisfy $\varphi$. If such a strategy
$\varphi$. If such a strategy exists, the specification is called exists, the specification is called \emph{realizable}. The synthesis algorithm
\emph{realizable}. The synthesis algorithm either produces a either produces a correct-by-construction controller or reports that no such
correct-by-construction controller or reports that no such controller can controller can exist. This realizability check is itself valuable: an
exist. This realizability check is itself valuable: an unrealizable unrealizable specification indicates conflicting or impossible requirements in
specification indicates conflicting or impossible requirements in the the original procedures. The current implementation and one of the main uses of
original procedures.\splitnote{Realizability is proven valuable: Katis 2022 FRET today is for exactly this purpose---multiple case studies have used FRET
(pp.7-10) shows FRET diagnosis found 8 minimal unrealizable cores in for the refinement of unrealizable specifications into realizable systems
infusion pump case; Pressburger 2023 (pp.19-21) shows unrealizability \cite{katis_realizability_2022, pressburger_using_2023}.
revealed under-specification (missing stay requirements in LPC aircraft),
driving iterative refinement---this suggests your synthesis approach will
help engineers catch requirement errors early.}
The main advantage of reactive synthesis is that at no point in the The main advantage of reactive synthesis is that at no point in the production
production of the discrete automaton is human engineering of the of the discrete automaton is human engineering of the implementation required.
implementation required. The resultant automaton is correct by construction. The resultant automaton is correct to the specification by construction. This
This method of construction eliminates the possibility of human error at the method of construction eliminates the possibility of human error at the
implementation stage entirely. \oldt{Instead, the effort on the human implementation stage entirely. The effort shifts entirely to specifying correct
designer is directed at the specification of system behavior itself. This has behavior rather than implementing it. This has two critical implications. First,
two critical implications. First, it makes the creation of the discrete every mode transition can be traced back through the specification to its
controller tractable. The reasons the controller changes between modes can be
traced back to the specification and thus to any requirements, which provides
a trace for liability and justification of system behavior. Second, discrete
control decisions made by humans are reliant on the human operator operating
correctly. Humans are intrinsically probabilistic creatures who cannot
eliminate human error. By defining the behavior of this system using temporal
logics and synthesizing the controller using deterministic algorithms, we are
assured that strategic decisions will always be made according to operating
procedures.} \newt{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. originating requirement, providing a clear liability and justification chain.
Second, by defining system behavior in temporal logic and synthesizing the Second, by defining system behavior in temporal logic and synthesizing the
controller using deterministic algorithms, discrete control decisions become controller using deterministic algorithms, discrete control decisions become
provably consistent with operating provably consistent with operating procedures.
procedures.}\dasinline{Some goofy issue-point stuff going on in this
paragraph.}\splitnote{Strix (Luttenberger 2020, pp.1-3) is a practical
reactive synthesis tool winning SYNTCOMP competitions; handles LTL specs for
systems with large state spaces. Strix uses parity games and
forward-explorative construction (pp.7-8) to
scale---recommend as your synthesis backend for nuclear
procedures.}\splitsuggest{Consider discussing scalability: Strix handles
large alphabets better (v19.07 update, p.30), but still struggles with very
large specifications. Document expected spec size for SmAHTR startup
procedures to set expectations.}
(Talk about how one would go from a discrete automaton to actual (Talk about how one would go from a discrete automaton to actual
code)\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable code)\splitnote{GR(1) fragment (Maoz \& Ringert 2015, pp.1-4) is tractable
@ -450,34 +352,22 @@ LTL specs fit GR(1) or full LTL needed---if full LTL required, computational
cost grows but Strix may handle it (confirm scalability claim with specific cost grows but Strix may handle it (confirm scalability claim with specific
spec size estimates for startup/shutdown procedures).} spec size estimates for startup/shutdown procedures).}
%%% NOTES (Section 3):
% - Mention computational complexity of synthesis (doubly exponential worst
% case)
% - Discuss how specification structure affects synthesis tractability
% - Reference GR(1) fragment as a tractable subset commonly used in practice
% - May want to include an example automaton figure
% ----------------------------------------------------------------------------
% 4. CONTINUOUS CONTROLLERS
% ----------------------------------------------------------------------------
\subsection{Continuous Control Modes} \subsection{Continuous Control Modes}
The synthesis of the discrete operational controller is only half of an The synthesis of the discrete operational controller is only half of an
autonomous controller. These control systems are hybrid, with both discrete autonomous controller. These control systems are hybrid, with both discrete and
and continuous components. This section describes the continuous control continuous components. This section describes the continuous control modes that
modes that execute within each discrete state, and how we verify that they execute within each discrete state, and how we verify that they satisfy the
satisfy the requirements imposed by the discrete layer. It is important to requirements imposed by the discrete layer. It is important to clarify the scope
clarify the scope of this methodology with respect to continuous controller of this methodology with respect to continuous controller design. This work will
design. This work \oldt{verifies} \newt{will verify continuous controllers; it does not synthesize them. The distinction
verify}\dasinline{Verb tense: ``will verify''.} continuous controllers; it parallels model checking in software verification: model checking does not tell
does not synthesize them. The distinction parallels model checking in engineers how to write correct software, but it verifies whether a given
software verification: model checking does not tell engineers how to write implementation satisfies its specification. Similarly, we assume that continuous
correct software, but it verifies whether a given implementation satisfies controllers can be designed using standard control theory techniques, and to
its specification. Similarly, we assume that continuous controllers can be that end, are not prohibitive to create. Our contribution is a verification
designed using standard control theory techniques. Our contribution is a framework that confirms candidate controllers compose correctly with the
verification framework that confirms candidate controllers compose correctly discrete layer to produce a safe hybrid system.
with the discrete layer to produce a safe hybrid system.
The operational control scope defines go/no-go decisions that determine what 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 kind of continuous control to implement. The entry or exit conditions of a
@ -485,12 +375,12 @@ discrete state are themselves the guard conditions $\mathcal{G}$ that define
the boundaries for each continuous controller's allowed state-space region. the boundaries for each continuous controller's allowed state-space region.
These continuous controllers all share a common state space, but each These continuous controllers all share a common state space, but each
individual continuous control mode operates within its own partition defined individual continuous control mode operates within its own partition defined
by the discrete state $q_i$ and the associated guards. This partitioning of by the discrete state $q_i$ and the associated guard conditions. This partitioning of
the continuous state space among several discrete vector fields has the continuous state space among several distinct vector fields has
traditionally been a difficult problem for validation and verification. The traditionally been a difficult problem for validation and verification. The
discontinuity of the vector fields at discrete state interfaces makes discontinuity of the vector fields at discrete state interfaces makes
reachability analysis computationally expensive, and analytic solutions often reachability analysis computationally expensive, and analytic solutions often
become intractable \cite{MANYUS THESIS}. become intractable \cite{kapuria_using_2025, lang_formal_2021}.
We circumvent these issues by designing our hybrid system from the bottom up 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 with verification in mind. Each continuous control mode has an input set and
@ -509,7 +399,7 @@ continuous controller design:
These are derived from invariants \(Inv\). These are derived from invariants \(Inv\).
\end{enumerate} \end{enumerate}
These sets come directly from the discrete controller synthesis and define These sets come directly from the discrete controller synthesis and define
precise objectives for continuous control.\dasinline{This SOUNDS like precise objectives for continuous control.\dasnote{This SOUNDS like
assume-guarantee stuff. Maybe make that connection formal and cite it?} The 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 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 $\mathcal{X}_{entry,i}$ to some state in $\mathcal{X}_{exit,i}$ while
@ -522,34 +412,29 @@ verifying 6 components in isolation then system---your three-mode structure
maps perfectly to this decomposition, reducing verification complexity from maps perfectly to this decomposition, reducing verification complexity from
curse of dimensionality.} curse of dimensionality.}
We classify continuous controllers into three types based on their We classify continuous controllers into three types based on their objectives:
objectives: transitory, stabilizing, and expulsory.\splitnote{This transitory, stabilizing, and expulsory. Each type has distinct verification
three-mode taxonomy is elegant --- maps verification tools to control requirements that determine which formal methods tools are appropriate.
objectives cleanly.} Each type has distinct verification requirements that
determine which formal methods tools are appropriate.
%%% NOTES (Section 4): \dasinline{
% - Add figure showing the relationship between entry/exit/safety sets \begin{itemize}
% - Discuss how standard control techniques (LQR, MPC, PID) fit into this \item Add figure showing the relationship between entry/exit/safety sets
% framework \item Mention assume guarantee compositional stuff and how that fits in here
% - Mention assume-guarantee reasoning for compositional verification \end{itemize}
}
% ----------------------------------------------------------------------------
% 4.1 TRANSITORY MODES
% ----------------------------------------------------------------------------
\subsubsection{Transitory Modes} \subsubsection{Transitory Modes}
Transitory modes are continuous controllers designed to move the plant from Transitory modes are continuous controllers designed to move the plant from one
one discrete operating condition to another. Their purpose is to execute discrete operating condition to another. Their purpose is to execute
transitions: starting from entry conditions, reach exit conditions, and transitions: starting from entry conditions, reach exit conditions, and maintain
maintain safety invariants throughout. Examples include power ramp-up safety invariants throughout. Examples include but are not limited to power
sequences, cooldown procedures, and load-following maneuvers. ramp-up sequences, cooldown procedures, and load-following maneuvers.
The control objective for a transitory mode can be stated formally. Given The control objective for a transitory mode can be stated formally. Given
entry conditions $\mathcal{X}_{entry}$, exit conditions entry conditions $\mathcal{X}_{entry}$, exit conditions
$\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and $\mathcal{X}_{exit}$, safety invariant $\mathcal{X}_{safe}$, and
closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy: closed-loop dynamics $\dot{x} = f(x)$, the controller must satisfy:
\[ \[
\forall x_0 \in \mathcal{X}_{entry}: \exists T > 0: x(T) \in \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} \mathcal{X}_{exit} \land \forall t \in [0,T]: x(t) \in \mathcal{X}_{safe}
@ -557,9 +442,9 @@ closed-loop dynamics $\dot{x} = f(x, u(x))$, the controller must satisfy:
That is, from any valid entry state, the trajectory must eventually reach the That is, from any valid entry state, the trajectory must eventually reach the
exit condition without ever leaving the safe region. exit condition without ever leaving the safe region.
Verification of transitory modes uses reachability analysis. Reachability Verification of transitory modes will use reachability analysis. Reachability
analysis computes the set of all states reachable from a given initial set analysis computes the set of all states reachable from a given initial set
under the system dynamics. For a transitory mode to be valid, the reachable under the system dynamics\dasnote{cite reachability tools here}. For a transitory mode to be valid, the reachable
set from $\mathcal{X}_{entry}$ must satisfy two conditions: set from $\mathcal{X}_{entry}$ must satisfy two conditions:
\begin{enumerate} \begin{enumerate}
\item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the \item The reachable set eventually intersects $\mathcal{X}_{exit}$ (the
@ -575,12 +460,12 @@ states reachable within time horizon $T$:
\mathcal{X}_{exit} \neq \emptyset \mathcal{X}_{exit} \neq \emptyset
\] \]
\textcolor{blue}{Because the discrete controller defines clear boundaries in Because the discrete controller defines clear boundaries in
continuous state space, the verification problem for each transitory mode is continuous state space, the verification problem for each transitory mode is
well-posed. We know the possible initial conditions, we know the target well-posed. We know the possible initial conditions, we know the target
conditions, and we know the safety envelope. The verification task is to conditions, and we know the safety envelope. The verification task is to
confirm that the candidate continuous controller achieves the objective from confirm that the candidate continuous controller achieves the objective from
all possible starting points.} all possible starting points.
Several tools exist for computing reachable sets of hybrid systems, including Several tools exist for computing reachable sets of hybrid systems, including
CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool depends on the CORA, Flow*, SpaceEx, and JuliaReach. The choice of tool depends on the
@ -608,21 +493,17 @@ verification, reducing complexity from monolithic analysis.}
% - Mention that the Mealy machine perspective unifies this: continuous system % - Mention that the Mealy machine perspective unifies this: continuous system
% IS the transition, entry/exit conditions are the discrete states % IS the transition, entry/exit conditions are the discrete states
% ----------------------------------------------------------------------------
% 4.2 STABILIZING MODES
% ----------------------------------------------------------------------------
\subsubsection{Stabilizing Modes} \subsubsection{Stabilizing Modes}
Stabilizing modes are continuous controllers with an objective of maintaining Stabilizing modes are continuous controllers with an objective of maintaining
a particular discrete state indefinitely. Rather than driving the system a particular discrete state indefinitely. Rather than driving the system
toward an exit \oldt{condition,} \newt{state,}\dasinline{``mode'' --- toward an exit state, they keep the system within a safe
``condition'' here sounds goofy.} they keep the system within a safe
operating region. Examples include steady-state power operation, hot standby, operating region. Examples include steady-state power operation, hot standby,
and load-following at constant power level. Reachability analysis for and load-following at constant power level. Reachability analysis for
stabilizing modes may not be a suitable approach to validation. Instead, we stabilizing modes may not be a suitable approach to validation. Instead, we
plan to use barrier certificates. Barrier certificates analyze the dynamics plan to use barrier certificates. Barrier certificates analyze the dynamics
of the system to determine whether flux across a given boundary exists. They of the system to determine whether flux across a given boundary
exists\dasnote{cite barrier certificate stuff here}. In other words, they
evaluate whether any trajectory leaves a given boundary. This definition is evaluate whether any trajectory leaves a given boundary. This definition is
exactly what defines the validity of a stabilizing continuous control mode. exactly what defines the validity of a stabilizing continuous control mode.
@ -646,16 +527,16 @@ this condition holds, no trajectory starting inside $\mathcal{C}$ can ever
leave. leave.
Because the design of the discrete controller defines careful boundaries in Because the design of the discrete controller defines careful boundaries in
continuous state space, the barrier is known prior to designing the continuous state space, the barrier \(\mathcal{C}\) is known prior to designing
continuous controller. This eliminates the search for an appropriate barrier the continuous controller. This eliminates the search for an appropriate barrier
and minimizes complication in validating stabilizing continuous control and minimizes complication in validating stabilizing continuous control modes.
modes. The discrete specifications tell us what region must be invariant; the The discrete specifications tell us what region must be invariant; the barrier
barrier certificate confirms that the candidate controller achieves this certificate confirms that the candidate controller achieves this invariance.
invariance.
Finding barrier certificates can be formulated as a sum-of-squares (SOS) Finding barrier certificates can be formulated as a sum-of-squares (SOS)
optimization problem for polynomial systems, or solved using satisfiability optimization problem for polynomial systems, or solved using satisfiability
modulo theories (SMT) solvers for broader classes of dynamics. The key modulo theories (SMT) solvers for broader classes of dynamics\dasnote{cite these
here}. The key
advantage is that the verification is independent of how the controller was advantage is that the verification is independent of how the controller was
designed. Standard control techniques can be used to build continuous designed. Standard control techniques can be used to build continuous
controllers, and barrier certificates provide a separate check that the controllers, and barrier certificates provide a separate check that the
@ -693,26 +574,20 @@ potentially anywhere in the state space, under degraded or uncertain
dynamics. Examples include emergency core cooling, reactor SCRAM sequences, dynamics. Examples include emergency core cooling, reactor SCRAM sequences,
and controlled depressurization procedures. and controlled depressurization procedures.
We can detect that physical failures exist because our physical controllers We can detect that physical failures exist because our physical controllers have
have been previously proven correct by reachability and barrier certificates. been previously proven correct by reachability and barrier certificates. We know
We know our controller cannot be incorrect for the nominal plant model, so our controller cannot be incorrect for the nominal plant model, so if an
if an invariant is violated, we know the plant dynamics have invariant is violated, we know the plant dynamics have changed. The mathematical
changed. \oldt{The HAHACS can identify that a fault occurred because a formulation for expulsory mode verification differs from transitory modes in two
discrete boundary condition was violated by the continuous physical key ways. First, the entry conditions may be the entire state space (or a large,
controller.} \newt{}\dasinline{This says the same thing as the sentence conservatively bounded region) rather than a well-defined entry set. The failure
right before it.} This is a direct consequence of having verified the may occur at any point during operation. Second, the dynamics include parametric
nominal continuous control modes: unexpected behavior implies off-nominal uncertainty representing failure modes:
conditions.
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} \dot{x} = f(x, u, \theta), \quad \theta \in \Theta_{failure}
\] \]
where $\Theta_{failure}$ captures the range of possible degraded plant% where $\Theta_{failure}$ captures the range of possible degraded plant%
\splitsuggest{GAP: None of the NEEDS\_REVIEWED papers directly address \splitsuggest{GAP: None of the NEEDS\_REVIEWED papers directly address
reachability with parametric uncertainty for failure mode analysis. SpaceEx reachability with parametric uncertainty for failure mode analysis. SpaceEx
@ -778,28 +653,16 @@ reliability requirements. The discrete automaton produced by reactive
synthesis will be compiled to run on Ovation controllers, with verification synthesis will be compiled to run on Ovation controllers, with verification
that the implemented behavior matches the synthesized specification exactly. that the implemented behavior matches the synthesized specification exactly.
For the continuous dynamics, we will use a small modular reactor For the continuous dynamics, we will use a small modular reactor simulation. The
simulation.\dasinline{Are we REALLY going to do this? Maybe not.} The SmAHTR SmAHTR (Small modular Advanced High Temperature Reactor) model provides a
(Small modular Advanced High Temperature Reactor) model provides a relevant relevant testbed for startup and shutdown procedures. The ARCADE (Advanced
testbed for startup and shutdown procedures. The ARCADE (Advanced Reactor Reactor Control Architecture Development Environment) interface will establish
Control Architecture Development Environment) interface will establish communication between the Emerson Ovation hardware and the reactor simulation,
communication between the Emerson Ovation hardware and the reactor enabling hardware-in-the-loop testing of the complete hybrid controller.
simulation, enabling hardware-in-the-loop testing of the complete hybrid
controller.
\oldt{Working with Emerson on such an implementation is an incredible The Emerson collaboration strengthens this work in two ways. Access to
advantage for the success and impact of this work. We will directly address
the gap of verification and validation methods for these systems and industry
adoption by forming a two-way exchange of knowledge between the laboratory
and commercial environments. This work stands to be successful with Emerson
implementation because we will have access to system experts at Emerson to
help with the fine details of using the Ovation system. At the same time, we
will have the benefit of transferring technology directly to industry with a
direct collaboration in this research, while getting an excellent perspective
of how our research outcomes can align best with customer needs.}
\newt{The Emerson collaboration strengthens this work in two ways. Access to
system experts at Emerson ensures that implementation details of the Ovation system experts at Emerson ensures that implementation details of the Ovation
platform are handled correctly. Direct industry collaboration provides an platform are handled correctly. Direct industry collaboration also provides an
immediate pathway for technology transfer and alignment with practical immediate pathway for technology transfer and alignment with practical
deployment requirements.}\splitnote{Kapuria 2025 validates hybrid control on deployment requirements.}\splitnote{Kapuria 2025 validates hybrid control on
SmAHTR: formal verification (d$\mathcal{L}$ + reachability, pp.37-70) proved SmAHTR: formal verification (d$\mathcal{L}$ + reachability, pp.37-70) proved

82
4-metrics-of-success/metrics.tex
View File

@ -1,41 +1,17 @@
\section{Metrics for Success} \section{Metrics for Success}
This research will be measured by advancement through Technology Readiness This research will be measured by advancement through Technology Readiness
Levels, progressing from fundamental concepts to validated prototype Levels (TRL), progressing from fundamental concepts to validated prototype
demonstration. This work begins at TRL 2--3 and aims to reach TRL 5, where demonstration. TRLs measure the gap between academic proof-of-concept and
system components operate successfully in a relevant laboratory practical deployment, which is precisely what this work aims to bridge. Academic
environment.\splitnote{TRL as primary metric is smart — speaks industry metrics alone cannot capture practical feasibility, and empirical metrics alone
language.} cannot demonstrate theoretical rigor. TRLs measure both simultaneously. This
This section explains why TRL advancement provides the most appropriate work begins at TRL 2--3 and aims to reach TRL 5, where system components operate
success metric and defines the specific criteria required to achieve TRL 5. successfully in a relevant laboratory environment. This section explains why TRL
advancement provides the most appropriate success metric and defines the
\oldt{Technology Readiness Levels provide the ideal success metric because specific criteria required to achieve TRL 5. Reaching TRL 5 provides a clear
they explicitly measure the gap between academic proof-of-concept and answer to industry questions about feasibility and maturity that academic
practical deployment---precisely what this work aims to bridge. Academic publications alone cannot.
metrics like papers published or theorems proved cannot capture practical
feasibility. Empirical metrics like simulation accuracy or computational
speed cannot demonstrate theoretical rigor. TRLs measure both dimensions
simultaneously.} \newt{TRLs measure the gap between academic
proof-of-concept and practical deployment, which is precisely what this work
aims to bridge. Academic metrics alone cannot capture practical feasibility,
and empirical metrics alone cannot demonstrate theoretical rigor. TRLs
measure both simultaneously.}\dasinline{Chop. No likey.}\splitnote{Good
framing — explains why other metrics are insufficient.} Advancing from TRL 3
to TRL 5 requires maintaining theoretical rigor while progressively
demonstrating practical feasibility. Formal verification must remain valid as
the system moves from individual components to integrated hardware testing.
The nuclear industry requires extremely high assurance before deploying new
control technologies. Demonstrating theoretical correctness alone is
insufficient for adoption; conversely, showing empirical performance without
formal guarantees fails to meet regulatory requirements. TRLs capture this
dual requirement naturally. Each level represents both increased practical
maturity and sustained theoretical validity. Furthermore, TRL assessment
forces explicit identification of remaining barriers to deployment. The
nuclear industry already uses TRLs for technology assessment, making this
metric directly relevant to potential adopters. Reaching TRL 5 provides a
clear answer to industry questions about feasibility and maturity that
academic publications alone cannot.
Moving from current state to target requires achieving three intermediate Moving from current state to target requires achieving three intermediate
levels, each representing a distinct validation milestone: levels, each representing a distinct validation milestone:
@ -66,26 +42,23 @@ be maintained throughout system integration.
\paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}} \paragraph{TRL 5 \textit{Laboratory Testing in Relevant Environment}}
For this research, TRL 5 means demonstrating the verified controller on For this research, TRL 5 means demonstrating the verified controller on
industrial control hardware through hardware-in-the-loop testing. The industrial control hardware through hardware-in-the-loop testing. The discrete
discrete automaton must be implemented on the Emerson Ovation control system automaton must be implemented on the Emerson Ovation control system and verified
and verified to match synthesized specifications exactly. Continuous to match synthesized specifications exactly. Continuous controllers must execute
controllers must execute at required rates. The ARCADE interface must at required rates. The ARCADE interface must establish stable real-time
establish stable real-time communication between the Emerson Ovation hardware communication between the Emerson Ovation hardware and SmAHTR simulation.
and SmAHTR simulation. Complete autonomous startup sequences must execute via Complete autonomous startup sequences must execute via hardware-in-the-loop
hardware-in-the-loop across the full operational envelope. The controller across the full operational envelope. The controller must handle off-nominal
must handle off-nominal scenarios to validate that expulsory modes function scenarios to validate that expulsory modes function correctly. For example,
correctly. For example, simulated sensor failures must trigger appropriate simulated sensor failures must trigger appropriate fault detection and mode
fault detection and mode transitions, and loss-of-cooling scenarios must transitions, and loss-of-cooling scenarios must activate SCRAM procedures as
activate SCRAM procedures as specified. Graded responses to minor specified. Graded responses to minor disturbances are outside this work's scope,
disturbances are outside this work's scope\oldt{.}\newt{, as they require as they require runtime optimization under uncertainty that extends beyond the
runtime optimization under uncertainty that extends beyond the correct-by-construction verification framework presented here. Formal
correct-by-construction verification framework presented
here.}\splitsuggest{Consider noting why graded responses are out of scope —
is it time, complexity, or scope creep? Brief justification helps.} Formal
verification results must remain valid, with discrete behavior matching verification results must remain valid, with discrete behavior matching
specifications and continuous trajectories remaining within verified bounds. specifications and continuous trajectories remaining within verified bounds.
This proves that the methodology produces verified controllers implementable This proves that the methodology produces verified controllers implementable on
on industrial hardware. industrial hardware.
Progress will be assessed quarterly through collection of specific data Progress will be assessed quarterly through collection of specific data
comparing actual results against TRL advancement criteria. Specification comparing actual results against TRL advancement criteria. Specification
@ -99,5 +72,4 @@ operating on industrial control hardware through hardware-in-the-loop
testing in a relevant laboratory environment. This establishes both testing in a relevant laboratory environment. This establishes both
theoretical validity and practical feasibility, proving that the methodology theoretical validity and practical feasibility, proving that the methodology
produces verified controllers and that implementation is achievable with produces verified controllers and that implementation is achievable with
current technology.\splitnote{Clear success criteria. Committee will know current technology.
exactly what ``done'' looks like.}

37
5-risks-and-contingencies/risks.tex
View File

@ -2,8 +2,7 @@
This research relies on several critical assumptions that, if invalidated, This research relies on several critical assumptions that, if invalidated,
would require scope adjustment or methodological would require scope adjustment or methodological
revision.\splitnote{Honest acknowledgment of risks with clear contingencies revision. The primary risks to successful
— committee will appreciate this.} The primary risks to successful
completion fall into four categories: computational tractability of synthesis completion fall into four categories: computational tractability of synthesis
and verification, complexity of the discrete-continuous interface, and verification, complexity of the discrete-continuous interface,
completeness of procedure formalization, and hardware-in-the-loop integration completeness of procedure formalization, and hardware-in-the-loop integration
@ -31,9 +30,8 @@ problems. Synthesis times exceeding 24 hours for simplified procedure subsets
would suggest complete procedures are intractable. Generated automata would suggest complete procedures are intractable. Generated automata
containing more than 1,000 discrete states would indicate the discrete state containing more than 1,000 discrete states would indicate the discrete state
space is too large for efficient verification. Specifications flagged as space is too large for efficient verification. Specifications flagged as
unrealizable by \oldt{FRET or Strix} \newt{realizability checking unrealizable by realizability checking
tools}\dasinline{Strix may not be the reactive synth tool anymore. Be more tools would reveal fundamental conflicts in the formalized procedures.
general.} would reveal fundamental conflicts in the formalized procedures.
Reachability analysis failing to converge within reasonable time bounds would Reachability analysis failing to converge within reasonable time bounds would
show that continuous mode verification cannot be completed with available show that continuous mode verification cannot be completed with available
computational resources. computational resources.
@ -51,22 +49,19 @@ as a constraint rather than a failure.
\subsection{Discrete-Continuous Interface Formalization} \subsection{Discrete-Continuous Interface Formalization}
The second critical assumption concerns the mapping between boolean guard The second critical assumption concerns the mapping between boolean guard
conditions in temporal logic and continuous state boundaries required for conditions in temporal logic and continuous state boundaries required for mode
mode transitions. This interface represents the fundamental challenge of transitions. This interface represents the fundamental challenge of hybrid
hybrid systems: relating discrete switching logic to continuous dynamics. systems: relating discrete switching logic to continuous dynamics. Temporal
Temporal logic operates on boolean predicates, while continuous control logic operates on boolean predicates, while continuous control requires
requires reasoning about differential equations and reachable sets. reasoning about differential equations and reachable sets. Some guard conditions
\oldt{Guard conditions requiring complex nonlinear predicates may resist may require complex nonlinear predicates that cannot be cleanly expressed as
boolean abstraction, making synthesis intractable.} \newt{Some guard boolean combinations of simple threshold checks, making synthesis intractable.
conditions may require complex nonlinear predicates that cannot be cleanly Continuous safety regions that cannot be expressed as conjunctions of verifiable
expressed as boolean combinations of simple threshold checks, making constraints would similarly create insurmountable verification challenges. The
synthesis intractable.}\dasinline{What does this mean?} Continuous safety risk extends beyond static interface definition to dynamic behavior across
regions that cannot be expressed as conjunctions of verifiable constraints transitions: barrier certificates may fail to exist for proposed transitions, or
would similarly create insurmountable verification challenges. The risk continuous modes may be unable to guarantee convergence to discrete transition
extends beyond static interface definition to dynamic behavior across boundaries.
transitions: barrier certificates may fail to exist for proposed transitions,
or continuous modes may be unable to guarantee convergence to discrete
transition boundaries.
Early indicators of interface formalization problems would appear during both Early indicators of interface formalization problems would appear during both
synthesis and verification phases. Guard conditions requiring complex synthesis and verification phases. Guard conditions requiring complex

3
6-broader-impacts/impacts.tex
View File

@ -76,6 +76,5 @@ control, aerospace systems, and autonomous transportation, where similar
economic and safety considerations favor increased autonomy with provable economic and safety considerations favor increased autonomy with provable
correctness guarantees. Demonstrating this approach in nuclear power---one of correctness guarantees. Demonstrating this approach in nuclear power---one of
the most regulated and safety-critical the most regulated and safety-critical
domains\splitnote{``If it works here, it works anywhere — strong closing domains---will establish both the technical feasibility and regulatory
argument.}---will establish both the technical feasibility and regulatory
pathway for broader adoption across critical infrastructure. pathway for broader adoption across critical infrastructure.

3
dane_proposal_format.cls
View File

@ -102,7 +102,8 @@
\newcommand{\bb}[1]{\mathbb{#1}} % blackboard bold (ℝ, ℚ, etc.) \newcommand{\bb}[1]{\mathbb{#1}} % blackboard bold (ℝ, ℚ, etc.)
% Default document metadata (can be overridden) % Default document metadata (can be overridden)
\title{From Cold Start to Critical:\\ Formal Synthesis of Autonomous Hybrid Controllers} \title{From Cold Start to Critical:\\ Synthesis of High Assurance Hybrid
Autonomous Control Systems}
\author{% \author{%
PI: Dane A. Sabo\\ PI: Dane A. Sabo\\
dane.sabo@pitt.edu\\ dane.sabo@pitt.edu\\