Edit State of Art: address all DAS+Split comments, add dL LIMITATION box, fix typo, trim redundancy

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

@@ -1,269 +1,303 @@
 \section{State of the Art and Limits of Current Practice}
 
 The principal aim of this research is to create autonomous reactor control
-systems that are tractably safe. To understand what is being automated, we must
+systems that are tractably safe. \oldt{To understand what is being automated,
-first understand how nuclear reactors are operated today. This section examines
+we must first understand how nuclear reactors are operated today. This section
-reactor operators and the operating procedures we aim to leverage, then
+examines reactor operators and the operating procedures we aim to leverage,
-investigates limitations of human-based operation, and concludes with current
+then investigates limitations of human-based operation, and concludes with
-formal methods approaches to reactor control 
+current formal methods approaches to reactor control systems.}
-systems.\splitnote{Good roadmap --- tells reader exactly what's 
+\newt{Understanding what is being automated requires understanding how
-coming.}\dasinline{Don't like ``we'' here. Sounds like
+nuclear reactors are operated today. This section examines reactor operating
-``we're going on an adventure!'' and feels jocular.
+procedures, investigates limitations of human-based operation, and reviews
-Maybe: ``To motivate this proposal, the state of
+current formal methods approaches to reactor control
-the art of nuclear reactor control, blah, and blah,
+systems.}\dasinline{Don't like ``we'' here. Sounds like ``we're going on an
-are discussed in this section.''}
+adventure!'' and feels jocular. Maybe: ``To motivate this proposal, the
+state of the art of nuclear reactor control, blah, and blah, are discussed
+in this section.''}
 
 \subsection{Current Reactor Procedures and Operation}
 
