2-state-of-the-art/state-of-art.tex

@@ -156,40 +156,9 @@ considerations: integration with legacy systems, human-system interaction in
 realistic operational contexts, and regulatory acceptance of formal methods as
 primary assurance evidence remain as significant challenges.
 
-\subsubsection{Temporal Logic and Formal Specification}
+\subsubsection{Sequent Calculus and Differential Dynamic Logic}
-
+A separate line of work
-Formal verification of any system requires a precise language for stating
+extends temporal logics to verify hybrid systems
-what the system must do. Temporal logic provides this language by extending
-classical propositional logic with operators that express properties over
-time. Where propositional logic can state that a condition is true or false,
-temporal logic can state that a condition must always hold, must eventually
-hold, or must hold until some other condition is met. This expressiveness
-makes temporal logic the foundation for specifying reactive systems---systems
-that continuously interact with their environment and must satisfy ongoing
-behavioral requirements.
-
-For nuclear control applications, temporal logic captures exactly the kinds
-of properties that matter: safety properties (``the reactor never enters an
-unsafe configuration''), liveness properties (``the system eventually reaches
-operating temperature''), and response properties (``if coolant pressure
-drops, shutdown initiates within bounded time''). These properties can be
-derived directly from operating procedures and regulatory requirements,
-creating a formal link between existing documentation and verifiable system
-behavior.
-
-NASA's Formal Requirements Elicitation Tool (FRET) bridges the gap between
-natural language requirements and temporal logic specifications. FRET
-provides a structured intermediate language that allows engineers to define
-temporal behavior without writing raw logic formulas. The HARDENS project
-used FRET for requirement capture, and it has been validated on aerospace
-systems including a Lift+Cruise aircraft with 53 formalized
-requirements~\cite{Pressburger2023}. FRET's ability to start with imprecise
-natural language and iteratively refine it into well-posed specifications
-makes it particularly suited to formalizing nuclear operating procedures.
-
-\subsubsection{Differential Dynamic Logic}
-
-A separate line of work extends temporal logics to verify hybrid systems
 directly. The result has been the field of differential dynamic logic (dL). dL
 introduces two additional operators into temporal logic: the box operator and
 the diamond operator. The box operator \([\alpha]\phi\) states that for some

6-broader-impacts/impacts.tex

@@ -30,12 +30,7 @@ exist.}
 This research directly addresses the multi-billion-dollar O\&M cost challenge
 through high-assurance autonomous control. Current nuclear operations require
 full control room staffing for each reactor, whether large conventional units
-or small modular designs. Over 3,600 active NRC-licensed reactor operators
+or small modular designs. These staffing requirements drive the high O\&M
-work in the United States~\cite{operator_statistics}, divided into Reactor
-Operators (ROs) and Senior Reactor Operators
-(SROs)~\cite{10CFR55}. Staffing requires at least two ROs and one SRO per
-unit~\cite{10CFR50.54}, with each operator requiring several years of
-training and NRC licensing. These staffing requirements drive the high O\&M
 costs that make nuclear power economically challenging, particularly for
 smaller reactor designs where the same staffing overhead must be spread
 across lower power output. Synthesizing provably correct hybrid controllers