227 lines
12 KiB
TeX
227 lines
12 KiB
TeX
\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
|
|
|
|
|