danesabo/Thesis
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Wrap lines to 80 chars

Browse Source
This commit is contained in:
Split 2026-03-17 21:00:40 -04:00
parent 24bae81304
commit 764e695c05
1 changed files with 8 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
3-research-approach/approach.tex
View File

@ -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 originates in requirements: statements about what the system must do, must not
do, and under what conditions. For nuclear systems, these requirements derive do, and under what conditions. For nuclear systems, these requirements derive
from multiple sources including regulatory mandates, design basis analyses, and from multiple sources including regulatory mandates, design basis analyses, and
aforementioned operating procedures. The challenge is formalizing these requirements with aforementioned operating procedures. The challenge is formalizing
sufficient precision that they can serve as the foundation for autonomous 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 control system synthesis and verification. We can build these requirements using
temporal logic. 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 framework to formalize it. This is why the approach is feasible for nuclear
applications specifically: the work of defining safe operating boundaries has applications specifically: the work of defining safe operating boundaries has
already been done by generations of nuclear engineers. The work of translating already been done by generations of nuclear engineers. The work of translating
these requirements from interpretable natural language to a formal requirement is these requirements from interpretable natural language to a formal
what remains to be done. requirement is what remains to be done.
Linear temporal logic (LTL) is particularly well-suited for specifying reactive Linear temporal logic (LTL) is particularly well-suited for specifying reactive
systems. LTL formulas are built from atomic propositions (our discrete 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. the boundaries for each continuous controller's allowed state-space region.
These continuous controllers all share a common state space, but each These continuous controllers all share a common state space, but each
individual continuous control mode operates within its own partition defined individual continuous control mode operates within its own partition defined
by the discrete state $q_i$ and the associated guard conditions. This partitioning of by the discrete state $q_i$ and the associated guard conditions.
the continuous state space among several distinct vector fields has This partitioning of the continuous state space among several
distinct vector fields has
traditionally been a difficult problem for validation and verification. The traditionally been a difficult problem for validation and verification. The
discontinuity of the vector fields at discrete state interfaces makes discontinuity of the vector fields at discrete state interfaces makes
reachability analysis computationally expensive, and analytic solutions often reachability analysis computationally expensive, and analytic solutions often