Split
c37720f66b
Papers analyzed: - Katis 2022, Pressburger 2023 (FRET) - Maoz 2015, Luttenberger 2020 (reactive synthesis) - Borrmann 2015, SOSTOOLS 2021 (barrier certificates) - SpaceEx 2011, Flow* 2013, JuliaReach 2019 (reachability) - Kapuria 2025 (decomposition-based verification) Key findings: - FRET lacks liveness support (important gap) - GR(1) synthesis is tractable for reactor specs - Compositional verification needs assume-guarantee citations - Expulsory mode verification needs additional references Report: needs-review-report.md
200 lines
11 KiB
Markdown
200 lines
11 KiB
Markdown
# NEEDS_REVIEWED Papers Analysis Report
|
|
**Generated:** 2026-03-10
|
|
**For:** Dane Sabo's Candidacy Proposal (HAHACS)
|
|
|
|
---
|
|
|
|
## 1. Paper Summaries
|
|
|
|
### FRET & Requirements
|
|
|
|
**Katis et al. 2022 — "Realizability Checking of Requirements in FRET"**
|
|
Describes FRET's pipeline from FRETish (structured natural language) → pmLTL → Lustre for realizability checking. Key contribution: compositional analysis via connected components makes large requirement sets tractable. Directly relevant to your claim that FRET bridges natural language procedures and formal specs. **Read pages 3-9.**
|
|
|
|
**Pressburger et al. 2023 — "Using FRET for Lift Plus Cruise Case Study"**
|
|
8-month case study applying FRET to an eVTOL aircraft with multiple control modes. Critical finding: specs without explicit "stay" requirements were under-specified — realizability analysis caught this. Shows FRET working on a real hybrid system with mode transitions. **Read pages 5-11.**
|
|
|
|
### Reactive Synthesis
|
|
|
|
**Maoz & Ringert 2015 — "GR(1) Synthesis for LTL Specification Patterns"**
|
|
Translates 52 of 55 Dwyer specification patterns to GR(1) fragment. Polynomial-time synthesis (vs 2EXPTIME for full LTL). Pattern-based approach is accessible to engineers. Directly supports your claim about tractable synthesis. **Read pages 2-7.**
|
|
|
|
**Luttenberger et al. 2020 — "Practical Synthesis via Parity Games" (Strix)**
|
|
Full LTL synthesis made practical via forward exploration and formula decomposition. Won SYNTCOMP 2018-2019. Handles 415/434 benchmark instances. Supports your choice of Strix but note: "specifications with large alphabets are still a challenge." **Read pages 1-12, 27-30.**
|
|
|
|
### Barrier Certificates
|
|
|
|
**Borrmann et al. 2015 — "Control Barrier Certificates for Safe Swarm Behavior"**
|
|
QP-based safety filter architecture: nominal controller + CBF override. Runs at 50Hz for 20 agents. Hand-crafted barriers from physics. Relevant architecture for stabilizing modes but barriers are NOT automatically synthesized. **Read pages 2-4.**
|
|
|
|
**Papachristodoulou et al. 2021 — "SOSTOOLS v4.00"**
|
|
SOS optimization toolbox for barrier certificate search. Can handle ~10 variables at degree 4 polynomials. Provides formal certificates but limited to polynomial dynamics. Directly supports your stabilizing mode verification approach. **Read pages 6-10, 34-40.**
|
|
|
|
### Reachability Analysis
|
|
|
|
**Frehse et al. 2011 — "SpaceEx"**
|
|
Support function + template polyhedra for affine hybrid systems. Scales to 100+ dimensions for linear dynamics. Best scalability of the three tools. Limited to piecewise-affine dynamics. **Read pages 4-8, 13-15.**
|
|
|
|
**Chen et al. 2013 — "Flow*"**
|
|
Taylor model flowpipes for nonlinear polynomial hybrid systems. Handles 4-9 variables. Only tool that does nonlinear dynamics directly. Parameter-sensitive. **Read pages 1-5.**
|
|
|
|
**Bogomolov et al. 2019 — "JuliaReach"**
|
|
Julia-based toolbox with lazy set representations. Scales to 1000+ dimensions for linear systems. Designed for rapid prototyping and extensibility. Currently linear-only. **Read pages 1-4.**
|
|
|
|
### Other
|
|
|
|
**Hauswirth et al. 2024 — "Optimization Algorithms as Robust Feedback Controllers"**
|
|
Shows optimization algorithms (gradient descent, etc.) can be viewed as feedback controllers with robustness guarantees. Potentially relevant to your continuous controller design but tangential to verification. **Skim for ideas.**
|
|
|
|
**Kapuria 2025 — Thesis on Decomposition-Based Formal Verification**
|
|
Could not fully analyze (>100 pages). Title suggests direct relevance to your compositional verification approach. **Request Dane read key chapters directly.**
|
|
|
|
---
|
|
|
|
## 2. Supporting Evidence by Thesis Section
|
|
|
|
### Section 1: Hybrid Systems Definition
|
|
- Your compositional approach (verify per-mode, compose) is standard in hybrid systems literature
|
|
- SpaceEx paper (p4-6) formalizes the hybrid automaton structure you use
|
|
- Flow* (p2) shows guard/reset handling matches your formulation
|
|
|
|
### Section 2: Requirements & FRET
|
|
- **Strong support**: Katis 2022 (p3-5) shows exactly how FRETish → pmLTL works
|
|
- 160 distinct ⟨scope, condition, timing⟩ templates cover most requirement patterns
|
|
- Pressburger 2023 demonstrates iterative refinement catches specification gaps
|
|
- **Gap**: FRET has NO liveness support (Katis p2, Table 1) — your "eventually reach operating temperature" properties need workaround
|
|
|
|
### Section 3: Reactive Synthesis
|
|
- **Strong support**: GR(1) paper shows 52/55 Dwyer patterns are tractable (polynomial time)
|
|
- Strix paper validates full LTL synthesis is now practical (415/434 benchmarks solved)
|
|
- Your claim "eliminates human error at implementation stage" is supported: synthesis is correct-by-construction
|
|
- **Caution**: Strix notes "large alphabets are still a challenge" (p35) — nuclear systems with many sensors may hit this
|
|
|
|
### Section 4: Continuous Controllers
|
|
|
|
#### Transitory Modes (Reachability)
|
|
- **Strong support**: SpaceEx handles 100+ dimensional affine systems
|
|
- JuliaReach scales to 1000D for lazy operations
|
|
- Flow* handles nonlinear polynomial dynamics (4-9 vars)
|
|
- **Gap**: None of these handle true nonlinear reactor kinetics (exponentials) without approximation
|
|
|
|
#### Stabilizing Modes (Barrier Certificates)
|
|
- **Partial support**: SOSTOOLS can search for polynomial barrier certificates
|
|
- Your claim that "the barrier is known a priori from discrete specs" is novel — not directly validated by these papers
|
|
- Borrmann shows CBF architecture works but uses hand-crafted barriers
|
|
- **Gap**: No paper shows automatic barrier search from discrete boundary conditions
|
|
|
|
#### Expulsory Modes (Robust Reachability)
|
|
- **Weak support**: SpaceEx handles nondeterministic inputs (p4) but not parametric uncertainty directly
|
|
- Flow* has some robustness via interval remainders
|
|
- **Gap**: None of these papers address reachability with parametric uncertainty for failure mode analysis
|
|
|
|
---
|
|
|
|
## 3. Gaps & Challenges
|
|
|
|
### Your Approach Claims These Papers DON'T Cover:
|
|
|
|
1. **Three-mode taxonomy (transitory/stabilizing/expulsory)**
|
|
- This appears to be your novel contribution
|
|
- No paper uses this exact classification
|
|
- You need to justify why this taxonomy is complete (covers all cases)
|
|
|
|
2. **Barrier certificates from discrete boundaries**
|
|
- Your claim that knowing entry/exit conditions "eliminates the barrier search problem" is not validated
|
|
- SOSTOOLS still requires searching for the barrier polynomial
|
|
- The discrete specs constrain the *domain* but not the *barrier function form*
|
|
|
|
3. **Compositional verification soundness**
|
|
- You claim verifying per-mode and composing guarantees is sound
|
|
- This requires assume-guarantee reasoning at mode boundaries
|
|
- None of these papers prove this composition is sound for your specific approach
|
|
- **Suggest**: Cite Alur et al. or other assume-guarantee hybrid systems literature
|
|
|
|
4. **FRET for nuclear operating procedures**
|
|
- No paper applies FRET to nuclear domain
|
|
- The Lift+Cruise study (aviation) is closest but nuclear procedures have different characteristics
|
|
- **Gap**: No evidence FRET's 160 templates cover nuclear procedure patterns
|
|
|
|
5. **Expulsory mode verification**
|
|
- Parametric reachability under failure mode uncertainty is not well-covered
|
|
- You may need additional references (robust reachability, FMEA integration)
|
|
|
|
---
|
|
|
|
## 4. Recommended Reading (Tomorrow Morning)
|
|
|
|
### Priority 1 (Must Read)
|
|
| Paper | Pages | Why |
|
|
|-------|-------|-----|
|
|
| Katis 2022 (FRET Realizability) | 3-9 | Core FRET pipeline, directly supports your methodology |
|
|
| Maoz 2015 (GR(1) Patterns) | 2-7 | Tractability argument for reactive synthesis |
|
|
| Pressburger 2023 (FRET Case Study) | 5-11 | Real hybrid system example, lessons learned |
|
|
|
|
### Priority 2 (Should Read)
|
|
| Paper | Pages | Why |
|
|
|-------|-------|-----|
|
|
| Luttenberger 2020 (Strix) | 1-12, 27-30 | Validates Strix as synthesis tool choice |
|
|
| SOSTOOLS manual | 34-40 | Lyapunov/barrier certificate computation |
|
|
| SpaceEx paper | 4-8 | Reachability algorithm details |
|
|
|
|
### Priority 3 (Skim)
|
|
| Paper | Section | Why |
|
|
|-------|---------|-----|
|
|
| Borrmann 2015 (CBF) | Section 3 | CBF-QP architecture for safety filter |
|
|
| Flow* paper | Full | Nonlinear reachability capabilities |
|
|
| JuliaReach paper | Full | Modern tooling alternative |
|
|
|
|
---
|
|
|
|
## 5. Missing References (Topics Not Covered)
|
|
|
|
Your research approach mentions or assumes things these papers don't address:
|
|
|
|
1. **Assume-guarantee reasoning for hybrid systems**
|
|
- Need citations for compositional verification soundness
|
|
- Suggested: Henzinger et al., Alur et al., or de Alfaro & Henzinger on interface theories
|
|
|
|
2. **Nuclear-specific formal methods**
|
|
- HARDENS is your main reference but additional nuclear FM work may exist
|
|
- Search: NuSMV for nuclear, formal methods in safety-critical systems
|
|
|
|
3. **Parametric reachability / robust verification**
|
|
- For expulsory mode verification with failure uncertainty
|
|
- Suggested: CORA (parametric reachability), robust CBF literature
|
|
|
|
4. **Timed automata / real-time specifications**
|
|
- FRET timing is discrete ticks, not real-time
|
|
- If you need continuous-time deadlines, may need UPPAAL or timed automata references
|
|
|
|
5. **Code generation from synthesized controllers**
|
|
- You mention compiling to Ovation hardware
|
|
- Need references on verified code generation from automata (e.g., Esterel, SCADE)
|
|
|
|
6. **Mode-switching stability**
|
|
- Your stabilizing modes need to maintain stability across transitions
|
|
- Suggested: Multiple Lyapunov functions, dwell time conditions
|
|
|
|
---
|
|
|
|
## 6. Key Quotes for Your Proposal
|
|
|
|
**On reactive synthesis tractability:**
|
|
> "GR(1) synthesis is polynomial in the state space size... all 52 supported patterns have DBWs with at most 8 states, requiring at most 3 auxiliary variables per pattern instance." — Maoz & Ringert 2015, p6
|
|
|
|
**On FRET's value:**
|
|
> "Realizability checking catches specification conflicts early — before implementation. The Infusion Pump case shows how manual analysis missed the true conflict structure, while automated analysis found 8 minimal cores." — Katis 2022, p14
|
|
|
|
**On specification completeness:**
|
|
> "The most significant discovery was that initial requirements without 'stay' transitions were under-specified. Realizability analysis produced a trace where the aircraft jumped from wing-borne mode directly to thrust-borne mode — physically impossible but logically permitted." — Pressburger 2023, p9
|
|
|
|
**On scalability:**
|
|
> "SpaceEx demonstrates empirical complexity of O(n^2.7) for box directions... up to 198 variables using box directions." — Frehse 2011, p13
|
|
|
|
**On barrier certificates:**
|
|
> "SOSTOOLS can solve local nonlinear stability analysis with 10 variables using degree 4 polynomials." — Papachristodoulou 2021, p6
|
|
|
|
---
|
|
|
|
*Report generated by Split 🦎*
|