Obsidian/Writing/ERLM/state-of-the-art/outline.md

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)