Dane Sabo
ea9b1f2b16
M .sessions/nvim_config.vim A .task/backlog.data A .task/completed.data A .task/pending.data A .task/undo.data A Writing/ERLM/state-of-the-art/outline.md
139 lines
4.6 KiB
Markdown
139 lines
4.6 KiB
Markdown
# Outline of State of the Art
|
|
|
|
## Writing is thinking, and this is like journaling
|
|
|
|
This research is really about using techniques that we
|
|
already have to make hybrid systems that from the jump are
|
|
provably adherent to requirements and in general that we can
|
|
say what they're gonna do fo sho. Does that make any sense?
|
|
|
|
The critical technologies to do this are as follows, in no
|
|
particular order: discrete system theory and reactive
|
|
synthesis, temporal logics, reachability for hybrid systems.
|
|
|
|
Things that are adjacent to what I'm doing but aren't what
|
|
I'm doing include stuff by Platzer and all the differential
|
|
dynamic logic stuff. His stuff looks like another way of
|
|
conquering this problem but adds a whole lot of complexity
|
|
and makes synthesis ambiguous. Great at checking, but what
|
|
does that mean for designing?
|
|
|
|
I feel like I should get more sources on designing hybrid
|
|
systems. I think there are some books out there about this
|
|
maybe.
|
|
|
|
----
|
|
**Outline**
|
|
----
|
|
|
|
## 1. Hybrid Control Systems Foundations
|
|
- **Classical hybrid systems theory** (Branicky, Liberzon,
|
|
Morse - switching systems)
|
|
- **Hybrid automata and modeling** (Henzinger, Alur, Dill)
|
|
- **Stability analysis for switching systems** (Shorten,
|
|
Narendra, Lin & Antsaklis)
|
|
|
|
**Key points to include:**
|
|
- Definition of hybrid systems and why they're needed for
|
|
complex control
|
|
- Challenges in stability analysis when switching between
|
|
controllers
|
|
- Gap between individual mode stability and overall system
|
|
stability
|
|
- Motivate why traditional control theory alone is
|
|
insufficient
|
|
|
|
## 2. Discrete Controller Synthesis
|
|
- **Reactive synthesis from temporal logic** (Pnueli, Bloem,
|
|
Ehlers)
|
|
- **Tools like Strix, TuLiP, SLUGS** - emphasize their
|
|
discrete-only assumptions
|
|
- **LTL/GR(1) synthesis** and why these assume instantaneous
|
|
transitions
|
|
|
|
**Key points to include:**
|
|
- Power of temporal logic for specifying complex behaviors
|
|
- Success of reactive synthesis in discrete domains
|
|
- Correctness-by-construction guarantees from synthesis
|
|
tools
|
|
- Critical limitation: assumption of instantaneous state
|
|
changes
|
|
- Why this breaks down for physical systems with continuous
|
|
dynamics
|
|
|
|
## 3. Continuous System Verification
|
|
- **Reachability analysis** (Girard, Le Guernic, Althoff -
|
|
especially for nonlinear systems)
|
|
- **Linear system verification** (Boyd, Dullerud - classical
|
|
control meets verification)
|
|
- **Set-based methods** (Mitchell, Tomlin for
|
|
Hamilton-Jacobi reachability)
|
|
|
|
**Key points to include:**
|
|
- Mature tools for analyzing continuous dynamics
|
|
- Reachability as the fundamental verification problem
|
|
- Computational challenges for nonlinear systems
|
|
- Gap: these are analysis tools, not synthesis tools
|
|
- They tell you if a controller works, but don't help design
|
|
it
|
|
|
|
## 4. Existing Hybrid Verification Approaches
|
|
- **Platzer's differential dynamic logic** (as you noted -
|
|
good for verification, unclear for synthesis)
|
|
- **SpaceEx, Flow*, dReach** - model checking tools that
|
|
don't synthesize
|
|
- **Contract-based design** (Benveniste,
|
|
Sangiovanni-Vincentelli)
|
|
|
|
**Key points to include:**
|
|
- Current approaches focus on verification after design
|
|
- Platzer's dL: powerful for proving correctness, but
|
|
synthesis unclear
|
|
- Model checking tools require pre-designed controllers
|
|
- Contract-based approaches: compositional but still
|
|
verification-focused
|
|
- Missing: unified synthesis framework that handles both
|
|
discrete and continuous
|
|
|
|
## 5. The Gap You're Filling
|
|
- **Why discrete synthesis + continuous verification hasn't
|
|
been unified**
|
|
- **Challenges with non-instantaneous transitions**
|
|
- **The synthesis vs. verification divide**
|
|
|
|
**Key points to include:**
|
|
- Fundamental mismatch: discrete synthesis assumes instant
|
|
transitions
|
|
- Physical reality: transitions take time and follow
|
|
continuous trajectories
|
|
- Current workflow: synthesize discrete, design continuous,
|
|
then verify
|
|
- Your contribution: unified framework for
|
|
correct-by-construction hybrid synthesis
|
|
- Nuclear startup as ideal testbed: well-defined continuous
|
|
dynamics + explicit procedural requirements
|
|
|
|
## Key Sources to Hunt Down
|
|
|
|
**Foundational hybrid systems:**
|
|
- Branicky's "Multiple Lyapunov functions and other analysis
|
|
tools"
|
|
- Liberzon's "Switching in Systems and Control"
|
|
- Antsaklis & Koutsoukos survey papers
|
|
|
|
**Reactive synthesis:**
|
|
- Ehlers & Topcu on GR(1) synthesis
|
|
- Recent Strix papers (Meyer, Sickert, Luttenberger)
|
|
- Wongpiromsarn's work on TuLiP
|
|
|
|
**Hybrid verification:**
|
|
- Althoff's reachability analysis work
|
|
- Girard's papers on abstraction-based verification
|
|
- Any recent survey on hybrid system verification tools
|
|
|
|
**Nuclear/critical systems control:**
|
|
- Look for papers on autonomous nuclear plant operation
|
|
- Regulatory papers on control system requirements (might be
|
|
more engineering sources)
|
|
|