From 764e695c05dab98f1cf17d0d49922d478ebc38c6 Mon Sep 17 00:00:00 2001 From: Split Date: Tue, 17 Mar 2026 21:00:40 -0400 Subject: [PATCH] Wrap lines to 80 chars --- 3-research-approach/approach.tex | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/3-research-approach/approach.tex b/3-research-approach/approach.tex index 7cfcb59..50b1437 100644 --- a/3-research-approach/approach.tex +++ b/3-research-approach/approach.tex @@ -225,8 +225,9 @@ instructions as a set of formal requirements. The behavior of any control system originates in requirements: statements about what the system must do, must not do, and under what conditions. For nuclear systems, these requirements derive from multiple sources including regulatory mandates, design basis analyses, and -aforementioned operating procedures. The challenge is formalizing these requirements with -sufficient precision that they can serve as the foundation for autonomous +aforementioned operating procedures. The challenge is formalizing +these requirements with sufficient precision that they can serve as +the foundation for autonomous control system synthesis and verification. We can build these requirements using temporal logic. @@ -253,8 +254,8 @@ experience. Our methodology assumes this domain knowledge exists and provides a framework to formalize it. This is why the approach is feasible for nuclear applications specifically: the work of defining safe operating boundaries has already been done by generations of nuclear engineers. The work of translating -these requirements from interpretable natural language to a formal requirement is -what remains to be done. +these requirements from interpretable natural language to a formal +requirement is what remains to be done. Linear temporal logic (LTL) is particularly well-suited for specifying reactive systems. LTL formulas are built from atomic propositions (our discrete @@ -365,8 +366,9 @@ discrete state are themselves the guard conditions $\mathcal{G}$ that define the boundaries for each continuous controller's allowed state-space region. These continuous controllers all share a common state space, but each individual continuous control mode operates within its own partition defined -by the discrete state $q_i$ and the associated guard conditions. This partitioning of -the continuous state space among several distinct vector fields has +by the discrete state $q_i$ and the associated guard conditions. +This partitioning of the continuous state space among several +distinct vector fields has traditionally been a difficult problem for validation and verification. The discontinuity of the vector fields at discrete state interfaces makes reachability analysis computationally expensive, and analytic solutions often