\section{Research Approach} \iffalse HACS: hybrid autonomous control system HAHACS: High-Assurance Hybrid AUtonomous Control System The research approach here needs to clearly outline the solution the the problem and identify the actions taken that will advance knowledge and solve the problem. First, what is the problem? \textit{ Inhibition to adopt hybrid autonomous control in critical infrastructure is rooted in safety concerns of system stability. Without a human in the loop with general intelligence, HACS have not been trusted where failure modes can be unique and novel. } So, what's the solution? \textit{ This research approach develops a methodology to build HACS that are provably safe. This methodology builds on existing technologies, and unifies different research thrusts to build a complete hybrid control system. To do this, the problem of a HAHCS is broken into three distinct pieces: \begin{enumerate} \item System specification: properties of the HAHaCS such as transition between control modes and system invariants are specified using a formal methods tool. - This provides exact behavior - allows realizabillity checking of controller specs. Can a controller actually be built from these specs? - ? - ? \item Discrete Behavior Synthesis: The discrete component of the controller is synthesized directly from system specifications using reactive synthesis. - This ELIMINATES wholesale the possibility of introducing logical bugs in the creation of the strategic part of the HAHCS. Critical decisions that are normally made by a human are automated directly from the formal specifications. - This does two critical things: - It makes the creation of the controller tractable. The reasons the controller changes between modes acn be traced back to the specification (and thus any requirements), which is a trace for liability and justification of system behavior - Discrete control decisions made by humans are reliant on the human operator operating correctly. Humans are intrinsically probabalistic creatures who cannot eliminate human error. By defining the behavior of this system using temporal logics and synthesizing the controller using deterministic algorithims, we are assured that strategic decisions will always be made as according to operating procedures. \item Continuous Behavior Synthesis and Verification: The continuous components of the controller are built using existing dynamics and control theory but then verified using reachability and barrier certificats. - It's very challenging (nigh impossible) to say for certain how to build any continuous control mode. That is honestly going to be have to left to the specific control system and its objectives. It's not really the point of this PhD to say how to do that. For that reason, I'm going to assume that controllers between modes are generally possible to build. That is to say that there exists a controller that can transition between modes, but it is a human hunt to find it. - To check if a candidate controller does transition between discrete modes, we do two things: - Check invariants using reachability. Specifications will require that control modes transiiton from one mode to the next, where appropriate. When this is the case, these invariants are extracted to be checked using reachability. The control mode is given the possible entry conditions of the 'entry' mode, and the possible 'exit' states are analyzed. A cont. controller passes this reachability test if there is no reachable state that is not at the exit condition of the state transition. --- This needs flushed out more. I think this can really be clarified using entry and exit conditions of Mealy machines. The continuous system IS the transition, and the reachabililty test is saying whether or not the physical system actually satisfies the entry and exit conditions. - Then, for systems that need to STAY within one mode, we will use barrier certificates. These can let us define a continuous state boundary, and define for a discrete controller state, the total controller will NOT leave the continuous boundary. - One thing that must be considered is the idea that this analysis is predicated on the physical system being correct to the model. If this isn't true, we must define continuous modes that catch failure states. If transition invariants are violated, we must shut down the system, and build safety oriented control modes that we can be sure with a much broader set of entry conditions will safely shut down the plant. -- Q for dan: is it critical to really have software to namedrop or is it better to stay amorphous on the technology? Iirc Manyu did a little bit of both. \end{enumerate} What's the intellectual merit? \textit{ There is no outstanding way to build HAHACS. This methodology provides a basis for systems engineers to think about the components of a HAHACS as interlocking pieces whos verification interlinks into a broader system. This will also motivate the adoption of temporal logic to define autonomous control systems, by allowing a close connection and tracability between requirements from regulations to system specifications. } } Some thoughts on invariants, and how they fit here: There are several types of safety invariants that HAHACS might have. 1. Conditions that initiate a switch between control modes (reactiive synthesis relevant) 2. Invariants about the stability of discrete states (barrier certificates) 3. Invariants ensuring the transition between discrete states (reachability) 4. Invariants about the timeliness of discrete transitions (??? Reachability?) How do we reason about all of these invariants. Well, fundamentally they can all be reasoned about with temporal logic statements. Using next and eventually operators, we can get to the fundamental behavior of all of these modes. What's challenging is the fact that we ensure that all of these specifications are validated differs between the type of invariant. This is really the beauty of this approach, and the intellectual merit. This proposal provides a way for hybrid control systems to be verified for autonomous control systems by diversifying the way that the invariants are checked. Reactive synthesis helps us build discrete controllers using specifications that have conditons that don't depend on time. These invariants generally are strategic decisions, such as changing between operating modes, initiating power level changes, or perhaps doing a refueling or shutdown routine. These specifications are able to be nearly directly drawn from operating procedures, and should be closely tied to instructions that would be used for human operators. They have checkpoints for the continuous system in between different control implements. An example is, raise power at a certain rate while ensure temperature remains between certain bounds. These conditions are physical states, but they are a binary result. The condition is really binary, desipite perhaps having units of celsius or %power. When we build discrete controllers from these specifications, we get the validation of the controller of these specs for free by nature of reactive synthesis tools. We get direct traceability from the operating procedure to the discrete controller implementation with minimal human effort. That being said, there are no free lunches here. Ultimately, we're controlling physical systems, and while we can automate the controller building between stratgic objectives, it is not trivial to do so for the controller of the physical process. These controllers are going to have to be built manually, with the continuous dynamics of the system in mind. Helpfully, if specifications are complete first, one can obtain discrete controller before building physical controllers. The result of this is a simplification of controller design, becuase the operational goals of each continuous controller is clearly outlined by the invariants that define the goal of each discrete mode. While for reactive synthesis purposes conditions such as a certain temperature being reached or power level attained are binary variables, the continuous physical meaning becomes important in the design and analysis of the physical controllers. The continuous value of these conditions becomes the goal of the continuous controller design, while also providing a basis to check controller performance. To check continuous controllers are valid, we can split continuous controller objectives into two types. First, we have continuous controllers that are designed to move the plant between two different discrete modes. These will be called 'transitory' controllers, because their entire purpose is to transition the plant betweeen between discrete control modes. Because of the specification of the hybrid control system a priori, we will have defined what the invariants of these transitions are in continuous state space. Then, once a continuosu controller design is developed, it can be validated using reachability analysis. The input set for the analysis is the possible states that enter this transitory mode, while the reachable states must be entirely contained within the exit invariant for the controller to pass. At the time of writing this proposal, it is not clear what the most efficient way to obetain this continuous controller is, but is generally beyond the scope of this work. It is assumed that they generally won't be so difficult to find for most systems, as the refinement of the discrete controller should simplify the control objectives of the physical controllers significantly. The second type of continuous controller that may be utilized in a HAHAHCS is a controller that tries to maintaine a continuous steady state, such that no discrete transitions are triggered. Reachability on these systems may not prove a prudent approach to validating this behavior for a candidate continuous controller, and instead, barrier certificates must be used. Barrier certificates analyze the dynamics of the system to say whether or not flux across a given boudnary exists. That is to say that they evaluate whether or not there is a trajectory or not that leaves a given boundary. This definition is exactly what defines the validity of a stabilizing continuous control mode. Once again, because the design of the discrete controller defines careful boundaries in continuous state space, the barrier is known a priori of which we must satisfy this condition. This will eliminate the search for such a barrier, and minimze complicatoin in validating stabilizing continuous control modes. Finally, consideration must be paid for when errors occur. The validation of these continuous control modes hinges upon having an assumption ofcorrect model, which in the case of a mechanical failure will almsot certainly be invalidated. Special continuous controllers for these conditions must be created, called 'explusory' control modes. These controllers will be responsible for ensuring safety in case of failure, and will be designed with reachability, but in this case, additional allocation for the allowing of physical parameters will be allowed in the analysis. Traditional safety analysis will also be used to identify potential failure modes, and the modelling of their worst case dynamics. The HAHCS will be able to idenfity why such a fault occors because an discrte boundary condition will be violated by the continuous physical controller. That is to say, since we will have validated the continuous control modes using reachability and barrier certificates a priori, we will know with certainty that the only room for dynamics to change is a shift in the plant dynamics, not that of the proven controller. \fi %%%%%%%%%% TABLESETTING % what is a hybrid system really for this proposal % Define: A hybrid system with continuous state space X ⊆ ℝⁿ and discrete modes Q = {q₁, q₂, ..., qₘ} % Each discrete mode qᵢ has an associated continuous state region Xᵢ ⊆ X % The discrete controller manages transitions between modes based on continuous state thresholds % what are requirements, anyways? % why do we care about defining the whole hybrid system into requirements? % How do different requirements line up into different parts of the system? % (operational vs strategic requirements and their relevance to different parts % of our system) Autonomous control systems are fundamentally different from automatic control systems. The difference between these systems is the level at which they operate. Automatic control systems are purely operational systems, To build a high-assurance hybrid autonomous control system (HAHACS), a mathematical description of the system must be established. This work will make use of automata theory while including logical statements and control theory. The nomenclature and lexicon between these fields is far from homogenous, and the reviewer of this proposal is not expected to be an expert in all fields simultaneously. To present the research ideas as clearly as possible in this section, the following syntax is explained. A hybrid system is a dynamical system that has both continuous and discrete states. The specific type of system discussed in this proposal are continuous autonomous hybrid systems. This means that these systems a) do not have external input \footnote{This is not strictly true in our case because we allow strategic inputs. For example, a remote powerplant may receive a start-up or shutdown command from a different location, but only this binary high level input is a strategic input.} and b) continuous states do not change instantaneously when discrete states change. For our systems of interest, the continuous states are physical, and are always Lipschitz continuous. This nomenclature is heavily borrowed from \cite{HANDBOOK ON HYBRID SYSTEMS CONTROL}, but is redefined here for convenience: \begin{equation} H = (\mathcal{Q}, \mathcal{X}, \mathbf{f}, Init, \mathcal{G}, \mathcal{R}, Inv) \end{equation} where: \begin{itemize} \item \( \mathcal{Q}\): is the discrete states of the system \item \( \mathcal{X}\): is the continuous states of the system \item \(\mathbf{f}: \mathcal{Q} \times \mathbb{R} \rightarrow \mathbb{R} \), where \(\mathbf{f}_i\) is a vector field that defines the continuous dynamics for each \(q_i\) \item \(Init\): the initial states of \(q\) and \(x\) \item \( G\): guard conditions that define when discrete state transitions occur \item \(\delta: \mathcal{Q} \times G \rightarrow \mathcal{Q}\), are the discrete state transition functions \item \mathcal{R}: Reset maps that define state 'jumps' \item \(Inv\): Safety invariants on the continuous dynamics \end{itemize} The creation of a HAHACS essentially boils down to the creation of such a tuple where there are proof artifacts that the intended behavior of the control system are satisfied by the actual implementation of the control systems. But to create such a HAHACS, we must first completely describe its behavior. %% Brief discussion on what each part of this tuple means for us \subsection{System Requirement and Specifications} Temporal logic is a powerful set of semantics to build systems that can have complex but deterministic behavior. %%%%%%%%%%% Building discrete controllers % Buildout of requirements from written procedures (this is easy for critical % systems - we already have the requirements) % What happens to the invariants that specify a continuous space? Save em for % later. Here they become binary for our purposes % KEY POINT: We don't IMPOSE discrete abstraction - we FORMALIZE existing practice % Operating procedures (esp. nuclear) already define go/no-go conditions as discrete predicates % e.g., "WHEN coolant temp >315°C AND pressurizer level 30-60% THEN MAY initiate load following" % These thresholds come from design-basis safety analysis, validated over decades % Our methodology assumes this domain knowledge exists and provides formalization framework % The discrete predicates p₁, p₂, ... are Boolean functions over continuous state: pᵢ: X → {true, false} % Q: How do we rigorously set thresholds for continuous→discrete abstraction? % Q: How do we handle hysteresis to prevent mode chattering near boundaries? % Q: How do we account for sensor noise and measurement uncertainty? % Q: How do we handle numerical precision issues when creating discrete automata? (relates to task 36) % Discrete controller implementation can be realized with reactive synthesis. % LTL specs to automata % talk a bit about tools here like FRET. Talk about previous attempts. Human control of nuclear power can be divided into three different scopes: strategic, operational, and tactical. Strategic control is the high-level and long term decision making for the plant. This level has objectives that are complex and economic in scale, such as managing labor needs and supply chains to optimize sheduled maintenence and downtime. The time scale on this level of control is long, often over months or years. The lowest level of control is the tactical level. This is the individual control of pumps, turbines, and chemistry of the plant. This level of control has already been somewhat automated today in nuclear power, and is generally considered 'automatic control' when autonomous. These controls are almost always continuous systems, and have a direct impact on the physical state of the plant. Tactical control objectives are things like maintaining a pressurizer level, maintaining a certain core temperature, or adjusting reactivity with a chemical shim. The level of control linking these two levels, then, is the operational control scope. Operational control is the primary responsibility of human operators today. Operational control takes the current strategic objective, and implements tactical control objectives to drive the plant towards strategic goals. In this way, it is the bridge between high and low level goals. A strategic goal may be to perform refueling at a certain time, while the tactical level of the plant currently is focused on mainting a certain core temperature. The operational level is what issues the shutdown procedure of the plant, using several smaller tactical goals along the way to achieve this objective. Thus, the combination of the operational and tactical level of the plant fundamentally forms a hybrid controller. The tactical level is the continuous evolution of the plant according to the control input and control law, while the operational level is a discrete state evolution which determines the tactical control law to reach different operational states. %%%%%%%%%%%% Building continuous controllers % The whole point of a hybrid system is that there are continuous components % underneath the digital system. We built the discrete like the physical doesn't % exist, but it really does. So how do we capture the physical system too? % SCOPE FRAMING: This methodology VERIFIES continuous controllers, not SYNTHESIZES them % Compare to model checking: doesn't tell you HOW to design software, verifies if it satisfies specs % We assume controllers can be designed using standard control theory techniques % Our contribution: verification that candidate controllers compose correctly with discrete layer % What are the main different kinds of continuous modes we may see? % Mathematical structure: Each discrete mode qᵢ provides three key pieces of information: % 1. Entry conditions: X_entry,i ⊆ X (initial state set) % 2. Exit conditions: X_exit,i ⊆ X (target state set) % 3. Invariants: X_safe,i ⊆ X (safety envelope during operation) % These come from the discrete controller synthesis and define objectives for continuous control % Q: Who designs the continuous controllers and how? This methodology verifies % them, but doesn't synthesize them. Is this a scope problem? %%%%%% Transitory modes % entry and exit conditions % the goal is getting from one physical state to another % MATHEMATICAL FORMULATION: % Control objective: reach(X_entry,i) → reach(X_exit,i) while maintaining x(t) ∈ X_safe,i % Standard control techniques (LQR, MPC, trajectory optimization) applied with these constraints % % VERIFICATION: Reachability analysis confirms ALL trajectories starting in X_entry,i % reach X_exit,i without violating X_safe,i % Formally: Reach(X_entry,i, f(x,u), T) ⊆ X_exit,i ∪ X_safe,i % where f(x,u) is the closed-loop continuous dynamics % % we have the physical requirements from earlier specifications. Here we use % them in a reachability analysis. This time, we use the actual physical values % instead of the binary yes/no we used for discrete % Q: How do we verify timing constraints? If a transitory controller eventually % reaches the exit condition but takes too long, that violates safety. Timed % automata? Timed reachability? % Q: Should formalize the Mealy machine perspective - continuous system IS the % transition, and entry/exit conditions are the discrete states. This could be % a unifying conceptual framework. %%%%%% stabilizing modes % these are control modes with an objective of KEEPING a certain discrete state % stable % % MATHEMATICAL FORMULATION: % Control objective: remain(X_target,i) where X_target,i ⊂ X_safe,i % Standard feedback control (PID, state feedback, LQG) applied to maintain equilibrium % % VERIFICATION: Barrier certificates prove closed-loop dynamics cannot escape X_safe,i % Formally: Find B(x) s.t. ∇B(x)·f(x,u) ≤ 0 for all x ∈ ∂X_safe,i % This proves no trajectory can cross the boundary (no flux out of safety region) % % we also have the physical requirements for this. These can be used for barrier % certificates. We can prove that our model won't leave a given area without % some disturbance. %%%%%% expulsory modes % I've made an implicit assumption when talking about transitory and stabilizing % modes. That our model is correct. This might not be true % In the case of a failure, our model will almost certainly be incorrect. For % this, we have to build safe shutdown modes too, since a human won't be in the % loop to shut things down. % % MATHEMATICAL FORMULATION: % Control objective: reach(X_current) → reach(X_safe_shutdown) under parameter uncertainty % where X_current may be anywhere in X (worst-case entry conditions) % Dynamics have parametric uncertainty: f(x,u,θ) where θ ∈ Θ_failure % % VERIFICATION: Parametric reachability analysis with robustness margins % Reach(X_current, f(x,u,θ), T) ⊆ X_safe_shutdown for all θ ∈ Θ_failure % Conservative bounds on Θ_failure come from FMEA/traditional safety analysis % WE can detect physical failures exist because our physical controllers have % previously been proven as correct by reachability and barrier certificates. We % KNOW our controller cannot be incorrect for the plant, so if an invariant is % violated, we KNOW it's the plant that has changed. % Q: What about sensor failures (wrong readings vs actual plant failure)? % Q: What about unmodeled disturbances that aren't failures? % Q: What if model uncertainty was too optimistic to begin with? % Need to be more precise about what "model failure" means and detect-ability. % We do this using continuous modes that shutdown the system, and using % reachability analysis with parametric uncertainty, we can prove for a range of % error conditions we can maintain safe shutdown. % Q: How much parametric uncertainty is enough? How do we determine bounds for % worst-case failure dynamics? Need methodology for this. %%%%%%%%%%%% Implementation with industrial partnerships %%%%%%% Emerson %talk about this % ovation system % scenic? Is that what they call it? % ripe partnership with Westinghouse % Likely build a model with a ccng plant. They already have sophisticated models % of them % build controller with simplified model, then test with high fidelity digital % twin % %%%%%%%%%%