From 2bcba39e020102379a4e68b7256c70f12452b6af Mon Sep 17 00:00:00 2001 From: Split Date: Mon, 16 Mar 2026 14:14:52 -0400 Subject: [PATCH] SOTA: add temporal logic + FRET subsection before dL, rename dL subsubsection --- 2-state-of-the-art/state-of-art.tex | 37 ++++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) diff --git a/2-state-of-the-art/state-of-art.tex b/2-state-of-the-art/state-of-art.tex index 3b0d3fd..6d5e64e 100644 --- a/2-state-of-the-art/state-of-art.tex +++ b/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} -A separate line of work -extends temporal logics to verify hybrid systems +\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 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