SOTA: add temporal logic + FRET subsection before dL, rename dL subsubsection

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

@@ -156,9 +156,40 @@ 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{Sequent Calculus and Differential Dynamic Logic}
+\subsubsection{Temporal Logic and Formal Specification}
-A separate line of work
+
-extends temporal logics to verify hybrid systems
+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
 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