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}
-
-Formal verification of any system requires a precise language for stating
-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
+\subsubsection{Sequent Calculus and 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
-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
+or small modular designs. 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