-Nuclear plant procedures exist in a hierarchy: normal operating procedures for
+\oldt{Nuclear plant procedures exist in a hierarchy: normal operating
-routine operations, abnormal operating procedures for off-normal conditions,
+procedures for routine operations, abnormal operating procedures for
-Emergency Operating Procedures (EOPs) for design-basis accidents, Severe
+off-normal conditions, Emergency Operating Procedures (EOPs) for
-Accident Management Guidelines (SAMGs) for beyond-design-basis events, and
+design-basis accidents, Severe Accident Management Guidelines (SAMGs) for
-Extensive Damage Mitigation Guidelines (EDMGs) for catastrophic damage
+beyond-design-basis events, and Extensive Damage Mitigation Guidelines
-scenarios.\dasinline{This sentence is MASSIVE. Why is
+(EDMGs) for catastrophic damage scenarios.} \newt{Nuclear plant operations
-there 6 lines describing different types of
+are governed by a hierarchy of written procedures, ranging from normal
-procedures? WHO CARES? Need a sentence after saying
+operating procedures for routine operations to Emergency Operating
-why we have these procedures.} These procedures must comply with 10 CFR 50.34(b)(6)(ii) and are
+Procedures (EOPs) for design-basis accidents and Severe Accident Management
-developed using guidance from NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their
+Guidelines (SAMGs) for beyond-design-basis events. These procedures exist
-development relies fundamentally on expert judgment and simulator validation
+because reactor operation requires deterministic responses to a wide range
-rather than formal verification. Procedures undergo technical evaluation,
+of plant conditions, from routine power changes to catastrophic
-simulator validation testing, and biennial review as part of operator
+failures.}\dasinline{This sentence is MASSIVE. Why is there 6 lines
-requalification under 10 CFR 55.59~\cite{10CFR55.59}. Despite this rigor,
+describing different types of procedures? WHO CARES? Need a sentence after
-procedures fundamentally lack formal verification of key safety 
+saying why we have these procedures.} These procedures must comply with 10
-properties.\dasinline{Does the audience know what formal
+CFR 50.34(b)(6)(ii) and are developed using guidance from
-verification is at this point? Probably, but should
+NUREG-0899~\cite{NUREG-0899, 10CFR50.34}, but their development relies
-say differently. Maybe `exhaustive' or
+fundamentally on expert judgment and simulator validation rather than formal
-`definitive'.} No
+verification.
-mathematical proof exists that procedures cover all possible plant states, that
-required actions can be completed within available timeframes, or that
-transitions between procedure sets maintain safety 
-invariants.\splitsuggest{This paragraph is doing a lot. Consider splitting: 
-first paragraph on the hierarchy and compliance, second on the lack of formal 
-verification. The ``No mathematical proof exists...'' sentence is powerful and 
-deserves emphasis.}
 
-\textbf{LIMITATION:} \textit{Procedures lack formal verification of correctness
+Procedures undergo technical evaluation, simulator validation testing, and
-and completeness.} Current procedure development relies on expert judgment and
+biennial review as part of operator requalification under 10 CFR
-simulator validation. No mathematical proof exists that procedures cover all
+55.59~\cite{10CFR55.59}. Despite this rigor, procedures fundamentally lack
-possible plant states, that required actions can be completed within available
+\oldt{formal verification of key safety properties.} \newt{exhaustive
-timeframes, or that transitions between procedure sets maintain safety
+verification of key safety properties.}\dasinline{Does the audience know
-invariants. Paper-based procedures cannot ensure correct application, and even
+what formal verification is at this point? Probably, but should say
-computer-based procedure systems lack the formal guarantees that automated
+differently. Maybe `exhaustive' or `definitive'.} No mathematical proof
-reasoning could provide.\splitpolish{This repeats the ``No mathematical 
+exists that procedures cover all possible plant states, that required actions
-proof exists...'' sentence almost verbatim from the paragraph above. Either 
+can be completed within available timeframes, or that transitions between
-cut it from the paragraph or from the LIMITATION box.}
+procedure sets maintain safety invariants.
 
-Nuclear plants operate with multiple control modes: automatic control, where the
+\textbf{LIMITATION:} \textit{Procedures lack exhaustive verification of
-reactor control system maintains target parameters through continuous reactivity
+correctness and completeness.} \oldt{Current procedure development relies on
-adjustment; manual control, where operators directly manipulate the reactor; and
+expert judgment and simulator validation. No mathematical proof exists that
-various intermediate modes. In typical pressurized water reactor operation, the
+procedures cover all possible plant states, that required actions can be
-reactor control system automatically maintains a floating average temperature
+completed within available timeframes, or that transitions between procedure
-and compensates for power demand changes through reactivity feedback loops
+sets maintain safety invariants. Paper-based procedures cannot ensure correct
-alone. Safety systems, by contrast, operate with implemented automation. Reactor
+application, and even computer-based procedure systems lack the formal
-Protection Systems trip automatically on safety signals with millisecond
+guarantees that automated reasoning could provide.} \newt{Paper-based
-response times, and engineered safety features actuate automatically on accident
+procedures cannot ensure correct application, and even computer-based
-signals without operator action required.
+procedure systems lack the guarantees that automated reasoning could
+provide.}\splitpolish{This repeats the ``No mathematical proof exists...''
+sentence almost verbatim from the paragraph above. Either cut it from the
+paragraph or from the LIMITATION box.}
 
-\dasinline{After reading the next sentence, ``key safety''
+Nuclear plants operate with multiple control modes: automatic control, where
-can honestly just be a semicolon.}
+the reactor control system maintains target parameters through continuous
-\dasinline{Not sure what the challenge actually is
+reactivity adjustment; manual control, where operators directly manipulate
-as this paragraph is written. What's the point?}
+the reactor; and various intermediate modes. In typical pressurized water
-The division between automated and human-controlled functions reveals the
+reactor operation, the reactor control system automatically maintains a
-fundamental challenge of hybrid control. Highly automated systems handle reactor
+floating average temperature and compensates for power demand changes through
-protection---automatic trips on safety parameters, emergency core cooling
+reactivity feedback loops alone. Safety systems, by contrast, operate with
+implemented automation. Reactor Protection Systems trip automatically on
+safety signals with millisecond response times, and engineered safety
+features actuate automatically on accident signals without operator action
+required.
+
+\oldt{The division between automated and human-controlled functions reveals
+the fundamental challenge of hybrid control. Highly automated systems handle
+reactor protection---automatic trips on safety parameters, emergency core
+cooling actuation, containment isolation, and basic process
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
+operators, however, retain control of strategic decision-making: power level
+changes, startup/shutdown sequences, mode transitions, and procedure
+implementation.} \newt{This division between automated and human-controlled
+functions is itself the hybrid control problem. Automated systems handle
+reactor protection: trips on safety parameters, emergency core cooling
 actuation, containment isolation, and basic process
-control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human operators,
+control~\cite{WRPS.Description, gentillon_westinghouse_1999}. Human
-however, retain control of strategic decision-making: power level changes,
+operators retain control of everything else: power level changes,
-startup/shutdown sequences, mode transitions, and procedure 
+startup/shutdown sequences, mode transitions, and procedure
-implementation.\splitnote{This is the key insight — the hybrid nature is 
+implementation.}\dasinline{After reading the next sentence, ``key safety''
-already there, just not formally verified.}
+can honestly just be a semicolon.}\dasinline{Not sure what the challenge
+actually is as this paragraph is written. What's the
+point?}\splitnote{This is the key insight — the hybrid nature is already
+there, just not formally verified.}
 
 \subsection{Human Factors in Nuclear Accidents}
 
-Current-generation nuclear power plants employ over 3,600 active NRC-licensed
+\oldt{Current-generation nuclear power plants employ over 3,600 active
-reactor operators in the United 
+NRC-licensed reactor operators in the United
-States~\cite{operator_statistics}.\dasinline{Why is this here? Should this
+States~\cite{operator_statistics}. These operators divide into Reactor
-be in broader impacts about running out of ROs?
+Operators (ROs), who manipulate reactor controls, and Senior Reactor
-As it is here I have no idea why this is here.} These
+Operators (SROs), who direct plant operations and serve as shift
-operators divide into Reactor Operators (ROs), who manipulate reactor controls,
+supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs and
-and Senior Reactor Operators (SROs), who direct plant operations and serve as
+one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
-shift supervisors~\cite{10CFR55}. Staffing typically requires at least two ROs
+operator requires several years of training.} \newt{Nuclear plant staffing
-and one SRO for current-generation units~\cite{10CFR50.54}. Becoming a reactor
+requires at least two Reactor Operators (ROs) and one Senior Reactor
-operator requires several years of training.
+Operator (SRO) per unit~\cite{10CFR50.54}, with operators requiring several
+years of training and NRC licensing under 10 CFR Part
+55~\cite{10CFR55}.}\dasinline{Why is this here? Should this be in broader
+impacts about running out of ROs? As it is here I have no idea why this is
+here.}
 
-The persistent role of human error in nuclear safety incidents---despite decades
+The persistent role of human error in nuclear safety incidents---despite
-of improvements in training and procedures---provides the most compelling
+decades of improvements in training and procedures---provides the most
-motivation for formal automated control with mathematical safety 
+compelling motivation for formal automated control with mathematical safety
-guarantees.\splitnote{Strong thesis for this subsection.}
+guarantees.\splitnote{Strong thesis for this subsection.} Operators hold
-Operators hold legal authority under 10 CFR Part 55 to make critical 
+legal authority under 10 CFR Part 55 to make critical
-decisions,\dasinline{Cite.}
+decisions~\cite{10CFR55},\dasinline{Cite.} including departing from normal
-including departing from normal regulations during emergencies. 
+regulations during emergencies. \oldt{The Three Mile Island (TMI) accident}
-\dasinline{Needs a connector here. Like ``But this can
+\newt{This authority itself introduces risk. The Three Mile Island (TMI)
-in and of itself prime plants for an accident.''
+accident}\dasinline{Needs a connector here. Like ``But this can in and of
-Then continue.}The Three Mile
+itself prime plants for an accident.'' Then continue.} demonstrated how a
-Island (TMI) accident demonstrated how a combination of personnel error, design
+combination of personnel error, design deficiencies, and component failures
-deficiencies, and component failures led to partial meltdown when operators
+led to partial meltdown when operators misread confusing and contradictory
-misread confusing and contradictory readings and shut off the emergency water
+readings and shut off the emergency water system~\cite{Kemeny1979}. The
-system~\cite{Kemeny1979}. The President's Commission on TMI identified a
+President's Commission on TMI identified a fundamental ambiguity: placing
-fundamental ambiguity: placing responsibility for safe power plant operations on
+responsibility for safe power plant operations on the licensee without
-the licensee without formal verification that operators can fulfill this
+formal verification that operators can fulfill this responsibility does not
-responsibility does not guarantee safety. This tension between operational
+guarantee safety. This tension between operational flexibility and safety
-flexibility and safety assurance remains unresolved: the person responsible for
+assurance remains unresolved: the person responsible for reactor safety is
-reactor safety is often the root cause of 
+often the root cause of failures.\splitnote{``the person responsible for
-failures.\splitnote{``the person responsible for reactor safety is often the 
+reactor safety is often the root cause of failures'' — devastating summary.
-root cause of failures'' — devastating summary. Very effective.}
+Very effective.}
 
 Multiple independent analyses converge on a striking statistic: 70--80\% of
-nuclear power plant events are attributed to human error, versus approximately
+nuclear power plant events are attributed to human error, versus
-20\% to equipment failures~\cite{WNA2020}. More significantly, the root cause of
+approximately 20\% to equipment failures~\cite{WNA2020}. More significantly,
-all severe accidents at nuclear power plants---Three Mile Island, Chernobyl, and
+the root cause of all severe accidents at nuclear power plants---Three Mile
-Fukushima Daiichi---has been identified as poor safety management and safety
+Island, Chernobyl, and Fukushima Daiichi---has been identified as poor
-culture: primarily human factors~\cite{hogberg_root_2013}. A detailed analysis
+safety management and safety culture: primarily human
-of 190 events at Chinese nuclear power plants from
+factors~\cite{hogberg_root_2013}. A detailed analysis of 190 events at
-2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved active
+Chinese nuclear power plants from
-errors, while 92\% were associated with latent errors---organizational and
+2007--2020~\cite{zhang_analysis_2025} found that 53\% of events involved
-systemic weaknesses that create conditions for 
+active errors, while 92\% were associated with latent
-failure.\splitnote{Strong empirical grounding. The Chinese plant data is a 
+errors---organizational and systemic weaknesses that create conditions for
+failure.\splitnote{Strong empirical grounding. The Chinese plant data is a
 nice addition — shows this isn't just a Western regulatory perspective.}
 
 
-\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability limits
+\textbf{LIMITATION:} \textit{Human factors impose fundamental reliability
-that cannot be overcome through training alone.} The persistent human
+limits that cannot be overcome through training alone.} The persistent human
-error contribution despite four decades of improvements demonstrates that these
+error contribution despite four decades of improvements demonstrates that
-limitations are fundamental rather than a remediable part of human-driven 
+these limitations are fundamental rather than a remediable part of
-control.\splitnote{Well-stated. The ``four decades'' point drives it home.}
+human-driven control.\splitnote{Well-stated. The ``four decades'' point
+drives it home.}
 
 \subsection{Formal Methods}
 \subsubsection{HARDENS}
 
 The High Assurance Rigorous Digital Engineering for Nuclear Safety (HARDENS)
-project represents the most advanced application of formal methods to nuclear
+project represents the most advanced application of formal methods to
-reactor control systems to date~\cite{Kiniry2024}.
+nuclear reactor control systems to date~\cite{Kiniry2024}.
 
-HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear control
+HARDENS aimed to address a fundamental dilemma: existing U.S. nuclear
-rooms rely on analog technologies from the 1950s--60s.\dasinline{Source?}
+control rooms rely on analog technologies from the
-This technology is
+1950s--60s.\dasinline{Source?} This technology is obsolete compared to
-obsolete compared to modern control systems and incurs significant risk and
+modern control systems and incurs significant risk and cost. The NRC
-cost. The NRC contracted Galois, a formal methods firm, to demonstrate that
+contracted Galois, a formal methods firm, to demonstrate that Model-Based
-Model-Based Systems Engineering and formal methods could design, verify, and
+Systems Engineering and formal methods could design, verify, and implement a
-implement a complex protection system meeting regulatory criteria at a fraction
+complex protection system meeting regulatory criteria at a fraction of
-of typical cost. The project delivered a Reactor Trip System (RTS)
+typical cost. The project delivered a Reactor Trip System (RTS)
-implementation with full traceability from NRC Request for Proposals and IEEE
+implementation with full traceability from \oldt{NRC Request for Proposals
-standards through formal architecture specifications to verified 
+and IEEE standards through formal architecture specifications to verified
-software.\dasinline{Wordsmith this to remove the RFP and
+software.} \newt{regulatory requirements through formal architecture
-IEEE standards language. Should just say
+specifications to verified software.}\dasinline{Wordsmith this to remove the
-requirements.}
+RFP and IEEE standards language. Should just say requirements.}
 
-HARDENS employed formal methods tools and techniques across the verification
+\oldt{HARDENS employed formal methods tools and techniques across the
-hierarchy.\dasinline{Zero discussion about what the
+verification hierarchy.} \newt{HARDENS employed formal methods tools at
-verification hierarchy is. What is a specification
+every level of system development, from high-level requirements through
-or a requirement to someone who hasn't heard of
+executable models to generated code.}\dasinline{Zero discussion about what
-one before?} High-level specifications used Lando, SysMLv2, and FRET (NASA Formal
+the verification hierarchy is. What is a specification or a requirement to
-Requirements Elicitation Tool) to capture stakeholder requirements, domain
+someone who hasn't heard of one before?} High-level specifications used
-engineering, certification requirements, and safety requirements. Requirements
+Lando, SysMLv2, and FRET (NASA Formal Requirements Elicitation Tool) to
-were analyzed for consistency, completeness, and realizability using SAT and SMT
+capture stakeholder requirements, domain engineering, certification
-solvers. Executable formal models used Cryptol to create a behavioral model of
+requirements, and safety requirements. Requirements were analyzed for
-the entire RTS, including all subsystems, components, and limited digital twin
+consistency, completeness, and realizability using SAT and SMT solvers.
+Executable formal models used Cryptol to create a behavioral model of the
+entire RTS, including all subsystems, components, and limited digital twin
 models of sensors, actuators, and compute infrastructure. Automatic code
 synthesis generated verifiable C implementations and SystemVerilog hardware
-implementations directly from Cryptol models---eliminating the traditional gap
+implementations directly from Cryptol models---eliminating the traditional
-between specification and implementation where errors commonly 
+gap between specification and implementation where errors commonly
 arise.\splitnote{Good technical depth on HARDENS toolchain.}
 
-Despite its accomplishments, HARDENS has a fundamental limitation directly
+\oldt{Despite its accomplishments, HARDENS has a fundamental limitation
-relevant to hybrid control synthesis: the project addressed only discrete
+directly relevant to hybrid control synthesis: the project addressed only
-digital control logic without modeling or verifying continuous reactor 
+discrete digital control logic without modeling or verifying continuous
-dynamics.\dasinline{Edit these to more clearly separate
+reactor dynamics. The Reactor Trip System specification and verification
-the context from the limit. The limitation should
+covered discrete state transitions (trip/no-trip decisions), digital sensor
-be in the limitation.}
+input processing through discrete logic, and discrete actuation outputs
-The Reactor Trip System specification and verification covered discrete state
+(reactor trip commands). The project did not address continuous dynamics of
-transitions (trip/no-trip decisions), digital sensor input processing through
+nuclear reactor physics. Real reactor safety depends on the interaction
-discrete logic, and discrete actuation outputs (reactor trip commands). The
+between continuous processes---temperature, pressure, neutron flux---evolving
-project did not address continuous dynamics of nuclear reactor physics. Real
+in response to discrete control decisions. HARDENS verified the discrete
-reactor safety depends on the interaction between continuous
+controller in isolation but not the closed-loop hybrid system behavior.}
-processes---temperature, pressure, neutron flux---evolving in response to
+\newt{Despite these accomplishments, HARDENS addressed only discrete digital
-discrete control decisions. HARDENS verified the discrete controller in
+control logic. The Reactor Trip System verification covered discrete state
-isolation but not the closed-loop hybrid system 
+transitions, digital sensor processing, and discrete actuation outputs. It
-behavior.\splitnote{Clear articulation of the gap your work fills.}
+did not model or verify continuous reactor dynamics. Real reactor safety
+depends on the interaction between continuous processes---temperature,
+pressure, neutron flux---evolving in response to discrete control decisions.
+HARDENS verified the discrete controller in isolation but not the
+closed-loop hybrid system behavior.}\dasinline{Edit these to more clearly
+separate the context from the limit. The limitation should be in the
+limitation.}\splitnote{Clear articulation of the gap your work fills.}
 
-\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic without
+\textbf{LIMITATION:} \textit{HARDENS addressed discrete control logic
-continuous dynamics or hybrid system verification.} Verifying discrete control
+without continuous dynamics or hybrid system verification.} Verifying
-logic alone provides no guarantee that the closed-loop system exhibits desired
+discrete control logic alone provides no guarantee that the closed-loop
-continuous behavior such as stability, convergence to setpoints, or maintained
+system exhibits desired continuous behavior such as stability, convergence to
-safety margins.
+setpoints, or maintained safety margins.
 
 HARDENS produced a demonstrator system at Technology Readiness Level 2--3
-(analytical proof of concept with laboratory breadboard validation) rather than
+(analytical proof of concept with laboratory breadboard validation) rather
-a deployment-ready system validated through extended operational testing. The
+than a deployment-ready system validated through extended operational
-NRC Final Report explicitly notes~\cite{Kiniry2024} that all material is
+testing. The NRC Final Report explicitly notes~\cite{Kiniry2024} that all
-considered in development, not a finalized product, and that ``The demonstration
+material is considered in development, not a finalized product, and that
-of its technical soundness was to be at a level consistent with satisfaction of
+``The demonstration of its technical soundness was to be at a level
-the current regulatory criteria, although with no explicit demonstration of how
+consistent with satisfaction of the current regulatory criteria, although
-regulatory requirements are 
+with no explicit demonstration of how regulatory requirements are
-met.''\dasinline{Check this quote. Absolutely damning
+met.''\dasinline{Check this quote. Absolutely damning for HARDENS if true
-for HARDENS if true and hilarious Galois said
+and hilarious Galois said this.} The project did not include deployment in
-this.} The project did not include deployment in
+actual nuclear facilities, testing with real reactor systems under
-actual nuclear facilities, testing with real reactor systems under operational
+operational conditions, side-by-side validation with operational analog RTS
-conditions, side-by-side validation with operational analog RTS systems,
+systems, systematic failure mode testing, NRC licensing review, or human
-systematic failure mode testing (radiation effects, electromagnetic
+factors validation with licensed operators in realistic control room
-interference, temperature extremes), NRC licensing review, or human factors
+scenarios.
-validation with licensed operators in realistic control room scenarios.
 
 \textbf{LIMITATION:} \textit{HARDENS achieved TRL 2--3 without experimental
-validation.}\dasinline{Same as before. Separate limit
+validation.} \oldt{While formal verification provides mathematical
-from context better.} While formal verification provides mathematical correctness
+correctness guarantees for the implemented discrete logic, the gap between
-guarantees for the implemented discrete logic, the gap between formal
+formal verification and actual system deployment involves myriad practical
-verification and actual system deployment involves myriad practical
+considerations: integration with legacy systems, long-term reliability under
-considerations: integration with legacy systems, long-term reliability
+harsh environments, human-system interaction in realistic operational
-under harsh environments, human-system interaction in realistic
+contexts, and regulatory acceptance of formal methods as primary assurance
-operational contexts, and regulatory acceptance of formal methods as
+evidence.} \newt{The gap between formal verification and actual system
-primary assurance evidence.
+deployment remains wide: integration with legacy systems, long-term
+reliability under harsh environments, human-system interaction, and
+regulatory acceptance of formal methods as primary assurance
+evidence.}\dasinline{Same as before. Separate limit from context better.}
 
 \subsubsection{Sequent Calculus and Differential Dynamic Logic}
-There has been additional work to do verification of hybrid systems by extending
+\oldt{There has been additional work to do verification of hybrid systems by
-the temporal logics 
+extending the temporal logics directly.} \newt{A separate line of work
-directly.\dasinline{Need to introduce temporal logic
+extends temporal logics to verify hybrid systems
-and FRET here first.} The result has been the field of differential
+directly.}\dasinline{Need to introduce temporal logic and FRET here first.}
-dynamic logic (dL). dL introduces two additional operators
+The result has been the field of differential dynamic logic (dL). dL
-into temporal logic: the box operator and the diamond operator. The box operator
+introduces two additional operators into temporal logic: the box operator and
-\([\alpha]\phi\) states that for some region \(\phi\), the hybrid system
+the diamond operator. The box operator \([\alpha]\phi\) states that for some
-\(\alpha\) always remains within that region. In this way, it is a safety
+region \(\phi\), the hybrid system \(\alpha\) always remains within that
-ivariant being enforced for the system.\splitfix{Typo: ``ivariant'' should be 
+region. In this way, it is a safety \oldt{ivariant} \newt{invariant} being
-``invariant''} The second operator, the diamond
+enforced for the system.\splitfix{Typo: ``ivariant'' should be
-operator \(<\alpha>\phi\) says that for the region \(\phi\), there is at least
+``invariant''} The second operator, the diamond operator
-one trajectory of \(\alpha\) that enters that region. This is a declaration of a
+\(<\alpha>\phi\) says that for the region \(\phi\), there is at least one
-liveness property. 
+trajectory of \(\alpha\) that enters that region. This is a declaration of a
+liveness property.
 
 %source: https://symbolaris.com/logic/dL.html
 
-While dL allows for the specification of these liveness and safety properties,
+While dL allows for the specification of these liveness and safety
-actually proving them for a given hybrid system is quite difficult. Automated
+properties, actually proving them for a given hybrid system is quite
-proof assistants such as KeYmaera X exist to help develop proofs of systems
+difficult. Automated proof assistants such as KeYmaera X exist to help
-using dL, but so far have been insufficient for reasonably complex hybrid
+develop proofs of systems using dL, but so far have been insufficient for
-systems. The main issue behind creating system proofs using dL is state space
+reasonably complex hybrid systems. The main issue behind creating system
-explosion and non-terminating 
+proofs using dL is state space explosion and non-terminating solutions.
-solutions.\splitsuggest{Consider adding a concrete example here — ``For 
-instance, a system with N modes and M continuous state variables...'' to give 
-readers a sense of the scaling problem.}
 %Source: that one satellite tracking paper that has the problem with the
 %gyroscopes overloding and needing to dump speed all the time
-Approaches have been made to alleviate
+Approaches have been made to alleviate these issues for nuclear power
-these issues for nuclear power contexts using contract and decomposition based
+contexts using contract and decomposition based methods, \oldt{but are far
-methods, but are far from a complete methodology to design systems 
+from a complete methodology to design systems with.} \newt{but do not yet
-with.\splitpolish{``but are far from a complete methodology to design systems 
+constitute a complete design methodology.}\splitpolish{``but are far from a
-with'' — awkward ending preposition. Try: ``but remain far from a complete 
+complete methodology to design systems with'' — awkward ending preposition.}
-design methodology'' or ``but do not yet constitute a complete design 
+%source: Manyu's thesis.
-methodology.''}
-%source: Manyu's thesis. 
 Instead, these approaches have been used on systems that have been designed a
-priori, and require expert knowledge to create the system proofs. 
+priori, and require expert knowledge to create the system proofs.
 
 %Maybe a limitation here? Something about dL doesn't scale or help in design
-%very much, so the limitation is that logic based hybrid system approaches have
+%very much, so the limitation is that logic based hybrid system approaches
-%not been used in the DESIGN of autonomous controllers, only in the analysis of
+%have not been used in the DESIGN of autonomous controllers, only in the
-%systems that already exist.
+%analysis of systems that already exist.
-\splitinline{Your comment here is spot-on. You should add a LIMITATION box: 
+
-\textit{Differential dynamic logic has been used for post-hoc analysis of 
+\textbf{LIMITATION:} \textit{Differential dynamic logic has been used for
-existing systems, not for the constructive design of autonomous controllers.} 
+post-hoc analysis of existing systems, not for the constructive design of
-This is exactly the gap you're filling — you're doing synthesis, not just 
+autonomous controllers.} Current dL-based approaches verify systems that
-verification.}
+have already been designed, requiring expert knowledge to construct proofs.
+They have not been applied to the synthesis of new controllers from
+operational requirements.\splitinline{Your comment here is spot-on. You
+should add a LIMITATION box: \textit{Differential dynamic logic has been
+used for post-hoc analysis of existing systems, not for the constructive
+design of autonomous controllers.} This is exactly the gap you're filling —
+you're doing synthesis, not just verification.}